Transcript Bart Verzijlenberg

Verification of a Concurrent
Priority Queue
Bart Verzijlenberg
November 27, 2007
Agenda






Brief Review
Verification Overview
Verification Results
Errors
Further Work
Conclusion
November 27, 2007
1
Brief Review



Priority Queue
Lock-free
Relies on atomic Compare and Swap
operations
November 27, 2007
2
Algorithm Review

The algorithm uses the Skip-List data structure



Extends the Skip-List for concurrent use
The Skip-List is sorted on the priority of the nodes
The algorithm is lock-free




No blocking
Prevent dead locks
Always progress by at least one operation
Risk of starvation
November 27, 2007
3
Algorithm Review
Skip-List



Multi-layer linked list
H forward pointers for a node of height h
Each pointer i points to the next node with
a height of at least i
November 27, 2007
4
Inserting in a Skip-List
Inserting 17 in the list
November 27, 2007
5
Verification Overview

Java Path Finder



Modified JPF script


Breadth-First Search
Depth-First Search
Increased stack size to 1536Mb
Vary the number of inserts/deletions

At what point does JPF crash?
November 27, 2007
6
Test Classes

Driver Class

Creates



Insert Thread


N insertThreads
M deleteThreads
Inserts a single number into the queue
Delete Thread


Loops until a single number removed from queue
Use of sleep important
November 27, 2007
7
Code Modifications


Maximum Level = 3
Probabilistic level selection replaced with a
random level

Probabilistic function calls random multiple
times


Too many additional paths for JPF
Removed back-off period
November 27, 2007
8
A Note

At the end of the code



Print “End of Code”
Marks each time JPF reaches the end of a
potential execution path
I consider each “End of Code” to
correspond with a different thread
interleaving (i.e. a path)
November 27, 2007
9
Verification Results

(1,2) = 1 Insert Thread, 2 Delete Threads
1,0
1,1
2,0
2,1
2,2
3,0
BFS
2 Paths
No Error
<1 Min
5 Paths
No Error
1 Min
8 Paths
No Error
1 Min
? Paths
Out of memory
27 Min
? Paths
Out of Memory
35 Min
? Paths
Out of memory
34 Min
DFS
2 Paths
No Error
<1 Min
5 Paths
No Error
<1 Min
10 Paths
No Error
<1 Min
15+ Paths
Out of Memory
2:15 Hours
6+ Paths
Out of Memory
15:40 Hours
18+ Paths
Out of Memory
5:20 Hours
November 27, 2007
10
By Comparison

Implemented simple priority queue test

java.util.PriorityQueue



Synchronized insert statement using a lock on
the queue
Able to test inserting 8 numbers quickly



Not safe for concurrency
3713 Paths
Tested in 45 Min
Inserting 10 numbers

Crashed after 60791 Paths
November 27, 2007
11
What is the Difference?

Using synchronized method

Very few points where a thread can take over


Lock Free


I.e. When one thread is inserting, none of the others can
insert at the same time
Threads can be interrupted after every instruction
This results in many more potential interleavings
November 27, 2007
12
Errors !

java.lang.OutOfMemoryError:
 GC overhead limit exceeded
More than 98% of time spent on GC
 Recovering less than 2% of the heap




java.lang.OutOfMemoryError:
 Java heap space
[SEVERE] JPF out of memory
[SEVERE] JPF exception, terminating:

class java.lang.NullPointerException: null
November 27, 2007
13
Further Work

Reduce Max level to 2



Enable back-off function
Find linearization points in the code


Further reducing number of paths
Add each number into two queues at the
same time
Try some of the other search classes
November 27, 2007
14
Conclusion

Testing at this point has not found errors



When inserting up to 2 numbers
When inserting 3 numbers (before crashing)
More work needed to reduce the chance
of errors further

Will not eliminate completely
November 27, 2007
15
Thank You
Questions?
November 27, 2007