Principles of concurrent and distributed programming /
Guardado en:
Autor principal: | |
---|---|
Formato: | Libro |
Lenguaje: | Inglés |
Publicado: |
Harlow :
Addison-Wesley,
2006
|
Edición: | 2nd. ed. |
Materias: | |
Aporte de: | Registro referencial: Solicitar el recurso aquí |
Tabla de Contenidos:
- Preface
- 1 What is Concurrent Programming?
- 1.1 Introduction
- 1.2 Concurrency as abstract parallelism
- 1.3 Multitasking
- 1.4 The terminology of concurrency
- 1.5 Multiple computers
- 1.6 The challenge of concurrent programming
- 2 The Concurrent Programming Abstraction
- 2.1 The role of abstraction
- 2.2 Concurrent execution as interleaving of atomic statements
- 2.3 Justification of the abstraction
- 2.4 Arbitrary interleaving
- 2.5 Atomic statements
- 2.6 Correctness
- 2.7 Fairness
- 2.8 Machine-code instructions
- 2.9 Volatile and non-atomic variables
- 2.10 The BACI concurrency simulator
- 2.11 Concurrency in Ada
- 2.12 Concurrency in Java
- 2.13 Writing concurrent programs in Promela
- 2.14 Supplement: the state diagram for the frog puzzle
- 3 The Critical Section Problem
- 3.1 Introduction
- 3.2 The definition of the problem
- 3.3 First attempt
- 3.4 Proving correctness with state diagrams
- 3.5 Correctness of the first attempt
- 3.6 Second attempt
- 3.7 Third attempt
- 3.8 Fourth attempt
- 3.9 Dekker’s algorithm
- 3.10 Complex atomic statements
- 4 Verification of Concurrent Programs
- 4.1 Logical specification of correctness properties
- 4.2 Inductive proofs of invariants
- 4.3 Basic concepts of temporal logic
- 4.4 Advanced concepts of temporal logic
- 4.5 A deductive proof of Dekker’s algorithm
- 4.6 Model checking
- 4.7 Spin and the Promela modeling language
- 4.8 Correctness specifications in Spin
- 4.9 Choosing a verification technique
- 5 Advanced Algorithms for the Critical Section Problem
- 5.1 The bakery algorithm
- 5.2 The bakery algorithm for N processes
- 5.3 Less restrictive models of concurrency
- 5.4 Fast algorithms
- 5.5 Implementations in Promela
- 6 Semaphores
- 6.1 Process states
- 6.2 Definition of the semaphore type
- 6.3 The critical section problem for two processes
- 6.4 Semaphore invariants
- 6.5 The critical section problem for N processes
- 6.6 Order of execution problems
- 6.7 The producer–consumer problem
- 6.8 Definitions of semaphores
- 6.9 The problem of the dining philosophers
- 6.10 Barz’s simulation of general semaphores
- 6.11 Udding’s starvation-free algorithm
- 6.12 Semaphores in BACI
- 6.13 Semaphores in Ada
- 6.14 Semaphores in Java
- 6.15 Semaphores in Promela
- 7 Monitors
- 7.1 Introduction
- 7.2 Declaring and using monitors
- 7.3 Condition variables
- 7.4 The producer–consumer problem
- 7.5 The immediate resumption requirement
- 7.6 The problem of the readers and writers
- 7.7 Correctness of the readers and writers algorithm
- 7.8 A monitor solution for the dining philosophers
- 7.9 Monitors in BACI
- 7.10 Protected objects
- 7.11 Monitors in Java
- 7.12 Simulating monitors in Promela
- 8 Channels
- 8.1 Models for communications
- 8.2 Channels
- 8.3 Parallel matrix multiplication
- 8.4 The dining philosophers with channels
- 8.5 Channels in Promela
- 8.6 Rendezvous
- 8.7 Remote procedure calls
- 9 Spaces
- 9.1 The Linda model
- 9.2 Expressiveness of the Linda model
- 9.3 Formal parameters
- 9.4 The master–worker paradigm
- 9.5 Implementations of spaces
- 10 Distributed Algorithms
- 10.1 The distributed systems model
- 10.2 Implementations
- 10.3 Distributed mutual exclusion
- 10.4 Correctness of the Ricart–Agrawala algorithm
- 10.5 The RA algorithm in Promela
- 10.6 Token-passing algorithms
- 10.7 Tokens in virtual trees
- 11 Global Properties
- 11.1 Distributed termination
- 11.2 The Dijkstra–Scholten algorithm
- 11.3 Credit-recovery algorithms
- 11.4 Snapshots
- 12 Consensus
- 12.1 Introduction
- 12.2 The problem statement
- 12.3 A one-round algorithm
- 12.4 The Byzantine Generals algorithm
- 12.5 Crash failures
- 12.6 Knowledge trees
- 12.7 Byzantine failures with three generals
- 12.8 Byzantine failures with four generals
- 12.9 The flooding algorithm
- 12.10 The King algorithm
- 12.11 Impossibility with three generals
- 13 Real-Time Systems
- 13.1 Introduction
- 13.2 Definitions
- 13.3 Reliability and repeatability
- 13.4 Synchronous systems
- 13.5 Asynchronous systems
- 13.6 Interrupt-driven systems
- 13.7 Priority inversion and priority inheritance
- 13.8 The Mars Pathfinder in Spin
- 13.9 Simpson’s four-slot algorithm
- 13.10 The Ravenscar profile
- 13.11 UPPAAL
- 13.12 Scheduling algorithms for real-time systems
- A The Pseudocode Notation
- B Review of Mathematical Logic
- B.1 The propositional calculus
- B.2 Induction
- B.3 Proof methods
- B.4 Correctness of sequential programs
- C Concurrent Programming Problems
- D Software Tools
- D.1 BACI and jBACI
- D.2 Spin and jSpin
- D.3 DAJ
- E Further Reading.