3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 44
Текст из файла (страница 44)
In Chapter 8 we study parallelism with shared variables and in Chapter 9 we add synchronization to shared variable parallelism. Disjoint parallelism provides a good preparation for studying these extensions. Disjointparallelism is also a good starting point for studying distributed programs inChapter 11.Under what conditions can parallel execution be reduced to a sequential execution? In other words, is there any simple syntactic criterion thatguarantees that all computations of a parallel program are equivalent to the2452467 Disjoint Parallel Programssequential execution of its components? Such questions led Hoare to an introduction of the concept of disjoint parallelism (Hoare [1972,1975]).
In thischapter we present an in-depth study of this concept.After introducing the syntax of disjoint parallel programs (Section 7.1) wedefine their semantics (Section 7.2). We then prove that all computations of adisjoint parallel program starting in the same initial state produce the sameoutput (the Determinism Lemma).In Section 7.3 we study the proof theory of disjoint parallel programs.The proof rule for disjoint parallelism simply takes the conjunction ofpre- and postconditions of the component programs.
Additionally, we needa proof rule dealing with the so-called auxiliary variables; these are variables used to express properties about the program execution that cannot beexpressed solely in terms of program variables.As a case study we prove in Section 7.4 the correctness of a disjoint parallelprogram FIND that searches for a positive element in an integer array.7.1 Syntax2477.1 SyntaxTwo while programs S1 and S2 are called disjoint if neither of them canchange the variables accessed by the other one; that is, ifchange(S1 ) ∩ var(S2 ) = ∅andvar(S1 ) ∩ change(S2 ) = ∅.Recall from Chapter 3 that for an arbitrary program S, change(S) is the setof simple and array variables of S that can be modified by it; that is, to whicha value is assigned within S by means of an assignment. Note that disjointprograms are allowed to read the same variables.Example 7.1.
The programs x := z and y := z are disjoint becausechange(x := z) = {x}, var(y := z) = {y, z} and var(x := z) = {x, z},change(y := z) = {y}.On the other hand, the programs x := z and y := x are not disjointbecause x ∈ change(x := z) ∩ var(y := x), and the programs a[1] := z andy := a[2] are not disjoint because a ∈ change(a[1] := z) ∩ var(y := a[2]). ⊓⊔Disjoint parallel programs are generated by the same clauses as those defining while programs in Chapter 3 together with the following clause for disjoint parallel composition:S ::= [S1 k.
. .kSn ],where for n > 1, S1 , . . ., Sn are pairwise disjoint while programs, called the(sequential) components of S. Thus we do not allow nested parallelism, but weallow parallelism to occur within sequential composition, conditional statements and while loops.It is useful to extend the notion of disjointness to expressions and assertions. An expression t and a program S are called disjoint if S cannot changethe variables of t; that is, ifchange(S) ∩ var(t) = ∅.Similarly, an assertion p and a program S are called disjoint if S cannotchange the variables of p; that is, ifchange(S) ∩ var(p) = ∅.2487 Disjoint Parallel Programs7.2 SemanticsWe now define semantics of disjoint parallel programs in terms of transitions.Intuitively, a disjoint parallel program [S1 k. .
.kSn ] performs a transition ifone of its components performs a transition. This form of modeling concurrency is called interleaving. Formally, we expand the transition system forwhile programs by the following transition rule(xvii)< Si , σ > → < T i , τ >< [S1 k. . .kSi k. . .kSn ], σ > → < [S1 k. . .kTi k. . .kSn ], τ >where i ∈ {1, . . . , n}.Computations of disjoint parallel programs are defined like those of sequential programs.
For example,< [x := 1ky := 2kz := 3], σ >→ < [Eky := 2kz := 3], σ[x := 1] >→ < [EkEkz := 3], σ[x := 1][y := 2] >→ < [EkEkE], σ[x := 1][y := 2][z := 3] >is a computation of [x := 1ky := 2kz := 3] starting in σ.Recall that the empty program E denotes termination. For example,[Eky := 2kz := 3] denotes a parallel program where the first componenthas terminated. We wish to express the idea that a disjoint parallel program S ≡ [S1 k. . .kSn ] terminates if and only if all its components S1 , . .
., Snterminate. To this end we identify[Ek. . .kE] ≡ E.This identification allows us to maintain the definition of a terminating computation given in Definition 3.1. For example, the final configuration in theabove computation is the terminating configuration< E, σ[x := 1][y := 2][z := 3] > .By inspection of the above transition rules, we obtainLemma 7.1. (Absence of Blocking) Every configuration < S, σ > withS 6≡ E and a proper state σ has a successor configuration in the transitionrelation → .Thus when started in a state σ a disjoint parallel program S ≡ [S1 k. . .kSn ]terminates or diverges. Therefore we introduce two types of input/outputsemantics for disjoint programs in just the same way as for while programs.7.2 Semantics249Definition 7.1.
For a disjoint parallel program S and a proper state σ(i) the partial correctness semantics is a mappingM[[S]] : Σ → P(Σ)withM[[S]](σ) = {τ |< S, σ > →∗ < E, τ >}(ii) and the total correctness semantics is a mappingMtot [[S]] : Σ → P(Σ ∪ {⊥})withMtot [[S]](σ) = M[[S]](σ) ∪ {⊥ | S can diverge from σ}.Recall that ⊥ is the error state standing for divergence.⊓⊔DeterminismUnlike while programs, disjoint parallel programs can generate more thanone computation starting in a given initial state.
Thus determinism in thesense of the Determinism Lemma 3.1 does not hold. However, we can provethat all computations of a disjoint parallel program starting in the sameinitial state produce the same output. Thus a weaker form of determinismholds here, in that for every disjoint parallel program S and proper stateσ, Mtot [[S]](σ) has exactly one element, either a proper state or the errorstate ⊥. This turns out to be a simple corollary to some results concerningproperties of abstract reduction systems.Definition 7.2.
A reduction system is a pair (A, → ) where A is a set and→ is a binary relation on A; that is, → ⊆ A × A. If a → b holds, we saythat a can be replaced by b. Let →∗ denote the transitive reflexive closureof → .We say that → satisfies the diamond property if for all a, b, c ∈ A withb 6= caւցbcimplies that for some d ∈ A2507 Disjoint Parallel Programsbcցւd.→ is called confluent if for all a, b, c ∈ Aa∗ւ ց∗bcimplies that for some d ∈ Abc∗ց ւ∗d.⊓⊔The following lemma due to Newman [1942] is of importance to us.Lemma 7.2. (Confluence) For all reduction systems (A, → ) the followingholds: if a relation → satisfies the diamond property then it is confluent.Proof.
Suppose that → satisfies the diamond property. Let →n stand forthe n-fold composition of → . A straightforward proof by induction on n ≥ 0shows that a → b and a →n c implies that for some i ≤ n and some d ∈ A,b →i d and c →ǫ d. Here c →ǫ d iff c → d or c = d. Thus a → b and a →∗ cimplies that for some d ∈ A, b →∗ d and c →∗ d.This implies by induction on n ≥ 0 that if a →∗ b and a →n c then forsome d ∈ A we have b →∗ d and c →∗ d. This proves confluence.⊓⊔To deal with infinite sequences, we need the following lemma.Lemma 7.3. (Infinity) Consider a reduction system (A, → ) where → satisfies the diamond property and elements a, b, c ∈ A with a → b, a → c andb 6= c. If there exists an infinite sequence a → b → .
. . passing through b thenthere exists also an infinite sequence a → c → . . . passing through c.Proof. Consider an infinite sequence a0 → a1 → . . . where a0 = a and a1 = b.Case 1. For some i ≥ 0, c →∗ ai .Then a → c →∗ ai → . . . is the desired sequence.Case 2.
For no i ≥ 0, c →∗ ai .We construct by induction on i an infinite sequence c0 → c1 → . . . suchthat c0 = c and for all i ≥ 0 ai → ci . c0 is already correctly defined. For i = 1note that a0 → a1 , a0 → c0 and a1 6= c0 . Thus by the diamond property thereexists a c1 such that a1 → c1 and c0 → c1 .Consider now the induction step. We have ai → ai+1 and ai → ci for somei > 0.
Also, since c →∗ ci , by the assumption ci 6= ai+1 . Again by the diamondproperty for some ci+1 , ai+1 → ci+1 and ci → ci+1 .⊓⊔7.2 Semantics251Definition 7.3. Let (A, → ) be a reduction system and a ∈ A. An elementb ∈ A is → -maximal if there is no c with b → c. We define nowyield(a) ={b | a →∗ b and b is → -maximal}∪ {⊥ | there exists an infinite sequence a → a1 → . . .}⊓⊔Lemma 7.4.
(Yield) Let (A, → ) be a reduction system where → satisfiesthe diamond property. Then for every a, yield(a) has exactly one element.Proof. Suppose that for some → -maximal b and c, a →∗ b and a →∗ c. ByConfluence Lemma 7.2, there is some d ∈ A with b →∗ d and c →∗ d. By the→ -maximality of b and c, both b = d and c = d; thus b = c.Thus the set {b | a →∗ b, b is → -maximal} has at most one element. Suppose it is empty. Then yield(a) = {⊥}.Suppose now that it has exactly one element, say b. Assume by contradiction that there exists an infinite sequence a → a1 → . .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
