Basics of concurrent and distributed programming

It is an excellent, world-known handbook on concurrent and distributed programming. The author begins the lecture by presenting classical problems of concurrency and basic mechanisms of synchronization processes. Then he goes on to discuss the problem of mutual exclusion and issues related to the verification of concurrent programs. Describes the baker algorithm and synchronization mechanisms in a shared memory model and in a model without common memory as well as classic distributed algorithms and real time systems. Each chapter ends with a set of exercises for self-solving. This guide is intended for IT students at all universities, programmers and IT system designers.

Table of Contents

Preface
Chapter 1. What is concurrent programming?
1.1.     Introduction       
1.2.     Concurrency as an abstraction of parallelism. Multitasking
1.3.     Terminology of concurrency
1.4.     Computers multiplied
1.5.      The tasks of concurrent programming

Chapter 2. Abstraction of concurrent programming
2.1.       The role of abstraction
2.2.       A concurrent execution as an interlace of atomic instructions   
2.3.       Justification of the adopted abstraction
2.4.       Any interleaving
2.5.       Atomic instructions
2.6.       correctness
2.7.       Honesty
2.8.       Machine orders "4
2.9.       Variable and nonatomic variables "4       
2.10.    BACIL concurrency simulator       
2.11.    Concurrency in AdaL        
2.12.    Concurrency in JavaL       
2.13.    Concurrency in PromelaL
2.14.    Addition: state diagram of a puzzle

Chapter 3. Testing of mutual exclusion
3.1.      Introduction       
3.2.      Formulating the problem
3.3.      First try
3.4.      Proving correctness by means of state diagrams      
3.5.      The correctness of the first attempt
3.6.      Second try
3.7.      Third attempt
3.8.      The fourth attempt
3.9.      Dekker algorithm
3.10.   Complex atomic instructions       

Chapter 4. Verification   correctness   concurrent programs
4.1.      Specification of correctness property in the language of logic   
4.2.      Inductive proofs of invariants
4.3.      Basic concepts of temporal logic       
4.4.      Advanced concepts of temporal logic ^
4.5.      Deductive proof of the correctness of the DekkerA algorithm
4.6.      Verification by model
4.7.     The Promel modeling language in the SpinL system        
4.8.      Verification of correctness conditions in the SpinL system     
4.9.      Selection of verification technique ^               

Chapter 5.   Complex algorithms for solving the problem of mutual exclusion "4
5.1.      Baking algorithm  
5.2.      Baker's algorithm for many processes                 
5.3.      Less restrictive concurrency models     
5.4.      Quick algorithms       
5.5.      Implementations in PromelaL language

Chapter 6.   semaphores
6.1.      Process states
6.2.      Definition of semaphore type
6.3.      The problem of mutual exclusion for two processes
6.4.      Semaphore invariants
6.5.      The problem of mutual exclusion for N processes     
6.6.      Problems that need to synchronize the execution order
6.7.      Problem of the producer-consumer
6.8.      Definitions of semaphores       
6.9.      The problem of five philosophers
6.10.   Barza simulation of general semaphores'4       
6.11.   Udding algorithm without starvation "4
6.12.   Semaphores in BACIL
6.13.   Semaphores in Ada ^
6.14.   Semaphores in language, TavaL       
6.15.   Semaphores in PromelaL language

Chapter 7. Monitors
7.1.      Introduction       
7.2.      Declaration and use of monitors
7.3.      Conditional variables
7.4.      Problem of the producer-consumer
7.5.      Requirement for immediate resumption of performance    
7.6.      The problem of readers and writers
7.7.      The correctness of the readers 'and writers' algorithm ^ 4
7.8.      A monitor solution to the problem of five philosophers
7.9.      Monitors in the BACI simulator
7.10.   Protected objects
7.11.   Monitors in Java ^ 1       
7.12.   Simulation of monitors in Promeli7 '

Chapter 8. Channels
8.1.      Communication models       
8.2.      Channels
8.3.      Parallel matrix multiplication
8.4.      The solution to the problem of five philosophers through channels     
8.5.      Channels in PromelaL language
8.6.      Dating
8.7.      Remote procedure calls "4

Chapter 9. Space
9.1.      Concurrency model used in Linda language
9.2.      Expression of the model in Linda language
9.3.      Formal parameters
9.4.      Pattern supervisor-worker
9.5.      Implementations of tuple spaceL

Chapter 10.   Distributed algorithms
10.1.   Distributed system model
10.2.   implementations       
10.3.   Mutual disintegration
10.4.   The correctness of the Ricart-Agrawali algorithm
10.5.   The RA algorithm in PromelaL
10.6.   Chip passing algorithms       
10.7.   Tokens in virtual trees ^ 1        

ChAPTeR 11. Global Properties
11.1.   Distributed completion of the implementation
11.2.   Dijkstra-Scholten algorithm
11.3.   Collection algorithms       
11.4.   Snapshots

Chapter 12.   Reconciliation
12.1.   Introduction       
12.2.   Formulating the problem
12.3.   One-round algorithm
12.4.   An algorithm of Byzantine generals
12.5.   collapse
12.6.   Knowledge trees
12.7.   Byzantine failures with three generals
12.8.   Byzantine failures with four generals
12.9.   Spreading algorithm
12.10. The king's algorithm
12.11. No solution for three generals ^ 1      

Chapter 13.   Real-time systems
13.1.   Introduction       
13.2.    definitions
13.4.    Reliability and repeatability
13.5.    Synchronous systems
13.6.    Asynchronous systems
13.7.    Systems controlled by interruptions       
13.8.    Reversal and inheritance of priorities
13.9.    Specification of the Mars Pathfmder probe in the Spin-6 system
13.10. Simpson's algorithm "4
13.11. RavenscarL profile
13.12. UPPAALL
13.13. Schedule algorithms for real-time systems

Appendix A.   pseudocode
Appendix B.   Basic concepts of mathematical logic
bl      Sentence calculus
B.2.      Induction
B.3.      Command methods       
B.4.      Correctness of sequential programs
Appendix C.   Concurrent programming problems
Appendix D.   Development tools
dl      BACI and jBACI simulators
D.2.      Spin and jSpin systems
D.3.      DAJ system
Appendix E.   Further reading
Bibliography
Index