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.

Mordechai (Moti) Ben-Ari is an Associate Professor in the Department of Science Teaching at the Weizmann Institute of Science in Rehovot, Israel

Preface	p. xi
What is Concurrent Programming?	p. 1
Introduction	p. 1
Concurrency as abstract parallelism	p. 2
Multitasking	p. 4
The terminology of concurrency	p. 4
Multiple computers	p. 5
The challenge of concurrent programming	p. 5
The Concurrent Programming Abstraction	p. 7
The role of abstraction	p. 7
Concurrent execution as interleaving of atomic statements	p. 8
Justification of the abstraction	p. 13
Arbitrary interleaving	p. 17
Atomic statements	p. 19
Correctness	p. 21
Fairness	p. 23
Machine-code instructions	p. 24
Volatile and non-atomic variables	p. 28
The BACI concurrency simulator	p. 29
Concurrency in Ada	p. 31
Concurrency in Java	p. 34
Writing concurrent programs in Promela	p. 36
Supplement: the state diagram for the frog puzzle	p. 37
The Critical Section Problem	p. 45
Introduction	p. 45
The definition of the problem	p. 45
First attempt	p. 48
Proving correctness with state diagrams	p. 49
Correctness of the first attempt	p. 53
Second attempt	p. 55
Third attempt	p. 57
Fourth attempt	p. 58
Dekker's algorithm	p. 60
Complex atomic statements	p. 61
Verification of Concurrent Programs	p. 67
Logical specification of correctness properties	p. 68
Inductive proofs of invariants	p. 69
Basic concepts of temporal logic	p. 72
Advanced concepts of temporal logic	p. 75
A deductive proof of Dekker's algorithm	p. 79
Model checking	p. 83
Spin and the Promela modeling language	p. 83
Correctness specifications in Spin	p. 86
Choosing a verification technique	p. 88
Advanced Algorithms for the Critical Section Problem	p. 93
The bakery algorithm	p. 93
The bakery algorithm for N processes	p. 95
Less restrictive models of concurrency	p. 96
Fast algorithms	p. 97
Implementations in Promela	p. 104
Semaphores	p. 107
Process states	p. 107
Definition of the semaphore type	p. 109
The critical section problem for two processes	p. 110
Semaphore invariants	p. 112
The critical section problem for N processes	p. 113
Order of execution problems	p. 114
The producer-consumer problem	p. 115
Definitions of semaphores	p. 119
The problem of the dining philosophers	p. 122
Barz's simulation of general semaphores	p. 126
Udding's starvation-free algorithm	p. 129
Semaphores in BACI	p. 131
Semaphores in Ada	p. 132
Semaphores in Java	p. 133
Semaphores in Promela	p. 134
Monitors	p. 145
Introduction	p. 145
Declaring and using monitors	p. 146
Condition variables	p. 147
The producer-consumer problem	p. 151
The immediate resumption requirement	p. 152
The problem of the readers and writers	p. 154
Correctness of the readers and writers algorithm	p. 157
A monitor solution for the dining philosophers	p. 160
Monitors in BACI	p. 162
Protected objects	p. 162
Monitors in Java	p. 167
Simulating monitors in Promela	p. 173
Channels	p. 179
Models for communications	p. 179
Channels	p. 181
Parallel matrix multiplication	p. 183
The dining philosophers with channels	p. 187
Channels in Promela	p. 188
Rendezvous	p. 190
Remote procedure calls	p. 193
Spaces	p. 197
The Linda model	p. 197
Expressiveness of the Linda model	p. 199
Formal parameters	p. 200
The master-worker paradigm	p. 202
Implementations of spaces	p. 204
Distributed Algorithms	p. 211
The distributed systems model	p. 211
Implementations	p. 215
Distributed mutual exclusion	p. 216
Correctness of the Ricart-Agrawala algorithm	p. 223
The RA algorithm in Promela	p. 225
Token-passing algorithms	p. 227
Tokens in virtual trees	p. 230
Global Properties	p. 237
Distributed termination	p. 237
The Dijkstra-Scholten algorithm	p. 243
Credit-recovery algorithms	p. 248
Snapshots	p. 250
Consensus	p. 257
Introduction	p. 257
The problem statement	p. 258
A one-round algorithm	p. 260
The Byzantine Generals algorithm	p. 261
Crash failures	p. 263
Knowledge trees	p. 264
Byzantine failures with three generals	p. 266
Byzantine failures with four generals	p. 268
The flooding algorithm	p. 271
The King algorithm	p. 274
Impossibility with three generals	p. 280
Real-Time Systems	p. 285
Introduction	p. 285
Definitions	p. 287
Reliability and repeatability	p. 288
Synchronous systems	p. 290
Asynchronous systems	p. 293
Interrupt-driven systems	p. 297
Priority inversion and priority inheritance	p. 299
The Mars Pathfinder in Spin	p. 303
Simpson's four-slot algorithm	p. 306
The Ravenscar profile	p. 309
UPPAAL	p. 311
Scheduling algorithms for real-time systems	p. 312
The Pseudocode Notation	p. 317
Review of Mathematical Logic	p. 321
The propositional calculus	p. 321
Induction	p. 323
Proof methods	p. 324
Correctness of sequential programs	p. 326
Concurrent Programming Problems	p. 331
Software Tools	p. 339
BACI and jBACI	p. 339
Spin and jSpin	p. 341
DAJ	p. 345
Further Reading	p. 349
Bibliography	p. 351
Index	p. 355
Table of Contents provided by Ingram. All Rights Reserved.

What is included with this book?

The New copy of this book will include any supplemental materials advertised. Please check the title of the book to determine if it should include any access cards, study guides, lab manuals, CDs, etc.

The Used, Rental and eBook copies of this book are not guaranteed to include any supplemental materials. Typically, only the book itself is included. This is true even if the title states it includes any access cards, study guides, lab manuals, CDs, etc.