Transcript Hussain - Wiki Index

Verifying a Two-Lock
Concurrent Queue
Hussain Tinwala
Fall 2007
Overview
•
•
•
•
Simulation Review
Searching for Deadlocks
Race Conditions
Queue Verification
Reviewing the Simulation
Searching for Deadlocks (1)
• JPF did not find errors…
• Introduced a problem I faced during implementation with
Dequeuer threads:
Searching for Deadlocks (2)
Searching for Deadlocks (3)
Run Simulation with 1 Enqueuer, 1 Dequeuer
and 1 node:
jpf -c jpf.properties…
gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet {Thread-0,>Thread-1}
Enqueuer.java:57
: synchronized(sim)
Enqueuer.java:59
: sim.notifyAll();
------------------------------------------------------ transition #47 thread: 1
gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet {>Thread-0}
Dequeuer.java:38
: synchronized (sim)
Dequeuer.java:40
: sim.wait();
====================================================== snapshot #1
thread index=1,name=Thread-0,status=WAITING,
this=Dequeuer@246,priority=5,lockCount=1
waiting on: Simulator@232
call stack:at Dequeuer.run(Dequeuer.java:40)
====================================================== results
error #1: gov.nasa.jpf.jvm.NotDeadlockedProperty \
"deadlock encountered: thread index=0,name=main,s..."
Race Conditions (1)
Two types:
- Critical: different outcomes
- Non-critical: eventual outcome of the
program is the same
modify
read
Both are
synchronized methods
Race Conditions (2)
prompt> jpf -c jpf.properties …
- Removed `synchronized’
- jpf with 1 Enqueuer and 1 Dequeuer --> no error
- jpf with 1 Enqueuer and n Dequeuers --> no error
- jpf with >1 Enqueuer --> error
- Enqueuer threads use both methods
- modifies a value
- reads a value
- Dequeuer threads only use `getNumEnqsLeft’
- reads a value
- Potential for a race condition…
Race Conditions (3)
- Using JPF to detect race conditions:
- Add to configuration file:
# listeners
jpf.listener=gov.nasa.jpf.tools.precise.PreciseRaceDetector
- Running JPF with 2 Enqueuers and 1 Dequeuer
- jpf -c jpf.properties…
name=Thread-1,status=RUNNING,this=Enqueuer@136,priority=5,lockCount=0
at Simulator.getNumEnqsLeft(Simulator.java:57)
at Enqueuer.run(Enqueuer.java:52)
Name=Thread-2,status=RUNNING,this=Enqueuer@137,priority=5,lockCount=0
owned locks:Simulator@232 (because method is synchronized)
at Simulator.decrementNumEnqsLeft(Simulator.java:53)
at Enqueuer.run(Enqueuer.java:51)
=========================================== results
error #1: gov.nasa.jpf.tools.PreciseRaceDetector "race for: "int
Simulator.numEnqsLeft" Thread-1 and Thread-2...”
=========================================== results
error #1: RaceDetector "potential field race: [email protected]"
So we have 2 Enqueuers
- One is updating the value
- The other is attempting to read it
Race Conditions (4)
- Adding `synchronized’ to the methods removes the
race condition
- Question: Do both methods need to be synchronized?
- Yes: To get rid of the race condition
- No: A race does not have to be bad
- Synchronizing the method that modifies a value may be
sufficient
- Added `synchronized’ only to the
decrementNumEnqsLeft method which is used by
Enqueuer threads.
- getNumEnqsLeft method left without `synchronized’
- Tested again: jpf -c jpf.properties …
Race Conditions (5)
- JPF finds no deadlocks or errors but it does find a race condition
- But that is okay… it is a non-critical race condition
- No matter what order the execution takes, there will always be AT LEAST
one Enqueuer thread that will find
- getNumEnqsLeft() == 0
- And so, it will be able to notify any waiting Dequeuer threads.
- Overall Advantage: There is less blocking in the Enqueuer thread
Verifying the Queue
• Nodes are always inserted after the last node in the
linked list
• Nodes are always deleted from the beginning of the
linked list
• Head always points to the first node in the list
• Tail always points to the last node in the list
• Potential Approach:
– Use a PropertyListener
• Ex: QueuePropertyListener extends PropertyListenerAdapter
– Then at each transition, verify the above mentioned
properties
Thank you
Questions?