3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 4
Текст из файла (страница 4)
. . . . . . . .Soundness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .9.4Case Study: Producer/Consumer Problem . . . . . . . . . . . . . . .9.5Case Study: The Mutual Exclusion Problem . . . . . . . . . . . . .Problem Formulation . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Verification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .A Busy Wait Solution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .A Solution Using Semaphores . . . . . . . . . . . . . . . . . . . . .
. . . . .9.6Allowing More Points of Interference . . . . . . . . . . . . . . . . . . . .9.7Case Study: Synchronized Zero Search . . . . . . . . . . . . . . . . . .Step 1. Simplifying the Program . . . . . . . . . . . . . . . . . . . . . . . .Step 2. Decomposing Total Correctness . . . . . . .
. . . . . . . . . .Step 3. Proving Termination . . . . . . . . . . . . . . . . . . . . . . . . . . .Step 4. Proving Partial Correctness . . . . . . . . . . . . . . . . . . . . .9.8Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . .9.9Bibliographic Remarks . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .3073093103113113133143163193243243263273313343353363373373423443458.58.68.78.88.98.109xxiPart IV Nondeterministic and Distributed Programs10 Nondeterministic Programs . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . .10.1Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .10.2Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Properties of Semantics . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . .10.3Why Are Nondeterministic Programs Useful? . . . . . . . . . . . .Symmetry . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .349351352353354355xxiiContentsNondeterminism . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . .Failures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Modeling Concurrency . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Verification . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . .Partial Correctness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Total Correctness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Soundness . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Case Study: The Welfare Crook Problem . . . . . . . . . . . . . . . .Transformation of Parallel Programs . . . . . . . . . . . . . . . . . . . .Exercises . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . .Bibliographic Remarks . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .35535635635735735735936036336837011 Distributed Programs . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . .11.1Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Sequential Processes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Distributed Programs . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .11.2Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .11.3Transformation into Nondeterministic Programs . . . . . . . . . .Semantic Relationship Between S and T (S) . . . . . . . .
. . . . . .Proof of the Sequentialization Theorem . . . . . . . . . . . . . . . . .11.4Verification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Partial Correctness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. .Weak Total Correctness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Total Correctness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Proof Systems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Soundness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. .11.5Case Study: A Transmission Problem . . . . . . . . . . . . . . . . . . .Step 1. Decomposing Total Correctness . . . . . . . . . . . . . . . . .Step 2. Proving Partial Correctness . . . . . . . . . . . . . . . . . . . . .Step 3. Proving Absence of Failures and of Divergence .
. . .Step 4. Proving Deadlock Freedom . . . . . . . . . . . . . . . . . . . . . .11.6Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .11.7Bibliographic Remarks . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .37337537537638038238238539039039139139239339639739739940040240512 Fairness . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .12.1The Concept of Fairness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Selections and Runs . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . .Fair Nondeterminism Semantics . . . . . . . . . . . . . . . . . . . . . . . .12.2Transformational Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . .12.3Well-Founded Structures . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . .12.4Random Assignment . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Verification . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .12.5Schedulers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .The Scheduler FAIR . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .40740941041241341341441541541942110.410.510.610.710.8Contents12.612.712.812.912.1012.11xxiiiThe Scheduler RORO .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .The Scheduler QUEUE . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Transformation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Verification . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . .Total Correctness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Soundness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Case Study: Zero Search . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . .Case Study: Asynchronous Fixed Point Computation . . . . .Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Bibliographic Remarks . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . .424426427430430438442446452455ASemantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 457BAxioms and Proof Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 459CProof Systems . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 471DProof Outlines . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 475References . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 477Index . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 491Author Index . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 496Symbol Index . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 501Part IIn the Beginning1 Introduction1.11.21.31.41.5PAn Example of a Concurrent Program . . . . . . . . . . . . . . . .Program Correctness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Structure of this Book . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . .Automating Program Verification . . . . . . . . . . . . . . . . . . . .Assertional Methods in Practice . . . . . . . . . . . . . . . . . . . . . .411131617ROGRAM VERIFICATION IS a systematic approach to provingthe correctness of programs.
Correctness means that the programsenjoy certain desirable properties. For sequential programs these propertiesare delivery of correct results and termination. For concurrent programs,that is, those with several active components, the properties of interferencefreedom, deadlock freedom and fair behavior are also important.The emphasis in this book is on verification of concurrent programs, in particular of parallel and distributed programs where the components communicate either via shared variables or explicit message passing.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
