book

Principles of Concurrent and Distributed Programming, Second Edition

Name: Principles of Concurrent and Distributed Programming, Second Edition
Author: M. Ben-Ari
ISBN: 9780321312839

by M. Ben-Ari

February 2006

Intermediate to advanced

384 pages

8h 32m

English

Addison-Wesley Professional

Read now

Unlock full access

Copyright
Preface
1. What is Concurrent Programming?
1.1. Introduction1.2. Concurrency as Abstract Parallelism1.3. Multitasking1.4. The Terminology of Concurrency1.5. Multiple Computers1.6. The Challenge of Concurrent ProgrammingTransition
2. The Concurrent Programming Abstraction
2.1. The Role of Abstraction2.2. Concurrent Execution as Interleaving of Atomic StatementsStatesScenarios2.3. Justification of the AbstractionMultitasking SystemsMultiprocessor ComputersDistributed Systems2.4. Arbitrary Interleaving2.5. Atomic Statements2.6. CorrectnessLinear and Branching Temporal LogicsA2.7. Fairness2.8. Machine-Code InstructionsARegister MachinesStack MachinesSource Statements and Machine Instructions2.9. Volatile and Non-Atomic VariablesA2.10. The BACI Concurrency SimulatorL2.11. Concurrency in AdaLVolatile and Atomic2.12. Concurrency in JavaLVolatile2.13. Writing Concurrent Programs in PromelaL2.14. Supplement: The State Diagram for the Frog PuzzleTransitionExercises
3. The Critical Section Problem
3.1. Introduction3.2. The Definition of the Problem3.3. First Attempt3.4. Proving Correctness with State DiagramsStatesState DiagramsAbbreviating the State Diagram3.5. Correctness of the First Attempt3.6. Second Attempt3.7. Third Attempt3.8. Fourth Attempt3.9. Dekker’s Algorithm3.10. Complex Atomic StatementsTransitionExercises
4. Verification of Concurrent Programs
4.1. Logical Specification of Correctness Properties4.2. Inductive Proofs of InvariantsProof of Mutual Exclusion for the Third Attempt4.3. Basic Concepts of Temporal LogicAlways and EventuallyDualitySequences of Operators4.4. Advanced Concepts of Temporal LogicAUntilNextDeduction with Temporal OperatorsSpecifying Overtaking4.5. A Deductive Proof of Dekker’s AlgorithmAReasoning About ProgressA Proof of Freedom From Starvation4.6. Model Checking4.7. Spin and the Promela Modeling LanguageL4.8. Correctness Specifications in SpinL4.9. Choosing a Verification TechniqueATransitionExercises
5. Advanced Algorithms for the Critical Section ProblemA
5.1. The Bakery Algorithm5.2. The Bakery Algorithm for N Processes5.3. Less Restrictive Models of Concurrency5.4. Fast AlgorithmsOutline of the Fast AlgorithmPartial Proof of the AlgorithmGeneralization to N Processes5.5. Implementations in PromelaLTransitionExercises
6. Semaphores
6.1. Process States6.2. Definition of the Semaphore Type6.3. The Critical Section Problem for Two Processes6.4. Semaphore Invariants6.5. The Critical Section Problem for N Processes6.6. Order of Execution Problems6.7. The Producer–Consumer ProblemInfinite BuffersBounded BuffersSplit Semaphores6.8. Definitions of SemaphoresStrong SemaphoresBusy-Wait SemaphoresAbstract Definitions of SemaphoresA6.9. The Problem of the Dining Philosophers6.10. Barz’s Simulation of General SemaphoresA6.11. Udding’s Starvation-Free AlgorithmA6.12. Semaphores in BACIL6.13. Semaphores in AdaL6.14. Semaphores in JavaL6.15. Semaphores in PromelaLProving Barz’s Algorithm in SpinATransitionExercises

