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