Principles of concurrent and distributed programming second edition/ M. Ben-Ari.
Material type: TextPublication details: Harlow, England ; New York : Addison-Wesley, 2006.Edition: 2nd edDescription: xv, 361 p. : ill. ; 24 cmISBN:- 032131283X (pbk.)
- 9780321312839 (pbk.)
Item type | Current library | Call number | Copy number | Status | Date due | Barcode | |
---|---|---|---|---|---|---|---|
Standard Loan | Thurles Library Main Collection | 004.352 BEN (Browse shelf(Opens below)) | 1 | Available | 30026000001676 |
Enhanced descriptions from Syndetics:
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.
Includes bibliographical references (p. 351-354) and index.
What is concurrent programming? -- The concurrent programming abstraction -- The critical section problem -- Verification of concurrent programs -- Advanced algorithms for the critical section problem -- Semaphores -- Monitors -- Channels -- Spaces -- Distributed algorithms -- Global properties -- Consensus -- Real-time systems.
Table of contents provided by Syndetics
- Preface (p. xi)
- 1 What is Concurrent Programming? (p. 1)
- 1.1 Introduction (p. 1)
- 1.2 Concurrency as abstract parallelism (p. 2)
- 1.3 Multitasking (p. 4)
- 1.4 The terminology of concurrency (p. 4)
- 1.5 Multiple computers (p. 5)
- 1.6 The challenge of concurrent programming (p. 5)
- 2 The Concurrent Programming Abstraction (p. 7)
- 2.1 The role of abstraction (p. 7)
- 2.2 Concurrent execution as interleaving of atomic statements (p. 8)
- 2.3 Justification of the abstraction (p. 13)
- 2.4 Arbitrary interleaving (p. 17)
- 2.5 Atomic statements (p. 19)
- 2.6 Correctness (p. 21)
- 2.7 Fairness (p. 23)
- 2.8 Machine-code instructions (p. 24)
- 2.9 Volatile and non-atomic variables (p. 28)
- 2.10 The BACI concurrency simulator (p. 29)
- 2.11 Concurrency in Ada (p. 31)
- 2.12 Concurrency in Java (p. 34)
- 2.13 Writing concurrent programs in Promela (p. 36)
- 2.14 Supplement: the state diagram for the frog puzzle (p. 37)
- 3 The Critical Section Problem (p. 45)
- 3.1 Introduction (p. 45)
- 3.2 The definition of the problem (p. 45)
- 3.3 First attempt (p. 48)
- 3.4 Proving correctness with state diagrams (p. 49)
- 3.5 Correctness of the first attempt (p. 53)
- 3.6 Second attempt (p. 55)
- 3.7 Third attempt (p. 57)
- 3.8 Fourth attempt (p. 58)
- 3.9 Dekker's algorithm (p. 60)
- 3.10 Complex atomic statements (p. 61)
- 4 Verification of Concurrent Programs (p. 67)
- 4.1 Logical specification of correctness properties (p. 68)
- 4.2 Inductive proofs of invariants (p. 69)
- 4.3 Basic concepts of temporal logic (p. 72)
- 4.4 Advanced concepts of temporal logic (p. 75)
- 4.5 A deductive proof of Dekker's algorithm (p. 79)
- 4.6 Model checking (p. 83)
- 4.7 Spin and the Promela modeling language (p. 83)
- 4.8 Correctness specifications in Spin (p. 86)
- 4.9 Choosing a verification technique (p. 88)
- 5 Advanced Algorithms for the Critical Section Problem (p. 93)
- 5.1 The bakery algorithm (p. 93)
- 5.2 The bakery algorithm for N processes (p. 95)
- 5.3 Less restrictive models of concurrency (p. 96)
- 5.4 Fast algorithms (p. 97)
- 5.5 Implementations in Promela (p. 104)
- 6 Semaphores (p. 107)
- 6.1 Process states (p. 107)
- 6.2 Definition of the semaphore type (p. 109)
- 6.3 The critical section problem for two processes (p. 110)
- 6.4 Semaphore invariants (p. 112)
- 6.5 The critical section problem for N processes (p. 113)
- 6.6 Order of execution problems (p. 114)
- 6.7 The producer-consumer problem (p. 115)
- 6.8 Definitions of semaphores (p. 119)
- 6.9 The problem of the dining philosophers (p. 122)
- 6.10 Barz's simulation of general semaphores (p. 126)
- 6.11 Udding's starvation-free algorithm (p. 129)
- 6.12 Semaphores in BACI (p. 131)
- 6.13 Semaphores in Ada (p. 132)
- 6.14 Semaphores in Java (p. 133)
- 6.15 Semaphores in Promela (p. 134)
- 7 Monitors (p. 145)
- 7.1 Introduction (p. 145)
- 7.2 Declaring and using monitors (p. 146)
- 7.3 Condition variables (p. 147)
- 7.4 The producer-consumer problem (p. 151)
- 7.5 The immediate resumption requirement (p. 152)
- 7.6 The problem of the readers and writers (p. 154)
- 7.7 Correctness of the readers and writers algorithm (p. 157)
- 7.8 A monitor solution for the dining philosophers (p. 160)
- 7.9 Monitors in BACI (p. 162)
- 7.10 Protected objects (p. 162)
- 7.11 Monitors in Java (p. 167)
- 7.12 Simulating monitors in Promela (p. 173)
- 8 Channels (p. 179)
- 8.1 Models for communications (p. 179)
- 8.2 Channels (p. 181)
- 8.3 Parallel matrix multiplication (p. 183)
- 8.4 The dining philosophers with channels (p. 187)
- 8.5 Channels in Promela (p. 188)
- 8.6 Rendezvous (p. 190)
- 8.7 Remote procedure calls (p. 193)
- 9 Spaces (p. 197)
- 9.1 The Linda model (p. 197)
- 9.2 Expressiveness of the Linda model (p. 199)
- 9.3 Formal parameters (p. 200)
- 9.4 The master-worker paradigm (p. 202)
- 9.5 Implementations of spaces (p. 204)
- 10 Distributed Algorithms (p. 211)
- 10.1 The distributed systems model (p. 211)
- 10.2 Implementations (p. 215)
- 10.3 Distributed mutual exclusion (p. 216)
- 10.4 Correctness of the Ricart-Agrawala algorithm (p. 223)
- 10.5 The RA algorithm in Promela (p. 225)
- 10.6 Token-passing algorithms (p. 227)
- 10.7 Tokens in virtual trees (p. 230)
- 11 Global Properties (p. 237)
- 11.1 Distributed termination (p. 237)
- 11.2 The Dijkstra-Scholten algorithm (p. 243)
- 11.3 Credit-recovery algorithms (p. 248)
- 11.4 Snapshots (p. 250)
- 12 Consensus (p. 257)
- 12.1 Introduction (p. 257)
- 12.2 The problem statement (p. 258)
- 12.3 A one-round algorithm (p. 260)
- 12.4 The Byzantine Generals algorithm (p. 261)
- 12.5 Crash failures (p. 263)
- 12.6 Knowledge trees (p. 264)
- 12.7 Byzantine failures with three generals (p. 266)
- 12.8 Byzantine failures with four generals (p. 268)
- 12.9 The flooding algorithm (p. 271)
- 12.10 The King algorithm (p. 274)
- 12.11 Impossibility with three generals (p. 280)
- 13 Real-Time Systems (p. 285)
- 13.1 Introduction (p. 285)
- 13.2 Definitions (p. 287)
- 13.3 Reliability and repeatability (p. 288)
- 13.4 Synchronous systems (p. 290)
- 13.5 Asynchronous systems (p. 293)
- 13.6 Interrupt-driven systems (p. 297)
- 13.7 Priority inversion and priority inheritance (p. 299)
- 13.8 The Mars Pathfinder in Spin (p. 303)
- 13.9 Simpson's four-slot algorithm (p. 306)
- 13.10 The Ravenscar profile (p. 309)
- 13.11 UPPAAL (p. 311)
- 13.12 Scheduling algorithms for real-time systems (p. 312)
- A The Pseudocode Notation (p. 317)
- B Review of Mathematical Logic (p. 321)
- B.1 The propositional calculus (p. 321)
- B.2 Induction (p. 323)
- B.3 Proof methods (p. 324)
- B.4 Correctness of sequential programs (p. 326)
- C Concurrent Programming Problems (p. 331)
- D Software Tools (p. 339)
- D.1 BACI and jBACI (p. 339)
- D.2 Spin and jSpin (p. 341)
- D.3 DAJ (p. 345)
- E Further Reading (p. 349)
- Bibliography (p. 351)
- Index (p. 355)