Table of Contents

1 Introduction.- 1.1 Concurrent Programs.- 1.2 Communication and Synchronization.- 1.3 Understanding Concurrent Programs.- 1.4 A Preview.- Historical Notes for Chapter 1.- Exercises for Chapter 1.- 2 Formal Logic.- 2.1 Formal Logical Systems.- 2.2 Propositional Logic.- 2.3 A Predicate Logic.- 2.4 Safety and Liveness Revisited.- Historical Notes for Chapter 2.- Exercises for Chapter 2.- 3 Temporal Logic.- 3.1 Informal Preview.- 3.2 Syntax and Meaning of Formulas.- 3.3 Axioms and Inference Rules.- 3.4 Temporal Logic Applications.- 3.5 About Modal Logics.- Historical Notes for Chapter 3.- Exercises for Chapter 3.- 4 Notation and Logic for Sequential Programming.- 4.1 Notation for Sequential Programs.- 4.2 Reasoning About Program States.- 4.3 Proof Outline Logic.- 4.4 Assignment to Composite Variables.- 4.5 A Predicate Transformer.- Historical Notes for Chapter 4.- Exercises for Chapter 4.- 5 Concurrency and Interference.- 5.1 Specifying Concurrency.- 5.2 Control Predicate Axioms.- 5.3 Interference Freedom.- 5.4 Hiding Control Predicates in Derived Terms.- 5.5 Synchronously Altered and Shared Assertions.- 5.6 Specifying Synchronization.- 5.7 Synchronization and Interference.- Historical Notes for Chapter 5.- Exercises for Chapter 5.- 6 Safety Properties: Invariance.- 6.1 Invariance Properties.- 6.2 Verifying Invariance Properties.- 6.3 Exclusion of Configurations.- 6.4 Direct Use of Proof Outlines.- 6.5 Developing Programs for Invariance Properties.- Historical Notes for Chapter 6.- Exercises for Chapter 6.- 7 Safety Properties with Past Terms.- 7.1 Historical Safety Properties.- 7.2 Past Extensions to Predicate Logic.- 7.3 Verifying Historical Safety Properties.- 7.4 Developing Programs for Historical Safety Properties.- 7.5 Auxiliary Variables.- 7.6 Some Cautions.- Historical Notes for Chapter 7.- Exercises for Chapter 7.- 8 Verifying Arbitrary Temporal Logic Properties.- 8.1 S-Temporal Logic Revisited.- 8.2 Unless Properties and Derivatives.- 8.3 Fairness Assumptions.- 8.4 Reasoning from Fairness Assumptions.- 8.5 Helpful Actions and Eventualities.- 8.6 Liveness for Mutual Exclusion.- Historical Notes for Chapter 8.- Exercises for Chapter 8.- 9 Programming with Fine-Grained Atomic Actions.- 9.1 Pretending Atomicity.- 9.2 Translation-Independent Reasoning.- 9.3 Implementing Condition Synchronization.- 9.4 Programming with the Subset.- 9.5 Synchronization and Interference Revisited.- 9.6 Interlock Instructions.- 9.7 Example: Barrier Synchronization.- Historical Notes for Chapter 9.- Exercises for Chapter 9.- 10 Semaphores, Locks, and Conditional Critical Regions.- 10.1 Semaphores.- 10.2 Change of Variable to use Semaphores.- 10.3 Binary Semaphores and Locks.- 10.4 Split Binary Semaphore Method.- 10.5 Conditional Critical Regions.- Historical Notes for Chapter 10.- Exercises for Chapter 10.- 11 Message Passing and Distributed Programming.- 11.1 Asynchronous Message-Passing.- 11.2 Synchronous Message-Passing.- 11.3 Derivation of Distributed Programs.- 11.4 Shared-Variable Representations.- Historical Notes for Chapter 11.- Exercises for Chapter 11.- 12 Putting It Together.- 12.1 On Languages.- 12.2 Principles for Verifying Safety and Liveness Properties.- 12.3 Proofs Only Increase Confidence.- 12.4 A Tool and Applications.- Historical Notes for Chapter 12.- References.