Concurrent Objects
Concurrent Objects Companion slides for The Art of Multiprocessor Programming by Maurice Herlihy & Nir Shavit
Concurrent Computation
Art of Multiprocessor Programming 2 Concurrent Computation memory object object
Objectivism
Art of Multiprocessor Programming 3 Objectivism • What is a concurrent object? – How do we describe one? – How do we implement one? – How do we tell if we’re right ?
Objectivism
Art of Multiprocessor Programming 4 Objectivism • What is a concurrent object? – How do we describe one? – How do we tell if we’re right ?
FIFO Queue: Enqueue Method
Art of Multiprocessor Programming 5 FIFO Queue: Enqueue Method q.enq( )
FIFO Queue: Dequeue Method
Art of Multiprocessor Programming 6 FIFO Queue: Dequeue Method q.deq()/
Lock-Based Queue
Art of Multiprocessor Programming 7 Lock-Based Queue head tail 0 2 1 5 4 3 y x capacity = 8 7 6
Lock-Based Queue
Art of Multiprocessor Programming 8 Lock-Based Queue head tail 0 2 1 5 4 3 y x capacity = 8 7 6 Fields protected by single shared lock
A Lock-Based Queue
class LockBasedQueue<T> { int head, tail; T[] items; Lock lock; public LockBasedQueue(int capacity) { head = 0; tail = 0; lock = new ReentrantLock(); items = (T[]) new Object[capacity]; } Art of Multiprocessor Programming 9 A Lock-Based Queue 0 1 capacity-1 2 head tail y z Fields protected by single shared lock
Lock-Based Queue
Art of Multiprocessor Programming 10 Lock-Based Queue head tail 0 2 1 5 4 3 Initially head = tail 7 6
A Lock-Based Queue
class LockBasedQueue<T> { int head, tail; T[] items; Lock lock; public LockBasedQueue( int capacity) { head = 0; tail = 0; lock = new ReentrantLock(); items = (T[]) new Object[capacity]; } Art of Multiprocessor Programming 11 A Lock-Based Queue 0 1 capacity-1 2 head tail y z Initially head = tail
Lock-Based deq()
Art of Multiprocessor Programming 12 Lock-Based deq() head tail 0 2 5 4 7 3 6 y x 1
Acquire Lock
Art of Multiprocessor Programming 13 Acquire Lock head tail 0 2 5 4 7 3 6 y x 1 Waiting to enqueue… My turn …
Implementation: deq()
public T deq() throws EmptyException { lock.lock(); try { if (tail == head) throw new EmptyException(); T x = items[head % items.length]; head++; return x; } finally { lock.unlock(); } } Art of Multiprocessor Programming 14 Implementation: deq() Acquire lock at method start 0 1 capacity-1 2 head tail y z
Check if Non-Empty
Art of Multiprocessor Programming 15 Check if Non-Empty head tail 0 2 5 4 7 3 6 y x 1 Waiting to enqueue…
Implementation: deq()
public T deq() throws EmptyException { lock.lock(); try { if (tail == head) throw new EmptyException(); T x = items[head % items.length]; head++; return x; } finally { lock.unlock(); } } Art of Multiprocessor Programming 16 Implementation: deq() If queue empty throw exception 0 1 capacity-1 2 head tail y z
Modify the Queue
Art of Multiprocessor Programming 17 Modify the Queue head tail 0 2 1 5 4 7 3 6 y x head Waiting to enqueue…
Implementation: deq()
public T deq() throws EmptyException { lock.lock(); try { if (tail == head) throw new EmptyException(); T x = items[head % items.length]; head++; return x; } finally { lock.unlock(); } } Art of Multiprocessor Programming 18 Implementation: deq() Queue not empty? Remove item and update head 0 1 capacity-1 2 head tail y z
Implementation: deq()
public T deq() throws EmptyException { lock.lock(); try { if (tail == head) throw new EmptyException(); T x = items[head % items.length]; head++; return x; } finally { lock.unlock(); } } Art of Multiprocessor Programming 19 Implementation: deq() Return result 0 1 capacity-1 2 head tail y z
Release the Lock
Art of Multiprocessor Programming 20 Release the Lock tail 0 2 1 5 4 7 3 6 y x head My turn!
Implementation: deq()
public T deq() throws EmptyException { lock.lock(); try { if (tail == head) throw new EmptyException(); T x = items[head % items.length]; head++; return x; } finally { lock.unlock(); } } Art of Multiprocessor Programming 21 Implementation: deq() Release lock no matter what! 0 1 capacity-1 2 head tail y z
Implementation: deq()
public T deq() throws EmptyException { lock.lock(); try { if (tail == head) throw new EmptyException(); T x = items[head % items.length]; head++; return x; } finally { lock.unlock(); } } Art of Multiprocessor Programming 22 Implementation: deq() Should be correct because modifications are mutually exclusive…
Now consider the following implementation
Art of Multiprocessor Programming 23 Now consider the following implementation • The same thing without mutual exclusion • For simplicity, only two threads – One thread enq only – The other deq only
Wait-free 2-Thread Queue
Art of Multiprocessor Programming 24 Wait-free 2-Thread Queue head tail 0 2 1 5 4 7 3 6 y x capacity = 8
Wait-free 2-Thread Queue
Art of Multiprocessor Programming 25 Wait-free 2-Thread Queue tail 0 2 5 4 7 3 6 y x 1 enq(z) deq() z head
Wait-free 2-Thread Queue
Art of Multiprocessor Programming 26 Wait-free 2-Thread Queue head tail 0 2 5 4 7 3 6 y 1 queue[tail] = z result = x z x
Wait-free 2-Thread Queue
Art of Multiprocessor Programming 27 Wait-free 2-Thread Queue tail 0 2 5 4 7 3 6 y 1 tail-- head++ z head x
Wait-free 2-Thread Queue
public class WaitFreeQueue { int head = 0, tail = 0; items = (T[]) new Object[capacity ]; public void enq(Item x) { if (tail-head == capacity) throw new FullException(); items[tail % capacity] = x; tail++; } public Item deq() { if (tail == head) throw new EmptyException(); Item item = items[head % capacity]; head++; return item; }} Art of Multiprocessor Programming 28 Wait-free 2-Thread Queue 0 1 capacity-1 2 head tail y z No lock needed !
Wait-free 2-Thread Queue
Wait-free 2-Thread Queue Art of Multiprocessor Programming 29 public T deq() throws EmptyException { lock.lock(); try { if (tail == head) throw new EmptyException(); T x = items[head % items.length]; head++; return x; } finally { lock.unlock(); } } How do we define “correct” when modifications are not mutually exclusive?
What is a Concurrent Queue?
Art of Multiprocessor Programming 30 What is a Concurrent Queue? • Need a way to specify a concurrent queue object • Need a way to prove that an algorithm implements the object’s specification • Lets talk about object specifications …
Correctness and Progress
Correctness and Progress • In a concurrent setting, we need to specify both the safety and the liveness properties of an object • Need a way to define – when an implementation is correct – the conditions under which it guarantees progress Art of Multiprocessor Programming 31 Lets begin with correctness
Sequential Objects
Art of Multiprocessor Programming 32 Sequential Objects • Each object has a state – Usually given by a set of fields – Queue example: sequence of items • Each object has a set of methods – Only way to manipulate state – Queue example: enq and deq methods
Sequential Specifications
Art of Multiprocessor Programming 33 Sequential Specifications • If (precondition) – the object is in such-and-such a state – before you call the method, • Then (postcondition) – the method will return a particular value – or throw a particular exception. • and (postcondition, con’t) – the object will be in some other state – when the method returns,
Pre and PostConditions for Dequeue
Art of Multiprocessor Programming 34 Pre and PostConditions for Dequeue • Precondition: – Queue is non-empty • Postcondition: – Returns first item in queue • Postcondition: – Removes first item in queue
Pre and PostConditions for Dequeue
Art of Multiprocessor Programming 35 Pre and PostConditions for Dequeue • Precondition: – Queue is empty • Postcondition: – Throws Empty exception • Postcondition: – Queue state unchanged
Why Sequential Specifications Totally Rock
Art of Multiprocessor Programming 36 Why Sequential Specifications Totally Rock • Interactions among methods captured by side- effects on object state – State meaningful 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 Specifications ?
Art of Multiprocessor Programming 37 What About Concurrent Specifications ? • Methods? • Documentation? • Adding new methods?
Methods Take Time
Art of Multiprocessor Programming 38 Methods Take Time time time
Methods Take Time
Art of Multiprocessor Programming 39 Methods Take Time time invocation 12:00 q.enq( ... ) time
Methods Take Time
Art of Multiprocessor Programming 40 Methods Take Time time Method call invocation 12:00 time q.enq( ... )
Methods Take Time
Art of Multiprocessor Programming 41 Methods Take Time time Method call invocation 12:00 time q.enq( ... )
Methods Take Time
Art of Multiprocessor Programming 42 Methods Take Time time Method call invocation 12:00 time void response 12:01 q.enq( ... )
Sequential vs Concurrent
Art of Multiprocessor Programming 43 Sequential vs Concurrent • Sequential – Methods take time? Who knew? • Concurrent – Method call is not an event – Method call is an interval .
Concurrent Methods Take Overlapping Time
Art of Multiprocessor Programming 44 time Concurrent Methods Take Overlapping Time time
Concurrent Methods Take Overlapping Time
Art of Multiprocessor Programming 45 time Concurrent Methods Take Overlapping Time time Method call
Concurrent Methods Take Overlapping Time
Art of Multiprocessor Programming 46 time Concurrent Methods Take Overlapping Time time Method call Method call
Concurrent Methods Take Overlapping Time
Art of Multiprocessor Programming 47 time Concurrent Methods Take Overlapping Time time Method call Method call Method call
Sequential vs Concurrent
Art of Multiprocessor Programming 48 Sequential vs Concurrent • Sequential: – Object needs meaningful state only between method calls • Concurrent – Because method calls overlap, object might never be between method calls
Sequential vs Concurrent
Art of Multiprocessor Programming 49 Sequential vs Concurrent • Sequential: – Each method described in isolation • Concurrent – Must characterize all possible interactions with concurrent calls • What if two enq s overlap? • Two deq s? enq and deq ? …
Sequential vs Concurrent
Art of Multiprocessor Programming 50 Sequential vs Concurrent • Sequential: – Can add new methods without affecting older methods • Concurrent: – Everything can potentially interact with everything else
Sequential vs Concurrent
Art of Multiprocessor Programming 51 Sequential vs Concurrent • Sequential: – Can add new methods without affecting older methods • Concurrent: – Everything can potentially interact with everything else Panic!
The Big Question
Art of Multiprocessor Programming 52 The Big Question • What does it mean for a concurrent object to be correct? – What is a concurrent FIFO queue? – FIFO means strict temporal order – Concurrent means ambiguous temporal order
Intuitively…
Art of Multiprocessor Programming 53 Intuitively… public T deq() throws EmptyException { lock.lock(); try { if (tail == head) throw new EmptyException(); T x = items[head % items.length]; head++; return x; } finally { lock.unlock(); } }
Intuitively…
Art of Multiprocessor Programming 54 Intuitively… public T deq() throws EmptyException { lock.lock(); try { if (tail == head) throw new EmptyException(); T x = items[head % items.length]; head++; return x; } finally { lock.unlock(); } } All queue modifications are mutually exclusive
Intuitively
Art of Multiprocessor Programming 55 time Intuitively q.deq q.enq enq deq lock() unlock() lock() unlock() Behavior is “Sequential” enq deq Lets capture the idea of describing the concurrent via the sequential
Linearizability
Art of Multiprocessor Programming 56 Linearizability • Each method should – “take effect” – Instantaneously – Between invocation and response events • Object is correct if this “sequential” behavior is correct • Any such concurrent object is – Linearizable™
Is it really about the object?
Art of Multiprocessor Programming 57 Is it really about the object? • Each method should – “take effect” – Instantaneously – Between invocation and response events • Sounds like a property of an execution… • A linearizable object : one all of whose possible executions are linearizable
Example
Art of Multiprocessor Programming 58 Example time time
Example
Art of Multiprocessor Programming 59 Example time q.enq(x) time
Example
Art of Multiprocessor Programming 60 Example time q.enq(x) q.enq(y) time
Example
Art of Multiprocessor Programming 61 Example time q.enq(x) q.enq(y) q.deq(x) time
Example
Art of Multiprocessor Programming 62 Example time q.enq(x) q.enq(y) q.deq(x) q.deq(y) time
Example
Art of Multiprocessor Programming 63 Example time q.enq(x) q.enq(y) q.deq(x) q.deq(y) linearizable q.enq(x) q.enq(y) q.deq(x) q.deq(y) time
Example
Art of Multiprocessor Programming 64 Example time q.enq(x) q.enq(y) q.deq(x) q.deq(y) Valid? q.enq(x) q.enq(y) q.deq(x) q.deq(y) time
Example
Art of Multiprocessor Programming 65 Example time
Example
Art of Multiprocessor Programming 66 Example time q.enq(x)
Example
Art of Multiprocessor Programming 67 Example time q.enq(x) q.deq(y)
Example
Art of Multiprocessor Programming 68 Example time q.enq(x) q.enq(y) q.deq(y)
Example
Art of Multiprocessor Programming 69 Example time q.enq(x) q.enq(y) q.deq(y) q.enq(x) q.enq(y)
Example
Art of Multiprocessor Programming 70 Example time q.enq(x) q.enq(y) q.deq(y) q.enq(x) q.enq(y) (5) not linearizable
Example
Art of Multiprocessor Programming 71 Example time time
Example
Art of Multiprocessor Programming 72 Example time q.enq(x) time
Example
Art of Multiprocessor Programming 73 Example time q.enq(x) q.deq(x) time
Example
Art of Multiprocessor Programming 74 Example time q.enq(x) q.deq(x) q.enq(x) q.deq(x) time
Example
Art of Multiprocessor Programming 75 Example time q.enq(x) q.deq(x) q.enq(x) q.deq(x) linearizable time
Example
Art of Multiprocessor Programming 76 Example time q.enq(x) time
Example
Art of Multiprocessor Programming 77 Example time q.enq(x) q.enq(y) time
Example
Art of Multiprocessor Programming 78 Example time q.enq(x) q.enq(y) q.deq(y) time
Example
Art of Multiprocessor Programming 79 Example time q.enq(x) q.enq(y) q.deq(y) q.deq(x) time
Art of Multiprocessor Programming 80 q.enq(x) q.enq(y) q.deq(y) q.deq(x) Comme ci Example time Comme ça multiple orders OK linearizable
Read/Write Register Example
Art of Multiprocessor Programming 81 Read/Write Register Example time read(1) write(0) write(1) write(2) time read(0)
Read/Write Register Example
Art of Multiprocessor Programming 82 Read/Write Register Example time read(1) write(0) write(1) write(2) time read(0) write(1) already happened
Read/Write Register Example
Art of Multiprocessor Programming 83 Read/Write Register Example time read(1) write(0) write(1) write(2) time read(0) write(1) write(1) already happened
Read/Write Register Example
Art of Multiprocessor Programming 84 Read/Write Register Example time read(1) write(0) write(1) write(2) time read(0) write(1) write(1) already happened not linearizable
Read/Write Register Example
Art of Multiprocessor Programming 85 Read/Write Register Example time read(1) write(0) write(1) write(2) time read(1) write(1) already happened
Read/Write Register Example
Art of Multiprocessor Programming 86 Read/Write Register Example time read(1) write(0) write(1) write(2) time read(1) write(1) write(2) write(1) already happened
Read/Write Register Example
Art of Multiprocessor Programming 87 Read/Write Register Example time read(1) write(0) write(1) write(2) time read(1) write(1) write(2) not linearizable write(1) already happened
Read/Write Register Example
Art of Multiprocessor Programming 88 Read/Write Register Example time write(0) write(1) write(2) time read(1)
Read/Write Register Example
Art of Multiprocessor Programming 89 Read/Write Register Example time write(0) write(1) write(2) time read(1) write(1) write(2)
Read/Write Register Example
Art of Multiprocessor Programming 90 Read/Write Register Example time write(0) write(1) write(2) time read(1) write(1) write(2) linearizable
Read/Write Register Example
Art of Multiprocessor Programming 91 Read/Write Register Example time read(1) write(0) write(1) write(2) time read(1)
Read/Write Register Example
Art of Multiprocessor Programming 92 Read/Write Register Example time read(1) write(0) write(1) write(2) time read(1) write(1)
Read/Write Register Example
Art of Multiprocessor Programming 93 Read/Write Register Example time read(1) write(0) write(1) write(2) time read(1) write(1) write(2)
Read/Write Register Example
Art of Multiprocessor Programming 94 Read/Write Register Example time read(1) write(0) write(1) write(2) time read(2) write(1) write(2) Not linearizable
Talking About Executions
Art of Multiprocessor Programming 95 Talking About Executions • Why? – Can’t we specify the linearization point of each operation without describing an execution? • Not Always – In some cases, linearization point depends on the execution
Formal Model of Executions
Art of Multiprocessor Programming 96 Formal Model of Executions • Define precisely what we mean – Ambiguity is bad when intuition is weak • Allow reasoning – Formal – But mostly informal • In the long run, actually more important • Ask me why!
Split Method Calls into Two Events
Art of Multiprocessor Programming 97 Split Method Calls into Two Events • Invocation – method name & args – q.enq(x) • Response – result or exception – q.enq(x) returns void – q.deq() returns x – q.deq() throws empty
Invocation Notation
Art of Multiprocessor Programming 98 Invocation Notation A q.enq(x) (4)
Invocation Notation
Art of Multiprocessor Programming 99 Invocation Notation A q.enq(x) thread (4)
Invocation Notation
Art of Multiprocessor Programming 100 Invocation Notation A q.enq(x) thread method (4)
Invocation Notation
Art of Multiprocessor Programming 101 Invocation Notation A q.enq(x) thread object (4) method
Invocation Notation
Art of Multiprocessor Programming 102 Invocation Notation A q.enq(x) thread object method arguments (4)
Response Notation
Art of Multiprocessor Programming 103 Response Notation A q: void (2)
Response Notation
Art of Multiprocessor Programming 104 Response Notation A q: void thread (2)
Response Notation
Art of Multiprocessor Programming 105 Response Notation A q: void thread result (2)
Response Notation
Art of Multiprocessor Programming 106 Response Notation A q: void thread object result (2)
Response Notation
Art of Multiprocessor Programming 107 Response Notation A q: void thread object result (2) Method is implicit
Response Notation
Art of Multiprocessor Programming 108 Response Notation A q: empty() thread object (2) Method is implicit exception
History - Describing an Execution
Art of Multiprocessor Programming 109 History - Describing an Execution A q.enq(3) A q:void A q.enq(5) B p.enq(4) B p:void B q.deq() B q:3 Sequence of invocations and responses H =
Definition
Art of Multiprocessor Programming 110 Definition • Invocation & response match if A q.enq(3) A q:void Thread names agree Object names agree Method call (1)
Object Projections
Art of Multiprocessor Programming 111 Object Projections A q.enq(3) A q:void B p.enq(4) B p:void B q.deq() B q:3 H =
Object Projections
Art of Multiprocessor Programming 112 Object Projections A q.enq(3) A q:void B p.enq(4) B p:void B q.deq() B q:3 H|q =
Thread Projections
Art of Multiprocessor Programming 113 Thread Projections A q.enq(3) A q:void B p.enq(4) B p:void B q.deq() B q:3 H =
Thread Projections
Art of Multiprocessor Programming 114 Thread Projections A q.enq(3) A q:void B p.enq(4) B p:void B q.deq() B q:3 H|B =
Complete Subhistory
Art of Multiprocessor Programming 115 Complete Subhistory 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 invocation is pending if it has no matching respnse H =
Complete Subhistory
Art of Multiprocessor Programming 116 Complete Subhistory A q.enq(3) A q:void A q.enq(5) B p.enq(4) B p:void B q.deq() B q:3 May or may not have taken effect H =
Complete Subhistory
Art of Multiprocessor Programming 117 Complete Subhistory A q.enq(3) A q:void A q.enq(5) B p.enq(4) B p:void B q.deq() B q:3 discard pending invocations H =
Complete Subhistory
Art of Multiprocessor Programming 118 Complete Subhistory A q.enq(3) A q:void B p.enq(4) B p:void B q.deq() B q:3 Complete(H) =
Sequential Histories
Art of Multiprocessor Programming 119 Sequential Histories A q.enq(3) A q:void B p.enq(4) B p:void B q.deq() B q:3 A q:enq(5) (4)
Sequential Histories
Art of Multiprocessor Programming 120 Sequential Histories A q.enq(3) A q:void B p.enq(4) B p:void B q.deq() B q:3 A q:enq(5) match (4)
Sequential Histories
Art of Multiprocessor Programming 121 Sequential Histories A q.enq(3) A q:void B p.enq(4) B p:void B q.deq() B q:3 A q:enq(5) match match (4)
Sequential Histories
Art of Multiprocessor Programming 122 Sequential Histories A q.enq(3) A q:void B p.enq(4) B p:void B q.deq() B q:3 A q:enq(5) match match match (4)
Sequential Histories
Art of Multiprocessor Programming 123 Sequential Histories A q.enq(3) A q:void B p.enq(4) B p:void B q.deq() B q:3 A q:enq(5) match match match Final pending invocation OK (4)
Sequential Histories
Art of Multiprocessor Programming 124 Sequential Histories A q.enq(3) A q:void B p.enq(4) B p:void B q.deq() B q:3 A q:enq(5) match match match Final pending invocation OK (4) Method calls of different threads do not interleave
Well-Formed Histories
Art of Multiprocessor Programming 125 Well-Formed Histories H= A q.enq(3) B p.enq(4) B p:void B q.deq() A q:void B q:3
Well-Formed Histories
Art of Multiprocessor Programming 126 Well-Formed Histories H= A q.enq(3) B p.enq(4) B p:void B q.deq() A q:void B q:3 H|B= B p.enq(4) B p:void B q.deq() B q:3 Per-thread projections sequential
Well-Formed Histories
Art of Multiprocessor Programming 127 Well-Formed Histories H= A q.enq(3) B p.enq(4) B p:void B q.deq() A q:void B q:3 H|B= B p.enq(4) B p:void B q.deq() B q:3 A q.enq(3) A q:void H|A= Per-thread projections sequential
Equivalent Histories
Art of Multiprocessor Programming 128 Equivalent Histories H= A q.enq(3) B p.enq(4) B p:void B q.deq() A q:void B q:3 Threads see the same thing in both A q.enq(3) A q:void B p.enq(4) B p:void B q.deq() B q:3 G= H|A = G|A H|B = G|B
Sequential Specifications
Art of Multiprocessor Programming 129 Sequential Specifications • A sequential specification is some way of telling whether a – Single-thread, single-object history – Is legal • For example: – Pre and post-conditions – But plenty of other techniques exist …
Legal Histories
Art of Multiprocessor Programming 130 Legal Histories • A sequential (multi-object) history H is legal if – For every object x – H|x is in the sequential spec for x
Precedence
Art of Multiprocessor Programming 131 Precedence A q.enq(3) B p.enq(4) B p.void A q:void B q.deq() B q:3 A method call precedes another if response event precedes invocation event Method call Method call (1)
Non-Precedence
Art of Multiprocessor Programming 132 Non-Precedence A q.enq(3) B p.enq(4) B p.void B q.deq() A q:void B q:3 Some method calls overlap one another Method call Method call (1)
Notation
Art of Multiprocessor Programming 133 Notation • Given – History H – method executions m 0 and m 1 in H • We say m 0 H m 1 , if – m 0 precedes m 1 • Relation m 0 H m 1 is a – Partial order – Total order if H is sequential m 0 m 1
Linearizability
Art of Multiprocessor Programming 134 Linearizability • History H is linearizable if it can be extended to G by – Appending zero or more responses to pending invocations – Discarding other pending invocations • So that G is equivalent to – Legal sequential history S – where G S
Ensuring G  S
Art of Multiprocessor Programming 135 Ensuring G S time a b time (8) G S c G G = {a c,b c} S = {a b,a c,b c} A limitation on the Choice of S!
Remarks
Art of Multiprocessor Programming 136 Remarks • Some pending invocations – Took effect, so keep them – Discard the rest • Condition G S – Means that S respects “real-time order” of G
Example
Art of Multiprocessor Programming 137 A q.enq(3) B q.enq(4) B q:void B q.deq() B q:4 B q:enq(6) Example time B.q.enq(4 ) A. q.enq(3) B.q.deq(4 ) B. q.enq(6)
Example
Art of Multiprocessor Programming 138 Example Complete this pending invocation time B.q.enq(4 ) B.q.deq(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) A. q.enq(3)
Example
Art of Multiprocessor Programming 139 Example Complete this pending invocation time B.q.enq(4 ) B.q.deq(4 ) B. q.enq(6) A.q.enq(3 ) A q.enq(3) B q.enq(4) B q:void B q.deq() B q:4 B q:enq(6) A q:void
Example
Art of Multiprocessor Programming 140 Example time B.q.enq(4 ) B.q.deq(4 ) B. q.enq(6) A.q.enq(3 ) A q.enq(3) B q.enq(4) B q:void B q.deq() B q:4 B q:enq(6) A q:void discard this one
Example
Art of Multiprocessor Programming 141 Example time B.q.enq(4 ) B.q.deq(4 ) A.q.enq(3 ) A q.enq(3) B q.enq(4) B q:void B q.deq() B q:4 A q:void discard this one
Example
Art of Multiprocessor Programming 142 A q.enq(3) B q.enq(4) B q:void B q.deq() B q:4 A q:void Example time B.q.enq(4 ) B.q.deq(4 ) A.q.enq(3 )
Example
Art of Multiprocessor Programming 143 A q.enq(3) B q.enq(4) B q:void B q.deq() B q:4 A q:void Example time B q.enq(4) B q:void A q.enq(3) A q:void B q.deq() B q:4 B.q.enq(4 ) B.q.deq(4 ) A.q.enq(3 )
Example
Art of Multiprocessor Programming 144 B.q.enq(4 ) B.q.deq(4 ) A.q.enq(3 ) A q.enq(3) B q.enq(4) B q:void B q.deq() B q:4 A q:void Example time B q.enq(4) B q:void A q.enq(3) A q:void B q.deq() B q:4 Equivalent sequential history
Composability Theorem
Art of Multiprocessor Programming 150 Composability Theorem • History H is linearizable if and only if – For every object x – H|x is linearizable • We care about objects only! – (Materialism?)
Why Does Composability Matter?
Art of Multiprocessor Programming 151 Why Does Composability Matter? • Modularity • Can prove linearizability of objects in isolation • Can compose independently-implemented objects
Reasoning About Linearizability: Locking
Art of Multiprocessor Programming 152 Reasoning About Linearizability: Locking public T deq() throws EmptyException { lock.lock(); try { if (tail == head) throw new EmptyException(); T x = items[head % items.length]; head++; return x; } finally { lock.unlock(); } } 0 1 capacity-1 2 head tail y z
Reasoning About Linearizability: Locking
Art of Multiprocessor Programming 153 Reasoning About Linearizability: Locking public T deq() throws EmptyException { lock.lock(); try { if (tail == head) throw new EmptyException(); T x = items[head % items.length]; head++; return x; } finally { lock.unlock(); } } Linearization points are when locks are released
More Reasoning: Wait-free
Art of Multiprocessor Programming 154 More Reasoning: Wait-free 0 1 capacity-1 2 head tail y z public class WaitFreeQueue { int head = 0, tail = 0; items = (T[]) new Object[capacity]; public void enq(Item x) { if (tail-head == capacity) throw new FullException(); items[tail % capacity] = x; tail++; } public Item deq() { if (tail == head) throw new EmptyException(); Item item = items[head % capacity]; head++; return item; }} 0 1 capacity-1 2 head tail y z
More Reasoning: Wait-free
public class WaitFreeQueue { int head = 0, tail = 0; items = (T[]) new Object[capacity ]; public void enq(Item x) { if (tail-head == capacity) throw new FullException(); items[tail % capacity] = x; tail++; } public Item deq() { if (tail == head) throw new EmptyException(); Item item = items[head % capacity]; head++; return item; }} Art of Multiprocessor Programming 155 More Reasoning: Wait-free 0 1 capacity-1 2 head tail y z Linearization order is order head and tail fields modified Remember that there is only one enqueuer and only one dequeuer
Strategy
Art of Multiprocessor Programming 156 Strategy • Identify one atomic step where method “happens” – Critical section – Machine instruction • Doesn’t always work – Might need to define several different steps for a given method
Linearizability: Summary
Art of Multiprocessor Programming 157 Linearizability: Summary • Powerful specification tool for shared objects • Allows us to capture the notion of objects being “atomic” • Don’t leave home without it
Alternative: Sequential Consistency
Art of Multiprocessor Programming 158 Alternative: Sequential Consistency • History H is Sequentially Consistent if it can be extended to G by – Appending zero or more responses to pending invocations – Discarding other pending invocations • So that G is equivalent to a – Legal sequential history S – Where G S Differs from linearizability
Sequential Consistency
Art of Multiprocessor Programming 159 Sequential Consistency • No need to preserve real-time order – Cannot re-order operations done by the same thread – Can re-order non-overlapping operations done by different threads • Often used to describe multiprocessor memory architectures
Example
Art of Multiprocessor Programming 160 Example time (5)
Example
Art of Multiprocessor Programming 161 Example time q.enq(x) (5)
Example
Art of Multiprocessor Programming 162 Example time q.enq(x) q.deq(y) (5)
Example
Art of Multiprocessor Programming 163 Example time q.enq(x) q.enq(y) q.deq(y) (5)
Example
Art of Multiprocessor Programming 164 Example time q.enq(x) q.enq(y) q.deq(y) q.enq(x) q.enq(y) (5)
Example
Art of Multiprocessor Programming 165 Example time q.enq(x) q.enq(y) q.deq(y) q.enq(x) q.enq(y) (5) not linearizable
Example
Art of Multiprocessor Programming 166 Example time q.enq(x) q.enq(y) q.deq(y) q.enq(x) q.enq(y) (5) Yet Sequentially Consistent
Theorem
Art of Multiprocessor Programming 167 Theorem Sequential Consistency is not composable
FIFO Queue Example
Art of Multiprocessor Programming 168 FIFO Queue Example time p.enq(x) p.deq(y) q.enq(x) time
FIFO Queue Example
Art of Multiprocessor Programming 169 FIFO Queue Example time p.enq(x) p.deq(y) q.enq(x) q.enq(y) q.deq(x) p.enq(y) time
FIFO Queue Example
Art of Multiprocessor Programming 170 FIFO Queue Example time p.enq(x) p.deq(y) q.enq(x) q.enq(y) q.deq(x) p.enq(y) History H time
H|p Sequentially Consistent
Art of Multiprocessor Programming 171 H|p Sequentially Consistent time p.enq(x ) p.deq(y ) p.enq(y ) q.enq(x) q.enq(y) q.deq(x) time
H|q Sequentially Consistent
Art of Multiprocessor Programming 172 H|q Sequentially Consistent time p.enq(x) p.deq(y) q.enq(x) q.enq(y) q.deq(x) p.enq(y) time
Ordering imposed by p
Art of Multiprocessor Programming 173 Ordering imposed by p time p.enq(x) p.deq(y) q.enq(x) q.enq(y) q.deq(x) p.enq(y) time
Ordering imposed by q
Art of Multiprocessor Programming 174 Ordering imposed by q time p.enq(x) p.deq(y) q.enq(x) q.enq(y) q.deq(x) p.enq(y) time
Ordering imposed by both
Art of Multiprocessor Programming 175 p.enq(x) Ordering imposed by both time q.enq(x) q.enq(y) q.deq(x) time p.deq(y) p.enq(y)
Combining orders
Art of Multiprocessor Programming 176 p.enq(x) Combining orders time q.enq(x) q.enq(y) q.deq(x) time p.deq(y) p.enq(y)
Fact
Art of Multiprocessor Programming 177 Fact • Most hardware architectures don’t support sequential consistency • Because they think it’s too strong • Here’s another story …
The Flag Example
Art of Multiprocessor Programming 178 The Flag Example time x.write(1) y.read(0) y.write(1) x.read(0) time
The Flag Example
Art of Multiprocessor Programming 179 The Flag Example time x.write(1) y.read(0) y.write(1) x.read(0) • Each thread’s view is sequentially consistent – It went first
The Flag Example
Art of Multiprocessor Programming 180 The Flag Example time x.write(1) y.read(0) y.write(1) x.read(0) • Entire history isn’t sequentially consistent – Can’t both go first
The Flag Example
Art of Multiprocessor Programming 181 The Flag Example time x.write(1) y.read(0) y.write(1) x.read(0) • Is this behavior really so wrong? – We can argue either way …
Opinion1: It’s Wrong
Art of Multiprocessor Programming 182 Opinion1: It’s Wrong • This pattern – Write mine, read yours • Is exactly the flag principle – Beloved of Alice and Bob – Heart of mutual exclusion • Peterson • Bakery, etc. • It’s non-negotiable!
Opinion2: But It Feels So Right …
Art of Multiprocessor Programming 183 Opinion2: But It Feels So Right … • Many hardware architects think that sequential consistency is too strong • Too expensive to implement in modern hardware • OK if flag principle – violated by default – Honored by explicit request
Memory Hierarchy
Art of Multiprocessor Programming 184 Memory Hierarchy • On modern multiprocessors, processors do not read and write directly to memory . • Memory accesses are very slow compared to processor speeds, • Instead, each processor reads and writes directly to a cache
Memory Operations
Art of Multiprocessor Programming 185 Memory Operations • To read a memory location, – load data into cache. • To write a memory location – update cached copy, – lazily write cached data back to memory
While Writing to Memory
Art of Multiprocessor Programming 186 While Writing to Memory • A processor can execute hundreds , or even thousands of instructions • Why delay on every memory write? • Instead, write back in parallel with rest of the program.
Revisionist History
Art of Multiprocessor Programming 187 Revisionist History • Flag violation history is actually OK – processors delay writing to memory – until after reads have been issued. • Otherwise unacceptable delay between read and write instructions. • Who knew you wanted to synchronize?
Who knew you wanted to synchronize?
Art of Multiprocessor Programming 188 Who knew you wanted to synchronize? • Writing to memory = mailing a letter • Vast majority of reads & writes – Not for synchronization – No need to idle waiting for post office • If you want to synchronize – Announce it explicitly – Pay for it only when you need it
Explicit Synchronization
Art of Multiprocessor Programming 189 Explicit Synchronization • Memory barrier instruction – Flush unwritten caches – Bring caches up to date • Compilers often do this for you – Entering and leaving critical sections • Expensive
Volatile
Art of Multiprocessor Programming 190 Volatile • In Java, can ask compiler to keep a variable up-to-date with volatile keyword • Also inhibits reordering, removing from loops, & other “optimizations”
Real-World Hardware Memory
Art of Multiprocessor Programming 191 Real-World Hardware Memory • Weaker than sequential consistency • But you can get sequential consistency at a price • OK for expert, tricky stuff – assembly language, device drivers, etc. • Linearizability more appropriate for high- level software
Linearizability
Art of Multiprocessor Programming 192 Linearizability • Linearizability – Operation takes effect instantaneously between invocation and response – Uses sequential specification, locality implies composablity – Good for high level objects
Correctness: Linearizability
Art of Multiprocessor Programming 193 Correctness: Linearizability • Sequential Consistency – Not composable – Harder to work with – Good way to think about hardware models • We will use linearizability as in the remainder of this course unless stated otherwise
Progress
Progress • We saw an implementation whose methods were lock-based (deadlock-free) • We saw an implementation whose methods did not use locks (lock-free) • How do they relate? Art of Multiprocessor Programming 194
Progress Conditions
Progress Conditions • Deadlock-free: some thread trying to acquire the lock eventually succeeds. • Starvation-free: every thread trying to acquire the lock eventually succeeds. • Lock-free: some thread calling a method eventually returns. • Wait-free: every thread calling a method eventually returns. Art of Multiprocessor Programming 195
Progress Conditions
Progress Conditions Art of Multiprocessor Programming 196 Wait-free Lock-free Starvation-free Deadlock-free Everyone makes progress Non-Blocking Blocking Someone makes progress
Summary
Art of Multiprocessor Programming 197 Summary • We will look at linearizable blocking and non-blocking implementations of objects.
Art of Multiprocessor Programming 198   creativecommons.org/licenses/by-sa/2.5/ Creative Commons Attribution-ShareAlike 2.5 License . • You are free: – to Share — to copy, distribute and transmit the work – to Remix — to adapt the work • Under the following conditions: – Attribution . You must attribute the work to “The Art of Multiprocessor Programming” (but not in any way that suggests that the authors endorse you or your use of the work). – Share Alike . If you alter, transform, or build upon this work, you may distribute the resulting work only under the same, similar or a compatible license. • For any reuse or distribution, you must make clear to others the license terms of this work. The best way to do this is with a link to – http://creativecommons.org/licenses/by-sa/3.0/. • Any of the above conditions can be waived if you get permission from the copyright holder. • Nothing in this license impairs or restricts the author's moral rights.