Principles of concurrent and distributed programming: algorithms and models

Content: Front Cover
Contents
Preface
Chapter 1: What is Concurrent Programming?
1.1: Introduction
1.2: Concurrency as abstract parallelism
1.3: Multitasking
1.4: The terminology of concurrency
1.5: Multiple computers
1.6: The challenge of concurrent programming
Transition
Chapter 2: The Concurrent Programming Abstraction
2.1: The role of abstraction
2.2: Concurrent execution as interleaving of atomic statements
States
Scenarios
2.3: Justification of the abstraction
Multitasking systems
Multiprocessor computers
Distributed systems
2.4: Arbitrary interleaving
2.5: Atomic statements. 2.6: CorrectnessLinear and branching temporal logics
2.7: Fairness
2.8: Machine-code instructions
Register machines
Stack machines
Source statements and machine instructions
2.9: Volatile and non-atomic variables
2.10: The BACI concurrency simulator
2.11: Concurrency in Ada
Volatile and atomic
2.12: Concurrency in Java
Volatile
2.13: Writing concurrent programs in Promela
2.14: Supplement: the state diagram for the frog puzzle
Transition
Exercises
Chapter 3: The Critical Section Problem
3.1: Introduction
3.2: The definition of the problem
3.3: First attempt. 3.4: Proving correctness with state diagramsStates
State diagrams
Abbreviating the state diagram
3.5: Correctness of the first attempt
3.6: Second attempt
3.7: Third attempt
3.8: Fourth attempt
3.9: Dekker's algorithm
3.10: Complex atomic statements
Transition
Exercises
Chapter 4: Verification of Concurrent Programs
4.1: Logical specification of correctness properties
4.2: Inductive proofs of invariants
Proof of mutual exclusion for the third attempt
4.3: Basic concepts of temporal logic
Always and eventually
Duality
Sequences of operators. 4.4: Advanced concepts of temporal logicUntil
Next
Deduction with temporal operators
Specifying overtaking
4.5: A deductive proof of Dekker's algorithm
Reasoning about progress
A proof of freedom from starvation
4.6: Model checking
4.7: Spin and the Promela modeling language
4.8: Correctness specifications in Spin
4.9: Choosing a verification technique
Transition
Exercises
Chapter 5: Advanced Algorithms for the Critical Section Problem
5.1: The bakery algorithm
5.2: The bakery algorithm for N processes
5.3: Less restrictive models of concurrency
5.4: Fast algorithms. Outline of the fast algorithmPartial proof of the algorithm
Generalization to N processes
5.5: Implementations in Promela
Transition
Exercises
Chapter 6: Semaphores
6.1: Process states
6.2: Definition of the semaphore type
6.3: The critical section problem for two processes
6.4: Semaphore invariants
6.5: The critical section problem for N processes
6.6: Order of execution problems
6.7: The producer-consumer problem
Infinite buffers
Bounded buffers
Split semaphores
6.8: Definitions of semaphores
Strong semaphores
Busy-wait semaphores
Abstract definitions of semaphores.