Euro-TM 1st Plenary Meeting — Ricardo Dias
1
On Using Separation Logic to
Detect Snapshot Isolation
Anomalies
Ricardo Dias, João Lourenço, João Seco
CITI/Universidade Nova de Lisboa
Dino Distefano
Queen Mary, University of London
19/05/2011
Objective
2

Investigate how to use Snapshot Isolation
implementation techniques to improve TM systems
performance while keeping the Serializable model
 No
need to collect Read-Sets
 No
need to detect Read-Write conflicts
 Reduce
network traffic in Distributed STM
Euro-TM 1st Plenary Meeting — Ricardo Dias
19/05/2011
Approach
3

Offer the Serializable Model to the programmer

Avoid write-skew anomalies with a mixed (static
and dynamic) approach
 Statically
 Correct
detect write-skew anomalies
the identified write-skews at runtime
Euro-TM 1st Plenary Meeting — Ricardo Dias
19/05/2011
SI Anomaly – Write Skew
4
Transaction 1
Transaction 2
Read X
Read X
Read Y
Read Y
Write X
Write Y
Impossible in
Serializable
Isolation
Commit
Commit
Euro-TM 1st Plenary Meeting — Ricardo Dias
19/05/2011
Write-Skew Definition
5
RS(T1) ∩ WS(T2) ≠ ∅ ∧ WS(T1) ∩ RS(T2) ≠ ∅ ∧ WS(T1) ∩ WS(T2) = ∅
ReadSet(T
1)
WriteSet(
T1)
WriteSet(
T2)
ReadSet(T
2)
AND
WriteSet(
T1)
WriteSet(
T2)
Euro-TM 1st Plenary Meeting — Ricardo Dias
19/05/2011
TM
Star
6
Static
Analysis
Transactional
Memory
StarTM
Snapshot
Isolation
Serialization
Anomalies
Euro-TM 1st Plenary Meeting — Ricardo Dias
19/05/2011
TM
Star
Workflow
7
Analyze
Transactional
Code
Generate
Read/Write-Sets
Detect
Write-Skews
Euro-TM 1st Plenary Meeting — Ricardo Dias
19/05/2011
TM
Star
Components
8
Memory
Access
Representation
Separation
Logic
SMT Solver
StarTM
Euro-TM 1st Plenary Meeting — Ricardo Dias
19/05/2011
Memory Access – Location
9
HEAP
STACK
…
0
1
2
3
4
5
6
4
5
7
8
5
2
3
…
x
0
y
1
0
z
6
1
(x,0)
(y,0)
2
(x,3),(y,2)
3
(z,1)
4
(x,1)
5
(x,2),(y,1)
6
(z,0)
ABSTRACT LOCATION
TrxSys Research Group Meeting
11/05/2011
Abstract Access
In a SL formula
instead of a memory
model
10
| ls(x, y) ∗ y → z ∗ ls(z,w)
ls(x,y) length table
x
y
y
x each Predicate
0
For
it is
yknown the
0 length
RS
= {x,
y, of
z} =
between each
pair
x { (x,N[>0]
[ 0, N[>0]+1 ] ) }
parameters
ABSTRACT LOCATION
x
(x,0)
y
(x, N[>0])
z
(x, N[>0]+1)
w
(x, N[>0]+1+M[>0])
TrxSys Research Group Meeting
11/05/2011
Write Skew Detection
11
Add (T1)
Remove (T2)
ReadSet:
ReadSet:
{ (x, [ 0, N[>0] ]) }
{ (x, [ 0, M[>0]+1 ]) }
WriteSet:
If N=2 and M=1
then
this [condition
{ (x,
N[>0], isN[>0]
satisfiable
WriteSet:
]) }
{ (x, [ M[>0], M[>0] ]) }
[0, N]
[0,∩2][M,
∩ [1,
M] 1]
≠∅
≠∅
∧ [N,
∧ [2,
N]2]∩∩[0,[0,M+1]
2] ≠ ≠
∅∅∧ ∧[2,[N,
2] N]
∩ [1,
∩ [M,
1] =M]
∅= ∅
TrxSys Research Group Meeting
11/05/2011
The Tool
12
SMT Solver
TM
Java
Classes
SL Theorem
Prover
Memory
Access
Computation
Read/Write
Set
Generation
Write-Skew
Detection
Result
File
Euro-TM 1st Plenary Meeting — Ricardo Dias
19/05/2011
TM
Star
Results
13
Benchmark
Singly
Linked List
BS Tree
Method
Duration
(sec)
#Coverage
(%)
#Final
States
Write-Skews
add
16
100
6
remove
15
100
6
(add, remove)
11
100
3
(remove, remove)
revert
11
100
3
treeAdd
21
100
69
8
contains
49
treeContains
atomicGetPacket
Intruder
(STAMP)
#LOC
atomicProcess
51
atomicGetComplete
0
15
100
51
9
77
2
173
89
17
15
73
2
Euro-TM 1st Plenary Meeting — Ricardo Dias
(atomicProcess,
atomicGetComplete)
19/05/2011
What Follows
14

StarTM identifies:
 Which
transactions trigger a write-skew
 Which
read and write access are involved in the write-
skew

Instrument application code to avoid a write-skew:
 Inject
necessary validations
 Force
specific read operations to conflict with write
operations  force some transactions to conflict if
executed concurrently
Euro-TM 1st Plenary Meeting — Ricardo Dias
19/05/2011
Thank You
15
Questions?
Euro-TM 1st Plenary Meeting — Ricardo Dias
19/05/2011