#51 JPF v4: Assertion failure for simple cyclic deadlock

[Strider]

JPF 4 (build 348 and older) fails to detect a simple cyclic deadlock when synchronized methods are used. It works when explicit synchronization is used with "synchronized (this)". For synchronized methods, an assertion failure is produced. Turning assertions off results in no deadlock being reported (which is incorrect).

JPF 3.0a successfully treats both cases.

The attached code is arranged so that code (1: correct case) is used if it is invoked without argument and code (2: leads to assertion failure) is used if it is invoked with an argument.

The second case fails with an AssertionError:

#using JPF4 rev 348

jpf Friendly a

JavaPathfinder v4.1 - (C) 1999-2007 RIACS/NASA Ames Research Center

====================================================== system under test
application: Friendly.java
arguments: a

====================================================== search started: 5/29/07 4:12 PM
java.lang.AssertionError: locking: Friendly@244 by Thread-0 failed, lock owned by: Thread-1
at gov.nasa.jpf.jvm.ElementInfo.lock(ElementInfo.java:979)
at gov.nasa.jpf.jvm.MethodInfo.enter(MethodInfo.java:638)
at gov.nasa.jpf.jvm.MethodInfo.execute(MethodInfo.java:684)
at gov.nasa.jpf.jvm.bytecode.INVOKESPECIAL.execute(INVOKESPECIAL.java:52)
at gov.nasa.jpf.jvm.ThreadInfo.executeInstruction(ThreadInfo.java:1596)
at gov.nasa.jpf.jvm.ThreadInfo.executeStep(ThreadInfo.java:2117)
at gov.nasa.jpf.jvm.SystemState.nextSuccessor(SystemState.java:449)
at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1224)
at gov.nasa.jpf.search.Search.forward(Search.java:357)
at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:86)
at gov.nasa.jpf.JPF.run(JPF.java:371)
at gov.nasa.jpf.JPF.main(JPF.java:298)

[Strider]

Simple program that reproduces assertion failure