3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 64
Текст из файла (страница 64)
Then S can deadlockfrom σ. So ∆ ∈ Mtot [[S]](σ). By contrast, the do loop in T (S) terminatesin a state satisfying pc1 = 4 ∧ pc2 = 2 ∧ pv3 = 0. However, the finalif statement in T (S) converts this “premature” termination into a failure.So fail ∈ Mtot [[T (S)]](σ).⊓⊔36810 Nondeterministic ProgramsThese examples reveal one severe drawback of the transformation: thestructure of the original parallel program gets lost. Instead, we are faced witha nondeterministic program on the level of an assembly language where eachatomic action is explicitly listed. Therefore we do not pursue this approachany further.In the next chapter we are going to see, however, that for distributed programs a corresponding transformation into nondeterministic programs doespreserve the program structure without introducing auxiliary variables andis thus very well suited as a basis for verification.10.7 Exercises10.1.
Prove the Input/Output Lemma 10.3.10.2. Prove the Change and Access Lemma 10.4.10.3. Let π be a permutation of the indices {1, . . . , n}. Prove that for N = Mand N = Mtot :(i) N [[if ⊓⊔ni=1 Bi → Si fi]]=N [[if ¤ni=1 Bπ(i) → Sπ(i) fi]],(ii) N [[do ⊓⊔ni=1 Bi → Si od]]=N [[do ¤ni=1 Bπ(i) → Sπ(i) od]].10.4. Prove that for N = M and N = Mtot :(i)N [[do ⊓⊔ni=1 Bi → Si od]]⊔ni=1 Bi → Si od= N [[ if ¤ni=1 Bi → Si ; do ⊓Vn¤ i=1 ¬Bi → skipfi]],(ii)N [[do ⊓⊔ni=1 Bi → Si od]]Wn= N [[do i=1 Bi → if ⊓⊔ni=1 Bi → Si fi od]].10.5.
Which of the following correctness formulas are true in the sense oftotal correctness?(i) {true} if x > 0 → x := 0¤x < 0 → x := 0 fi {x = 0},(ii) {true} if x > 0 → x := 1¤x < 0 → x := 1 fi {x = 1},(iii){true}if x > 0 → x := 0¤ x = 0 → skip¤ x < 0 → x := 0fi{x = 0},10.7 Exercises369(iv){true}if x > 0 → x := 1¤ x = 0 → skip¤ x < 0 → x := 1fi{x = 1},(v) {true} if x > 0 then x := 0 else x := 0 fi {x = 0},(vi) {true} if x > 0 then x := 1 else x := 1 fi {x = 1}.Give both an informal argument and a formal proof in the systems T N orTW.10.6. Prove the Soundness of PN and TN Theorem 10.1.Hint. Follow the pattern of the proof of the Soundness of PW and TW Theorem 3.1 and use Lemma 10.3.10.7.
Develop systematically a program that checks if x appears in an arraysection a[0 : n − 1].10.8. Transform the parallel program MUTEX-S of Section 9.5, which ensures mutual exclusion with the help of semaphores, into a nondeterministicprogram using the transformation of Section 10.6.10.9. Prove that for every parallel program S ≡ [S1 k. .
.kSn ] with sharedvariables there exists a nondeterministic program T (S) and a set of variables{pc1 , . . ., pcn } not appearing in S such that for all proper states σMtot [[S]](σ) = Mtot [[T (S)]](σ) mod {pc1 , . . ., pcn }.Which semantic relationship can be established for the case of parallel programs with synchronization?Hint. See the discussion at the end of Section 10.6.10.10.
Define the weakest liberal precondition and the weakest precondition of a nondeterministic program by analogy with while programs (seeDefinition 3.10). Assume the analogue of the Definability Theorem 3.4 fornondeterministic programs. Prove that(i) wlp(S1 ; S2 , q) ↔ wlp(S1 , wlp(S2 , q)),Vn(ii) wlp(if ⊓⊔ni=1 Bi → Si fi, q) ↔ i=1 (Bi → wlp(Si , q)),(iii)wlp(do ⊓⊔ni=1 Bi → Si od, q) ∧ Bifor i ∈ {1, . . . , n},→ wlp(Si , wlp(do ⊓⊔ni=1 Bi → Si od, q))Vnn(iv) wlp(do ⊓⊔i=1 Bi → Si od, q) ∧ i=1 ¬Bi → q,37010 Nondeterministic Programs(v) |= {p} S {q} iff p → wlp(S, q).Prove that the above statements (i), (iii) and (iv) hold when wlp is replacedby wp.
Also prove that(vi) |=tot {p} S {q} iff p → wp(S, q),WnVn(vii) wp(if ⊓⊔ni=1 Bi → Si fi, q) ↔ ( i=1 Bi ) ∧ i=1 (Bi → wp(Si , q)).10.11.(i) Prove that the proof system P N is complete for partial correctness ofnondeterministic programs.(ii) Suppose that the set of all integer expressions is expressive in the senseof Definition 3.13. Prove that the proof system T N is complete for totalcorrectness of nondeterministic programs.Hint. Modify the proof of the Completeness Theorem 3.5 and use Exercise 10.10.10.8 Bibliographic RemarksWe have studied here a number of issues concerning a special type of nondeterministic programs introduced in Dijkstra [1975].
Their correctness andvarious semantics are discussed in de Bakker [1980] and Apt [1984].Their systematic development was originated in Dijkstra [1976] and waspopularized and further explained in Gries [1981]. In the 1980s the journalScience of Computer Programming carried a regular problem section on thismatter edited by M. Rem. The program for the welfare crook developed inSection 10.5 is due to W. Feijen. The presentation chosen here is due to Gries[1981].The first treatment of nondeterminism in the framework of program verification is due to Lauer [1971], where a proof rule for the or construct (themeaning of S1 or S2 is to execute either S1 or S2 ) is introduced.
This approach to nondeterminism is extensively discussed in de Bakker [1980] wherefurther references can be found.The idea of linking parallel programs to nondeterministic programs goesback to the work of Ashcroft and Manna [1971] and Flon and Suzuki [1978,1981]. This approach reappears in the book on UNITY by Chandy andMisra [1988], and in the work on action systems by Back [1989] and Backand von Wright [2008]. UNITY programs and action systems are particularlysimple nondeterministic programs consisting of an initialization part and asingle do loop containing only atomic actions. This is exactly the class ofnondeterministic programs into which we have transformed parallel programsin Section 10.6.10.8 Bibliographic Remarks371The main emphasis of the work of Chandy and Misra and of Back lies in thesystematic development of parallel programs on the basis of equivalent nondeterministic ones.
The systematic development of parallel implementationsstarting from sequential programs of a particular simple form (i.e., nestedfor loops) is pursued by Lengauer [1993].Related to the approach of action systems are the system specificationmethod TLA (Temporal Logic of Actions) by Lamport [1994,2003] and theabstract machines in the B-method by Abrial [1996]. The latter method hasrecently been extended to Event-B (see, for example, Abrial and Hallerstede [2007] and Abrial [2009]). Also here the basic form of the specificationsconsists of an initialization part and a single do loop containing only atomicactions.11 Distributed Programs11.111.211.311.411.511.611.7MSyntax .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Transformation into Nondeterministic Programs . . . . . . .Verification . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Case Study: A Transmission Problem . . . . . . . . . . . . . . . . .Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
.Bibliographic Remarks . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .375380382390396402405ANY REAL SYSTEMS consist of a number of physically distributed components that work independently using their privatestorage, but also communicate from time to time by explicit message passing.Such systems are called distributed systems.Distributed programs are abstract descriptions of distributed systems.
Adistributed program consists of a collection of processes that work concurrently and communicate by explicit message passing. Each process can accessa set of variables which are disjoint from the variables that can be changedby any other process.There are two ways of organizing message passing. We consider here synchronous communication where the sender of a message can deliver it onlywhen the receiver is ready to accept it at the same moment. An exampleis communication by telephone. Synchronous communication is also calledhandshake communication or rendezvous.
Another possibility is asynchronous37337411 Distributed Programscommunication where the sender can always deliver its message. This stipulates an implicit buffer where messages are kept until the receiver collectsthem. Communication by mail is an example. Asynchronous communicationcan be modeled by synchronous communication if the buffer is introduced asan explicit component of the distributed system.As a syntax for distributed programs we introduce in Section 11.1 a subset of the language CSP (Communicating Sequential Processes) due to Hoare[1978,1985]. This variant of CSP extends Dijkstra’s guarded command language (studied in Chapter 10) and disjoint parallel composition (studied inChapter 7) by adding input/output commands for synchronous communication.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
