1 of 159

Concurrent Objects

Companion slides for

The Art of Multiprocessor Programming

by Maurice Herlihy & Nir Shavit

2 of 159

Concurrent Computation

Art of Multiprocessor Programming

2

memory

object

object

3 of 159

Objectivism

  • What is a concurrent object?
    • How do we describe one?
    • How do we implement one?
    • How do we tell if we’re right?

Art of Multiprocessor Programming

3

4 of 159

FIFO Queue: Enqueue Method

Art of Multiprocessor Programming

4

q.enq( )

5 of 159

FIFO Queue: Dequeue Method

Art of Multiprocessor Programming

5

q.deq()/

6 of 159

A Lock-Based Queue

Art of Multiprocessor Programming

6

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];

}

7 of 159

A Lock-Based Queue

Art of Multiprocessor Programming

7

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];

}

0

1

capacity-1

2

head

tail

y

z

Queue fields protected by single shared lock

8 of 159

A Lock-Based Queue

Art of Multiprocessor Programming

8

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];

}

0

1

capacity-1

2

head

tail

y

z

Initially head = tail

9 of 159

Implementation: Deq

Art of Multiprocessor Programming

9

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

10 of 159

Implementation: Deq

Art of Multiprocessor Programming

10

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();

}

}

Method calls

mutually exclusive

0

1

capacity-1

2

head

tail

y

z

0

1

capacity-1

2

head

tail

y

z

11 of 159

Implementation: Deq

Art of Multiprocessor Programming

11

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();

}

}

If queue empty

throw exception

0

1

capacity-1

2

head

tail

y

z

0

1

capacity-1

2

head

tail

y

z

12 of 159

Implementation: Deq

Art of Multiprocessor Programming

12

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();

}

}

Queue not empty:

remove item and update

head

0

1

capacity-1

2

head

tail

y

z

0

1

capacity-1

2

head

tail

y

z

13 of 159

Implementation: Deq

Art of Multiprocessor Programming

13

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();

}

}

Return result

0

1

capacity-1

2

head

tail

y

z

0

1

capacity-1

2

head

tail

y

z

14 of 159

Implementation: Deq

Art of Multiprocessor Programming

14

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();

}

}

Release lock no matter what!

0

1

capacity-1

2

head

tail

y

z

0

1

capacity-1

2

head

tail

y

z

15 of 159

Implementation: Deq

Art of Multiprocessor Programming

15

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();

}

}

Should be correct because

modifications are mutually exclusive…

16 of 159

Now consider the following implementation

  • The same thing without mutual exclusion
  • For simplicity, only two threads
    • One thread enq only
    • The other deq only

Art of Multiprocessor Programming

16

17 of 159

Wait-free 2-Thread Queue

Art of Multiprocessor Programming

17

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;

}}

18 of 159

Wait-free 2-Thread Queue

Art of Multiprocessor Programming

18

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

19 of 159

Wait-free 2-Thread Queue

Art of Multiprocessor Programming

19

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

Queue is updated without a lock!

How do we define “correct” when modifications are not mutually exclusive?

20 of 159

Defining concurrent queue implementations

  • 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 …

Art of Multiprocessor Programming

20

21 of 159

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

21

Lets begin with correctness

22 of 159

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,

​

Art of Multiprocessor Programming

22

23 of 159

Pre and PostConditions for Dequeue

  • Precondition:
    • Queue is non-empty
  • Postcondition:
    • Returns first item in queue
  • Postcondition:
    • Removes first item in queue

Art of Multiprocessor Programming

23

24 of 159

Pre and PostConditions for Dequeue

  • Precondition:
    • Queue is empty
  • Postcondition:
    • Throws Empty exception
  • Postcondition:
    • Queue state unchanged

Art of Multiprocessor Programming

24

25 of 159

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

Art of Multiprocessor Programming

25

26 of 159

What About Concurrent Specifications ?

  • Methods?
  • Documentation?
  • Adding new methods?

Art of Multiprocessor Programming

26

27 of 159

Methods Take Time

Art of Multiprocessor Programming

27

time

time

28 of 159

Methods Take Time

