Opened 17 years ago

Closed 17 years ago

#29 closed defect (fixed)

matrix multiplication tiling is incorrect

Reported by: Stephen Siegel Owned by: zirkel
Priority: major Milestone:
Component: examples Version: 1.0
Keywords: tile example matrix multiplication Cc:

Description

In the matrix multiplication example, tass correctly points out that there can be an array out of bounds error. This is because we are not assuming that BB divides N. To fix it, you need to possibly adjust the loop upper limit on the last iteration----see tile example.

Change History (3)

comment:1 by zirkel, 17 years ago

Status: newaccepted

comment:2 by zirkel, 17 years ago

The out of bounds problem is corrected. However, there is now a new error:

java.lang.RuntimeException: Unknown or unimplemented expression type: (LET cvc_0 = X3[0]
IN IF ((1 + (-1 * X1)) = 0) THEN 0 ELSE IF (X1 = 0) THEN (0 + (1 * cvc_0[X1] * X2[X1][0]) + (1 * cvc_0[0] * X2[0][0])) ELSE matrixMultiplicationImpl_2_P0_S0_F0_V7[0][X1] ENDIF ENDIF)

at edu.udel.cis.vsl.minimp.symbolic.prover.CVC3TheoremProver.convertBack(CVC3TheoremProver.java:647)
at edu.udel.cis.vsl.minimp.symbolic.prover.CVC3TheoremProver.simplify(CVC3TheoremProver.java:443)
at edu.udel.cis.vsl.minimp.symbolic.SymUniverse.subscriptExpression(SymUniverse.java:1482)
at edu.udel.cis.vsl.minimp.symbolic.SymUniverse.subscriptExpression(SymUniverse.java:1498)
at edu.udel.cis.vsl.minimp.value.impl.ValueFactory.subscript(ValueFactory.java:287)
at edu.udel.cis.vsl.minimp.semantics.impl.Evaluator.evaluateReference(Evaluator.java:238)
at edu.udel.cis.vsl.minimp.semantics.impl.Evaluator.evaluateSubscript(Evaluator.java:246)
at edu.udel.cis.vsl.minimp.semantics.impl.Evaluator.evaluateBinary(Evaluator.java:170)
at edu.udel.cis.vsl.minimp.semantics.impl.Evaluator.evaluate(Evaluator.java:145)
at edu.udel.cis.vsl.minimp.semantics.impl.Evaluator.evaluateBinary(Evaluator.java:173)
at edu.udel.cis.vsl.minimp.semantics.impl.Evaluator.evaluate(Evaluator.java:145)
at edu.udel.cis.vsl.minimp.semantics.impl.Executor.executeAssignment(Executor.java:150)
at edu.udel.cis.vsl.minimp.semantics.impl.Executor.execute(Executor.java:67)
at edu.udel.cis.vsl.minimp.verify.std.StateManager.nextState(StateManager.java:74)
at edu.udel.cis.vsl.minimp.verify.std.StateManager.nextState(StateManager.java:1)
at edu.udel.cis.vsl.minimp.search.DfsSearcher.proceedToNewState(DfsSearcher.java:141)
at edu.udel.cis.vsl.minimp.search.DfsSearcher.search(DfsSearcher.java:102)
at edu.udel.cis.vsl.minimp.search.DfsSearcher.search(DfsSearcher.java:88)
at edu.udel.cis.vsl.minimp.verify.Verification.verify(Verification.java:90)
at edu.udel.cis.vsl.minimp.Minimp.verify(Minimp.java:224)
at edu.udel.cis.vsl.minimp.Minimp.main(Minimp.java:314)

comment:3 by zirkel, 17 years ago

Resolution: fixed
Status: acceptedclosed

The out of bounds error is corrected.

Note: See TracTickets for help on using tickets.