jpf-concurrent usage

[Manuel Bravo]

Hi everyone,

I need to use jpf-concurrent. Nevertheless, I am not sure whether I am using it or not. How can I make sure?

I have added the extension to jpf.properties and I am using: @using jpf-concurrent, in my *.jpf file. The target application uses ReentrantLocks; therefore, in order to check whether the extension is being used, I added a simple println line in the jpg-concurrent class (gov.nasa.jpf.concurrent.ReentrantLock) everytime lock() method is called. I was expecting to see that line printed whenever my application call the method, but it is not happening. What am I doing wrong? I did check jpf-concurrent paper and it should be sufficient with the stuff I have done for configuring it.

Best,

Manuel

[Manuel Bravo]

I kind of manage to make it work. I have some questions regarding jpg-concurrent:

- When a ReentrantLock is acquired (by calling lock() method), is method objectLocked(JVM vm) (of a listener) notified?. In my experiments it is not, I would like to make sure.

- is park/unpark only triggered by await and signal in a application that only uses ReentrantLocks and Conditions?.

Thank you for your time.

Best,

Manuel

[Mateusz Ujma]

Dear Manuel,

The objectLocked(JVM vm) method is not executed when acquiring ReentrantLock, this is caused by the fact that ReentrantLock uses Unsafe class for thread blocking and not "synchronisation" keyword.

I am not sure if I understand your second question, park/unpark is called from Condition class as well as from ReentrantLock and almost any other class in jpf-concurrent that requires thread blocking.

Best regards

Mateusz Ujma

[Manuel Bravo]

Let me try to extend my question:

As far as I understand (reading jpf-concurrent code), an await call parks the thread, while a signal call unpark a thread. The unparked thread is the the thread that first call await for that condition. I think I got it till here. Nevertheless I am experimenting some weird cases:

For instance, lets imagine the next execution:

Having three threads. Two of them have called await; therefore they are parked. Now imagine the third one calls signal, then the thread who called await first should be unparked and a GC  should be triggered. Nevertheless, in the method public static void unpark__Ljava_lang_Object_2__V (MJIEnv env, int unsafeRef, int objRef) { of JPF_sun_misc_Unsafe (of jpf-core), the invocation can be repeated by calling env.repeatInvocation(). Therefore, the signal call will be repeated and the other thread (the one which is still parked) will be unparked.

It is not so easy to explain.. I hope it is clear.

To sum up, shouldn't a signal only unpark one thread?

Best,

Manuel

[Mateusz Ujma]

To sum up, shouldn't a signal only unpark one thread?

It depends whether we have fair or unfair ReentrantLock, in unfair you
unpark all threads but only one will acquire the lock and continue
(other will be parked again). In fair version you unpark the thread
that waited the longest time.

Best

Mateusz

> --
>
> ---
> You received this message because you are subscribed to a topic in the
> Google Groups "Java™ Pathfinder" group.
> To unsubscribe from this topic, visit
> https://groups.google.com/d/topic/java-pathfinder/ijzwdUZ5nZI/unsubscribe?hl=en.
> To unsubscribe from this group and all its topics, send an email to
> java-pathfind...@googlegroups.com.
> For more options, visit https://groups.google.com/groups/opt_out.
>
>



--
Best regards

Mateusz Ujma

[Manuel Bravo]

I might be doing sth wrong, but using a fair ReentrantLock, both threads are unparked, just the first one changed his state to RUNNING. The second one gets unparked but it does not change his state; therefore, it would be blocked forever (waiting state) since it is not parked again. 

Why the invocation of the nativeSignal has to be repeated?

Best,

Manuel

[Mateusz Ujma]

This is code for signal() method:

public boolean signal() {
if (getCurrentVersion().getQueuedThreads().size() > 0) {
removeAndUnpark(getCurrentVersion().getQueuedThreads().get(0));
saveVersion();
return true;
}
return false;
}

In my previous email I was wrong saying that all threads would be
woken up in case of unfair ReentrantLock. The default is the "fair"
behaviour (SDK does not specify whether Condition operations should be
fair/unfair). If you observe that all threads are unparked when
signal() is executed that might be a bug. Can you sent me a code
snippet showing that ?

[Manuel Bravo]

It is the same code that I have. The problem is that removeAndUnpark method calls unpack. Then unpack method calls JPF_sun_misc_Unsafe.unpark__Ljava_lang_Object_2__V from jpf-core. This is the method:

public static void unpark__Ljava_lang_Object_2__V (MJIEnv env, int unsafeRef, int objRef) {

    ThreadInfo ti = env.getThreadInfo();

    if (!ti.isFirstStepInsn()){

        System.out.println("No first step");

      ThreadInfo tiParked = env.getThreadInfoForObjRef(objRef);    

      if (tiParked == null || tiParked.isTerminated()){

        return;

      }      

      

      SystemState ss = env.getSystemState();

      int permitRef = env.getReferenceField( objRef, "permit");

      ElementInfo eiPermit = env.getElementInfo(permitRef);

      if (tiParked.getLockObject() == eiPermit){

        // note that 'permit' is only used in park/unpark, so there never is more than

        // one waiter, which immediately becomes runnable again because it doesn't hold a lock

        // (park is a lockfree wait). unpark() therefore has to be a right mover

        // and we have to register a ThreadCG here

        eiPermit.notifies(ss, ti, false);

        

        ChoiceGenerator<?> cg = env.getSchedulerFactory().createUnparkCG(tiParked);

        if (cg != null){

          ss.setNextChoiceGenerator(cg);

          System.out.println("Repeating invocation");

          env.repeatInvocation();

        }

        

      } else {

          System.out.println("Yes first step");

        eiPermit.setBooleanField("blockPark", false);

      }      

    }

  }

As you can see (in the underlined line), the execution of the signal can be repeated (env.repeatInvocation()). This repetition will call signal method and it would unpark another thread (in case there are still some). Therefore, it is not unparking every parked thread, but a maximum of two.

In think this is a problem and I am experimenting with it. I did modify removeAndUnpark method. This is my version and it seems to solve the problem:

private void removeAndUnpark(ThreadInfo t) {

    ThreadInfo ti = env.getThreadInfo();

    if (!ti.isFirstStepInsn()){

      System.out.println("Unparking thread: "+t);

      getCurrentVersion().removeThreadFromQueue(t);

      getCurrentVersion().addRecentlySignalled(t);

      unpark(t.getThreadObjectRef());

    }

  }

Nevertheless, I do not know whether this modification could affect other parts of the extension (since I am not an expert).

Please, find attached a silly application that reproduces the bug. It can produce deadlock, but the important part is that 2 threads are waiting when a third thread makes the signal. Adding System.out.println("Unparking thread: "+t); at the beginning of the method removeAndUnpark you will be able to see it.

I hope everything is clear. Thank you for your time.

Best,

Manuel

[Mateusz Ujma]

The fix seems ok.

Can you sent it to Nastaran (nastaran.shafiei AT gmail.com) as at this
point I don't have access to the repository.

Best regards

Mateusz Ujma

On Wed, May 8, 2013 at 4:41 PM, Manuel Bravo

[Manuel Bravo]

Sure, what do you want me to send? Just the class Condition.java (the one that contains the fix)?

Best,

Manuel

[Mateusz Ujma]

The best would be if you could write an regression test and include
the fix in a patch (diff) form.

On Fri, May 10, 2013 at 12:14 AM, Manuel Bravo