"gov.nasa.jpf.test.java.concurrent.CountDownLatchTest" and "gov.nasa.jpf.test.java.concurrent.ExecutorServiceTest" fails on Java-17

[eklaDFF]

gov.nasa.jpf.test.java.concurrent.CountDownLatchTest and gov.nasa.jpf.test.java.concurrent.ExecutorServiceTest both fails with error message as :

gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
java.lang.UnsatisfiedLinkError: cannot find native java.lang.invoke.MethodHandleNatives.registerNatives
    at java.lang.invoke.MethodHandleNatives.registerNatives(no peer)
    at java.lang.invoke.MethodHandleNatives.<clinit>(MethodHandleNatives.java:105)
    at java.lang.invoke.MemberName$Factory.resolve(MemberName.java:1085)
    at java.lang.invoke.MemberName$Factory.resolveOrFail(MemberName.java:1114)
    at java.lang.invoke.MethodHandles$Lookup.resolveOrFail(MethodHandles.java:3641)
    at java.lang.invoke.MethodHandles$Lookup.findStaticVarHandle(MethodHandles.java:3241)
    at java.util.concurrent.ForkJoinPool.<clinit>(ForkJoinPool.java:3488)
    at java.util.concurrent.locks.AbstractQueuedSynchronizer$ConditionObject.await(AbstractQueuedSynchronizer.java:1623)
    at java.util.concurrent.LinkedBlockingQueue.take(LinkedBlockingQueue.java:435)
    at java.util.concurrent.ThreadPoolExecutor.getTask(ThreadPoolExecutor.java:1062)
    at java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1122)
    at java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:635)

[cyrille-artho]

JPF has a different way of handling native code (with @MJI annotation and native peers). We currently have a native peer for MethodHandle but not MethodHandleNatives. Maybe we can resolve this by providing an empty stub in a native peer for MethodHandleNatives. Try creating src/peers/gov/nasa/jpf/vm/JPF_java_lang_invoke_MethodHandleNatives.java with an empty stub for the (mangled) method representing registerNatives.

[eklaDFF]

Please review it too @cyrille-artho

[cyrille-artho]

You have made one PR that fixes one of the unit tests that previously failed. I have merged that PR. Is there something else to review? You can either share a branch or make a PR with draft status if you'd like us to review some work in progress.

[eklaDFF]

public class JPF_java_lang_invoke_MethodHandleNatives extends NativePeer {
    @MJI
    public static void registerNatives____V(MJIEnv env, int clsObjRef) {
        // empty stub
    }
}

And then new error StackTrace are :

====================================================== error 1
gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
java.lang.UnsatisfiedLinkError: cannot find native java.lang.invoke.MethodHandleNatives.getNamedCon
    at java.lang.invoke.MethodHandleNatives.getNamedCon(gov.nasa.jpf.vm.JPF_java_lang_invoke_MethodHandleNatives)
    at java.lang.invoke.MethodHandleNatives.verifyConstants(MethodHandleNatives.java:228)
    at java.lang.invoke.MethodHandleNatives.<clinit>(MethodHandleNatives.java:251)
    at java.lang.invoke.MemberName$Factory.resolve(MemberName.java:1085)
    at java.lang.invoke.MemberName$Factory.resolveOrFail(MemberName.java:1114)
    at java.lang.invoke.MethodHandles$Lookup.resolveOrFail(MethodHandles.java:3641)
    at java.lang.invoke.MethodHandles$Lookup.findStaticVarHandle(MethodHandles.java:3241)
    at java.util.concurrent.ForkJoinPool.<clinit>(ForkJoinPool.java:3488)
    at java.util.concurrent.locks.AbstractQueuedSynchronizer$ConditionObject.await(AbstractQueuedSynchronizer.java:1623)
    at java.util.concurrent.LinkedBlockingQueue.take(LinkedBlockingQueue.java:435)
    at java.util.concurrent.ThreadPoolExecutor.getTask(ThreadPoolExecutor.java:1062)
    at java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1122)
    at java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:635)

And here is the details for above error :

private static native int getNamedCon(int which, Object[] name);

    static boolean verifyConstants() {
        Object[] box = { null };
        for (int i = 0; ; i++) {
            box[0] = null;
            int vmval = getNamedCon(i, box);
            if (box[0] == null)  break;
            String name = (String) box[0];
            try {
                Field con = Constants.class.getDeclaredField(name);
                int jval = con.getInt(null);
                if (jval == vmval)  continue;
                String err = (name+": JVM has "+vmval+" while Java has "+jval);
                if (name.equals("CONV_OP_LIMIT")) {
                    System.err.println("warning: "+err);
                    continue;
                }
                throw new InternalError(err);
            } catch (NoSuchFieldException | IllegalAccessException ex) {
                String err = (name+": JVM has "+vmval+" which Java does not define");
                // ignore exotic ops the JVM cares about; we just wont issue them
                //System.err.println("warning: "+err);
                continue;
            }
        }
        return true;
    }

    static {
        assert(verifyConstants());
    }

