Additional Information
Book Details
Abstract
Principles of Concurrent and Distributed Programming provides an introduction to concurrent programming focusing on general principles and not on specific systems.
Software today is inherently concurrent or distributed – from event-based GUI designs to operating and real-time systems to Internet applications. The new edition of this classic introduction to concurrency has been completely revised in view of the growing importance of concurrency constructs embedded in programming languages and of formal methods such as model checking that are widely used in industry.
Table of Contents
| Section Title | Page | Action | Price |
|---|---|---|---|
| Front Cover | Front Cover | ||
| Contents | v | ||
| Preface | xi | ||
| Chapter 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 | ||
| Transition | 6 | ||
| Chapter 2: The Concurrent Programming Abstraction | 7 | ||
| 2.1: The role of abstraction | 7 | ||
| 2.2: Concurrent execution as interleaving of atomic statements | 8 | ||
| States | 10 | ||
| Scenarios | 12 | ||
| 2.3: Justification of the abstraction | 13 | ||
| Multitasking systems | 14 | ||
| Multiprocessor computers | 15 | ||
| Distributed systems | 16 | ||
| 2.4: Arbitrary interleaving | 17 | ||
| 2.5: Atomic statements | 19 | ||
| 2.6: Correctness | 21 | ||
| Linear and branching temporal logics | 22 | ||
| 2.7: Fairness | 23 | ||
| 2.8: Machine-code instructions | 24 | ||
| Register machines | 24 | ||
| Stack machines | 25 | ||
| Source statements and machine instructions | 27 | ||
| 2.9: Volatile and non-atomic variables | 28 | ||
| 2.10: The BACI concurrency simulator | 29 | ||
| 2.11: Concurrency in Ada | 31 | ||
| Volatile and atomic | 33 | ||
| 2.12: Concurrency in Java | 34 | ||
| Volatile | 35 | ||
| 2.13: Writing concurrent programs in Promela | 36 | ||
| 2.14: Supplement: the state diagram for the frog puzzle | 37 | ||
| Transition | 39 | ||
| Exercises | 39 | ||
| Chapter 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 | ||
| States | 49 | ||
| State diagrams | 50 | ||
| Abbreviating the state diagram | 53 | ||
| 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 | ||
| Transition | 63 | ||
| Exercises | 63 | ||
| Chapter 4: Verification of Concurrent Programs | 67 | ||
| 4.1: Logical specification of correctness properties | 68 | ||
| 4.2: Inductive proofs of invariants | 69 | ||
| Proof of mutual exclusion for the third attempt | 70 | ||
| 4.3: Basic concepts of temporal logic | 72 | ||
| Always and eventually | 72 | ||
| Duality | 74 | ||
| Sequences of operators | 74 | ||
| 4.4: Advanced concepts of temporal logic | 75 | ||
| Until | 75 | ||
| Next | 76 | ||
| Deduction with temporal operators | 77 | ||
| Specifying overtaking | 78 | ||
| 4.5: A deductive proof of Dekker’s algorithm | 79 | ||
| Reasoning about progress | 80 | ||
| A proof of freedom from starvation | 82 | ||
| 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 | ||
| Transition | 90 | ||
| Exercises | 90 | ||
| Chapter 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 | ||
| Outline of the fast algorithm | 98 | ||
| Partial proof of the algorithm | 101 | ||
| Generalization to N processes | 104 | ||
| 5.5: Implementations in Promela | 104 | ||
| Transition | 104 | ||
| Exercises | 105 | ||
| Chapter 6: Semaphores | 107 | ||
| 6.1: Process states | 107 | ||
| 6.2: Definition of the semaphore type | 109 | ||
| 6.3: The critical section problem for two processes | 110 | ||
| 6.4: Semaphore invariants | 112 | ||
| 6.5: The critical section problem for N processes | 113 | ||
| 6.6: Order of execution problems | 114 | ||
| 6.7: The producer–consumer problem | 115 | ||
| Infinite buffers | 117 | ||
| Bounded buffers | 118 | ||
| Split semaphores | 119 | ||
| 6.8: Definitions of semaphores | 119 | ||
| Strong semaphores | 120 | ||
| Busy-wait semaphores | 120 | ||
| Abstract definitions of semaphores | 121 | ||
| 6.9: The problem of the dining philosophers | 122 | ||
| 6.10: Barz’s simulation of general semaphores | 126 | ||
| 6.11: Udding’s starvation-free algorithm | 129 | ||
| 6.12: Semaphores in BACI | 131 | ||
| 6.13: Semaphores in Ada | 132 | ||
| 6.14: Semaphores in Java | 133 | ||
| 6.15: Semaphores in Promela | 134 | ||
| Proving Barz’s algorithm in Spin | 136 | ||
| Transition | 136 | ||
| Exercises | 138 | ||
| Chapter 7: Monitors | 145 | ||
| 7.1: Introduction | 145 | ||
| 7.2: Declaring and using monitors | 146 | ||
| 7.3: Condition variables | 147 | ||
| Simulating semaphores | 148 | ||
| Operations on condition variables | 149 | ||
| Correctness of the semaphore simulation | 150 | ||
| 7.4: The producer–consumer problem | 151 | ||
| 7.5: The immediate resumption requirement | 152 | ||
| 7.6: The problem of the readers and writers | 154 | ||
| 7.7: Correctness of the readers and writers algorithm | 157 | ||
| 7.8: A monitor solution for the dining philosophers | 160 | ||
| 7.9: Monitors in BACI | 162 | ||
| 7.10: Protected objects | 162 | ||
| Protected objects in Ada | 166 | ||
| 7.11: Monitors in Java | 167 | ||
| Synchronized blocks | 172 | ||
| 7.12: Simulating monitors in Promela | 173 | ||
| Transition | 175 | ||
| Exercises | 176 | ||
| Chapter 8: Channels | 179 | ||
| 8.1: Models for communications | 179 | ||
| Synchronous vs. asynchronous communications | 179 | ||
| Addressing | 180 | ||
| Data flow | 181 | ||
| CSP and occam | 181 | ||
| 8.2: Channels | 181 | ||
| 8.3: Parallel matrix multiplication | 183 | ||
| Selective input | 186 | ||
| 8.4: The dining philosophers with channels | 187 | ||
| 8.5: Channels in Promela | 188 | ||
| 8.6: Rendezvous | 190 | ||
| The rendezvous in Ada | 191 | ||
| 8.7: Remote procedure calls | 193 | ||
| Transition | 194 | ||
| Exercises | 195 | ||
| Chapter 9: Spaces | 197 | ||
| 9.1: The Linda model | 197 | ||
| 9.2: Expressiveness of the Linda model | 199 | ||
| 9.3: Formal parameters | 200 | ||
| 9.4: The master–worker paradigm | 202 | ||
| Granularity | 203 | ||
| 9.5: Implementations of spaces | 204 | ||
| C-Linda | 205 | ||
| JavaSpaces | 205 | ||
| Java | 206 | ||
| Promela | 208 | ||
| Transition | 209 | ||
| Exercises | 209 | ||
| Chapter 10: Distributed Algorithms | 211 | ||
| 10.1: The distributed systems model | 211 | ||
| Communications channels | 212 | ||
| Sending and receiving messages | 212 | ||
| Concurrency within the nodes | 214 | ||
| Studying distributed algorithms | 214 | ||
| 10.2: Implementations | 215 | ||
| 10.3: Distributed mutual exclusion | 216 | ||
| Initial development of the algorithm | 216 | ||
| The scenario of an example | 218 | ||
| Equal ticket numbers | 220 | ||
| Choosing ticket numbers | 220 | ||
| Quiescent nodes | 221 | ||
| 10.4: Correctness of the Ricart–Agrawala algorithm | 223 | ||
| 10.5: The RA algorithm in Promela | 225 | ||
| 10.6: Token-passing algorithms | 227 | ||
| 10.7: Tokens in virtual trees | 230 | ||
| Transition | 233 | ||
| Exercises | 234 | ||
| Chapter 11: Global Properties | 237 | ||
| 11.1: Distributed termination | 237 | ||
| Preliminary algorithm | 239 | ||
| Correctness of the preliminary algorithm | 240 | ||
| 11.2: The Dijkstra–Scholten algorithm | 243 | ||
| Correctness of the Dijkstra–Scholten algorithm | 246 | ||
| Performance | 247 | ||
| 11.3: Credit-recovery algorithms | 248 | ||
| 11.4: Snapshots | 250 | ||
| Correctness of the Chandy–Lamport algorithm | 254 | ||
| Transition | 255 | ||
| Exercises | 256 | ||
| Chapter 12: Consensus | 257 | ||
| 12.1: Introduction | 257 | ||
| 12.2: The problem statement | 258 | ||
| 12.3: A one-round algorithm | 260 | ||
| 12.4: The Byzantine Generals algorithm | 261 | ||
| 12.5: Crash failures | 263 | ||
| 12.6: Knowledge trees | 264 | ||
| 12.7: Byzantine failures with three generals | 266 | ||
| 12.8: Byzantine failures with four generals | 268 | ||
| Correctness | 269 | ||
| Complexity | 270 | ||
| 12.9: The flooding algorithm | 271 | ||
| 12.10: The King algorithm | 274 | ||
| Correctness | 279 | ||
| Complexity | 279 | ||
| 12.11: Impossibility with three generals | 280 | ||
| Transition | 281 | ||
| Exercises | 282 | ||
| Chapter 13: Real-Time Systems | 285 | ||
| 13.1: Introduction | 285 | ||
| The Ada Real-Time Annex | 287 | ||
| 13.2: Definitions | 287 | ||
| 13.3: Reliability and repeatability | 288 | ||
| The Ariane 5 rocket | 288 | ||
| The space shuttle | 290 | ||
| 13.4: Synchronous systems | 290 | ||
| 13.5: Asynchronous systems | 293 | ||
| Priorities and preemptive scheduling | 294 | ||
| 13.6: Interrupt-driven systems | 297 | ||
| Interrupt overflow in the Apollo 11 lunar module | 298 | ||
| 13.7: Priority inversion and priority inheritance | 299 | ||
| Priority inheritance | 301 | ||
| Priority inversion from queues | 302 | ||
| Priority ceiling locking | 302 | ||
| The Mars Pathfinder | 302 | ||
| 13.8: The Mars Pathfinder in Spin | 303 | ||
| 13.9: Simpson’s four-slot algorithm | 306 | ||
| 13.10: The Ravenscar profile | 309 | ||
| Suspension objects | 310 | ||
| 13.11: UPPAAL | 311 | ||
| 13.12: Scheduling algorithms for real-time systems | 312 | ||
| The rate monotonic algorithm | 313 | ||
| The earliest deadline first algorithm | 313 | ||
| Transition | 313 | ||
| Exercises | 314 | ||
| A: The Pseudocode Notation | 317 | ||
| Structure | 317 | ||
| Syntax | 317 | ||
| Semantics | 318 | ||
| Synchronization constructs | 319 | ||
| B: Review of Mathematical Logic | 321 | ||
| B.1: The propositional calculus | 321 | ||
| Syntax | 321 | ||
| Semantics | 322 | ||
| Logical equivalence | 323 | ||
| B.2: Induction | 323 | ||
| B.3: Proof methods | 324 | ||
| Model checking | 324 | ||
| Deductive proof | 325 | ||
| Material implication | 325 | ||
| B.4: Correctness of sequential programs | 326 | ||
| Verification in SPARK | 328 | ||
| C: Concurrent Programming Problems | 331 | ||
| D: Software Tools | 339 | ||
| D.1: BACI and jBACI | 339 | ||
| D.2: Spin and jSpin | 341 | ||
| The jSpin user interface | 342 | ||
| How Spin verifies properties | 343 | ||
| D.3: DAJ | 345 | ||
| E: Further Reading | 349 | ||
| Websites | 350 | ||
| Bibliography | 351 | ||
| Index | 355 | ||
| Back Cover | Back Cover |