Art of Multiprocessor Programming

28

time

invocation 12:00

q.enq(...)

time

29 of 159

Methods Take Time

Art of Multiprocessor Programming

29

time

Method call

invocation 12:00

time

q.enq(...)

30 of 159

Methods Take Time

Art of Multiprocessor Programming

30

time

Method call

invocation 12:00

time

q.enq(...)

31 of 159

Methods Take Time

Art of Multiprocessor Programming

31

time

Method call

invocation 12:00

time

void

response 12:01

q.enq(...)

32 of 159

Sequential vs Concurrent

  • Sequential
    • Methods take time? Who knew?
  • Concurrent
    • Method call is not an event
    • Method call is an interval.

​

Art of Multiprocessor Programming

32

33 of 159

Concurrent Methods Take Overlapping Time

Art of Multiprocessor Programming

33

time

time

34 of 159

Concurrent Methods Take Overlapping Time

Art of Multiprocessor Programming

34

time

time

Method call

35 of 159

Concurrent Methods Take Overlapping Time

Art of Multiprocessor Programming

35

time

time

Method call

Method call

36 of 159

Concurrent Methods Take Overlapping Time

Art of Multiprocessor Programming

36

time

time

Method call

Method call

Method call

37 of 159

Sequential vs Concurrent

  • Sequential:
    • Each method described in isolation
  • Concurrent
    • Must characterize all possible interactions with concurrent calls
      • What if two enqs overlap?
      • Two deqs? enq and deq? …

Art of Multiprocessor Programming

37

38 of 159

Sequential vs Concurrent

  • Sequential:
    • Can add new methods without affecting older methods
  • Concurrent:
    • Everything can potentially interact with everything else

Art of Multiprocessor Programming

38

39 of 159

Sequential vs Concurrent

  • Sequential:
    • Can add new methods without affecting older methods
  • Concurrent:
    • Everything can potentially interact with everything else

Art of Multiprocessor Programming

39

Panic!

40 of 159

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

Art of Multiprocessor Programming

40

41 of 159

Intuitively…

Art of Multiprocessor Programming

41

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();

}

}

42 of 159

Intuitively…

Art of Multiprocessor Programming

42

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 modifications

of queue are done

mutually exclusive

43 of 159

Intuitively

Art of Multiprocessor Programming

43

time

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

44 of 159

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™

Art of Multiprocessor Programming

44

45 of 159

Example

Art of Multiprocessor Programming

45

time

time

(6)

46 of 159

Example

Art of Multiprocessor Programming

46

time

q.enq(x)

time

(6)

47 of 159

Example

Art of Multiprocessor Programming

47

time

q.enq(x)

q.enq(y)

time

(6)

48 of 159

Example

Art of Multiprocessor Programming

48

time

q.enq(x)

q.enq(y)

q.deq(x)

time

(6)

49 of 159

Example

Art of Multiprocessor Programming

49

time

q.enq(x)

q.enq(y)

q.deq(x)

q.deq(y)

time

(6)

50 of 159

Example

Art of Multiprocessor Programming

50

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

(6)

51 of 159

Example

Art of Multiprocessor Programming

51

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

(6)

52 of 159

Example

Art of Multiprocessor Programming

52

time

(5)

53 of 159

Example

Art of Multiprocessor Programming

53

time

q.enq(x)

(5)

54 of 159

Example

Art of Multiprocessor Programming

54

time

q.enq(x)

q.deq(y)

(5)

55 of 159

Example

Art of Multiprocessor Programming

55

time

q.enq(x)

q.enq(y)

q.deq(y)

(5)

56 of 159

Example

Art of Multiprocessor Programming

56

time

q.enq(x)

q.enq(y)

q.deq(y)

q.enq(x)

q.enq(y)

(5)

57 of 159

Example

Art of Multiprocessor Programming

57

time

q.enq(x)

q.enq(y)

q.deq(y)

q.enq(x)

q.enq(y)

(5)

not linearizable

58 of 159

Example

Art of Multiprocessor Programming

58

time

time

(4)

59 of 159

Example

Art of Multiprocessor Programming

59

time

q.enq(x)