[cyrille-artho]

This is a non-public function in a package-private class, so it is difficult to implement something that works on JPF. We can try to exploit the fact that box[0] is null before the function is called; it is expected to modify that value when further checking is needed, otherwise the loop exists with break. So a stub that returns 0 should work in the sense that the function above exits (as box[0] remains null).

If we get a lot of further problems that we cannot resolve with empty stubs, we have to try adding a model class that intercepts a call earlier in the stack trace at the very top of this issue.

[eklaDFF]

@MJI
    public static int getNamedCon__I_3Ljava_lang_Object_2__I(MJIEnv env, int clsObjRef, int which, int nameArrayRef) {
        // empty stub, returning 0 or an appropriate value if needed
        return 0;
    }

====================================================== error 1
gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
java.lang.ExceptionInInitializerError
    at java.util.concurrent.ForkJoinPool.<clinit>(ForkJoinPool.java:3490)
    at java.util.concurrent.locks.AbstractQueuedSynchronizer$ConditionObject.await(AbstractQueuedSynchronizer.java:1623)
    at java.util.concurrent.LinkedBlockingQueue.take(LinkedBlockingQueue.java:435)
    at java.util.concurrent.ThreadPoolExecutor.getTask(ThreadPoolExecutor.java:1062)
    at java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1122)
    at java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:635)
Caused by: java.lang.IllegalAccessException: no such field: java.util.concurrent.ForkJoinPool.poolIds/int/getStatic
    at java.lang.invoke.MemberName.makeAccessException(MemberName.java:972)
    at java.lang.invoke.MemberName$Factory.resolveOrFail(MemberName.java:1117)
    at java.lang.invoke.MethodHandles$Lookup.resolveOrFail(MethodHandles.java:3641)
    at java.lang.invoke.MethodHandles$Lookup.findStaticVarHandle(MethodHandles.java:3241)
    at java.util.concurrent.ForkJoinPool.<clinit>(ForkJoinPool.java:3488)
    at java.util.concurrent.locks.AbstractQueuedSynchronizer$ConditionObject.await(AbstractQueuedSynchronizer.java:1623)
    at java.util.concurrent.LinkedBlockingQueue.take(LinkedBlockingQueue.java:435)
    at java.util.concurrent.ThreadPoolExecutor.getTask(ThreadPoolExecutor.java:1062)
    at java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1122)
    at java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:635)
Caused by: java.lang.UnsatisfiedLinkError: cannot find native java.lang.invoke.MethodHandleNatives.resolve
    at java.lang.invoke.MethodHandleNatives.resolve(gov.nasa.jpf.vm.JPF_java_lang_invoke_MethodHandleNatives)
    at java.lang.invoke.MemberName$Factory.resolve(MemberName.java:1085)
    at java.lang.invoke.MemberName$Factory.resolveOrFail(MemberName.java:1114)
    at java.lang.invoke.MethodHandles$Lookup.resolveOrFail(MethodHandles.java:3641)
    at java.lang.invoke.MethodHandles$Lookup.findStaticVarHandle(MethodHandles.java:3241)
    at java.util.concurrent.ForkJoinPool.<clinit>(ForkJoinPool.java:3488)
    at java.util.concurrent.locks.AbstractQueuedSynchronizer$ConditionObject.await(AbstractQueuedSynchronizer.java:1623)
    at java.util.concurrent.LinkedBlockingQueue.take(LinkedBlockingQueue.java:435)
    at java.util.concurrent.ThreadPoolExecutor.getTask(ThreadPoolExecutor.java:1062)
    at java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1122)
    at java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:635)

[cyrille-artho]

It looks like the reflection operations need more support; similar to JPFFieldVarHandle and its peer, we have to provide key methods for method handles. I think the best course of action is to create a very small test that uses reflection to obtain such a handle, run the example on the regular JVM to make sure it succeeds, and then start looking into JPF's data structures and how to use them in the MethodHandle API.

[eklaDFF]

It's a bit complex one understand the background here. I don't think I fully understand what you were saying about… Could you tell me a bit more?

Is it about providing key methods like java.lang.invoke.MethodHandleNatives.resolve() methods here ?

static native MemberName resolve(MemberName self, Class<?> caller, int lookupMode,
            boolean speculativeResolve) throws LinkageError, ClassNotFoundException;

[cyrille-artho]

Let's look at this during the meeting tomorrow. I think it's better to try to resolve the string encoding issue first (and if you get completely stuck, some compiler warnings). The problem here is that it seems we have to support too many non-public classes if we try to support MethodHandleNatives. It looks like it's better to make the "cut" at MethodHandles and look at replacing java.lang.invoke.MethodHandles$Lookup.findStaticVarHandle.

[eklaDFF]

