Problems with tass verify, ArrayIndexOutOfBounds Exception

[rdeaton]

Run on latest svn, [1063]. Trace is attached.

MiniMP rdeaton$ ./tass verify examples/simpleMP/simpleMPImplGood.mmp
+----------------------------------------------------------------------+
| TASS: Toolkit for Accurate Scientific Software |
| version 1.0.r1054 (2009-08-29) http://vsl.cis.udel.edu/tass |
+----------------------------------------------------------------------+

command : verify
model : simpleMPImplGood.mmp(np=1)
Deadlock detection : absolute
Reduction : standard
verbose: : No
simplify: : No
bufferBound : 10
use loop technique : false

java.lang.ArrayIndexOutOfBoundsException: 1

at edu.udel.cis.vsl.minimp.model.impl.Model.process(Model.java:526)
at edu.udel.cis.vsl.minimp.semantics.impl.Evaluator.process(Evaluator.java:349)
at edu.udel.cis.vsl.minimp.semantics.impl.Evaluator.evaluateNotEmpty(Evaluator.java:370)
at edu.udel.cis.vsl.minimp.semantics.impl.Evaluator.evaluate(Evaluator.java:159)
at edu.udel.cis.vsl.minimp.verify.std.Enabler.proceedToNext(Enabler.java:74)
at edu.udel.cis.vsl.minimp.verify.std.Enabler.enabledTransitions(Enabler.java:105)
at edu.udel.cis.vsl.minimp.verify.std.Enabler.enabledTransitions(Enabler.java:18)
at edu.udel.cis.vsl.minimp.search.DfsSearcher.proceedToNewState(DfsSearcher.java:146)
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:441)
at edu.udel.cis.vsl.minimp.Minimp.main(Minimp.java:535)

java.lang.ArrayIndexOutOfBoundsException: 1
No deadlock possible at this state.
Writing counterexample to simpleMPImplGood.trace...done.
Writing model to simpleMPImplGood.model...done.
Program terminated.
Property doesn't hold: counterexample found.
Execution time is: 0.298s.

[rdeaton]

As trace couldn't be uploaded (see #76 for the automated trac ticket), I'm pasting it here.

simpleMPImplGood Trace summary:

Step 1: State 0 -- simpleMPImplGood.mmp line 10 [main@0->main@1] "i = 7;" -> State 1
Step 2: State 1 -- simpleMPImplGood.mmp line 11 [main@1->main@2] "j = 5;" -> State 2
Step 3: State 2 -- simpleMPImplGood.mmp line 12 [main@2->main@3] "k = 0;" -> State 3
Step 4: State 3 -- simpleMPImplGood.mmp line 13 [main@3->main@4] "m = 0;" -> State 4
Step 5: State 4 -- simpleMPImplGood.mmp line 14 [main@4->main@5] "if (PID == 0)" [true]

simpleMPImplGood Trace details:

begin State 0

onStack = true;
seen = true;
pathCondition : true
begin model state

begin shared variables

s = undefined;
t = undefined;

end shared variables;
begin process 0

begin stack frame 0

function : main;
location : 0;
i = undefined;
j = undefined;
k = undefined;
m = undefined;

end stack frame 0;

end process 0;

end model state

end State 0

Step 1: State 0 -- simpleMPImplGood.mmp line 10 [main@0->main@1] "i = 7;" -> State 1

begin State 1

onStack = true;
seen = true;
pathCondition : true
begin model state

begin shared variables

s = undefined;
t = undefined;

end shared variables;
begin process 0

begin stack frame 0

function : main;
location : 1;
i = 7;
j = undefined;
k = undefined;
m = undefined;

end stack frame 0;

end process 0;

end model state

end State 1

Step 2: State 1 -- simpleMPImplGood.mmp line 11 [main@1->main@2] "j = 5;" -> State 2

begin State 2

onStack = true;
seen = true;
pathCondition : true
begin model state

begin shared variables

s = undefined;
t = undefined;

end shared variables;
begin process 0

begin stack frame 0

function : main;
location : 2;
i = 7;
j = 5;
k = undefined;
m = undefined;

end stack frame 0;

end process 0;

end model state

end State 2

Step 3: State 2 -- simpleMPImplGood.mmp line 12 [main@2->main@3] "k = 0;" -> State 3

begin State 3

onStack = true;
seen = true;
pathCondition : true
begin model state

begin shared variables

s = undefined;
t = undefined;

end shared variables;
begin process 0

begin stack frame 0

function : main;
location : 3;
i = 7;
j = 5;
k = 0;
m = undefined;

end stack frame 0;

end process 0;

end model state

end State 3

Step 4: State 3 -- simpleMPImplGood.mmp line 13 [main@3->main@4] "m = 0;" -> State 4

begin State 4

onStack = true;
seen = true;
pathCondition : true
begin model state

begin shared variables

s = undefined;
t = undefined;

end shared variables;
begin process 0

begin stack frame 0

function : main;
location : 4;
i = 7;
j = 5;
k = 0;
m = 0;

end stack frame 0;

end process 0;

end model state

end State 4

Step 5: State 4 -- simpleMPImplGood.mmp line 14 [main@4->main@5] "if (PID == 0)" [true]

[Stephen Siegel]

I think the problem is that this example requires at least 2 processes to run but it is invoked with 1 process (the default). But it is supposed to fail nicely and report the problem, rather than die with an ArrayOutOfBoundsException. Looks like this falls under my domain, so I will fix it. (Steve).

[Stephen Siegel]

Added checks that PID is in range in Evaluator and Executor. Now throws nice exception if not.