Transcript sequential verification for serializability

Sequential reductions for
verifying serializability
Hagit Attiya
G. Ramalingam
Noam Rinetzky
Technion & EPFL
MSR India
University of London
The goal
Verify concurrent data structures
• Pre-execution static analysis
E.g., linked list with hand-over-hand locking
• memory safety (no memory leaks)
• shape invariants (it’s a list)
• “atomicity” (serializability)
Find sequential reductions
 Consider only sequential executions
 But conclude that properties hold in all
executions
Back-of-envelop estimate of gain
Static analysis of a linked-list algorithm
[Amit, Rinetzky, Reps, Sagiv, Yahav, CAV 2007]
– Verifies e.g., memory safety, sortedness,
pointed-to by a variable, heap sharing
One thread (sequential)
10s
3.6MB
Two threads (interleaved)
~4h
886MB
Three threads (interleaved)
> 8h
----
Serializability
[Papadimitriou ‘79]
interleaved execution
operation
~~ ~~ ~~
~ thread-local views
complete non-interleaved execution
Serializability assists verification
Concurrent code M
Π
= all executions of M
cni-Π = all complete non-interleaved
executions of M  Π
φ
= some thread-local property
If M is serializable
Then Π ⊨ φ  cni-Π ⊨ φ
How do we know that M is serializable,
w/o
all executions?
If
M considering
is serializable
I.e., byΠchecking
only cni-executions
Then
⊨ φ  cni-Π
⊨φ
Special (and common) case:
Disciplined programming with locks
Guard access to data with locks
Access data only after getting a lock for it
(well-lockedness)
Follow a locking protocol that guarantees
conflict serializability
E.g., two-phase locking (2PL)
or tree locking (TL)
Two-phase locking
[Papadimitriou `79]
• Locks acquire (grow) phase
followed by locks release (shrink) phase
No lock is acquired after some lock is released
t2
t1
H
t1
t1
t1
Tree (hand-over-hand) locking
[Bayer & Scholnick ‘77] [Kedem & Sliberschatz ‘76] [Smadi ‘76]
• Except for the first lock, acquire a lock only
when holding the lock on its parent
• No lock is acquired after being released
t1
H
t2
t1
t1
Tree (hand-over-hand) locking
[Bayer & Scholnick ‘77] [Kedem & Sliberschatz ‘76] [Smadi ‘76]
• Except for the first lock, acquire a lock only
when holding the lock on its parent
• No lock is acquired after being released
t2
t2
H
t1
t1
Yes!
– for databases
– concurrency control monitor
ensures that M follows the
locking policy
run-time
Notat
two-phase
locked
But only in interleaved
 M is serializable
No!
executions
– for static analysis
– no central monitor
void p() {
acquire(B)
B = 0
int b = B
release(B)
if (b) Y = 2
acquire(A)
}
void q() {
acquire(B)
B = 1
release(B)
}
How to (statically) verify that M follows a locking policy?
Our approach
Applies for local conflict-serializable (LCS)
locking protocols
– Use only thread-local information (see next)
E.g., two phase locking, tree locking,
(dynamic) DAG locking…
But not protocols that rely on a concurrency
control monitor!
Thread-local properties
A thread-owned view contains the values of
thread’s local variables &
global variables locked by it
A property φ is thread-local if it
– Can be expressed in terms of thread-owned
views
– Is prefix closed
A thread-local property of an execution holds
in every execution indistinguishable from it
Our contribution: Easy step
cni-Π = all complete non-interleaved
executions of M  Π
non-interleaved execution
Two phase locking
Tree locking
Dynamic tree locking
Dynamic DAG locking
For any LCS locking policy LP
Π ⊨ LP  ni-Π ⊨ LP
For any thread-local property φ
Π ⊨ φ  ni-Π ⊨ φ
Ni-reduction: Proof sketch
If all ni-executions follow LP
 all executions follow LP
σ is the shortest execution that does not follow LP
(t,e)
σ
σ’
σ’ follows LP, guarantees conflict-serializability
there is a ni-execution that is “equivalent” to σ’
Ni-reduction: Proof sketch
(cont.)
there is a ni-execution that is “equivalent” to σ’
σ’
(t,e)
σ’ni
(t,e)
σni
there is a ni-execution that is “equivalent” to σ
where LP is violated
Further reduction
acni-Π = all almost-complete non-interleaved
executions of M  Π
almost complete non-interleaved execution
For any LCS locking policy LP
Π ⊨ LP  acni-Π ⊨ LP
Acni-reduction: A complication
Need to argue about termination
int X=0, Y=0
Observe
Y == 1 &
violates 2PL
void p() {
acquire(Y)
y = Y
release(Y);
if (y ≠ 0)
acquire(X)
X = 3
release(X)
}
Y is set to 1 &
the method
enters an
void q() {
if (random(5) infinite
== 3){ loop
acquire(Y)
Y = 1
release(Y)
while (true) nop
}
}
Acni-reduction: Termination
For any “terminating” LCS locking policy LP
Π ⊨ LP  acni-Π ⊨ LP
 Can use sequential reduction to verify
termination
Acni-reduction: Proof ideas
Start from a ni-execution (and rely on the
previous, ni-reduction to get there)
Create its equivalent completion, if possible
Does not access variables
accessed by later threads
Not always possible, e.g.,
t1:lock(v), t1:lock(u), t2:lock(u)
v
u
Implications for statis analysis
• Pessimistic analysis (over approximate)
– Analyze a module from every possible state
• Semi-optimistic analysis
– Analyze a module only from states that occur after a
sequence of modules ran one after the other
Ni-reduction
• Optimistic analysis (precise)
– Analyze a module only from states that occur
after a sequence of modules ran to completion
(one after the other)
Acni-reduction
Initial analysis results
Shape analysis of hand-over-hand lists
Our method
TVLA prior
Separation logic*
3.5s
4.0MB
596.1s
90.3MB
0.4s
0.2MB
* Does not verify sortedness of list and fails to verify linearizability
in some cases
Shape analysis of hand-over-hand trees (for the first time)
Our method
124.6s
90.6MB
What’s next?
• Further extensions, esp., for software
transactional memory
– aborted transactions
– non-locking non-conflict based serializability
(e.g., using timestamps)
• Combine with other reductions
[Guerraoui, Henzinger, Jobstmann, Singh]
And beyond…
• The cost of verifying adherence to a locking
policy in an acni- / ni-execution
• Automatic insertion of lock acquire / release
commands
… Or fences?
Thank you!