time

(4)

60 of 159

Example

Art of Multiprocessor Programming

60

time

q.enq(x)

q.deq(x)

time

(4)

61 of 159

Example

Art of Multiprocessor Programming

61

time

q.enq(x)

q.deq(x)

q.enq(x)

q.deq(x)

time

(4)

62 of 159

Example

Art of Multiprocessor Programming

62

time

q.enq(x)

q.deq(x)

q.enq(x)

q.deq(x)

linearizable

time

(4)

63 of 159

Example

Art of Multiprocessor Programming

63

time

q.enq(x)

time

(8)

64 of 159

Example

Art of Multiprocessor Programming

64

time

q.enq(x)

q.enq(y)

time

(8)

65 of 159

Example

Art of Multiprocessor Programming

65

time

q.enq(x)

q.enq(y)

q.deq(y)

time

(8)

66 of 159

Example

Art of Multiprocessor Programming

66

time

q.enq(x)

q.enq(y)

q.deq(y)

q.deq(x)

time

(8)

67 of 159

Art of Multiprocessor Programming

67

q.enq(x)

q.enq(y)

q.deq(y)

q.deq(x)

Comme ci

Example

time

Comme ça

multiple orders OK

linearizable

68 of 159

Read/Write Register Example

Art of Multiprocessor Programming

68

time

read(1)

write(0)

write(1)

write(2)

time

read(0)

(4)

69 of 159

Read/Write Register Example

Art of Multiprocessor Programming

69

time

read(1)

write(0)

write(1)

write(2)

time

read(0)

write(1) already happened

(4)

70 of 159

Read/Write Register Example

Art of Multiprocessor Programming

70

time

read(1)

write(0)

write(1)

write(2)

time

read(0)

write(1)

write(1) already happened

(4)

71 of 159

Read/Write Register Example

Art of Multiprocessor Programming

71

time

read(1)

write(0)

write(1)

write(2)

time

read(0)

write(1)

write(1) already happened

(4)

not linearizable

72 of 159

Read/Write Register Example

Art of Multiprocessor Programming

72

time

read(1)

write(0)

write(1)

write(2)

time

read(1)

write(1) already happened

(4)

73 of 159

Read/Write Register Example

Art of Multiprocessor Programming

73

time

read(1)

write(0)

write(1)

write(2)

time

read(1)

write(1)

write(2)

(4)

write(1) already happened

74 of 159

Read/Write Register Example

Art of Multiprocessor Programming

74

time

read(1)

write(0)

write(1)

write(2)

time

read(1)

write(1)

write(2)

not linearizable

(4)

write(1) already happened

75 of 159

Read/Write Register Example

Art of Multiprocessor Programming

75

time

write(0)

write(1)

write(2)

time

read(1)

(4)

76 of 159

Read/Write Register Example

Art of Multiprocessor Programming

76

time

write(0)

write(1)

write(2)

time

read(1)

write(1)

write(2)

(4)

77 of 159

Read/Write Register Example

Art of Multiprocessor Programming

77

time

write(0)

write(1)

write(2)

time

read(1)

write(1)

write(2)

linearizable

(4)

78 of 159

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

​

Art of Multiprocessor Programming

78

79 of 159

Invocation Notation

Art of Multiprocessor Programming

79

A q.enq(x)

80 of 159

Invocation Notation

Art of Multiprocessor Programming

80

A q.enq(x)

thread

81 of 159

Invocation Notation

Art of Multiprocessor Programming

81

A q.enq(x)

thread

method

82 of 159

Invocation Notation

Art of Multiprocessor Programming

82

A q.enq(x)

thread

object

method

83 of 159

Invocation Notation

Art of Multiprocessor Programming

83

A q.enq(x)

thread

object

method

arguments

84 of 159

History - Describing an Execution

Art of Multiprocessor Programming

84

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 =

85 of 159

Definition

  • Invocation & response match if

​

Art of Multiprocessor Programming

85

A q.enq(3)

A q:void

Thread names agree

Object names agree

Method call

(1)

86 of 159

Object Projections

Art of Multiprocessor Programming

86

A q.enq(3)

