CSE 440: Advanced Algorithms
Lecture 10: Concurrent Data Structures
Linearizability: ART Ch. 3
Examples (overview): ART Ch. 9, 11, 13
Chromatic Tree: https://link.springer.com/content/pdf/10.1007/s002360050057.pdf
Objective
• How to prove that a concurrent data structure is correct?
• Relevant questions
• How to implement a concurrent data structure?
• How to prove that a sequential data structure is correct?
Correctness Definition
• Idea #1: mutual exclusion
• Use locks to gain an exclusive “sequential” access to the data structure.
• Pros
• Easytoreasonabout
correctness
• Cons
• Terrible performance
• Counterintuitive to the main objective of concurrency
Correctness Definition
• Idea #2: data race freedom
• Avoid having two operations access the same memory location and at least one of the instructions performs a write.
• Pros
• Guaranteedcorrectness
• Betterperformance(sometimes) than mutual exclusion
• Cons
• Most(efficient)concurrentdata structures are NOT data race free, yet correct!!
Correctness Definition
• Idea # 3: inherit definitions from database community • Sequential consistency
• Serializability
• Strict serializability •…
Close enough, but needs some adaptations
• Idea # 4: Linearizability (Herlihy and Wing’1990)
• Informally
• Equivalencetoacorrectsequentialdatastructure!!
• Similartotheabovecorrectnessdefinitions(somehowinvariantof serializability)
Let’s define first what is a correct sequential data structure
Sequential Specifications
• Data structures can be described using “states” and “operations”
• Example: Queue
• State: sequence of items
• Operations: enqueue and dequeue
• Operations can be described using pre/post conditions
State 1
precondition object’s state before invoking the method
op(x, y, …)/R
State 2
postcondition
the object’s state and return value once the method returns
Sequential Specifications
• FIFO queue examples <9, 3, 7>
precondition object’s state: <9, 3, 7>
deq()/9
<3, 7>
postcondition object’s state: <3, 7> return value: 9
<>
precondition object’s state: <>
deq()/ EmptyException
<>
postcondition object’s state: <> return value: EmptyException
Why Sequential Specifications
• Interactions among methods captured by side- effects on object state
• State meaningful only between method calls
• Documentation size linear in number of methods
• Each method described in isolation
• Can add new methods
• Without changing descriptions of old methods
What about Concurrent Data Structures?
• All previous properties are messed up if we have a concurrent execution
• object might never be between method calls
• All methods must be described together (since they may
overlap)
• Adding new methods may break correctness of previous ones.
• How to restore all of that
• Prove this concurrent execution is equivalent to a sequential execution
Linearizability
• First (less informal) definition of linearizability
• Each method call should appear to take effect instantaneously at some moment between its invocation and response.
• This moment is called “linearization point”
Linearizability
• Important notes
• The previous definition is for a specific “execution”.
• A linearizable object: one all of whose possible executions are linearizable • Linearization points are not our goal, but the tools to reach goal:
• You can define different linearization points for different executions, but this is not the common case.
• How to guess the linearization points • Sometimes can be straightforward
• Lock acquisition, CAS operation, transaction commit • Sometimes more subtle
proving that all possible executions are linearizable.
• More details in CSE 375/475
Examples (from Herlihy’s slides)
q.enq(x)
q.enq(y) q.deq(x)
time
q.deq(y)
Examples (from Herlihy’s slides)
q.enq(x) q.deq(y)
q.enq(y)
time
Examples (from Herlihy’s slides)
q.enq(x) q.deq(y)
q.enq(y)
q.deq(x)
time
Examples (from Herlihy’s slides)
write(0) read(1) write(2) write(1)
time
read(0)
Examples (from Herlihy’s slides)
write(0) write(2) write(1)
time
read(1)
Examples (from Herlihy’s slides)
q.enq(x)
q.deq(x)
time
More Formal Definition
• An execution of a concurrent system is modeled by a history
A q.enq(3)
A q:void
A q.enq(5)
B p.enq(4)
B p:void
B q.deq()
B q:3
History
A finite sequence of method invocation and response events
H=
Method call
a pair of matching invocation and response
Pending invocation
no matching response
More Formal Definition
A q.enq(3)
A q:void
A q.enq(5)
B p.enq(4)
B p:void
B q.deq()
B q:3
An extension of H
constructed by appending responses to zero or more pending invocations of H
Sub-history
subsequence of the history
H=
Complete(H)
sub-history of H consisting of all matching invocations and responses
More Formal Definition
A q.enq(3)
A q:void
A q.enq(5)
B p.enq(4)
B p:void
B q.deq()
B q:3
Sequential History
(1) the first event of H is an invocation
(2) each invocation, except possibly the last, is immediately followed by a matching response.
In other words: method calls of different threads do not overleap
H=
More Formal Definition
A q.enq(3)
A q:void
A q.enq(5)
B p.enq(4)
B p:void
B q.deq()
B q:3
object sub-history H|B subsequence of all events whose thread is A
H=
thread sub-history H|A subsequence of all events whose thread is A
More Formal Definition
Well-formed History
each thread sub-history is sequential.
Equivalent Histories H and H’
for every thread A, H|A = H’|A
A q.enq(3)
B p.enq(4)
B p:void
B q.deq()
A q:void
B q:3
A q.enq(3)
A q:void
B p.enq(4)
B p:void
B q.deq()
B q:3
H= G=
More Formal Definition
Sequential Specifications of an Object
Set of all sequential histories for the object
Legal sequential history
each object sub-history is legal (i.e., in the sequential specifications) for that object.
A q.enq(3)
B p.enq(4)
B p:void
B q.deq()
A q:void
B q:3
A q.enq(3)
A q:void
B p.enq(4)
B p:void
B q.deq()
B q:3
H= G=
More Formal Definition
• Precedence Relation
• Given two method calls m0 and m1 in a history H
• We say m0èH m1 (m0 precedes m1) if m0’s response event comes before m1’s invocation event in H.
• Relation m0èH m1 is a • Partial order
m0
m0
m1
m0 precedes m1
m0 and m1 are incomparable
m1
• Total order if H is sequential
m0 m1 OR m1 m0
More Formal Definition
A history H is linearizable if it has an extension H’ and there is a legal sequential history S such that
• Complete(H’) is equivalent to S, and
• If method call m0 precedes method call m1 in H, then the
same is true in S.
• Discussion
• Why the extension H’ not the original H?
• What if this extension does not happen?
More Formal Definition
A history H is linearizable if it has an extension H’ and there is a legal sequential history S such that
• Complete(H’) is equivalent to S, and
• If method call m0 precedes method call m1 in H, then the
same is true in S.
• Examples
A q.enq(3)
B q.enq(4)
B q:void
B q.deq()
B q:3
B q:enq(6)
A q.enq(3)
B q.enq(4)
B q:void
B q.deq()
B q:4
B q:enq(6)
What is Good About Linearizability
• Makes sense!! • Composable
• H is linearizable if, and only if, for each object x, H|x is linearizable.
• Allows modular design of data structures.
• Neither sequential consistency nor serializability are composable
• Better fit memory models but not concurrent data structures
Examples of Linearizable Data Structures
Objective
• Linearizable but efficient implementation
• You can always acquire a global lock, but we don’t want to do
that.
• Examples
• Linked lists and optimistic synchronization • Hash tables and natural parallelism
• Stacks and elimination
• Balanced trees and decoupling
Elimination Backoff Stack
• Push(x)/Pop
• Select a random location in Elimination Array
• Back-off for some time in this array
• If a (push/pop) match is found at this time, exchange values
without accessing the stack
• Otherwise, execute the operation in the stack itself
Elimination Backoff Stack
• Linearization points
• Operations complete on the stack
• Same as any other stack (assume coarse-grained lock for simplicity) • Operations complete on the Elimination array
• The moment at which they exchange values.
• Precisely, two moments, with a very small delta between them
lazy Linked List
• Insert(x)/Delete(x)
a
b
de
• Traverse without locking until you identify “pred” and “curr” nodes
• Curr is the smallest element greater than or equal to x.
• Acquire locks only on pred and curr, then validate that:
• Neither pred nor the curr nodes has been logically deleted • pred still points to curr.
• If validation fails, retry
• If validation succeeds, complete operation • Unsuccessful insert (curr == x): return false
• Successful insert (curr != x): link new node and return true
• Unsuccessful insert (curr != x): return false
• Successful delete (curr == x): mark curr as logically deleted and then unlink it
lazy Linked List
• Contains(x)
• Traverses the list once ignoring locks
• Wait-free operation
• Returns true if the node it was searching for is present and
unmarked
• Return false otherwise
• When a node greater than x is found
• When x is found but marked as logically deleted
lazy Linked List
• Linearization points? • Successful Insert
• When pred.next is updated (while acquiring lock) • Successful Delete
• When curr is logically deleted • Unsuccessful Insert/Delete
• When curr is checked (while acquiring lock) • Successful Contains
• When an unmarked matching node is found • Unsuccessful Contains
• ???
Hash Tables
• Closed addressing
• Use Per-bucket (readers/writer) locks
• Linearizationpoints:whenlockisacquired
• Use linearizable (e.g., lazy) linked list in each bucket.
• Linearizationpoint:list’slinearizationpoint
• Open addressing
• Probing techniques will make it hard to have an efficient algorithm • Alternative: Cuckoo hashing
• Usetwotableswithtwodifferenthashfunctions
• Alloperations:check(andthuslock)onlytwolocations
• Duringinsertifbothlocationsareoccupied
• Kick out the currently existing element in one of the tables
• Recursively insert this kicked out element in the other table
Balanced Trees
• Split operation into
• Eager “semantic access” phase
• Insert: attach node without re-balancing
• Remove: mark node as logically deleted
• Lazy “structural adaptation” phase • Rebalancing
• Physical deletion.
• Examples
• Chromatic Tree (Acta Informatica’1996) • CF-Tree (EuroPar’2013)
• TxCF-Tree (DISC’2015)
• Linearizability?
• Who cares about structural adaptations (as long as they do not interfere with semantic accesses.
Thanks!