3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 67

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 67)

This explains why in (ii) we have to dealwith fail and ⊥ together.Finally, deadlocks do not arise when executing nondeterministic programs.Deadlocks of S are transformed into terminal configurations of T (S) in whose38411 Distributed Programsstate the condition TERM does not hold. A simple example for this is theprogramS ≡ [do c!1 → skip od || skip].Then T (S) ≡ skip because the set Γ of matching guards is empty. Thus Sends in a deadlock whereas T (S) terminates in a state satisfying ¬T ERM .The contraposition of this observation is stated in (iii).To prove the above theorem we introduce some auxiliary notions and provesome of their properties.In a transition of a computation of S either one or two processes areactivated, depending on whether transition rule (xvii) or axiom (xxiv) isused, or transition axiom (xxv) applies.

When one process is activated ina transition, then we attach to → its index and when two processes areactivated, say Si and Sj with i < j, then we attach to → the pair (i, j).iIf a transition C → D is obtained by applying transition rule (xvii), theniwe say that the process Si executes a private action in C → D, and if it isobtained by applying transition axiom (xxiv), then we say that the processiSi exits its main loop in C → D.

Alternatively, we can say that the transitioniC → D consists of a private action of Si or of the main loop exit of Si . Finally,(i,j)if C −→ D, then we say that each of the processes Si and Sj takes part in a(i,j)communication in C −→ D.Fix now some A, B ∈ {1, . . . , n} ∪ {(i, j) | i, j ∈ {1, . . . , n} and i < j}. WeABsay that the relations → and → commute, if for all configurations C, Dwhere D is not a failure,ABBAC → ◦ → D iff C → ◦ → D,where ◦ denotes relational composition as defined in Section 2.1.The following two simple lemmata are of importance to us.Lemma 11.2. (Commutativity)ij(i) For i, j ∈ {1, .

. . , n} the relations → and → commute.(i,j)k(ii) For distinct i, j, k ∈ {1, . . . , n} with i < j, the relations −→ and →commute.Proof. See Exercise 11.2.⊓⊔Lemma 11.3. (Failure) Consider configurations C, F where F is a failureand distinct i, j, B ∈ {1, . . . , n}. Suppose that A = i or A = (i, j) with i < j.ThenABBC → ◦ → F implies C → F ′for some failure F ′ .11.3 Transformation into Nondeterministic Programs385Proof. See Exercise 11.2.Proof of the Sequentialization Theorem 11.1We follow the approach of the Atomicity Theorem 8.1.Step 1 We first introduce the notion of a good computation of the distributedprogram S. We call a computation of S good if the components S1 , .

. ., Sn ofS are activated in the following order:(i) first execute the subprograms S1,0 , . . ., Sn,0 of S1 , . . ., Sn , respectively,in that order, for as long as possible;(ii) in case no failure or divergence arises,– pick up a pair of matching generalized guards gi,j and gk,ℓ whoseBoolean parts evaluate to true, contained, respectively, in processesSi and Sk with i < k;– perform the communication, and– execute the subprograms Si,j and Sk,ℓ of Si and Sk , respectively, inthat order, for as long as possible;(iii) repeat step (ii) for as long as possible;(iv) in case no failure or divergence arises, exit the main loop whereverpossible, in the order determined by the processes’ indices.A transition sequence is good if it is a prefix of a good computation.Step 2 We now define a notion of equivalence between the computations ofS and T (S).

Let η be a computation of S and ξ a computation of T (S).We say that η and ξ are 1-equivalent if(i) η and ξ start in the same state,(ii) for all states σ such that σ |= TERM , η terminates in σ iff ξ terminatesin σ,(iii) for all states σ such that σ |= ¬TERM , η ends in a deadlock with stateσ iff ξ terminates in σ,(iv) η ends in a failure iff ξ ends in a failure,(v) η is infinite iff ξ is infinite.We prove the following two claims.• Every computation of T (S) is 1-equivalent to a good computation of S;• every good computation of S is 1-equivalent to a computation of T (S).Consider a computation ξ of T (S) starting in a state σ. We constructa 1-equivalent good computation η of S which proceeds through the same38611 Distributed Programssequence of states as ξ (disregarding their repetitions) by analyzing the successive transitions of ξ. Let < S ′ , σ ′ > be a configuration occurring in ξ.

ThenS ′ is of one of the following forms:1.2.3.4.R; S ′′ where R is a substatement of the process Si ,do ⊓⊔(i,j,k,ℓ)∈Γ Bi,j ∧ Bk,ℓ → Eff (αi,j , αk,ℓ ); Si,j ; Sk,ℓ od,Eff (αi,j , αk,ℓ ); S ′′ for some i, j, k, ℓ and S ′′ ,E.The initial configuration of η is < S, σ >. Let < R′ , σ ′ > be the lastconstructed configuration of η and let < S ′ , σ ′ > → < T, σ ′′ > be thecurrently analyzed transition of ξ.(a) If S ′ is of the form 1, then we obtain the next configuration of η byactivating in < R′ , σ ′ > the process Si so that it executes the actionperformed in < S ′ , σ ′ > → < T, σ ′′ > , by using transition rule (xvii)introduced in Section 7.2.(b) If S ′ is of the form 2 and T is of the form 3, then we obtain the next configuration of η by activating in < R′ , σ ′ > processes Si and Sk so that theytake part in a communication between αi,j and αk,l , by using transitionaxiom (xxv) introduced in the previous section.

