Principles of Concurrent and Distributed Programming, Second Edition

Principles of Concurrent and Distributed Programming, Second Edition

Released February 2006
Publisher(s): Addison-Wesley Professional
ISBN: 9780321312839

Read it now on the O’Reilly learning platform with a 10-day free trial.

O’Reilly members get unlimited access to books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.

Start your free trial

Book description

The latest edition of a classic text on concurrency and distributed programming – from a winner of the ACM/SIGCSE Award for Outstanding Contribution to Computer Science Education.

Table of contents

  1. Copyright
  2.  
  3.  
  4. Preface
  5. 1. What is Concurrent Programming?
    1. 1.1. Introduction
    2. 1.2. Concurrency as Abstract Parallelism
    3. 1.3. Multitasking
    4. 1.4. The Terminology of Concurrency
    5. 1.5. Multiple Computers
    6. 1.6. The Challenge of Concurrent Programming
      1. Transition
  6. 2. The Concurrent Programming Abstraction
    1. 2.1. The Role of Abstraction
    2. 2.2. Concurrent Execution as Interleaving of Atomic Statements
      1. States
      2. Scenarios
    3. 2.3. Justification of the Abstraction
      1. Multitasking Systems
      2. Multiprocessor Computers
      3. Distributed Systems
    4. 2.4. Arbitrary Interleaving
    5. 2.5. Atomic Statements
    6. 2.6. Correctness
      1. Linear and Branching Temporal LogicsA
    7. 2.7. Fairness
    8. 2.8. Machine-Code InstructionsA
      1. Register Machines
      2. Stack Machines
      3. Source Statements and Machine Instructions
    9. 2.9. Volatile and Non-Atomic VariablesA
    10. 2.10. The BACI Concurrency SimulatorL
    11. 2.11. Concurrency in AdaL
      1. Volatile and Atomic
    12. 2.12. Concurrency in JavaL
      1. Volatile
    13. 2.13. Writing Concurrent Programs in PromelaL
    14. 2.14. Supplement: The State Diagram for the Frog Puzzle
      1. Transition
      2. Exercises
  7. 3. The Critical Section Problem
    1. 3.1. Introduction
    2. 3.2. The Definition of the Problem
    3. 3.3. First Attempt
    4. 3.4. Proving Correctness with State Diagrams
      1. States
      2. State Diagrams
      3. Abbreviating the State Diagram
    5. 3.5. Correctness of the First Attempt
    6. 3.6. Second Attempt
    7. 3.7. Third Attempt
    8. 3.8. Fourth Attempt
    9. 3.9. Dekker’s Algorithm
    10. 3.10. Complex Atomic Statements
      1. Transition
      2. Exercises
  8. 4. Verification of Concurrent Programs
    1. 4.1. Logical Specification of Correctness Properties
    2. 4.2. Inductive Proofs of Invariants
      1. Proof of Mutual Exclusion for the Third Attempt
    3. 4.3. Basic Concepts of Temporal Logic
      1. Always and Eventually
      2. Duality
      3. Sequences of Operators
    4. 4.4. Advanced Concepts of Temporal LogicA
      1. Until
      2. Next
      3. Deduction with Temporal Operators
      4. Specifying Overtaking
    5. 4.5. A Deductive Proof of Dekker’s AlgorithmA
      1. Reasoning About Progress
      2. A Proof of Freedom From Starvation
    6. 4.6. Model Checking
    7. 4.7. Spin and the Promela Modeling LanguageL
    8. 4.8. Correctness Specifications in SpinL
    9. 4.9. Choosing a Verification TechniqueA
      1. Transition
      2. Exercises
  9. 5. Advanced Algorithms for the Critical Section ProblemA
    1. 5.1. The Bakery Algorithm
    2. 5.2. The Bakery Algorithm for N Processes
    3. 5.3. Less Restrictive Models of Concurrency
    4. 5.4. Fast Algorithms
      1. Outline of the Fast Algorithm
      2. Partial Proof of the Algorithm
      3. Generalization to N Processes
    5. 5.5. Implementations in PromelaL
      1. Transition
      2. Exercises
  10. 6. Semaphores
    1. 6.1. Process States
    2. 6.2. Definition of the Semaphore Type
    3. 6.3. The Critical Section Problem for Two Processes
    4. 6.4. Semaphore Invariants
    5. 6.5. The Critical Section Problem for N Processes
    6. 6.6. Order of Execution Problems
    7. 6.7. The Producer–Consumer Problem
      1. Infinite Buffers
      2. Bounded Buffers
      3. Split Semaphores
    8. 6.8. Definitions of Semaphores
      1. Strong Semaphores
      2. Busy-Wait Semaphores
      3. Abstract Definitions of SemaphoresA
    9. 6.9. The Problem of the Dining Philosophers
    10. 6.10. Barz’s Simulation of General SemaphoresA
    11. 6.11. Udding’s Starvation-Free AlgorithmA
    12. 6.12. Semaphores in BACIL
    13. 6.13. Semaphores in AdaL
    14. 6.14. Semaphores in JavaL
    15. 6.15. Semaphores in PromelaL
      1. Proving Barz’s Algorithm in SpinA
      2. Transition
      3. Exercises
  11. 7. Monitors
    1. 7.1. Introduction
    2. 7.2. Declaring and Using Monitors
    3. 7.3. Condition Variables
      1. Simulating Semaphores
      2. Operations on Condition Variables
      3. Correctness of the Semaphore Simulation
    4. 7.4. The Producer–Consumer Problem
    5. 7.5. The Immediate Resumption Requirement
    6. 7.6. The Problem of the Readers and Writers
    7. 7.7. Correctness of the Readers and Writers AlgorithmA
    8. 7.8. A Monitor Solution for the Dining Philosophers
    9. 7.9. Monitors in BACIL
    10. 7.10. Protected Objects
      1. Protected Objects in AdaL
    11. 7.11. Monitors in JavaL
      1. Synchronized Blocks
    12. 7.12. Simulating Monitors in PromelaL
      1. Transition
      2. Exercises
  12. 8. Channels
    1. 8.1. Models for Communications
      1. Synchronous vs. Asynchronous Communications
      2. Addressing
      3. Data Flow
      4. CSP and Occam
    2. 8.2. Channels
    3. 8.3. Parallel Matrix Multiplication
      1. Selective Input
    4. 8.4. The Dining Philosophers with Channels
    5. 8.5. Channels in PromelaL
    6. 8.6. Rendezvous
      1. The Rendezvous in AdaL
    7. 8.7. Remote Procedure CallsA
      1. Transition
      2. Exercises
  13. 9. Spaces
    1. 9.1. The Linda Model
    2. 9.2. Expressiveness of the Linda Model
    3. 9.3. Formal Parameters
    4. 9.4. The Master–Worker Paradigm
      1. Granularity
    5. 9.5. Implementations of SpacesL
      1. C-Linda
      2. JavaSpaces
      3. Java
      4. Promela
      5. Transition
      6. Exercises
  14. 10. Distributed Algorithms
    1. 10.1. The Distributed Systems Model
      1. Communications Channels
      2. Sending and Receiving Messages
      3. Concurrency within the Nodes
      4. Studying Distributed Algorithms
    2. 10.2. Implementations
    3. 10.3. Distributed Mutual Exclusion
      1. Initial Development of the Algorithm
      2. The Scenario of an Example
      3. Equal Ticket Numbers
      4. Choosing Ticket Numbers
      5. Quiescent Nodes
    4. 10.4. Correctness of the Ricart–Agrawala Algorithm
    5. 10.5. The RA Algorithm in PromelaL
    6. 10.6. Token-Passing Algorithms
    7. 10.7. Tokens in Virtual TreesA
      1. Transition
      2. Exercises
        1. Ricart–Agrawala
        2. Ricart–Agrawala Token-Passing Algorithm
        3. Neilsen–Mizuno Algorithm
  15. 11. Global Properties
    1. 11.1. Distributed Termination
      1. Preliminary Algorithm
      2. Correctness of the Preliminary Algorithm
    2. 11.2. The Dijkstra–Scholten Algorithm
      1. Correctness of the Dijkstra–Scholten Algorithm
      2. Performance
    3. 11.3. Credit-Recovery Algorithms
    4. 11.4. Snapshots
      1. Correctness of the Chandy–Lamport Algorithm
      2. Transition
      3. Exercises
        1. Dijkstra–Scholten
        2. Credit-Recovery
        3. Chandy–Lamport
  16. 12. Consensus
    1. 12.1. Introduction
    2. 12.2. The Problem Statement
    3. 12.3. A One-Round Algorithm
    4. 12.4. The Byzantine Generals Algorithm
    5. 12.5. Crash Failures
    6. 12.6. Knowledge Trees
    7. 12.7. Byzantine Failures with Three Generals
    8. 12.8. Byzantine Failures with Four Generals
      1. Correctness
      2. Complexity
    9. 12.9. The Flooding Algorithm
    10. 12.10. The King Algorithm
      1. Correctness
      2. Complexity
    11. 12.11. Impossibility with Three GeneralsA
      1. Transition
      2. Exercises
  17. 13. Real-Time Systems
    1. 13.1. Introduction
      1. The Ada Real-Time AnnexL
    2. 13.2. Definitions
    3. 13.3. Reliability and Repeatability
      1. The Ariane 5 Rocket
      2. The Space Shuttle
    4. 13.4. Synchronous Systems
    5. 13.5. Asynchronous Systems
      1. Priorities and Preemptive Scheduling
    6. 13.6. Interrupt-Driven Systems
      1. Interrupt Overflow in the Apollo 11 Lunar Module
    7. 13.7. Priority Inversion and Priority Inheritance
      1. Priority Inheritance
      2. Priority Inversion from Queues
      3. Priority Ceiling Locking
      4. The Mars Pathfinder
    8. 13.8. The Mars Pathfinder in SpinL
    9. 13.9. Simpson’s Four-Slot AlgorithmA
    10. 13.10. The Ravenscar ProfileL
      1. Suspension Objects
    11. 13.11. UPPAALL
    12. 13.12. Scheduling Algorithms for Real-Time Systems
      1. The Rate Monotonic Algorithm
      2. The Earliest Deadline First Algorithm
      3. Transition
      4. Exercises
  18. A. The Pseudocode Notation
    1. Structure
    2. Syntax
    3. Semantics
    4. Synchronization Constructs
  19. B. Review of Mathematical Logic
    1. B.1. The Propositional Calculus
      1. Syntax
      2. Semantics
      3. Logical Equivalence
    2. B.2. Induction
    3. B.3. Proof Methods
      1. Model Checking
      2. Deductive Proof
      3. Material Implication
    4. B.4. Correctness of Sequential Programs
      1. Verification in SPARKL
  20. C. Concurrent Programming Problems
  21. D. Software Tools
    1. D.1. BACI and jBACI
    2. D.2. Spin and jSpin
      1. The jSpin User Interface
      2. How Spin Verifies Properties
    3. D.3. DAJ
  22. E. Further Reading
    1. Websites
  23. Bibliography

Product information

  • Title: Principles of Concurrent and Distributed Programming, Second Edition
  • Author(s):
  • Release date: February 2006
  • Publisher(s): Addison-Wesley Professional
  • ISBN: 9780321312839