Test "gov.nasa.jpf.test.java.concurrent.SemaphoreTest" fails on OpenJDK-17

[eklaDFF]

Hi @cyrille-artho , this test also fails on OpenJDK-17

Here is the Standard Output :

running jpf with args:
JavaPathfinder core system v8.0 (rev 76cd506eb2d0de999cc263b3315b4f930c1505ad) - (C) 2005-2014 United States Government. All rights reserved.

====================================================== system under test
gov.nasa.jpf.test.java.concurrent.SemaphoreTest.runTestMethod()

====================================================== search started: 20/06/24, 11:37 pm
[WARNING] orphan NativePeer method: jdk.internal.misc.Unsafe.getUnsafe()Lsun/misc/Unsafe;
Thread-1 acquiring resource..
Thread-1 got resource: Resource-0
Thread-1 releasing resource: Resource-0
Thread-1 released
Thread-2 acquiring resource..
Thread-2 got resource: Resource-0
Thread-2 releasing resource: Resource-0
Thread-2 released
Thread-2 acquiring resource..
Thread-1 released
Thread-2 got resource: Resource-0
Thread-2 releasing resource: Resource-0
Thread-2 released
Thread-1 released
Thread-2 got resource: Resource-0
Thread-2 releasing resource: Resource-0
Thread-2 released

====================================================== error 1
gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
java.lang.NoSuchMethodError: jdk.internal.misc.Unsafe.getAndBitwiseAndInt(Ljava/lang/Object;JI)I
    at java.util.concurrent.locks.AbstractQueuedSynchronizer$Node.getAndUnsetStatus(AbstractQueuedSynchronizer.java:468)
    at java.util.concurrent.locks.AbstractQueuedSynchronizer.signalNext(AbstractQueuedSynchronizer.java:610)
    at java.util.concurrent.locks.AbstractQueuedSynchronizer.releaseShared(AbstractQueuedSynchronizer.java:1095)
    at java.util.concurrent.Semaphore.release(Semaphore.java:432)
    at gov.nasa.jpf.test.java.concurrent.SemaphoreTest.putItem(SemaphoreTest.java:92)
    at gov.nasa.jpf.test.java.concurrent.SemaphoreTest$Client.run(SemaphoreTest.java:116)

