Transcript Nastaran Shafiei

VERIFICATION OF A NON-BLOCKING
ARRAY-BASED QUEUE ALGORITHM
Nastaran Shafiei
1
Outline



Algorithm Description
Algorithm Implementation
Verification



Simulating Shared Variables
Linearizability
Java Pathfider Results
2
The Algorithm

Finite array, Q
Counters, FRONT and REAR
Operations: enqueue, dequeue
Elements of the queue

Using compare-and-swap



3
Implementation
NonblockingQueue
Enqueue
L: int
Q: AtomicLongArray
REAR: AtomicLong
FRONT: AtomicLong
getValPart(long queue)
getRefPart(long var)
getQueueItem(int val, int ref)
main(String[] args)
Dequeue
val: int
Enqueue(int value)
void run()
void run()
Thread
…
…
4
Shared Variables
public static AtomicLongArray Queue;
public static AtomicLong REAR;
public static AtomicLong FRONT;
Atomic variables



Extend the concept of volatile variables
compareAndSet()
not supported by java pathfinder
5
Simulating Atomic Variables

AtomicLongArray
long array

AtomicLong

Using volatile keyword

Simulating compareAndSwap()
long

synchronized method

Atomic execution methods



beginAtomic() and endAtomic()
Declared in gov.nasa.jpf.jvm.Verify
Atomic block with respect to the whole program
6
Linearizability


Correctness condition
Definition:


every concurrent execution = some legal sequential execution
Linearization point (enqueue)
A
C
B
Enqueue process:
Queue.compareAndSet( i, expected, newItem) = true
7
Linearizability

Linearization point (dequeue)
A
C
B
Dequeue process:
Queue.compareAndSet( i, expected, emptyItem)=true

To prove linearizability

Invariants were developed describing expected properties of the
shared variables.
8
Linearizability
Auxiliary variables
Shared Variables
long r
REAR
long f
FRONT
long aq[]
Q[]
9
Linearizability

At enqueue linearization point:



aq[r%L] = newItem
r++
At dequeue linearization point:


aq[f%L] = emptyItem
f++
10
Linearizability

Invariant
Place of assertion
REAR == r-1
Enqueue linearization point
FRONT == f-1
Dequeue linearization point
aq[r%L] == Q[REAR%L]
synchronized CAS of REAR
aq[f%L] == Q[FRONT%L]
synchronized CAS of FRONT
Assertion method



Declared in gov.nasa.jpf.jvm.Verify
public static void assert ( boolean b)
Checks that b evaluates to true
11
Java Pathfinder Results

Using beginAtomic() and endAtomic()


Purpose: Simulate CAS/cut down state space
Jpf killed a thread and exited (even for 1 thread)
Using synchronized method to simulate CAS


Up to 3 threads: no errors detected
4 threads:



DFS : no errors detected
BFS gave Out.MemoryError : GC overhead limit exceeded
More: Out.MemoryError
12
Questions?
13