matmat compare: outputs not equivalent?

[Stephen Siegel]

Running compare on matmat, everything seems fine until the end, when the results are compared. Here is the command:

compare -simplify  -verbose /Users/siegel/Documents/workspace/MiniMP/examples/matmat/matmat-seq_1_1_2.mmp -np 1 /Users/siegel/Documents/workspace/MiniMP/examples/matmat/matmat-par_1_1_2.mmp -np 2

Here is the report that the two results may differ, but they look the same!:

Possible violation detected with specification at State 47
Possible incorrect final value for implementation output variable c at State 90.
Expected value: real[X2][X1]: matmat-seq_1_1_2_V5<(0, 0), (X3[0, 0]*X4[0, 0])><(1, 0), (X4[0, 0]*X3[0, 1])>
Actual value: real[X2][X1]: matmat-par_1_1_2_V5<(0, 0), (X3[0, 0]*X4[0, 0])><(1, 0), (X4[0, 0]*X3[0, 1])>

Here is the actual CVC3 query that returns false:

CVC3 prover invoked with query: TRUE under context TRUE 
Valid
CVC3 prover invoked with query: TRUE under context TRUE 
Valid
CVC3 prover invoked with query: (FORALL (_BD1TY0: INT, _BD2TY0: INT): (LET cvc_1 = X3[0],
cvc_2 = X4[0][0],
cvc_7 = (cvc_1[0] * cvc_2),
cvc_5 = (cvc_2 * cvc_1[1]),
cvc_9 = (_BD2TY0 * -1),
cvc_6 = (_BD2TY0 = 0),
cvc_0 = (_BD1TY0 = 0),
cvc_4 = ((cvc_9 + 1) = 0),
cvc_3 = matmat-seq_1_1_2_V5[_BD1TY0],
cvc_8 = matmat-par_1_1_2_V5[_BD1TY0]
IN ((IF cvc_4 THEN IF cvc_0 THEN cvc_5 ELSE cvc_3[1] ENDIF ELSE IF cvc_6 THEN IF cvc_0 THEN cvc_7 ELSE cvc_3[0] ENDIF ELSE cvc_3[_BD2TY0] ENDIF ENDIF = IF cvc_4 THEN IF cvc_0 THEN cvc_5 ELSE cvc_8[1] ENDIF ELSE IF cvc_6 THEN IF cvc_0 THEN cvc_7 ELSE cvc_8[0] ENDIF ELSE cvc_8[_BD2TY0] ENDIF ENDIF) OR NOT ((0 <= ((cvc_9 + -1) + X2)) AND ((0 <= _BD2TY0) AND ((0 <= (((_BD1TY0 * -1) + -1) + X2)) AND (0 <= _BD1TY0))))))) under context ((0 <= (X2 + -2)) AND ((0 <= (X0 + -1)) AND ((0 <= (X1 + -1)) AND ((0 <= (X2 + -1)) AND ((0 <= ((X2 * -1) + 2)) AND ((0 <= X2) AND ((0 <= ((X1 * -1) + 1)) AND ((0 <= X1) AND ((0 <= ((X0 * -1) + 1)) AND (0 <= X0)))))))))) 
Invalid

Any ideas what is going on?

[zirkel]

I made an attempt to translate the cvc3 query into a more readable form:

forall integers y1, y2:

(if(y2 = 1){

if(y1 = 0){

X4[0][0]*X3[0][1]

}
else {

matmat-seq_1_1_2_V5[y1][1]

}

}
else{

if(y2 = 0){

if(y1 = 0){

X3[0][0]*X4[0][0]

}
else{

matmat-seq_1_1_2_V5[y1][0]

}

}
else{

matmat-seq_1_1_2_V5[y1][y2]

}

}

if(y2 = 1) {

if(y1 = 0){

X4[0][0]*X3[0][1]

}
else{

matmat-par_1_1_2_V5[y1][1]

}

}
else{

if(y2 = 0){

if(y1 = 0){

X3[0][0]*X4[0][0]

}
else{

matmat-par_1_1_2_V5[y1][0]

}

}
else{

matmat-par_1_1_2_V5[y1][y2]

}

})

