Transcript slides
Comparison Under Abstraction
for Verifying Linearizability
Daphna Amit
Tom Reps
Eran Yahav
Noam Rinetzky
Mooly Sagiv
Tel Aviv University
University of Wisconsin
IBM T.J. Watson
Research Center
Verification Challenge
T1
T2
Tn
...
concurrent
data structure
• Unbounded dynamically-allocated concurrent data structure
• Non blocking stack [Treiber, '86]
• Non blocking queue [Michael and Scott, PODC’96]
• …
• Challenge: automatically prove linearizability
Linearizability [Herlihy and Wing, TOPLAS'90]
• Linearizable data structure
– Sequential specification defines legal sequential executions
– Concurrent operations allowed to be interleaved
– Operations appear to execute atomically
• External observer gets the illusion that each operation takes effect
instantaneously at some point between its invocation and its response
push(4)
T1
push(7)
push(7)
concurrent
LIFO stack
pop():4
time
T2
Last In
First Out
Main Contributions
• A conservative automatic algorithm for verifying linearizability
– Unbounded linked concurrent data structures
– Fixed (arbitrary) number of threads
– Implementation and experimental results
• A novel shape abstraction that allows comparison between
mutable linked data structures
Our Approach
• Construct for every concurrent execution an “equivalent” sequential
execution
– Simultaneously manipulate 2 data structures
• Concurrent data structure (manipulated by interleaved operations)
• Sequential data structure (manipulated by atomic operations)
– Executable sequential specification
T1
concurrent
stack
T2
T1
T2
sequential
stack
Our Approach
• Construct for every concurrent execution an “equivalent” sequential
execution
– Compare results of matching operations
T1
concurrent
stack
T2
push(4)
push(7)
pop():4
time
T1
T2
sequential
stack
push(7)
push(4)
pop():4
Why
Main
Is ItObservation
Challenging?
Show that the observable behavior along every
concurrent execution trace is equivalent to that of
a corresponding sequential execution trace
Comparison under abstraction of
unbounded state systems may be
possible when the difference
betweenbetween
the systems
is bounded
Comparison
two unbounded
heaps over
an unbounded number of traces
of unbounded length
Comparison under abstraction
Outline
• How to construct the sequential
executions?
• How to compare unbounded heaps under
abstraction?
Outline
• How to construct the sequential
execution?
Inspired by Flanagan, SPIN’04
• How to compare unbounded heaps under
abstraction?
Fixed Linearization Points
• Every operation has a (user-specified) fixed linearization point
– A statement at which the operation appears to take effect
• Show that these linearization points are correct for every concurrent
execution
• User may specify
– Several (alternative) linearization points
– Certain types of conditional linearization points
Verification of Fixed Linearization Points
• Compare each concurrent execution to a specific sequential
execution
• Show that every (terminating) concurrent operation returns the
same result as its sequential counterpart
Concurrent
Execution
operation
linearization
point
...
linearization
point
compare
results
Sequential
Execution
compare
results
Conjoined
Execution
Treiber's Non-Blocking Stack
3
1
Top
4
Push Operation
3
1
Top
4
void push (Stack S, data_type v) {
Node x = alloc(sizeof(Node));
xd = v;
do {
Node t = STop;
xn = t;
} while ( !
CAS(&STop, t, x)
);
}
t
Top
7
x
if (STop == t)
STop = x; evaluate to true;
else
evaluate to false;
Pop Operation
3
1
Top
4
s
Top
7
t
return 7
data_type pop (Stack S) {
do {
Node t = STop;
if (t == NULL)
return EMPTY;
Node s = tn;
} while ( !
CAS(&STop, t, s)
);
data_type r = td;
return r;
}
Example: Conjoined Execution (1)
T1 T2
3
3
Top
t
1
1
Top
Top
4
4
Top
x
x
B: push(7)
A: push(4)
t
7
x
Linearization Point
Concurrent
Stack
Sequential
Stack
Example: Conjoined Execution (2)
T1 T2
B: push(7)
3
3
1
1
4
4
Top
7
7
Top
x
x
A: push(4)
t
failed CAS
7
Top
t
x
Top
Linearization Point
Concurrent
Stack
Sequential
Stack
Example: Conjoined Execution (3)
T1 T2
B: push(7)
3
3
1
1
4
4
A: push(4)
A: pop()
Top
s
Top
t
Top
s
7
7
Top
t
matching
Linearization
Point return values
Concurrent Sequential
Stack
Stack
Conjoined Execution
Top
3
3
1
1
Top
Top
4
3
3
1
1
Top
linearization
point
Throughout
conjoined execution,
two stacks remain
almost isomorphic
4
Concurrent Sequential
Stack
Stack
Top
3
3
1
1
4
Top
Top
3
3
1
1
4
4
Top
Atomic Operation
Top
3
3
1
1
4
4
Top
Outline
• How to construct the sequential
execution?
• How to compare unbounded heaps under
abstraction?
Delta Abstraction
Starting Point: Canonical Abstraction [ SRW'02 ]
x
7
n
4
n
1
n
3
n
x
n
summary node
Concretization
x
x
x
7
5
3
n
n
n
4
n
1
n
3
8
2
n
3
n
9
n
7
n
x
n
summary node
Comparison of Responses Under Abstraction
Concrete Domain
Top
3
3
1
9
1
3
4
5
4
6
7
3
Concurrent
Stack
7
11
Abstract Domain
• Separate abstractions will not do
Top
Sequential
Stack
Top
?
Concurrent
Stack
?
=
?
Top
Sequential
Stack
Main Idea
3
3
Isomorphic Sub-graphs
1
1
4
4
Top
t
abstract away
Maintain a mapping
between memory layouts
of concurrent and
sequential
data structures
track precisely
Top
7
x
Concurrent
Stack
Sequential
Stack
Recording Isomorphism Using Correlation Relation
Top
3
3
1
1
4
4
7
7
Top
• All nodes are correlated
• Correlated nodes are similar (successors also correlated or both null)
• Nodes pointed-to by Top are correlated
Isomorphism Under Delta Abstraction
3
similar
1
similar
4
similar
3
1
duo-object
Top
7
similar
4
7
Top
Isomorphism
Under
Bounded
Delta Abstraction
Isomorphism
Under
Delta Abstraction
3
similar
1
similar
4
similar
3
1
summary
duo-object
duo-object
Top
7
similar
4
7
Top
Constructing the Correlation Relation
• Incrementally constructed during execution
• Nodes allocated by matching push operations are correlated
• Correlated nodes have equal data values
– Show that matching pops return data values of correlated nodes
Conjoined Execution Under Abstraction (1)
T1 T2
similar
B: push(7)
A: push(4)
t
similar
Top
t
similar
Top
x
Top
x
Top
x
Linearization Point
Concurrent
Stack
Sequential
Stack
Conjoined Execution Under Abstraction (2)
T1 T2
similar
B: push(7)
A: push(4)
similar
t
similar
Top
failed CAS
Top
t
x
similar
Top
x
Linearization Point
Concurrent
Stack
Top
x
Sequential
Stack
Conjoined Execution Under Abstraction (3)
T1 T2
B: push(7)
A: push(4)
similar
A: pop()
Bounded difference
may be at an
unbounded distance
from the root
Top
similar
similar
Partial isomorphism
can be maintained
under abstraction
since
the difference
between
the memory layouts
is bounded
Top
matching return values
Concurrent
Stack
Sequential
Stack
Experimental Results
Verification (Time)
Verification (Space)
16000
16,000
2
14000
2
200000
# of States
12000
Seconds
250000
250,000
10000
8000
6000
4000
2
3
2000
2
100000
0
3
2
0
[1]
[2] NBQ
[3]
[2] 2LQ
[4]
[1]
[2] NBQ
Benchmark
[3]
[2] 2LQ
[4]
Benchmark
Falsification (Time)
Falsification (Space)
20000
20,000
250
250
# of States
200
Seconds
4
50000
4
2
150000
150
100
50
0
[1]
[1]
[2]
NBQ
[2]
NBQ
[2]
2LQ
[2]
2LQ
[4]
Benchmark
18000
16000
14000
12000
10000
8000
6000
4000
2000
0
[1]
[1]
[2]
NBQ
[2]
NBQ
[2]
2LQ
[2]
2LQ
Benchmark
[1] Treiber, '86
[3] Doherty et al., FORTE'04
[2] Michael and Scott, PODC’96
[4] Vafeiadis et al., PPoPP'06
[4]
Related Methods
• Manual
– Rely-guarantee reasoning [Vafeiadis et al., PPoPP'06]
• Semi-automatic
– Proving simulation relation between I/O Automata using PVS
[Doherty et al., FORTE'04]
• Automatic
– Proving atomicity of procedures [Wang and Stoller, PPoPP'05]
More general
Future
Work
Limitations
• User-specified guess of fixed linearization points
• User-specified fixed correlation rule
• Fixed number of threads
– Arbitrary in theory
– Small in practice (scalability)
• Assuming memory is garbage collected
Summary
• A conservative automatic algorithm for verifying linearizability of
unbounded linked concurrent data structures
– Sequential specification
– Conjoined executions
• Delta abstraction: A novel heap abstraction
– Maintains an isomorphism between mutable linked data structures under
abstraction
• Implementation and experimental results
–
–
–
–
Non blocking stack [Treiber, '86]
Non blocking queue [Michael and Scott, PODC’96] [Doherty et al., FORTE'04]
2 lock queue [Michael and Scott, PODC’96 ]
Set with fine grained locking [Vafeiadis et al., PPoPP'06 ]
Main Observation
Comparison under abstraction
of unbounded state systems
may be possible when the
difference between the systems
is bounded
The End
MSc Thesis: www.cs.tau.ac.il/~amitdaph
Stack's Most-General Client
void client (Stack S) {
do {
if (?)
push(S, rand());
else
pop(S);
} while ( 1 );
}