Deadlock not being detected

[Maria Ramos]

I have defined a simple bank class which is attached to this issue.
Basically it's a bank with a map of ids (ints) to accounts (instances of the class Account) and a lock (RentrantReadWriteLock) to control the access to this map. The class Account has a balance (int) and a lock (ReentrantLock) to protect the balance from concurrent accesses. Thus, we have concurrency control for:

• an individual account to prevent, for example, an withdraw and a deposit at the same time for the same account;
• the whole bank to prevent, for example, a removal and a deposit at the same time for the same account.

In the class defined there's a problem with the method transfer: in certain situations it can lead to a deadlock. This happens because the locks for the accounts are not obtained in order:
cfrom = accounts.get(from); cto = accounts.get(to);

For instance, if there's a transfer from account0 to account1 in thread1 at the same time as a transfer from account1 to account0 in thread2, the following thread interleaving leads to a deadlock:

• thread1 acquires lock from account0
• thread2 acquires lock from account1
• thread1 tries to acquire lock from account1 but it's taken
• thread2 tries to acquire lock from account0 but it's taken

I have been trying to catch this deadlock with jpf and it does not report it. I have been using the default jpf.properties, the only change I made was remove the gov.nasa.jpf.vm.NoUncaughtExceptionsProperty from search.properties. The application properties is as simple as:

target = BankReadWriteLock
classpath=.

I have tried to add to the application properties the gov.nasa.jpf.listener.DeadlockAnalyzer listener but it didn't work either.

This is the output I receive:

I find it to be very strange the fact that it only reports one new state. It seems like different thread interleavings are not being considered.

Is there a problem with the configuration I am using or jpf is really not catching this deadlock?

[Cyrille Artho]

Hi,

I have tried to run your example (without its jpf.properties file, as that was not working on my system), and I get an error trace that seems to indicate an issue with the Java libraries. So I'm unable to reproduce your issue until I have figured out that part.

gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
java.lang.Error: java.lang.NoSuchFieldException: tid
    at java.util.concurrent.locks.ReentrantReadWriteLock.<clinit>(ReentrantReadWriteLock.java:1506)
    at BankReadWriteLock.<init>(BankReadWriteLock.java:39)
    at BankReadWriteLock.main(BankReadWriteLock.java:147)
Caused by: java.lang.NoSuchFieldException: tid
    at java.lang.Class.getDeclaredField(gov.nasa.jpf.vm.JPF_java_lang_Class)
    at java.util.concurrent.locks.ReentrantReadWriteLock.<clinit>(ReentrantReadWriteLock.java:1504)
    at BankReadWriteLock.<init>(BankReadWriteLock.java:39)
    at BankReadWriteLock.main(BankReadWriteLock.java:147)

In your case, you don't hit this issue; what version of Java do you use to run JPF?

Different versions of Java sometimes produce different results. If you show me the output of "java -version", we can see if that is the reason why.

--

Regards,

Cyrille Artho

[Maria Ramos]

Hi!

I said earlier that I removed the gov.nasa.jpf.vm.NoUncaughtExceptionsProperty from the search.properties of the jpf.properties file. I removed it  because I was not interested in that listener and the error you are getting is reported by it. I added it back and got the same error as you, which helped me catch the deadlock. I resolved that error with what was said in this thread. 

But I had other situation where the deadlock is not being detected, even with this fix. 

It's exactly the same example but now I'm testing the function totalBalance of the class. 

totalBalance calculates the total balance of the bank with 2 phase locking. The implementation that is attached to this message is not doing it correctly, because the locks of the accounts are not being acquired in order. So, it is possible that the following scenario happens:

- thread1 acquires lock for account0

- thread1 acquires lock for account1

- thread2 acquires lock for account2

- thread2 tries to acquire lock for account1 but it was already acquired

- thread1 tries to acquire lock for account2 but it was already acquired

This is the output I get:

Differently from the previuos output, there are several states being searched, but no deadlock ever being detected.

Thanks for the help!