Let the resulting statebe τ . In this case the next configuration of ξ is < T, σ ′′ > → < S ′′ , τ >and we skip its analysis.(c) If S ′ is of the form 2 and T is of the form 4, then we obtain the nextk configurations of η, where k ∈ {0, . . ., n}, by activating inthe orderVmidetermined by their indices those processes Si for which σ |= j=1¬Bi,jholds (k denotes the total number of such processes). All these processesexit their main loops; so for each of them we use transition axiom (xxiv)introduced in the previous section.We first prove that a sequence so constructed is indeed a computationof S.

To this end we need to check that adjacent configurations form legaltransitions. Case (a) is clear. For case (b) it suffices to note that the transition< S ′ , σ ′ > → < T, σ ′′ > in ξ could take place only when σ ′ |= Bi,j ∧ Bk,ℓ ;thus condition 1 for using transition axiom (xxv) is satisfied.Finally, case (c) arises when the transition < S ′ , σ ′ > → < T, σ ′′ > consists of the main loop exit within T (S). By assumption, ξ properly terminates.By construction, for each activated process Si the corresponding conditionfor using transition axiom (xxiv) is satisfied.In the above construction the case when S ′ is of the form 3 does not arisebecause in case (b) we skipped the analysis of one transition.Thus η is a computation of S and by construction it is a good one.To see that ξ and η are 1-equivalent, notice that conditions (i), (iv) and (v)are already satisfied. Moreover, if in case (c) σ |= TERM holds, then j = nso all processes S1 , .

. ., Sn exit their main loops and η terminates. Also, if in11.3 Transformation into Nondeterministic Programs387case (c) σ |= ¬TERM holds, then η ends in a deadlock. Thus conditions (ii)and (iii) are also satisfied.We have thus established the first of the two claims formulated at thebeginning of this step. The second claim follows by noticing that the aboveconstruction in fact establishes a 1-1 correspondence between all computations of T (S) and all good computations of S.Step 3 We define a notion of equivalence between the computations of S.Let η and ξ be computations of S.We say that η and ξ are 2-equivalent if(i)(ii)(iii)(iv)η and ξ start in the same state,for all states σ, η terminates in σ iff ξ terminates in σ,η ends in a failure or is infinite iff ξ ends in a failure or is infinite,for all states σ, η ends in a deadlock with state σ iff ξ ends in a deadlockwith state σ.For example, if η and ξ start in the same state, η ends in a failure and ξis infinite, then η and ξ are 2-equivalent.Step 4 We prove that every computation of S is 2-equivalent to a goodcomputation of S.First, we define a number of auxiliary concepts concerning computationsof S.

Let ξ be a computation of S and let C be a configuration in ξ. Denoteby ξ[C] the prefix of ξ ending in C.We say that a process Si is passive after C in ξ if it is not activated in ξafter C. Note that Si is passive after C in ξ iff• for a subprogram R of Si , in every configuration of ξ after C, the ithprocess is of the form at(R, Si ).We say that a process Si is abandoned in ξ if for some configuration C inξ• Si is passive after C in ξ,• i is the least index in {1, .

. . , n} such that a private action of Si can beexecuted in C.Let C(Si ) be the first such configuration in ξ. Note that C(Si ) is not the lastconfiguration of ξ.Consider two processes Si and Sj that are abandoned in ξ. We say thatSi is abandoned before Sj in ξ if C(Si ) occurs in ξ before C(Sj ).We now define an operation on computations of S. Let ξ be such a computation and assume that Si is a process that is abandoned in ξ.

A computationη of S is obtained by inserting a step of Si in ξ as follows. Denote C(Si ) byiC. Suppose that C → D for some D.38811 Distributed ProgramsiIf D is a failure, then η is defined as ξ[C] followed by the transition C → D.Otherwise, let ξ ′ be the suffix of ξ starting at the first configuration of ξafter C. Perform the following two steps:• In all configurations of ξ ′ , change the ith process to the ith process of D,• in all states of ξ ′ change the values of the variables in change(Si ) to theirvalues in the state of D.Let γ be the resulting computation. η is now defined as ξ[C] followed byiC → D followed by γ.It is easy to see that due to disjointness of the processes, η is indeed acomputation of S that starts in the same state as ξ (see Exercise 11.3).We call a computation of S almost good if no process Si is abandoned init.

Характеристики

Список файлов книги