Assistance Needed with Deadlock Detection in JPF about jpf-core HOT 5 CLOSED

What is the output that you get, and what output do you expect? If one thread is sometimes blocked, that's not a deadlock. It seems like there is always one thread that can continue, at least after an initial quick look at your code.

from jpf-core.

Is it true that only holding one lock and waiting for another lock to be released can be considered a deadlock? In this program, if the consumer executes first, it will block at line 12 (wait) in Semaphore.java. For the consumer to continue, the producer must execute line 9 (notifyAll()) in Semaphore.java. However, since the producer cannot execute the put() method, all threads will be in a blocked state. Can this situation be considered a deadlock? Can it be identified like the classic scenario of T1: lock(l1); lock(l2); and T2: lock(l2); lock(l1);?

from jpf-core.

JPF can find deadlocks in such situations, too. Can you please share your code in a way that it can be copied and ran locally? The most efficient way would be a small git repo with all the code and JPF configuration set up.

from jpf-core.

Thank you, I found a stupid error in one of my Settings

from jpf-core.

Thank you for confirming. We can close this issue then.

from jpf-core.