Principles of concurrent and distributed programming /

Guardado en:
Detalles Bibliográficos
Autor principal: Ben-Ari, Mordechai
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.