Principles of concurrent and distributed programming: algorithms and models

Preface 5
1 What is Concurrent Programming? 11
 1.1 Introduction 11
 1.2 Concurrency as abstract parallelism 12
 1.3 Multitasking 14
 1.4 The terminology of concurrency 14
 1.5 Multiple computers 15
 1.6 The challenge of concurrent programming 15
2 The Concurrent Programming Abstraction 17
 2.1 The role of abstraction 17
 2.2 Concurrent execution as interleaving of atomic statements 18
 2.3 Justification of the abstraction 23
 2.4 Arbitrary interleaving 27
 2.5 Atomic statements 29
 2.6 Correctness 31
 2.7 Fairness 33
 2.8 Machine-code instructions 34
 2.9 Volatile and non-atomic variables 38
 2.10 The BACI concurrency simulator 39
 2.11 Concurrency in Ada 41
 2.12 Concurrency in Java 44
 2.13 Writing concurrent programs in Promela 46
 2.14 Supplement: the state diagram for the frog puzzle 47
3 The Critical Section Problem 55
 3.1 Introduction 55
 3.2 The definition of the problem 55
 3.3 First attempt 58
 3.4 Proving correctness with state diagrams 59
 3.5 Correctness of the first attempt 63
 3.6 Second attempt 65
 3.7 Third attempt 67
 3.8 Fourth attempt 68
 3.9 Dekker’s algorithm 70
 3.10 Complex atomic statements 71
4 Verification of Concurrent Programs 77
 4.1 Logical specification of correctness properties 78
 4.2 Inductive proofs of invariants 79
 4.3 Basic concepts of temporal logic 82
 4.4 Advanced concepts of temporal logic 85
 4.5 A deductive proof of Dekker’s algorithm 89
 4.6 Model checking 93
 4.7 Spin and the Promela modeling language 93
 4.8 Correctness specifications in Spin 96
 4.9 Choosing a verification technique 98
5 Advanced Algorithms for the Critical Section Problem 103
 5.1 The bakery algorithm 103
 5.2 The bakery algorithm for N processes 105
 5.3 Less restrictive models of concurrency 106
 5.4 Fast algorithms 107
 5.5 Implementations in Promela 114
6 Semaphores 117
 6.1 Process states 117
 6.2 Definition of the semaphore type 119
 6.3 The critical section problem for two processes 120
 6.4 Semaphore invariants 122
 6.5 The critical section problem for N processes 123
 6.6 Order of execution problems 124
 6.7 The producer–consumer problem 125
 6.8 Definitions of semaphores 129
 6.9 The problem of the dining philosophers 132
 6.10 Barz’s simulation of general semaphores 136
 6.11 Udding’s starvation-free algorithm 139
 6.12 Semaphores in BACI 141
 6.13 Semaphores in Ada 142
 6.14 Semaphores in Java 143
 6.15 Semaphores in Promela 144
7 Monitors 155
 7.1 Introduction 155
 7.2 Declaring and using monitors 156
 7.3 Condition variables 157
 7.4 The producer–consumer problem 161
 7.5 The immediate resumption requirement 162
 7.6 The problem of the readers and writers 164
 7.7 Correctness of the readers and writers algorithm 167
 7.8 A monitor solution for the dining philosophers 170
 7.9 Monitors in BACI 172
 7.10 Protected objects 172
 7.11 Monitors in Java 177
 7.12 Simulating monitors in Promela 183
8 Channels 189
 8.1 Models for communications 189
 8.2 Channels 191
 8.3 Parallel matrix multiplication 193
 8.4 The dining philosophers with channels 197
 8.5 Channels in Promela 198
 8.6 Rendezvous 200
 8.7 Remote procedure calls 203
9 Spaces 207
 9.1 The Linda model 207
 9.2 Expressiveness of the Linda model 209
 9.3 Formal parameters 210
 9.4 The master–worker paradigm 212
 9.5 Implementations of spaces 214
10 Distributed Algorithms 221
 10.1 The distributed systems model 221
 10.2 Implementations 225
 10.3 Distributed mutual exclusion 226
 10.4 Correctness of the Ricart–Agrawala algorithm 233
 10.5 The RA algorithm in Promela 235
 10.6 Token-passing algorithms 237
 10.7 Tokens in virtual trees 240
11 Global Properties 247
 11.1 Distributed termination 247
 11.2 The Dijkstra–Scholten algorithm 253
 11.3 Credit-recovery algorithms 258
 11.4 Snapshots 260
12 Consensus 267
 12.1 Introduction 267
 12.2 The problem statement 268
 12.3 A one-round algorithm 270
 12.4 The Byzantine Generals algorithm 271
 12.5 Crash failures 273
 12.6 Knowledge trees 274
 12.7 Byzantine failures with three generals 276
 12.8 Byzantine failures with four generals 278
 12.9 The flooding algorithm 281
 12.10 The King algorithm 284
 12.11 Impossibility with three generals 290
13 Real-Time Systems 295
 13.1 Introduction 295
 13.2 Definitions 297
 13.3 Reliability and repeatability 298
 13.4 Synchronous systems 300
 13.5 Asynchronous systems 303
 13.6 Interrupt-driven systems 307
 13.7 Priority inversion and priority inheritance 309
 13.8 The Mars Pathfinder in Spin 313
 13.9 Simpson’s four-slot algorithm 316
 13.10 The Ravenscar profile 319
 13.11 UPPAAL 321
 13.12 Scheduling algorithms for real-time systems 322
A The Pseudocode Notation 327
B Review of Mathematical Logic 331
 B.1 The propositional calculus 331
 B.2 Induction 333
 B.3 Proof methods 334
 B.4 Correctness of sequential programs 336
C Concurrent Programming Problems 341
D Software Tools 349
 D.1 BACI and jBACI 349
 D.2 Spin and jSpin 351
 D.3 DAJ 355
E Further Reading 359
Bibliography 361
Index 365