7. Monitors
7.1. Introduction7.2. Declaring and Using Monitors7.3. Condition VariablesSimulating SemaphoresOperations on Condition VariablesCorrectness of the Semaphore Simulation7.4. The Producer–Consumer Problem7.5. The Immediate Resumption Requirement7.6. The Problem of the Readers and Writers7.7. Correctness of the Readers and Writers AlgorithmA7.8. A Monitor Solution for the Dining Philosophers7.9. Monitors in BACIL7.10. Protected ObjectsProtected Objects in AdaL7.11. Monitors in JavaLSynchronized Blocks7.12. Simulating Monitors in PromelaLTransitionExercises
8. Channels
8.1. Models for CommunicationsSynchronous vs. Asynchronous CommunicationsAddressingData FlowCSP and Occam8.2. Channels8.3. Parallel Matrix MultiplicationSelective Input8.4. The Dining Philosophers with Channels8.5. Channels in PromelaL8.6. RendezvousThe Rendezvous in AdaL8.7. Remote Procedure CallsATransitionExercises
9. Spaces
9.1. The Linda Model9.2. Expressiveness of the Linda Model9.3. Formal Parameters9.4. The Master–Worker ParadigmGranularity9.5. Implementations of SpacesLC-LindaJavaSpacesJavaPromelaTransitionExercises
10. Distributed Algorithms
10.1. The Distributed Systems ModelCommunications ChannelsSending and Receiving MessagesConcurrency within the NodesStudying Distributed Algorithms10.2. Implementations10.3. Distributed Mutual ExclusionInitial Development of the AlgorithmThe Scenario of an ExampleEqual Ticket NumbersChoosing Ticket NumbersQuiescent Nodes10.4. Correctness of the Ricart–Agrawala Algorithm10.5. The RA Algorithm in PromelaL10.6. Token-Passing Algorithms10.7. Tokens in Virtual TreesATransitionExercisesRicart–AgrawalaRicart–Agrawala Token-Passing AlgorithmNeilsen–Mizuno Algorithm
11. Global Properties
11.1. Distributed TerminationPreliminary AlgorithmCorrectness of the Preliminary Algorithm11.2. The Dijkstra–Scholten AlgorithmCorrectness of the Dijkstra–Scholten AlgorithmPerformance11.3. Credit-Recovery Algorithms11.4. SnapshotsCorrectness of the Chandy–Lamport AlgorithmTransitionExercisesDijkstra–ScholtenCredit-RecoveryChandy–Lamport
12. Consensus
12.1. Introduction12.2. The Problem Statement12.3. A One-Round Algorithm12.4. The Byzantine Generals Algorithm12.5. Crash Failures12.6. Knowledge Trees12.7. Byzantine Failures with Three Generals12.8. Byzantine Failures with Four GeneralsCorrectnessComplexity12.9. The Flooding Algorithm12.10. The King AlgorithmCorrectnessComplexity12.11. Impossibility with Three GeneralsATransitionExercises
13. Real-Time Systems
13.1. IntroductionThe Ada Real-Time AnnexL13.2. Definitions13.3. Reliability and RepeatabilityThe Ariane 5 RocketThe Space Shuttle13.4. Synchronous Systems13.5. Asynchronous SystemsPriorities and Preemptive Scheduling13.6. Interrupt-Driven SystemsInterrupt Overflow in the Apollo 11 Lunar Module13.7. Priority Inversion and Priority InheritancePriority InheritancePriority Inversion from QueuesPriority Ceiling LockingThe Mars Pathfinder13.8. The Mars Pathfinder in SpinL13.9. Simpson’s Four-Slot AlgorithmA13.10. The Ravenscar ProfileLSuspension Objects13.11. UPPAALL13.12. Scheduling Algorithms for Real-Time SystemsThe Rate Monotonic AlgorithmThe Earliest Deadline First AlgorithmTransitionExercises
A. The Pseudocode Notation
StructureSyntaxSemanticsSynchronization Constructs
B. Review of Mathematical Logic
B.1. The Propositional CalculusSyntaxSemanticsLogical EquivalenceB.2. InductionB.3. Proof MethodsModel CheckingDeductive ProofMaterial ImplicationB.4. Correctness of Sequential ProgramsVerification in SPARKL
C. Concurrent Programming Problems
D. Software Tools
D.1. BACI and jBACID.2. Spin and jSpinThe jSpin User InterfaceHow Spin Verifies PropertiesD.3. DAJ
E. Further Reading
Websites
Bibliography

Overview

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.

Become an O’Reilly member and get unlimited access to this title plus top books and audiobooks from O’Reilly and nearly 200 top publishers, thousands of courses curated by job role, 150+ live events each month,
and much more.

Read now

Unlock full access

More than 5,000 organizations count on O’Reilly

O’Reilly covers everything we've got, with content to help us build a world-class technology community, upgrade the capabilities and competencies of our teams, and improve overall team performance as well as their engagement.

Julian F.

Head of Cybersecurity

I wanted to learn C and C++, but it didn't click for me until I picked up an O'Reilly book. When I went on the O’Reilly platform, I was astonished to find all the books there, plus live events and sandboxes so you could play around with the technology.

Addison B.

Field Engineer

I’ve been on the O’Reilly platform for more than eight years. I use a couple of learning platforms, but I'm on O'Reilly more than anybody else. When you're there, you start learning. I'm never disappointed.

Amir M.

Data Platform Tech Lead

I'm always learning. So when I got on to O'Reilly, I was like a kid in a candy store. There are playlists. There are answers. There's on-demand training. It's worth its weight in gold, in terms of what it allows me to do.

Mark W.

Embedded Software Engineer

A Common-Sense Guide to Data Structures and Algorithms, Second Edition, 2nd Edition

Publisher Resources

ISBN: 9780321312839Purchase book

Cloud Computing

Data Engineering

Data Science

AI & ML

Programming Languages

Software Architecture

IT/Ops

Security

Design

Business

Soft Skills