| |
| |
| Preface | |
| |
| |
| |
| What is Concurrent Programming? | |
| |
| |
| |
| Introduction | |
| |
| |
| |
| Concurrency as abstract parallelism | |
| |
| |
| |
| Multitasking | |
| |
| |
| |
| The terminology of concurrency | |
| |
| |
| |
| Multiple computers | |
| |
| |
| |
| The challenge of concurrent programming | |
| |
| |
| |
| The Concurrent Programming Abstraction | |
| |
| |
| |
| The role of abstraction | |
| |
| |
| |
| Concurrent execution as interleaving of atomic statements | |
| |
| |
| |
| Justification of the abstraction | |
| |
| |
| |
| Arbitrary interleaving | |
| |
| |
| |
| Atomic statements | |
| |
| |
| |
| Correctness | |
| |
| |
| |
| Fairness | |
| |
| |
| |
| Machine-code instructions | |
| |
| |
| |
| Volatile and non-atomic variables | |
| |
| |
| |
| The BACI concurrency simulator | |
| |
| |
| |
| Concurrency in Ada | |
| |
| |
| |
| Concurrency in Java | |
| |
| |
| |
| Writing concurrent programs in Promela | |
| |
| |
| |
| Supplement: the state diagram for the frog puzzle | |
| |
| |
| |
| The Critical Section Problem | |
| |
| |
| |
| Introduction | |
| |
| |
| |
| The definition of the problem | |
| |
| |
| |
| First attempt | |
| |
| |
| |
| Proving correctness with state diagrams | |
| |
| |
| |
| Correctness of the first attempt | |
| |
| |
| |
| Second attempt | |
| |
| |
| |
| Third attempt | |
| |
| |
| |
| Fourth attempt | |
| |
| |
| |
| Dekker's algorithm | |
| |
| |
| |
| Complex atomic statements | |
| |
| |
| |
| Verification of Concurrent Programs | |
| |
| |
| |
| Logical specification of correctness properties | |
| |
| |
| |
| Inductive proofs of invariants | |
| |
| |
| |
| Basic concepts of temporal logic | |
| |
| |
| |
| Advanced concepts of temporal logic | |
| |
| |
| |
| A deductive proof of Dekker's algorithm | |
| |
| |
| |
| Model checking | |
| |
| |
| |
| Spin and the Promela modeling language | |
| |
| |
| |
| Correctness specifications in Spin | |
| |
| |
| |
| Choosing a verification technique | |
| |
| |
| |
| Advanced Algorithms for the Critical Section Problem | |
| |
| |
| |
| The bakery algorithm | |
| |
| |
| |
| The bakery algorithm for N processes | |
| |
| |
| |
| Less restrictive models of concurrency | |
| |
| |
| |
| Fast algorithms | |
| |
| |
| |
| Implementations in Promela | |
| |
| |
| |
| Semaphores | |
| |
| |
| |
| Process states | |
| |
| |
| |
| Definition of the semaphore type | |
| |
| |
| |
| The critical section problem for two processes | |
| |
| |
| |
| Semaphore invariants | |
| |
| |
| |
| The critical section problem for N processes | |
| |
| |
| |
| Order of execution problems | |
| |
| |
| |
| The producer-consumer problem | |
| |
| |
| |
| Definitions of semaphores | |
| |
| |
| |
| The problem of the dining philosophers | |
| |
| |
| |
| Barz's simulation of general semaphores | |
| |
| |
| |
| Udding's starvation-free algorithm | |
| |
| |
| |
| Semaphores in BACI | |
| |
| |
| |
| Semaphores in Ada | |
| |
| |
| |
| Semaphores in Java | |
| |
| |
| |
| Semaphores in Promela | |
| |
| |
| |
| Monitors | |
| |
| |
| |
| Introduction | |
| |
| |
| |
| Declaring and using monitors | |
| |
| |
| |
| Condition variables | |
| |
| |
| |
| The producer-consumer problem | |
| |
| |
| |
| The immediate resumption requirement | |
| |
| |
| |
| The problem of the readers and writers | |
| |
| |
| |
| Correctness of the readers and writers algorithm | |
| |
| |
| |
| A monitor solution for the dining philosophers | |
| |
| |
| |
| Monitors in BACI | |
| |
| |
| |
| Protected objects | |
| |
| |
| |
| Monitors in Java | |
| |
| |
| |
| Simulating monitors in Promela | |
| |
| |
| |
| Channels | |
| |
| |
| |
| Models for communications | |
| |
| |
| |
| Channels | |
| |
| |
| |
| Parallel matrix multiplication | |
| |
| |
| |
| The dining philosophers with channels | |
| |
| |
| |
| Channels in Promela | |
| |
| |
| |
| Rendezvous | |
| |
| |
| |
| Remote procedure calls | |
| |
| |
| |
| Spaces | |
| |
| |
| |
| The Linda model | |
| |
| |
| |
| Expressiveness of the Linda model | |
| |
| |
| |
| Formal parameters | |
| |
| |
| |
| The master-worker paradigm | |
| |
| |
| |
| Implementations of spaces | |
| |
| |
| |
| Distributed Algorithms | |
| |
| |
| |
| The distributed systems model | |
| |
| |
| |
| Implementations | |
| |
| |
| |
| Distributed mutual exclusion | |
| |
| |
| |
| Correctness of the Ricart-Agrawala algorithm | |
| |
| |
| |
| The RA algorithm in Promela | |
| |
| |
| |
| Token-passing algorithms | |
| |
| |
| |
| Tokens in virtual trees | |
| |
| |
| |
| Global Properties | |
| |
| |
| |
| Distributed termination | |
| |
| |
| |
| The Dijkstra-Scholten algorithm | |
| |
| |
| |
| Credit-recovery algorithms | |
| |
| |
| |
| Snapshots | |
| |
| |
| |
| Consensus | |
| |
| |
| |
| Introduction | |
| |
| |
| |
| The problem statement | |
| |
| |
| |
| A one-round algorithm | |
| |
| |
| |
| The Byzantine Generals algorithm | |
| |
| |
| |
| Crash failures | |
| |
| |
| |
| Knowledge trees | |
| |
| |
| |
| Byzantine failures with three generals | |
| |
| |
| |
| Byzantine failures with four generals | |
| |
| |
| |
| The flooding algorithm | |
| |
| |
| |
| The King algorithm | |
| |
| |
| |
| Impossibility with three generals | |
| |
| |
| |
| Real-Time Systems | |
| |
| |
| |
| Introduction | |
| |
| |
| |
| Definitions | |
| |
| |
| |
| Reliability and repeatability | |
| |
| |
| |
| Synchronous systems | |
| |
| |
| |
| Asynchronous systems | |
| |
| |
| |
| Interrupt-driven systems | |
| |
| |
| |
| Priority inversion and priority inheritance | |
| |
| |
| |
| The Mars Pathfinder in Spin | |
| |
| |
| |
| Simpson's four-slot algorithm | |
| |
| |
| |
| The Ravenscar profile | |
| |
| |
| |
| UPPAAL | |
| |
| |
| |
| Scheduling algorithms for real-time systems | |
| |
| |
| |
| The Pseudocode Notation | |
| |
| |
| |
| Review of Mathematical Logic | |
| |
| |
| |
| The propositional calculus | |
| |
| |
| |
| Induction | |
| |
| |
| |
| Proof methods | |
| |
| |
| |
| Correctness of sequential programs | |
| |
| |
| |
| Concurrent Programming Problems | |
| |
| |
| |
| Software Tools | |
| |
| |
| |
| BACI and jBACI | |
| |
| |
| |
| Spin and jSpin | |
| |
| |
| |
| DAJ | |
| |
| |
| |
| Further Reading | |
| |
| |
| Bibliography | |
| |
| |
| Index | |