====================================================== snapshot #1
thread java.lang.Thread:{id:1,name:Thread-1,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  call stack:
    at gov.nasa.jpf.test.java.concurrent.SemaphoreTest.putItem(SemaphoreTest.java:97)
    at gov.nasa.jpf.test.java.concurrent.SemaphoreTest$Client.run(SemaphoreTest.java:116)

thread java.lang.Thread:{id:2,name:Thread-2,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  call stack:
    at java.util.concurrent.locks.AbstractQueuedSynchronizer.acquire(AbstractQueuedSynchronizer.java:715)
    at java.util.concurrent.locks.AbstractQueuedSynchronizer.acquireSharedInterruptibly(AbstractQueuedSynchronizer.java:1047)
    at java.util.concurrent.Semaphore.acquire(Semaphore.java:318)
    at gov.nasa.jpf.test.java.concurrent.SemaphoreTest.getItem(SemaphoreTest.java:72)
    at gov.nasa.jpf.test.java.concurrent.SemaphoreTest$Client.run(SemaphoreTest.java:108)

====================================================== results
error #1: gov.nasa.jpf.vm.NoUncaughtExceptionsProperty "java.lang.NoSuchMethodError: jdk.internal.misc.Uns..."

====================================================== search finished: 20/06/24, 11:37 pm

[cyrille-artho]

Thanks for noticing this. This may be easier to fix than other issues, because all we need is an implementation of getAndBitwiseAndInt with the equivalent behavior; we don't need it to be optimized in any way.

[eklaDFF]

/**
     * Atomically replaces the current value of a field or array element within
     * the given object with the result of bitwise AND between the current value
     * and mask.
     *
     * @param o object/array to update the field/element in
     * @param offset field/element offset
     * @param mask the mask value
     * @return the previous value
     * @since 9
     */
    @ForceInline
    public final int getAndBitwiseAndInt(Object o, long offset, int mask) {
        int current;
        do {
            current = getIntVolatile(o, offset);
        } while (!weakCompareAndSetInt(o, offset,
                                                current, current & mask));
        return current;
    }

/** Volatile version of {@link #getInt(Object, long)}  */
    @IntrinsicCandidate
    public native int     getIntVolatile(Object o, long offset);

@IntrinsicCandidate
    public final boolean weakCompareAndSetInt(Object o, long offset,
                                              int expected,
                                              int x) {
        return compareAndSetInt(o, offset, expected, x);
    }

/**
     * Atomically updates Java variable to {@code x} if it is currently
     * holding {@code expected}.
     *
     * <p>This operation has memory semantics of a {@code volatile} read
     * and write.  Corresponds to C11 atomic_compare_exchange_strong.
     *
     * @return {@code true} if successful
     */
    @IntrinsicCandidate
    public final native boolean compareAndSetInt(Object o, long offset,
                                                 int expected,
                                                 int x);

Overall the method getAndBitwiseAndInt(Object o, long offset, int mask) depends on native methods.

Please explain the working of getAndBitwiseAndInt() method, so that we could create the same on our own.

[cyrille-artho]

This method access an array element (getIntVolatile) and then applies the bit mask mask to it: current will be set to current & mask. The entire operation is atomic. The latter is not too hard to achieve in JPF as long as the calculation is done at JPF level (in a native peer), because native peers are atomic by design. There are also already helper methods in JPF's Unsafe, such as compareAndSetInt.

[eklaDFF]

Hi, after implementing the getAndBitwiseAndInt() method,

hanged on :

: <============-> 96% EXECUTING [35m 5s] :test > 80 tests completed, 2 failed :test > Executing test gov.nasa.jpf.test.java.concurrent.ExecutorServiceTest

We are working on gov.nasa.jpf.test.java.concurrent.SemaphoreTest and testing it alone also get hanged on.

[cyrille-artho]

Can you please share your work in progress (on a branch in your repo) so we can take a look at it? These atomic functions can be tricky because they have to be implemented correctly so JPF does not end up using native functionality that may wait on something that never happens (which is probably what you are observing when you see no progress).

[eklaDFF]

https://github.com/eklaDFF/jpf-core/tree/getAndBitwiseAndIntBRANCH

[cyrille-artho]

Thanks for sharing. As you have adapted a few lines from OpenJDK 17, you have changed the loop from

do { ... } while (!weakCompareAndSetInt(...))

to

do { ... } while (weakCompareAndSetInt(...))

I guess this was accidental? I assume that weakCompareAndSetInt behaves the same in JPF as in OpenJDK, so negating its return value will likely yield a wrong result. I get an infinite loop when I run the tests on your branch, probably due to the negated while condition?

[eklaDFF]

Hi, as I mentioned earlier that after implementing do { ... } while (!weakCompareAndSetInt(...)) we got new sort of error as below :

 running jpf with args:
JavaPathfinder core system v8.0 (rev ba7891bcf8074e7481d9921ebd71dfaf7be172bf) - (C) 2005-2014 United States Government. All rights reserved.

====================================================== system under test
gov.nasa.jpf.test.java.concurrent.SemaphoreTest.runTestMethod()

====================================================== search started: 28/06/24, 11:36 am
[WARNING] orphan NativePeer method: jdk.internal.misc.Unsafe.getUnsafe()Lsun/misc/Unsafe;
Thread-1 acquiring resource..
Thread-1 got resource: Resource-0
Thread-1 releasing resource: Resource-0
Thread-1 released
Thread-2 acquiring resource..
Thread-2 got resource: Resource-0
Thread-2 releasing resource: Resource-0
Thread-2 released
Thread-2 acquiring resource..
Thread-1 released
Thread-2 got resource: Resource-0
Thread-2 releasing resource: Resource-0
Thread-2 released
Thread-1 released
Thread-2 got resource: Resource-0
Thread-2 releasing resource: Resource-0
Thread-2 released
Thread-1 released

====================================================== error 1
gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
java.lang.NoSuchMethodError: jdk.internal.misc.Unsafe.putIntOpaque(Ljava/lang/Object;JI)V
    at java.util.concurrent.locks.AbstractQueuedSynchronizer$Node.clearStatus(AbstractQueuedSynchronizer.java:477)
    at java.util.concurrent.locks.AbstractQueuedSynchronizer.acquire(AbstractQueuedSynchronizer.java:720)
    at java.util.concurrent.locks.AbstractQueuedSynchronizer.acquireSharedInterruptibly(AbstractQueuedSynchronizer.java:1047)
    at java.util.concurrent.Semaphore.acquire(Semaphore.java:318)
    at gov.nasa.jpf.test.java.concurrent.SemaphoreTest.getItem(SemaphoreTest.java:72)
    at gov.nasa.jpf.test.java.concurrent.SemaphoreTest$Client.run(SemaphoreTest.java:108)

====================================================== snapshot #1
thread java.lang.Thread:{id:2,name:Thread-2,status:UNBLOCKED,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  call stack:
    at java.util.concurrent.locks.AbstractQueuedSynchronizer$Node.clearStatus(AbstractQueuedSynchronizer.java:477)
    at java.util.concurrent.locks.AbstractQueuedSynchronizer.acquire(AbstractQueuedSynchronizer.java:720)
    at java.util.concurrent.locks.AbstractQueuedSynchronizer.acquireSharedInterruptibly(AbstractQueuedSynchronizer.java:1047)
    at java.util.concurrent.Semaphore.acquire(Semaphore.java:318)
    at gov.nasa.jpf.test.java.concurrent.SemaphoreTest.getItem(SemaphoreTest.java:72)
    at gov.nasa.jpf.test.java.concurrent.SemaphoreTest$Client.run(SemaphoreTest.java:108)

====================================================== results
error #1: gov.nasa.jpf.vm.NoUncaughtExceptionsProperty "java.lang.NoSuchMethodError: jdk.internal.misc.Uns..."

====================================================== search finished: 28/06/24, 11:36 am

jdk.internal.misc.Unsafe.putIntOpaque(...) uses a native method which is already present in our Unsafe.java class. Like below :

public final void putIntOpaque(Object o, long offset, int x) {
    putIntVolatile(o, offset, x);
  }

And.. finally this test PASSED

[cyrille-artho]

OK, this suggests that getAndBitwiseAndIntBRANCH now works. For each missing putWhateverOpaque method, forward it to putWhateverVolatile. Does that work?

[eklaDFF]

Taking about to implement all methods similar to that ? (putIntOpaque())

[cyrille-artho]

Yes, within JPF, we can forward a call to the Opaque accessors to the Volatile counterpart.

[eklaDFF]

Yes, it worked .

[cyrille-artho]

Please make a PR with the additional methods in Unsafe.

[eklaDFF]

Hi, due working parallel on different issues, I am messed up with creating isolated clean PR.

Scenario is, while working on getAndBitwiseAndIntBRANCH there is some changes merged into Original jpf. To create isolated PR, I will have to rebase getAndBitwiseAndIntBRANCH so that my forked branch can compare with jpf/java-17 branch.

Here, I'm messed with it while doing this. There is not much resources which can understand my scenario.

How can I do this ?

[eklaDFF]

Please let me know, how can I do it for later ?

By the way, deleted this branch and created new one with same name and re-implemented those codes for now : PR #468

[cyrille-artho]

Fixed by PR #468