Concurrency Verification: Introduction to Compositional and Non-compositional Methods

by Willem-Paul de Roever , Frank de Boer , Ulrich Hanneman , Jozef Hooman , Yassine Lakhnech , Mannes Poel , Job Zwiers

• ISBN13: 9780521806084
• ISBN10: 0521806089
• Format: Hardcover
• Copyright: 2001-11-26
• Publisher: Cambridge University Press

Summary

This is a systematic and comprehensive introduction both to compositional proof methods for the state-based verification of concurrent programs, such as the assumption-commitment and rely-guarantee paradigms, and to noncompositional methods, whose presentation culminates in an exposition of the communication-closed-layers (CCL) paradigm for verifying network protocols. Compositional concurrency verification methods reduce the verification of a concurrent program to the independent verification of its parts. If those parts are tightly coupled, one additionally needs verification methods based on the causal order between events. These are presented using CCL. The semantic approach followed here allows a systematic presentation of all these concepts in a unified framework which highlights essential concepts. The book is self-contained, guiding the reader from advanced undergraduate level to the state-of-the-art. Every method is illustrated by examples, and a picture gallery of some of the subject's key figures complements the text.

Table of Contents

Preface	ix
Part I: Introduction and Overview	1	(70)
Introduction	2	(69)
Central Questions	2	(1)
Structure of this Chapter	2	(1)
Basic Concepts of Concurrency	3	(5)
Why Concurrent Programs Should be Proved Correct	8	(25)
The Approach of this Book	33	(13)
Compositionality	46	(16)
From Noncomp. to Comp. Proof Methods--a historical perspective	62	(9)
Part II: The Inductive Assertion Method	71	(248)
Floyd's Inductive Assertion Method for Transition Diagrams	72	(47)
Objectives of Part II	72	(3)
Structure of this Chapter	75	(1)
Sequential Transition Diagrams and Systems	76	(6)
Specification and Correctness Statements	82	(6)
A Proof Method for Partial Correctness	88	(4)
Soundness	92	(1)
Semantic Completeness of the Inductive Assertion Method	93	(5)
Proving Convergence	98	(6)
Proving Absence of Runtime Errors	104	(7)
Historical Notes	111	(8)
The Inductive Assertion Method for Shared-Variable Concurrency	119	(102)
Objective and Structure of this Chapter	119	(2)
A Characterisation of Concurrent Execution	121	(11)
Is this Characterisation of Concurrent Execution Justified?	132	(2)
The Generalisation of Floyd's Approach to Nondeterministic Interleavings	134	(3)
Concurrent Transition Systems with Shared Variables	137	(51)
Proving Convergence for Shared-Variable Concurrency	188	(15)
Proving Deadlock Freedom	203	(3)
Proving Absence of Runtime Errors	206	(2)
Historical Notes	208	(13)
The Inductive Assertion Method for Synchronous Message Passing	221	(70)
Objective and Introduction	221	(2)
Structure of this Chapter	223	(1)
Syntax and Semantics of Synchronous Transition Diagrams	223	(4)
Proof Methods for Partial Correctness	227	(22)
Semantic Completeness	249	(15)
Technical Note: Modifications Towards Compositionality	264	(5)
A Modular Method for Proving Convergence	269	(8)
Verifying Deadlock Freedom	277	(2)
Proving Absence of Runtime Errors	279	(3)
Historical Notes	282	(9)
Expressibility and Relative Completeness	291	(28)
Objective	291	(1)
Structure of this Chapter	292	(1)
Syntactic Notions	292	(6)
Partial Correctness of Syntactic Transition Diagrams	298	(2)
Relative Completeness of Floyd's Inductive Assertion Method	300	(9)
Relative Completeness of the Method of Owicki & Gries	309	(3)
Relative Completeness of the Method of Apt, Francez & de Roever	312	(4)
Historical Notes	316	(3)
Picture Gallery	319	(34)
Part III: Compositional Methods based on Assertion Networks	353	(134)
Introduction to Compositional Reasoning	354	(13)
Motivation	354	(2)
Introduction to Part III and to this Chapter	356	(3)
Assume-Guarantee-based Reasoning	359	(2)
Assumption-Commitment-based Reasoning	361	(2)
Rely-Guarantee-based Reasoning	363	(4)
Compositional Proof Methods: Synchronous Message Passing	367	(71)
Objective and Introduction	367	(1)
Structure of the Chapter	368	(1)
Top-level Synchronous Message Passing	369	(10)
A Compositional Proof Method for Nested Parallelism	379	(18)
Assumption-Commitment-based Reasoning	397	(32)
Historical Notes	429	(9)
Compositional Proof Methods: Shared-Variable Concurrency	438	(49)
Introduction and Overview	438	(1)
Concurrent Transition Diagrams	439	(1)
Top-Level Shared-Variable Concurrency	440	(7)
The Rely-Guarantee Method	447	(32)
Historical Notes	479	(8)
Part IV: Hoare Logic	487	(166)
A Proof System for Sequential Programs Using Hoare Triples	488	(43)
Introduction and Overview of Hoare Logics	488	(9)
Structure of this Chapter	497	(1)
Syntax and Informal Meaning of GCL + Programs	498	(3)
Semantics of GCL+	501	(5)
A Proof System for GCL+ Programs	506	(5)
Soundness and Relative Completeness	511	(6)
Proof Outlines	517	(4)
Alternative Definitions of Proof Outlines	521	(1)
Examples of Verification during Program Development	522	(4)
Historical Notes	526	(5)
A Hoare Logic for Shared-Variable Concurrency	531	(69)
Introduction and Overview	531	(1)
Syntax and Informal Meaning of SVL Programs	532	(5)
Semantics of SVL+	537	(3)
A Proof System for SVL Programs	540	(23)
An Extended Example: Concurrent Garbage Collection	563	(21)
Completeness of the Owicki & Gries Method	584	(16)
A Hoare Logic for Synchronous Message Passing	600	(53)
Structure of this Chapter	600	(1)
Syntax and Informal Meaning of DML Programs	601	(5)
Semantics of DML	606	(2)
A Hoare Logic for Synchronous Message Passing	608	(22)
Soundness and Relative Completeness of this Hoare Logic	630	(8)
Technical Note: Modifications Towards Compositionality	638	(15)
Part V: Layered Design	653	(57)
Transformational Design and Hoare Logic	654	(56)
Introduction and Overview	654	(6)
Structure of this Chapter	660	(1)
Syntax and Informal Meaning of SVL++ Programs	660	(2)
The Semantics of SVL++ Programs	662	(1)
Partial Orders and Temporal Logic	663	(13)
The Communication-Closed-Layers Laws	676	(12)
The Two-Phase Commit Protocol	688	(6)
Assertion-Based Program Transformations	694	(2)
Loop Distribution	696	(4)
Set-partitioning Revisited	700	(4)
Historical Notes	704	(6)
Bibliography	710	(37)
Glossary of Symbols	747	(14)
Index	761