A q:void

B p.enq(4)

B p:void

B q.deq()

B q:3

​

​

H =

87 of 159

Object Projections

Art of Multiprocessor Programming

87

A q.enq(3)

A q:void

B p.enq(4)

B p:void

B q.deq()

B q:3

​

​

H|q =

88 of 159

Thread Projections

Art of Multiprocessor Programming

88

A q.enq(3)

A q:void

B p.enq(4)

B p:void

B q.deq()

B q:3

​

​

H|B =

89 of 159

Sequential Histories

Art of Multiprocessor Programming

89

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)

90 of 159

Sequential Histories

Art of Multiprocessor Programming

90

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)

91 of 159

Sequential Histories

Art of Multiprocessor Programming

91

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)

92 of 159

Sequential Histories

Art of Multiprocessor Programming

92

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)

93 of 159

Sequential Histories

Art of Multiprocessor Programming

93

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)

94 of 159

Sequential Histories

Art of Multiprocessor Programming

94

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

95 of 159

Well-Formed Histories

Art of Multiprocessor Programming

95

H=

A q.enq(3)

B p.enq(4)

B p:void

B q.deq()

A q:void

B q:3

96 of 159

Well-Formed Histories

Art of Multiprocessor Programming

96

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

97 of 159

Well-Formed Histories

Art of Multiprocessor Programming

97

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

98 of 159

Equivalent Histories

Art of Multiprocessor Programming

98

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

99 of 159

Legal Histories

  • A sequential (multi-object) history H is legal if
    • For every object x
    • H|x is in the sequential specification for x

Art of Multiprocessor Programming

99

100 of 159

Precedence

Art of Multiprocessor Programming

100

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)

101 of 159

Non-Precedence

Art of Multiprocessor Programming

101

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)

102 of 159

Notation

  • Given
    • History H
    • method executions m0 and m1 in H
  • We say m0 🡺H m1, if
    • m0 precedes m1
  • Relation m0 🡺H m1 is a
    • Partial order
    • Total order if H is sequential

​

​

​

Art of Multiprocessor Programming

102

m0

m1

103 of 159

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

Art of Multiprocessor Programming

103

104 of 159

What is 🡺G ⊂ 🡺S�

Art of Multiprocessor Programming

104

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!

105 of 159

Remarks

  • Some pending invocations
    • Took effect, so keep them
    • Discard the rest
  • Condition 🡺G ⊂ 🡺S
    • Means that S respects “real-time order” of G

​

Art of Multiprocessor Programming

105

106 of 159

Example

Art of Multiprocessor Programming

106

A q.enq(3)

B q.enq(4)

B q:void

B q.deq()

B q:4

B q:enq(6)

time

B.q.enq(4)

A. q.enq(3)

B.q.deq(4)

B. q.enq(6)

107 of 159

Example

Art of Multiprocessor Programming

107

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)

108 of 159

Example

Art of Multiprocessor Programming

108

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

109 of 159

Example

Art of Multiprocessor Programming

109

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

110 of 159

Example

Art of Multiprocessor Programming

110

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

111 of 159

Example

Art of Multiprocessor Programming

111

A q.enq(3)

B q.enq(4)

B q:void

B q.deq()

B q:4

A q:void

time

B.q.enq(4)

B.q.deq(4)

A.q.enq(3)

112 of 159

Example

Art of Multiprocessor Programming

112

A q.enq(3)

B q.enq(4)

B q:void

B q.deq()

B q:4

A q:void

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)

113 of 159

Example

Art of Multiprocessor Programming

113

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

time

B q.enq(4)

B q:void

A q.enq(3)

A q:void

B q.deq()

B q:4

Equivalent sequential history

114 of 159

Composability Theorem

  • History H is linearizable if and only if
    • For every object x
    • H|x is linearizable
  • We care about objects only!
    • (Materialism?)

Art of Multiprocessor Programming

114

115 of 159

Linearizability: Summary

  • Powerful specification tool for shared objects
  • Allows us to capture the notion of objects being “atomic”
  • Don’t leave home without it

​

Art of Multiprocessor Programming

115

116 of 159

