Contents

Preface xi

1 What is Concurrent Programming? 1

1.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1

1.2 Concurrency as abstract parallelism . . . . . . . . . . . . . . . . 2

1.3 Multitasking . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4

1.4 The terminology of concurrency . . . . . . . . . . . . . . . . . 4

1.5 Multiple computers . . . . . . . . . . . . . . . . . . . . . . . . 5

1.6 The challenge of concurrent programming . . . . . . . . . . . . 5

2 The Concurrent Programming Abstraction 7

2.1 The role of abstraction . . . . . . . . . . . . . . . . . . . . . . . 7

2.2 Concurrent execution as interleaving of atomic statements . . . . 8

2.3 Justification of the abstraction . . . . . . . . . . . . . . . . . . . 13

2.4 Arbitrary interleaving . . . . . . . . . . . . . . . . . . . . . . . 17

2.5 Atomic statements . . . . . . . . . . . . . . . . . . . . . . . . . 19

2.6 Correctness . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21

2.7 Fairness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23

2.8 Machine-code instructions . . . . . . . . . . . . . . . . . . . . . 24

2.9 Volatile and non-atomic variables . . . . . . . . . . . . . . . . . 28

2.10 The BACI concurrency simulator . . . . . . . . . . . . . . . . . 29

2.11 Concurrency in Ada . . . . . . . . . . . . . . . . . . . . . . . . 31

2.12 Concurrency in Java . . . . . . . . . . . . . . . . . . . . . . . . 34

2.13 Writing concurrent programs in Promela . . . . . . . . . . . . . 36

2.14 Supplement: the state diagram for the frog puzzle . . . . . . . . 37

3 The Critical Section Problem 45

3.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45

3.2 The definition of the problem . . . . . . . . . . . . . . . . . . . 45

3.3 First attempt . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48

3.4 Proving correctness with state diagrams . . . . . . . . . . . . . . 49

3.5 Correctness of the first attempt . . . . . . . . . . . . . . . . . . 53

3.6 Second attempt . . . . . . . . . . . . . . . . . . . . . . . . . . . 55

3.7 Third attempt . . . . . . . . . . . . . . . . . . . . . . . . . . . 57

3.8 Fourth attempt . . . . . . . . . . . . . . . . . . . . . . . . . . . 58

3.9 Dekker's algorithm . . . . . . . . . . . . . . . . . . . . . . . . 60

3.10 Complex atomic statements . . . . . . . . . . . . . . . . . . . . 61

4 Verification of Concurrent Programs 67

4.1 Logical specification of correctness properties . . . . . . . . . . 68

4.2 Inductive proofs of invariants . . . . . . . . . . . . . . . . . . . 69

4.3 Basic concepts of temporal logic . . . . . . . . . . . . . . . . . 72

4.4 Advanced concepts of temporal logic . . . . . . . . . . . . . . . 75

4.5 A deductive proof of Dekker's algorithm . . . . . . . . . . . . . 79

4.6 Model checking . . . . . . . . . . . . . . . . . . . . . . . . . . 83

4.7 Spin and the Promela modeling language . . . . . . . . . . . . . 83

4.8 Correctness specifications in Spin . . . . . . . . . . . . . . . . . 86

4.9 Choosing a verification technique . . . . . . . . . . . . . . . . . 88

5 Advanced Algorithms for the Critical Section Problem 93

5.1 The bakery algorithm . . . . . . . . . . . . . . . . . . . . . . . 93

5.2 The bakery algorithm for N processes . . . . . . . . . . . . . . 95

5.3 Less restrictive models of concurrency . . . . . . . . . . . . . . 96

5.4 Fast algorithms . . . . . . . . . . . . . . . . . . . . . . . . . . . 97

5.5 Implementations in Promela . . . . . . . . . . . . . . . . . . . . 104