3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 71
Текст из файла (страница 71)
Call the resulting programs general distributed programs.11.7 Bibliographic Remarks405(i) Extend the definition of semantics to general distributed programs.(ii) Let R ≡ S0 ; [S1 k. . .kR0 ; Si k. . .kSn ] be a general distributed programwhere R0 and S0 are nondeterministic programs. Consider the generaldistributed program T ≡ S0 ; R0 ; [S1 k. . .kSi k. . .kSn ].
Prove thatM[[R]] = M[[T ]].What can be stated for Mwtot and Mtot ?Hint. Use the Sequentialization Theorem 11.1 and the Input/OutputLemma 10.3.11.7 Bibliographic RemarksWe have studied here distributed programs that can be defined in a simplesubset of CSP of Hoare [1978]. This subset was introduced in Apt [1986].In the original definition of CSP i/o commands can appear at every positionwhere assignments are allowed.
On the other hand, process names were usedinstead of channel names in i/o commands, and output commands were notallowed as guards of alternative and repetitive commands. A modern versionof CSP without these restrictions is presented in Hoare [1985]. This booktakes up concepts from process algebra as in CCS (Calculus for Communicating Systems) of Milner [1980,1989]. The most complete presentation ofthis modern CSP can be found in Roscoe [1998].A first semantics of CSP programs can be found in Francez et al. [1979].Simplified definitions are given in Francez, Lehmann and Pnueli [1984] andin Brookes, Hoare and Roscoe [1984].
The operational semantics presentedhere is based on Plotkin [1982].Proof systems for the verification of CSP programs were first introducedin Apt, Francez, and de Roever [1980], and in Levin and Gries [1981]. Theseproof systems represent an analogue of the Owicki/Gries method describedin Chapter 8: first proof outlines are established for the sequential processesof a distributed program and then their compatibility is checked using a socalled cooperation test.
This test is a counterpart of the test of interferencefreedom for parallel programs. The proof systems of Apt, Francez, and deRoever and of Levin and Gries are explained in Francez [1992]. An overviewof various proof systems for CSP is given in Hooman and de Roever [1986].The approach to verification of distributed programs presented in thischapter is due to Apt [1986]. The basic idea is to avoid the complex cooperation test by considering only a subset of CSP programs. In Apt, Bougéand Clermont [1987], and in Zöbel [1988] it has been shown that each CSPprogram can indeed be transformed into a program in this subset called itsnormal form.
The price of this transformation is that it introduces additionalcontrol variables into the normal form program in the same way as program40611 Distributed Programscounter variables were introduced to transform parallel programs into nondeterministic ones in Section 10.6.For CSP programs that manipulate a finite state space, behavioral properties can be verified automatically using the so-called FDR model checker,a commercially available tool, see Roscoe [1994] and Formal Systems (Europe) Ltd. [2003]. For general CSP programs the compositional verificationtechniques of Zwiers [1989] can be used.
See also de Roever et al. [2001].Research on CSP led to the design of the programming language OCCAM,see INMOS [1984], for distributed transputer systems. A systematic development of OCCAM programs from specifications has been studied as partof the European basic research project ProCoS (Provably Correct Systems),see Bowen et al.
[1996] for an overview and the papers by Schenke [1999],Schenke and Olderog [1999], and Olderog and Rössig [1993] for more details.CSP has been combined with specification methods for data (and time)to integrated specification formalisms for reactive (and real-time) systems.Examples of such combinations are CSP-OZ by Fischer [1997], Circus byWoodcock and Cavalcanti [2002], and, for the case of real-time, TCOZ byMahony and Dong [1998] and CSP-OZ-DC by Hoenicke and Olderog [2002]and Hoenicke [2006]. For applications of CSP-OZ see the papers by Fischerand Wehrheim [1999], Möller et al.
[2008], and Basin et al. [2007]. For automatic verification of CSP-OZ-DC specifications against real-time propertieswe refer to Meyer et al. [2008].12 Fairness12.112.212.312.412.512.612.712.812.912.1012.11AThe Concept of Fairness . . . . . . . . . . . . . . . . . . . . . . . .
. . . . .Transformational Semantics . . . . . . . . . . . . . . . . . . . . . . . . . .Well-Founded Structures . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Random Assignment . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Schedulers . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Transformation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Verification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Case Study: Zero Search . . . . . . .
. . . . . . . . . . . . . . . . . . . . . .Case Study: Asynchronous Fixed Point Computation . .Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Bibliographic Remarks . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .409413413414419427430442446452405S WE HAVE seen in the zero search example of Chapter 1, fairness isan important hypothesis in the study of parallel programs. Fairnessmodels the idea of “true parallelism,” where every component of a parallelprogram progresses with unknown, but positive speed.
In other words, everycomponent eventually executes its next enabled atomic instruction.Semantically, fairness can be viewed as an attempt at reducing the amountof nondeterminism in the computations of programs. Therefore fairness canbe studied in any setting where nondeterminism arises. In this chapter westudy fairness in the simplest possible setting of this book, the class of nondeterministic programs studied in Chapter 10.Since parallel and distributed programs can be transformed into nondeterministic ones (see Sections 10.6 and 11.3), the techniques presented here40740812 Fairnesscan in principle be applied to the study of fairness for concurrent programs.However, a more direct approach is possible that does not involve any program transformations.
The precise presentation is beyond the scope of thisedition of the book.In Section 12.1 we provide a rigorous definition of fairness. The assumption of fairness leads to so-called unbounded nondeterminism; this makesreasoning about fairness difficult. In Section 12.2 we outline an approach toovercome this difficulty by reducing fair nondeterminism to usual nondeterminism by means of a program transformation.To cope with the unbounded nondeterminism induced by fairness, thistransformation uses an additional programming construct: the random assignment. In Section 12.4 semantics and verification of nondeterministic programs in presence of random assignment are discussed.
In Section 12.5 random assignments are used to construct an abstract scheduler FAIR thatexactly generates all fair computations. We also show that two widely usedschedulers, the round robin scheduler and a scheduler based on queues, arespecific instances of FAIR.In Section 12.6 we define the program transformation announced in Section 12.2 by embedding the scheduler FAIR into a given nondeterministicprogram. In Section 12.7 this transformation is used to develop a proof ruledealing with fairness.We demonstrate the use of this proof rule in two case studies. In Section 12.8 we apply this proof rule in a case study that deals with a nondeterministic version of the zero search program of Chapter 1, and in Section 12.9we prove correctness of a nondeterministic program for the asynchronouscomputation of fixed points.
In both cases the assumption of fairness is crucial in the termination proof.12.1 The Concept of Fairness40912.1 The Concept of FairnessTo illustrate the concept of fairness in the setting of nondeterministic programs, consider the programPU1 ≡ signal := false;do ¬signal → “print next line”⊓⊔ ¬signal → signal := trueod.The letters P and U in the program name PU1 stand for printer and user ; thefirst guarded command is meant to represent a printer that continuously outputs a line from a file until the user, here represented by the second guardedcommand, signals that it should terminate. But does the printer actuallyreceive the termination signal? Well, assuming that the user’s assignmentsignal := true is eventually executed the program PU1 terminates.However, the semantics of nondeterministic programs as defined in Chapter 10 does not guarantee this.
Indeed, it permits infinite computations thatcontinuously select the first guarded command. To enforce termination onehas to assume fairness.Often two variants of fairness are distinguished. Weak fairness requiresthat every guarded command of a do loop, which is from some moment oncontinuously enabled, is activated infinitely often. Under this assumption acomputation of PU1 cannot forever activate its first component (the printer)because the second command (the user) is continuously enabled. Thus theassignment signal := true of PU1 is eventually executed.
This leads totermination of PU1.PU1 is a particularly simple program because the guards of its do loopare identical. Thus, as soon as this guard becomes false, the loop is certainto terminate. Loops with different guards can exhibit more complicated computations. Consider, for example, the following variant of our printer-userprogram:PU2 ≡ signal := false; full-page := false; ℓ := 0;do ¬signal → “print next line”;ℓ := (ℓ + 1) mod 30;full-page := ℓ = 0⊓⊔ ¬signal ∧ full-page → signal := trueod.Again, the printer, represented by the first command, continuously outputsa line from a file until the user, represented by the second command, signalsthat it should terminate.
But the user will issue the termination signal only ifthe printer has completed its current page. We assume that each page consistsof 30 lines, which are counted modulo 30 in the integer variable ℓ.What about termination of PU2 ? Since the guard “full-page” of the secondcommand is never continuously enabled, the assumption of weak fairness41012 Fairnessdoes not rule out an infinite computation where only the first command isactivated.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
