Transcript Niloufar Shafiei

Verification of obstruction-free
algorithm with contention
management
Niloufar Shafiei
Agenda






The algorithm
Correctness condition for shared objects
Java PathFinder
Verification challenges
Verification
Summary
2
The algorithm
 Obstruction-free deque algorithm with different
contention management policies
 AtomicLongArray
 AtomicLong
 How should the algorithm behave? (correctness)
 Data structure represents the abstract deque at any time
 All operations terminate
 No livelock or deadlock
3
Correctness condition for shared
objects implementations
 Find the linearization point
4
Correctness condition for shared
objects implementations
 Find the linearization point
time
?
push(v1)
push(v2)
pop
stack
5
Correctness condition for shared
objects implementations
 Find the linearization point
time
?
push(v1) X
push(v2) X
X
v2
v1
stack
pop
empty
6
Check the correctness of shared
object implementation
 Find the linearization point
 Define abstract variables (abstract stack,…)
 Change the abstract variables at linearization
points
 At all linearization points, check if the abstract
variables are consistent with data structures
 In java, insert assert(expression) atomically at
linearization points
 Synchronized block
 Atomic block
7
Java PathFinder
 JPF
 Model checker
 Deadlocks
 Invariants
 User-defined assertions
 JPF versus Spin
 JPF covers the java programming language (not more than
10000 lines)
 JPF design goal is to make it as modular and understandable as
possible
 Spin is faster than JPF
8
Verification challenges
 JPF does not support AtomicLongArray and
AtomicLong
 Volatile Long[] and Long
 Synchronized methods to implement C&S
 Warning “unprotected field access of deque”
 JPF employ Partial Order Reduction to save space
 For lock protection, determines if a field access is scheduling
relevant (transaction boundary)
 vm.por.sync_detection=false
9
State search
 JPF searches
 DFS
 With backtracking is most appropriate for checking
liveness properties
 BFS
 Search.heuristic.class = gov.nasa.jpf.search.heuristic.BFSHeuristic
10
Verification
Result
Number of
paths
1 thread
(DFS - BFS)
No error
4
2 threads
(DFS - BFS)
3 threads
No error
135 - 120
Out of
memory
>1200
11
Verification
 How to save the memory?
 More synchronized methods
 Synchronized blocks and Atomic blocks (Verify class)
 Local instructions
 At most one shared memory instruction
 No instruction prevent the program from accessing
endAtomic()
 Return - break - join - if statement
12
Verification
 Atomic blocks
 Sometimes threads loop in Atomic block
Result
Number of
paths
1 thread
Processes
killed
0
2 threads
Processes
killed
0
3 threads
Processes
killed
0
 Why processes killed?
 Need memory more than available memory
13
Verification
 Synchronized blocks
Result
Number of
paths
1 thread
(DFS - BFS)
No error
4
2 threads
(DFS - BFS)
3 threads
No error
135 - 120
Out of
memory
>1200
Why results are not improved?
Partial Order reduction
14
Summary
 Correctness conditions of shared object
 Java PathFinder
 Verification of shared deque
implementation with JPF
15
Questions?
16