search

javapathfinder / jpf-core

JPF is an extensible software analysis framework for Java bytecode. jpf-core is the basis for all JPF projects; you always need to install it. It contains the basic VM and model checking infrastructure, and can be used to check for concurrency defects like deadlocks, and unhandled exceptions like NullPointerExceptions and AssertionErrors.
517 stars 326 forks source link

"gov.nasa.jpf.test.java.concurrent.ConcurrentSkipListMapTest" fails on Java-17 #471

Open eklaDFF opened 3 days ago

eklaDFF commented 3 days ago

gov.nasa.jpf.test.java.concurrent.ConcurrentSkipListMapTest Test fails on Java-17. Throws error as :

gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
java.lang.NoSuchMethodError: java.lang.invoke.JPFFieldVarHandle.weakCompareAndSetRelease(Ljava/util/concurrent/atomic/Striped64;JJ)Z
    at java.util.concurrent.atomic.Striped64.casBase(Striped64.java:181)
    at java.util.concurrent.atomic.LongAdder.add(LongAdder.java:87)
    at java.util.concurrent.ConcurrentSkipListMap.addCount(ConcurrentSkipListMap.java:441)
    at java.util.concurrent.ConcurrentSkipListMap.doPut(ConcurrentSkipListMap.java:683)
    at java.util.concurrent.ConcurrentSkipListMap.put(ConcurrentSkipListMap.java:1347)
    at gov.nasa.jpf.test.java.concurrent.ConcurrentSkipListMapTest.testFunctionality(ConcurrentSkipListMapTest.java:37)
    at java.lang.reflect.Method.invoke(gov.nasa.jpf.vm.JPF_java_lang_reflect_Method)
    at gov.nasa.jpf.util.test.TestJPF.runTestMethod(TestJPF.java:648)
eklaDFF commented 2 days ago

@cyrille-artho Look into this also, as #459 may take more time

cyrille-artho commented 1 day ago

JPF (jpf-core) does not implement the full memory model in detail. We therefore do not have to implement the subtle differences that can arise between compareAndSet and compareAndSetRelease. The latter can simply call the former.

For details, see, e.g., https://chatgpt.com/share/65641ce7-6af3-4123-bca6-b0e8cc05ee25 https://link.springer.com/chapter/10.1007/978-3-642-28756-5_16

cyrille-artho commented 1 day ago

When you implement this, please add a comment that clarifies that JPF does not generate all possible outcomes here.

eklaDFF commented 7 hours ago

Here is the implementation :

boolean weakCompareAndSetRelease(Object aqs, int expect, int update){
    return compareAndSet(aqs,expect,update); // JPF here do not clarify about generating all possible outcomes
}
boolean weakCompareAndSetRelease(Object owner, long expect, long update){
    return compareAndSet(owner, expect, update); // JPF here do not clarify about generating all possible outcomes
}
boolean weakCompareAndSetRelease(Object aqs, Object expect, Object update){
   return compareAndSet(aqs, expect, update); // JPF here do not clarify about generating all possible outcomes
}

And now the test passes.