Alternative: Sequential Consistency

Art of Multiprocessor Programming

116

  • 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

117 of 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

Art of Multiprocessor Programming

117

118 of 159

Example

Art of Multiprocessor Programming

118

time

(5)

119 of 159

Example

Art of Multiprocessor Programming

119

time

q.enq(x)

(5)

120 of 159

Example

Art of Multiprocessor Programming

120

time

q.enq(x)

q.deq(y)

(5)

121 of 159

Example

Art of Multiprocessor Programming

121

time

q.enq(x)

q.enq(y)

q.deq(y)

(5)

122 of 159

Example

Art of Multiprocessor Programming

122

time

q.enq(x)

q.enq(y)

q.deq(y)

q.enq(x)

q.enq(y)

(5)

123 of 159

Example

Art of Multiprocessor Programming

123

time

q.enq(x)

q.enq(y)

q.deq(y)

q.enq(x)

q.enq(y)

(5)

not linearizable

124 of 159

Example

Art of Multiprocessor Programming

124

time

q.enq(x)

q.enq(y)

q.deq(y)

q.enq(x)

q.enq(y)

(5)

Yet Sequentially Consistent

125 of 159

Theorem

Sequential Consistency is not a local property

​

(and thus we lose composability…)

Art of Multiprocessor Programming

125

126 of 159

FIFO Queue Example

Art of Multiprocessor Programming

126

time

p.enq(x)

p.deq(y)

q.enq(x)

time

127 of 159

FIFO Queue Example

Art of Multiprocessor Programming

127

time

p.enq(x)

p.deq(y)

q.enq(x)

q.enq(y)

q.deq(x)

p.enq(y)

time

128 of 159

FIFO Queue Example

Art of Multiprocessor Programming

128

time

p.enq(x)

p.deq(y)

q.enq(x)

q.enq(y)

q.deq(x)

p.enq(y)

History H

time

129 of 159

H|p Sequentially Consistent

Art of Multiprocessor Programming

129

time

p.enq(x)

p.deq(y)

p.enq(y)

q.enq(x)

q.enq(y)

q.deq(x)

time

130 of 159

H|q Sequentially Consistent

Art of Multiprocessor Programming

130

time

p.enq(x)

p.deq(y)

q.enq(x)

q.enq(y)

q.deq(x)

p.enq(y)

time

131 of 159

Ordering imposed by p

Art of Multiprocessor Programming

131

time

p.enq(x)

p.deq(y)

q.enq(x)

q.enq(y)

q.deq(x)

p.enq(y)

time

132 of 159

Ordering imposed by q

Art of Multiprocessor Programming

132

time

p.enq(x)

p.deq(y)

q.enq(x)

q.enq(y)

q.deq(x)

p.enq(y)

time

133 of 159

Ordering imposed by both

Art of Multiprocessor Programming

133

p.enq(x)

time

q.enq(x)

q.enq(y)

q.deq(x)

time

p.deq(y)

p.enq(y)

134 of 159

Combining orders

Art of Multiprocessor Programming

134

p.enq(x)

time

q.enq(x)

q.enq(y)

q.deq(x)

time

p.deq(y)

p.enq(y)

135 of 159

Quiescent Consistency

  • Is this execution linearizable?
  • Is it sequentially consistent?
  • Is it just nothing?

135

136 of 159

Quiescent Consistency

  • Is this execution linearizable? NO
  • Is it sequentially consistent? NO
  • Is it just nothing?

136

137 of 159

Quiescent Consistency

Quiescent consistency allows a group of overlapping calls to be re-ordered. They cannot be re-ordered across a “quiet” region.

137

138 of 159

Quiescent Consistency

138

Quiescently Consistent

139 of 159

What is this?

  • Is this execution linearizable?
  • Is it sequentially consistent?
  • Is it quiescently consistent?

139

140 of 159

What is this?

  • Is this execution linearizable? NO
  • Is it sequentially consistent? YES
  • Is it quiescently consistent? YES

140

141 of 159

What is this?

  • Is this execution linearizable?
  • Is it sequentially consistent?
  • Is it quiescently consistent?

141

142 of 159

