3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 63
Текст из файла (страница 63)
Of course the simplest choicefor B1 , B2 and B3 are, respectively, i 6= iv, j 6= jv and k 6= kv but thevalues iv, jv and kv cannot be used in the program. On the other hand,p ∧ i 6= iv is equivalent to p ∧ i < iv which means by the definition of iv, jvand kv that a[i] is not the crook. Now, assuming p, the last statement isguaranteed if a[i] < b[j]. Indeed, a, b and c are ordered, so p ∧ a[i] < b[j]implies a[i] < b[jv] = a[iv] which implies i < iv.We can thus choose a[i] < b[j] for the guard B1 .
In a similar fashion wecan choose the other two guards which yield the following proof outline:{r}i := 0; j := 0; k = 0;{inv : p}{bd : t}do a[i] < b[j] → {p ∧ a[i] < b[j]}{p ∧ i < iv}i := i + 1¤ b[j] < c[k] → {p ∧ b[j] < c[k]}{p ∧ j < jv}j := j + 1¤ c[k] < a[i] → {p ∧ c[k] < a[i]}{p ∧ k < kv}k := k + 1od{p ∧ ¬(a[i] < b[j]) ∧ ¬(b[j] < c[k]) ∧ ¬(c[k] < a[i])}{q}.10.6 Transformation of Parallel Programs363Summarizing, we developed the following desired program:CROOK ≡ i := 0; j := 0; kdo a[i] < b[j] →¤ b[j] < c[k] →¤ c[k] < a[i] →od.= 0;i := i + 1j := j + 1k := k + 1In developing this program the crucial step consisted of the choice of theguards B1 , B2 and B3 .
Accidentally, the choice made turned out to be sufficient to ensure that upon loop termination the postcondition q holds.10.6 Transformation of Parallel ProgramsLet us return now to the issue of modeling parallel programs by means ofnondeterministic programs, originally mentioned in Section 10.3.Reasoning about parallel programs with shared variables is considerablymore complicated than reasoning about sequential programs:• the input/output behavior is not compositional, that is, cannot be solelydetermined by the input/output behavior of their components,• correctness proofs require a complicated test of interference freedom.The question arises whether we cannot avoid these difficulties by decomposingthe task of verifying parallel programs into two steps:(1) transformation of the considered parallel programs in nondeterministicsequential ones,(2) verification of the resulting nondeterministic programs using the proofsystems of this chapter.For disjoint parallelism this can be done very easily.
Recall from the Sequentialization Lemma 7.7 that every disjoint parallel program S ≡ [S1 k. . .kSn ]is equivalent to the while program T ≡ S1 ; . . .; Sn .For parallel programs with shared variables things are more difficult. First,since these programs exhibit nondeterminism, such a transformation yieldsnondeterministic programs. Second, to simulate all the possible interleavingsof the atomic actions, this transformation requires additional variables actingas program counters. More precisely, the transformation of a parallel programS ≡ [S1 k.
. .kSn ]in the syntax of Chapter 9 into a nondeterministic program T (S) introducesa fresh integer variable pci for each component Si . This variable models a program counter for Si which during its execution always points to that atomicaction of Si which is to be executed next. To define the values of the program36410 Nondeterministic Programscounters, the component programs S1 , .
. . , Sn are labeled in a preparatorystep.In general, a component program R is transformed into a labeled programR̂ by inserting in R pairwise distinct natural numbers k as labels of theform “k :” at the following positions outside of any atomic region and anyawait statement:••••••ininininininfrontfrontfrontfrontfrontfrontofofofofofofeacheacheacheacheacheachskip statement,assignment u := t,if symbol,while symbol,atomic region hS0 i,await symbol.For a labeled program R̂ let f irst(R̂) denote the first label in R̂ andlast(R̂) the last label in R̂. For each labeled component program Ŝi of S werequire that the labels are chosen as consecutive natural numbers starting at0. Thus the labels in Ŝi aref irst(Ŝi ) = 0, 1, 2, 3, .
. . , last(Ŝi ).For checking termination we definetermi = last(Ŝi ) + 1.Now we transform S into T (S) by referring to the labeled component programs Ŝ1 , . . . , Ŝn :T (S) ≡ pc1 := 0; . . . pcn := 0;do T1 (Ŝ1 )(term1 )¤ T2 (Ŝ2 )(term2 )..................¤ Tn (Ŝn )(termn )od;if T ERM → skip fi.Here pc1 , . . . , pcn are integer variables that do not occur in S and that modelthe program counters of the components Si . The Boolean expressionVnT ERM ≡ i=1 pci = termirepresents the termination condition for the labeled components Ŝ1 , . . .
, Ŝn .Each component transformation Ti (Ŝi )(termi ) translates into one or moreguarded commands, separated by the ¤ symbol. We define these componenttransformationsTi (R̂)(c)10.6 Transformation of Parallel Programs365by induction on the structure of the labeled component program R̂, takingan additional label c ∈ N as a parameter modeling the continuation valuethat the program counter pci assumes upon termination of R̂:• Ti (k : skip)(c) ≡ pci = k → pci := c,• Ti (k : u := t)(c) ≡ pci = k → u := t; pci := c,• Ti (R̂1 ; R̂2 )(c) ≡Ti (R̂1 )(f irst(R̂2 ))¤ Ti (R̂2 )(c),• Ti (k : if B then R̂1 else R̂2 fi)(c) ≡pci = k ∧ B → pci := f irst(R̂1 )¤ pci = k ∧ ¬B → pci := f irst(R̂2 )¤ Ti (R̂1 )(c)¤ Ti (R̂2 )(c),• Ti (k : while B do R̂ od)(c) ≡pci = k ∧ B → pci := f irst(R̂)¤ pci = k ∧ ¬B → pci := c¤ Ti (R̂)(k),• Ti (k : hS0 i)(c) ≡ pci = k → S0 ; pci := c,• Ti (k : await B then S0 end)(c) ≡ pci = k ∧ B → S0 ; pci := c.To see this transformation in action let us look at an example.Example 10.2.
Consider the parallel composition S ≡ [S1 k S2 ] in the program FINDPOS of Case Study 8.6. The corresponding labeled componentsareŜ1 ≡ 0: while i < min(oddtop, eventop) do1: if a[i] > 0 then 2: oddtop := i else 3: i := i + 2 fiodandŜ2 ≡ 0: while j < min(oddtop, eventop) do1: if a[j] > 0 then 2: eventop := j else 3: j := j + 2 fiod.Since each component program uses the labels 1, 2, 3, the termination valuesare term1 = term2 = 4.
Therefore S is transformed intoT (S) ≡ pc1 := 0; pc2 := 0;do T1 (Ŝ1 )(4)¤ T2 (Ŝ2 )(4)od;if pc1 = 4 ∧ pc2 = 4 → skip fi,36610 Nondeterministic Programswhere for the first component we calculateT1 (Ŝ1 )(4) ≡ pc1 = 0 ∧ i < min(oddtop, eventop) → pc1 := 1¤ pc1 = 0 ∧ ¬(i < min(oddtop, eventop)) → pc1 := 4¤ T1 (1 : if . . .
fi)(0),T1 (1 : if . . . fi)(0) ≡ pc1 = 1 ∧ a[i] > 0 → pc1 := 2¤ pc1 = 1 ∧ ¬(a[i] > 0) → pc1 := 3¤ T1 (2 : oddtop := i)(0)¤ T1 (3 : i := i + 2)(0),T1 (2 : oddtop := i)(0) ≡ pc1 = 2 → oddtop := i; pc1 := 0,T1 (3 : i := i + 2)(0) ≡ pc1 = 3 → i := i + 2; pc1 := 0.Altogether we obtain the following nondeterministic program:T (S) ≡ pc1 := 0; pc2 := 0;do pc1 = 0 ∧ i < min(oddtop, eventop) → pc1 := 1¤ pc1 = 0 ∧ ¬(i < min(oddtop, eventop)) → pc1 := 4¤ pc1 = 1 ∧ a[i] > 0 → pc1 := 2¤ pc1 = 1 ∧ ¬(a[i] > 0) → pc1 := 3¤ pc1 = 2 → oddtop := i; pc1 := 0¤ pc1 = 3 → i := i + 2; pc1 := 0¤ pc2 = 0 ∧ j < min(oddtop, eventop) → pc2 := 1¤ pc2 = 0 ∧ ¬(j < min(oddtop, eventop)) → pc2 := 4¤ pc2 = 1 ∧ a[j] > 0 → pc2 := 2¤ pc2 = 1 ∧ ¬(a[j] > 0) → pc2 := 3¤ pc2 = 2 → eventop := j; pc2 := 0¤ pc2 = 3 → j := j + 2; pc2 := 0od;if pc1 = 4 ∧ pc2 = 4 → skip fiNote that upon termination of the do loop the assertion pc1 = 4 ∧ pc2 = 4holds, so the final if statement has no effect here.⊓⊔For parallel programs S with shared variables, one can prove that S andT (S) are equivalent modulo the program counter variables.
In other words,using the mod notation of Section 2.3, we have for every proper state σ:Mtot [[S]](σ) = Mtot [[T (S)]](σ) mod {pc1 , . . ., pcn }.For parallel programs with synchronization the relationship between S andT (S) is more complex because deadlocks of S are transformed into failuresof T (S) (see Exercise 10.9). As an illustration let us look at the followingartificial parallel program with an atomic region and an await statement.Example 10.3.
Consider the parallel program S ≡ [S1 kS2 kS3 ] with the following labeled components:10.6 Transformation of Parallel Programs367Ŝ1 ≡ 0 : if x = 0 then 1 : x := x + 1; 2 : x := x + 2 else 3 : x := x − 1 fi,Ŝ2 ≡ 0 : while y < 10 do 1 : hy := y + 1; z := z − 1i od,Ŝ3 ≡ 0 : await z 6= y then done := true end.Note that term1 = 4, term2 = 2, and term3 = 1. Thus S is transformed intothe following nondeterministic program:T (S) ≡ pc1 := 0; pc2 := 0; pc3 := 0;do T1 (Ŝ1 )(4)¤ T2 (Ŝ2 )(2)¤ T3 (Ŝ3 )(1)od;if pc1 = 4 ∧ pc2 = 2 ∧ pc3 = 1 → skip fiwhere we calculate for the component transformations:T1 (Ŝ1 )(4) ≡ pc1 = 0 ∧ x = 0 → pc1 := 1¤ pc1 = 0 ∧ ¬(x = 0) → pc1 := 3¤ pc1 = 1 → x := x + 1; pc1 := 2¤ pc1 = 2 → x := x + 2; pc1 := 4¤ pc1 = 3 → x := x − 1; pc1 := 4,T2 (Ŝ2 )(2) ≡ pc2 = 0 ∧ y < 10 → pc2 := 1¤ pc2 = 0 ∧ ¬(y < 10) → pc2 := 2¤ pc2 = 1 → y := y + 1; z := z − 1; pc1 := 0,T3 (Ŝ3 )(1) ≡ pc3 = 0 ∧ z 6= y → done := true; pc3 := 1.Altogether we obtainT (S) ≡ pc1 := 0; pc2 := 0; pc3 := 0;do pc1 = 0 ∧ x = 0 → pc1 := 1¤ pc1 = 0 ∧ ¬(x = 0) → pc1 := 3¤ pc1 = 1 → x := x + 1; pc1 := 2¤ pc1 = 2 → x := x + 2; pc1 := 4¤ pc1 = 3 → x := x − 1; pc1 := 4¤ pc2 = 0 ∧ y < 10 → pc2 := 1¤ pc2 = 0 ∧ ¬(y < 10) → pc2 := 2¤ pc2 = 1 → y := y + 1; z := z − 1; pc1 := 0¤ pc3 = 0 ∧ z 6= y → done := true; pc3 := 1od;if pc1 = 4 ∧ pc2 = 2 ∧ pc3 = 1 → skip fi.Consider now a state σ satisfying z = y = 10.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