NOT((0<=-y2-1+X2) && ((0<=y2) && ((0<=-y1-1+X2) && (0<=y1))))

under context
1 <= X2 <= 2
X1 = 1
0 <= X0 <= 1

[zirkel]

File containing more readable version of CVC3 input

[Stephen Siegel]

This is an excerpt from CVC3TheoremProver.java. I believe this is attempting to iterate through the dimensions of a multi-dimensional array. However the variable left is never updated in the while loop, so the variable storing the upper bound upper is always the same as it was on iteration 0, i.e., the upper bound of the outermost dimension is used for every dimension. This might explain the failure.

  	//convert it to forall expressions when comparing array type expressions.
    	else
    	{
    		//Extract the dimensions and create temporary bound variables
    		List boundVars = new Vector();
    		checkTypeConsistency(left.getType(), right.getType());
    		String tempName = "_TASS_index";
    		Type type = vc.intType();
    		int id = 0;
    		Expr lowerBound = vc.ratExpr(0);
    		Expr upperBound = null;
    		
    		Expr predicate = null;
    		
    		SymType leftType = left.getType();
    		
    		//Create new bound variables
    		while(!(leftType instanceof SymSimpleType))
    		{
    			SymExpression upper = ((SymArray)(left.getType())).getDimension();
    			upperBound = parseSymExpr(upper);
    			Expr boundVar = vc.boundVarExpr(tempName + id,  tempName + id, type);
    			boundVars.add(boundVar);
    			
    			if(predicate == null)
    			{
    				predicate = vc.andExpr(vc.geExpr(boundVar, lowerBound), vc.ltExpr(boundVar, upperBound));
    			}
    			else
    			{
    				predicate = vc.andExpr(predicate, vc.andExpr(vc.geExpr(boundVar, lowerBound), vc.ltExpr(boundVar, upperBound)));
    			}
    			
    			leftType = ((SymArray)leftType).getBaseType();
    			//Increase id number to generate different bound variable names.
    			id++;
    		}

[ywei]

Bug fixed. The matmat JUnit test can pass except when using the urgent strategy. The test reported that a possible absolute deadlock detected.

[Stephen Siegel]

For me, all matmat tests pass, including textCompareUrgent.

[ywei]

Here is what I got from testCompareUrgent:

Using URGENT strategy.
Number of states seen: 21
Number of transitions: 20
Number of states matched: 0

Number of states seen: 48
Number of transitions: 47
Number of states matched: 0

Possible violation detected with specification at State 47
Possible deadlock detected in implementation.
Absolute deadlock possible at State 20.
Process 0: at location 9. Cannot prove enabling statement valid:
false
Process 1: at location 30. Cannot prove enabling statement valid:
false

Writing specification trace to /Users/ywei/Documents/MiniMP/MiniMPOutput/spec.trace...done.
Writing implementation trace to /Users/ywei/Documents/MiniMP/MiniMPOutput/impl.trace...done.
Writing specification model to /Users/ywei/Documents/MiniMP/MiniMPOutput/spec.model...done.
Writing implementation model to /Users/ywei/Documents/MiniMP/MiniMPOutput/impl.model...done.

[Stephen Siegel]

This is weird. If I just run the Matmat tests alone, I get the same thing you get. If however I run all of the JUnit tests at once, the Matmat tests all pass, including compareUrgent. In addition, they run much faster. Does the same thing happen to the rest of you? Any explanation?

[Stephen Siegel]

Think I figured it out. The tests are all getting their parameters from the static fields of ExecConfig. This class is only loaded once by the JVM. So the values set by the previous test are in effect when this test runs. The previous test was the last test in the SimpleArrayFailTest class, and this test set the deadlock property to "Ignore". That remains in effect through the Matmat tests (until it is finally re-set in the test TestComparePotential).

Using static data in this way is not a good idea. The data should be encapsulated in an object which is passed around as an argument. For a quick fix, you can just make sure to re-set everything in the static class before each test. Will start a separate ticket for this.

Oh, and the reason the urgent compare test was failing was because the buffer bound was set to 0, which resulted in deadlock. The buffer bound should always be positive for any program that does message passing. The command line already checks for this, but the tests bypass the command line. So correct all tests to use positive buffer bound in case of message passing programs.