What is this?

  • Is this execution linearizable? NO
  • Is it sequentially consistent? YES
  • Is it quiescently consistent? NO

142

143 of 159

What is this?

  • Is this execution linearizable?
  • Is it sequentially consistent?
  • Is it quiescently consistent?

143

144 of 159

What is this?

  • Is this execution linearizable? YES
  • Is it sequentially consistent? YES
  • Is it quiescently consistent? YES

144

145 of 159

Is there overlap?

NOTE: Any linearizable execution is also sequentially consistent and quiescently consistent.

145

146 of 159

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

Art of Multiprocessor Programming

146

147 of 159

Progress Conditions

  • Deadlock-free
  • Starvation-free
  • Lock-free
  • Wait-Free

147

148 of 159

Deadlock-Free

  • If some thread calls lock()
    • And never acquires the lock
    • Then other threads must complete lock() and unlock() calls infinitely often
  • System as a whole makes progress
    • Even if individuals starve

Art of Multiprocessor Programming

148

149 of 159

Starvation-Free

  • If some thread calls lock()
    • It will eventually acquire the lock
  • Individual threads make progress

Art of Multiprocessor Programming

149

150 of 159

Lock-Free

  • Infinitely often, some method completes in a finite number of steps
  • System as a whole makes progress
    • Even if individuals starve

Art of Multiprocessor Programming

150

151 of 159

Wait-Free

  • Infinitely often, some method completes in a finite number of steps
  • Individual threads make progress

Art of Multiprocessor Programming

151

152 of 159

Progress Conditions

152

​

Blocking

Non-Blocking

One Thread Makes Progres

Deadlock-Free

Lock-free

All threads make progress

Starvation-free

Wait-Free

153 of 159

MyAtomicInt

public class MyAtomicInt {

Lock lock = new ReentrantLock();

volatile int value;

public MyAtomicInt() {}

public MyAtomicInt(int value) { this.value = value; }

public int get() { return value; }

public void set(int value) { this.value = value; }

public int getAndIncrement() {

try {

lock.lock();

return value++;

} finally {

lock.unlock(); } }

​

153

154 of 159

MyAtomicInt

  • Can’t deadlock!
  • Use is composable!
  • Hardware implementation exists!
  • getAndIncrement() can be wait free!
  • We’ll learn a lot more about the later.

154

155 of 159

How to know what’s what?

MyAtomicInt ai = new MyAtomicInt(0);

final int N = 10000;

final int N_THREADS = 10;

for (int i = 0; i < N_THREADS; i++) {

new Thread(() -> {

for (int j = 0; j < N; j++) {

ai.incrementAndGet();

}

}).start();

}

while (Thread.activeCount() > 2) { Thread.yield(); }

System.out.println(ai);

​

155

156 of 159

How to know what’s what?

MyAtomicInt ai = new MyAtomicInt(0);

final int N = 10000;

final int N_THREADS = 10;

for (int i = 0; i < N_THREADS; i++) {

new Thread(() -> {

for (int j = 0; j < N; j++) {

ai.incrementAndGet();

}

}).start();

}

while (Thread.activeCount() > 2) { Thread.yield(); }

System.out.println(ai);

​

156

Each thread is wait-free

|

|

Single instruction

157 of 159

How to know what’s what?

MyAtomicInt ai = new MyAtomicInt(0);

final int N = 10000;

final int N_THREADS = 10;

for (int i = 0; i < N_THREADS; i++) {

new Thread(() -> {

for (int j = 0; j < N; j++) {

ai.incrementAndGet();

}

}).start();

}

while (Thread.activeCount() > 2) { Thread.yield(); }

System.out.println(ai);

​

157

Whole code is lock-free

|

|

While loop usually means not wait free

158 of 159

Unfortunately...

package java.util.concurrent.atomic;

​

public class AtomicInteger extends Number implements java.io.Serializable {

….

public final int getAndIncrement() {

for (;;) {

int current = get();

int next = current + 1;

if (compareAndSet(current, next))

return current; } }

​

​

158

159 of 159

Art of Multiprocessor Programming

159

         �This work is licensed under a 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.

​