After issue #475, we have solved the major complexity of this problem. Thank You @cyrille-artho . Your bit by bit explanation made it.

Here is the next sort of error :

====================================================== error 1
gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
java.lang.NoSuchMethodException: jdk.internal.access.SharedSecrets.setJavaSecurityAccess(Ljdk/internal/access/JavaSecurityAccess;)V
    at java.security.ProtectionDomain.<clinit>(ProtectionDomain.java:133)
    at java.util.concurrent.ForkJoinPool.contextWithPermissions(ForkJoinPool.java:764)
    at java.util.concurrent.ForkJoinPool$DefaultForkJoinWorkerThreadFactory.<clinit>(ForkJoinPool.java:804)
    at java.util.concurrent.ForkJoinPool.<clinit>(ForkJoinPool.java:3506)
    at java.util.concurrent.locks.AbstractQueuedSynchronizer$ConditionObject.await(AbstractQueuedSynchronizer.java:1623)
    at java.util.concurrent.LinkedBlockingQueue.take(LinkedBlockingQueue.java:435)
    at java.util.concurrent.ThreadPoolExecutor.getTask(ThreadPoolExecutor.java:1062)
    at java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1122)
    at java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:635)

From this, we clearly see that there is a missing method setJavaSecurityAccess(). This method is not a complex one, below is the code from OpenJDK to understand it.

...
private static JavaSecurityAccess javaSecurityAccess;
...
public static void setJavaSecurityAccess(JavaSecurityAccess jsa) {
        javaSecurityAccess = jsa;
    }

This method sets the value of JavaSecurityAccess javaSecurityAccess. So copied them to our own model class as it is.

[eklaDFF]

gov.nasa.jpf.test.java.concurrent.ExecutorServiceTest PASSED after above method implementation.

But for gov.nasa.jpf.test.java.concurrent.CountDownLatchTest, error trace is :

====================================================== error 1
gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
java.lang.NoSuchMethodError: jdk.internal.misc.Unsafe.weakCompareAndSetReference(Ljava/lang/Object;JLjava/lang/Object;Ljava/lang/Object;)Z
    at java.util.concurrent.locks.AbstractQueuedSynchronizer$Node.casNext(AbstractQueuedSynchronizer.java:465)
    at java.util.concurrent.locks.AbstractQueuedSynchronizer.cleanQueue(AbstractQueuedSynchronizer.java:743)
    at java.util.concurrent.locks.AbstractQueuedSynchronizer.cancelAcquire(AbstractQueuedSynchronizer.java:776)
    at java.util.concurrent.locks.AbstractQueuedSynchronizer.acquire(AbstractQueuedSynchronizer.java:725)
    at java.util.concurrent.locks.AbstractQueuedSynchronizer.acquireInterruptibly(AbstractQueuedSynchronizer.java:958)
    at java.util.concurrent.locks.ReentrantLock$Sync.lockInterruptibly(ReentrantLock.java:161)
    at java.util.concurrent.locks.ReentrantLock.lockInterruptibly(ReentrantLock.java:372)
    at java.util.concurrent.LinkedBlockingQueue.take(LinkedBlockingQueue.java:432)
    at java.util.concurrent.ThreadPoolExecutor.getTask(ThreadPoolExecutor.java:1062)
    at java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1122)
    at java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:635)

Now we can see that we need method jdk.internal.misc.Unsafe.weakCompareAndSetReference(...).

Here is it's implementation in OpenJDK :

public final boolean weakCompareAndSetReference(Object o, long offset,
                                                    Object expected,
                                                    Object x) {
        return compareAndSetReference(o, offset, expected, x);
    }

In our model class jdk.internal.misc.Unsafe, we already have compareAndSetReference(...) method as a native method. So again just copied it (weakCompareAndSetReference).

---

Now BOTH Tests PASSES

[cyrille-artho]

Great! This is again one correct behavior that may ignore some subsequent possible behaviors, as we don't implement the full JMM semantics in this case.

[eklaDFF]

Should I create PR for this now ?

Also, do we have to keep those 6 tests ?

[cyrille-artho]

Yes, please create a PR for this. Which six tests are you referring to? The tests regarding var handles? A PR should always pair a fix (or enhancement) with at least one test that shows what the fix achieved. So at least one new (or strengthened) test should show that the old version of the code failed in some way (at least one test should fail without the implementation changes), and the implementation changes fix all previously failing tests. If you create a PR that supports the var handle functionality correctly, make sure you include the six new tests for that.

[eklaDFF]

"Which six tests are you referring to? The tests regarding var handles?" -----> Yes, those Tests we wrote for analysing instance and static variables. testFindVarHandleInstanceField() testFindVarHandleStaticField() testFindVarHandleNoSuchField() testFindStaticVarHandleInstanceField() testFindStaticVarHandleStaticField() testFindStaticVarHandleNoSuchField()

I am keeping these in PR as it will explain the situation more in future.

[eklaDFF]

PR #478