Processes are in the Eye of the Beholder

Leslie Lamport December 25, 1994 revised January 16, 1996

ii \begin{matrix}c \\ ◯ \end{matrix}Digital Equipment Corporation 1994

This work may not be copied or reproduced in whole or in part for any commercial purpose. Permission to copy in whole or in part without payment of fee is granted for nonprofit educational and research purposes provided that all such whole or partial copies include the following: a notice that such copying is by permission of the Systems Research Center of Digital Equipment Corporation in Palo Alto, California; an acknowledgment of the authors and individual contributors to the work; and all applicable portions of the copyright notice. Copying, reproducing, or republishing for any other purpose shall require a license with payment of fee to the Systems Research Center. All rights reserved. iv Author’s Abstract

A two-process algorithm is shown to be equivalent to an N -process one, illustrating the insubstantiality of processes. A formal equivalence proof in TLA (the Temporal Logic of Actions) is sketched. vi

Contents

1 Introduction 1 2 The Algorithm in TLA 3 3 The Proof 8

3.1 Step 1: Removing the Process Structure . . . . . . . . . . . . 9 3.2 Step 2: Adding History Variables . . . . . . . . . . . . . . . . 12 3.3 Step 3: Equivalence of Φ_{2}^{h} and Φ_{N}^{h} . . . . . . . . . . . . . . . 12

4 Further Remarks 17 A Proof of the Theorem 19 B Proof of Lemma 1 21 References 24 viii

1 Introduction

Processes are often taken to be the fundamental building blocks of concurrency. A concurrent algorithm is traditionally represented as the composition of processes. We show by an example that processes are an artifact of how an algorithm is represented. The difference between a two-process representation and a four-process representation of the same algorithm is no more fundamental than the difference between 2 + 2 and 1 + 1 + 1 + 1.

Our example is a fifo ring buffer, pictured in Figure 1. The ith input value received on channel in is stored in buf [i−1 mod N ], until it is sent on channel out. Input and output may occur concurrently, but input is enabled only when the buffer is not full, and output is enabled only when the buffer is not empty.

Figure 2 shows a representation of the ring buffer as a two-process program in a CSP-like language [2]. (We ignore CSP’s termination convention; the loops are assumed never to terminate.) The variables p and g record the number of values received on channel in by the Receiver process and sent on channel out by the Sender process, respectively. Declaring p and g to be internal means that their values are not externally visible, so a compiler is free to implement them any way it can, or to eliminate them entirely.

The intuitive meaning of this program should be clear to readers acquainted with CSP. We will not attempt to give a rigorous meaning to the program text. Programming languages evolved as a method of describing algorithms to compilers, not as a method for reasoning about them. We do not know how to write a completely formal proof that two programminglanguage representations of the ring buffer are equivalent. In Section 2, we represent the program formally in TLA, the Temporal Logic of Actions [5]. Figure 2 will serve only as an intuitive description of the TLA formula.

Figure 3 shows another representation of the ring buffer, where IsNext

buf [0] ; buf [1] ; ⋮ ; buf [N −1]

in

out

Figure 1: A ring buffer. in, out : channel of Value buf array 0 . . N −1 of Value p, g : internal Natural initially 0

Receiver :: ∗\left[{p − g ≠ N → in ? buf [p mod N ]; \atop p := p +1}\right]

||

Sender :: ∗\left[{p − g ≠ 0 → out ! buf [g mod N ]; \atop g := g +1}\right]

Figure 2: The ring buffer, represented in a CSP-like language.

in, out : channel of Value buf array 0 . . N −1 of Value pp, gg : internal array 0 . . N −1 of {0, 1} initially 0

Buffer(i : 0 . . N −1) ::

∗[\begin{matrix}empty : & IsNext(pp, i) & → & in ? buf [i]; \\ & & & pp[i] := 1 − pp[i] ; \\ full : & IsNext(gg, i) & → & out ! buf [i]; \\ & & & gg[i] := 1 − gg[i] \end{matrix} ]

Figure 3: Another representation of the ring buffer.

p  pp[0] pp[1] pp[2] pp[3]
0  0  0  0  0
1  1  0  0  0
2  1  1  0  0
3  1  1  1  0
4  1  1  1  1
5  0  1  1  1
6  0  0  1  1
⋮  ⋮  ⋮  ⋮  ⋮

Figure 4: The correspondence between values of pp and p, for N = 4.

is defined by

IsNext(r, i) =^{Δ} if i = 0 then r[0] = r[N −1] else r[i] ≠ r[i −1]

This is as an N -process program; the ith process, Buffer(i), reads and writes buf [i]. Variables p and g of the two-process program are replaced by arrays pp and gg of bits. Array elements pp[i] and gg[i] are read and written by process Buffer(i), and are read by process Buffer(i +1 mod N ).

The two programs are equivalent because the values assumed by pp and gg in the N -process program correspond directly to the values assumed by p and g in the two-process one. The correspondence between pp and p is shown in Figure 4 for N = 4. A boxed number in the pp[i] column indicates that IsNext(pp, i) equals true. The correspondence between gg and g is the same.

It is not hard to argue informally that the two programs are equivalent. Formalizing this argument should be as straightforward as proving formally that 222 + 222 equals 111 + 111 + 111 + 111. But, even if straightforward, a completely formal proof of either result from first principles is not trivial. In Section 3, we sketch a formal TLA proof that the two versions of the ring buffer are equivalent.

2 The Algorithm in TLA

We now write the TLA formulas that describe the programs of Figures 2 and 3. The program texts do not tell us what liveness properties are assumed. To make the example more interesting, we assume no liveness properties for sending values on the in channel, but we require that every value received in the buffer be eventually sent on the out channel. For the two-process program, this means assuming fairness for the Sender, but not for the Receiver. For the N -process program, it means assuming fairness for the full action of each process, but not for the empty action.

The program texts also do not determine the grain of atomicity. For simplicity, we assume that an entire guarded command is a single atomic operation. Thus, evaluating a guard and executing the subsequent communication and assignment statements is taken to be an indivisible step.

We give an interleaving representation of the ring buffer—one in which sending and receiving are represented by distinct atomic actions. In Section 4, we describe how the specifications and proofs could be written in terms of a noninterleaving representation that allows values to be sent and received simultaneously.

We use the following notation: N is the set of natural numbers; Z_{m} is the set {0, …, m−1}; square brackets denote function application; [S → T ] is the set of functions with domain S and range a subset of T ; [i ∈ S ↦ e] is the function f with domain S such that f [i] = e for all i ∈ S; [f except ![i] = e] is the function f̂ that is the same as f except f̂[i] = e; angle brackets enclose tuples; t[i] is the ith component of tuple t, so ⟨v, w ⟩[2] = w; and S \T is the set of elements in S that are not in T .

A TLA formula is an assertion about behaviors, which are sequences of states. Steps (pairs of successive states) in a behavior are described by actions, which are boolean-valued expressions containing primed and unprimed variables; unprimed variables refer to the old state and primed variables refer to the new state. To describe CSP-style communication, we represent a channel by a variable and represent the sending of a value by a change to that variable. We define Channel(V ) to be the set of legal values of a channel of type V , and Comm(v, c) to be the action that represents communicating a value v on channel c. The actual definitions, given below, are irrelevant; we require only that a Comm(v, c) action changes c, if v ∈ V and c ∈ Channel(V ).

Channel(V ) =^{Δ} V × Z_{2}
Comm(v, c) =^{Δ} c′ = ⟨v, 1 − c[2]⟩

The TLA formula Π_{2} that represents the two-process program is defined in Figure 5. We now explain that definition.

Type2 =^{Δ} ∧ p, g ∈ N

∧ buf ∈ [Z_{N} → Value] ∧ in, out ∈ Channel(Value)

UnB(i) =^{Δ} [j ∈ Z_{N} \{i} ↦ buf [j ]]

Rcv =^{Δ} ∧ p − g ≠ N

∧ p′ = p + 1

∧ Comm(buf′[p mod N ], in)

∧ unchanged ⟨g, out, UnB(p mod N )⟩

Snd =^{Δ} ∧ p − g ≠ 0

∧ g′ = g + 1

∧ Comm(buf [g mod N ], out) ∧ unchanged ⟨p, buf , in ⟩

Φ_{2} =^{Δ} ∧ □Type2

∧ (p = 0) ∧ □[Rcv]_{⟨p,buf ,in ⟩}
∧ (g = 0) ∧ □[Snd]_{⟨g,out ⟩} ∧ WF_{⟨g,out ⟩}(Snd)
Π_{2}  =^{Δ} ∃ ∃ ∃ ∃ ∃ ∃ p, g : Φ_{2}

Figure 5: The TLA formula Π_{2} representing the two-process program.

A list of expressions bulleted by ∧ denotes their conjunction; indentation is used to eliminate parentheses. If formula F is written as such a list, then F .i is its ith conjunct—for example, Rcv.2 is p′ = p+1. A similar convention is used for disjunctions.

The state predicate Type2 asserts that each variable has the correct type. (The array variable buf of the programming language representation becomes a variable whose value is a function.) The type declarations of the two-process program are represented by the TLA formula □Type2, which asserts that Type2 equals true in all states of the behavior.

Action Snd describes a step of the Sender process; it can occur only when p − g ≠ 0, and it increments g by 1, communicates buf [g mod N ] on channel out, and leaves p, buf , and in unchanged (unchanged v is defined to equal v′ = v). Similarly, action Rcv describes a step of the Receiver process. The conjunct Rcv.3 asserts that the value buf′[p mod N ] (the new value of buf [p mod N ]) is communicated on channel in. The state function UnB(i) is defined so that, if it is unchanged, then buf [j ] is unchanged for all j ≠ i. Thus, Rcv asserts that the new value of buf [p mod N ] is the value communicated on channel in, and that buf [j ] remains unchanged for all j ≠ p mod N .

Formula Φ_{2}.2 describes the Receiver process. It asserts that p is initially 0, and that every step is a Rcv step or leaves p, buf , and in unchanged ([A]_{v} is defined to equal A ∨ (v′ = v)). Steps that leave p, buf , and in unchanged represent steps of the Receiver’s environment—either steps of the Sender or steps of the entire program’s environment. The conjunct Φ_{2}.3 similarly represents the Sender process. The formula WF_{⟨g,out ⟩}(Snd) asserts weak fairness of the Snd action. In general, WF_{v}(A) asserts that if action ⟨A⟩_{v} (defined to equal A ∧ (v′ ≠ v)) remains continuously enabled, then an ⟨A⟩_{v} step must eventually occur.

Formula Φ_{2} is the conjunction of the specifications of the two processes with the formula asserting type correctness. It describes the two-process program with p and g visible. The complete program specification Π_{2} is obtained by hiding p and g. In logic, hiding means existential quantification; in temporal logic, flexible variables (distinct from rigid variables like N ) are hidden with the temporal existential quantifier ∃ ∃ ∃ ∃ ∃ ∃.

The conjunct □Type2 of Φ_{2} makes type correctness an explicit part of the specification. We put type-correctness assumptions in our specifications to make them as much like Figures 2 and 3 as possible. However, to avoid errors, it is usually better to let type correctness be a consequence of the specification. We could rewrite Φ_{2} as follows to eliminate the conjunct □Type2. The conjunct □Type2.1 is already redundant because it is implied by Φ_{2}.2 ∧ Φ_{2}.3. We can eliminate □Type2.3 by making Type2.3 part of the initial condition, since Type2.3 ∧ Φ_{2}.2 ∧ Φ_{2}.3 implies □Type2.3. (The proof requires the fact that c ∈ Channel(V ) and Comm(v, c) imply c′ ∈ Channel(V ).) We can eliminate □Type2.2 in the same way, if we modify Rcv so it leaves the domain of buf unchanged.

The TLA formula Π_{N} that represents the N -process program is defined in Figure 6. There are two things in this definition that merit further explanation. First, we introduce an array ctl to represent the control state. The value of ctl[i] equals “empty” if control in process Buffer(i) is at the point labeled empty, and it equals “full” if control is at full. Second, we introduce an action NotProc(i) that has no obvious counterpart in Figure 3 or in Π_{2}. The specifications of the two processes in Figure 2 are especially simple because each variable is changed by an action of only one of the processes. For example, a step of the Sender’s environment can be characterized as any step that leaves g and out unchanged. We can think of g and out as belonging to the Sender. In the N -process program, pp[i], gg[i], and ctl[i] belong to Buffer(i). However, in and out don’t belong to any single process; they can be changed by a step of any of the N pro-TypeN =^{Δ}

∧ pp, gg ∈ [Z_{N} → Z_{2}] ∧ ctl ∈ [Z_{N} → {“empty”, “full”}] ∧ buf ∈ [Z_{N} → Value] ∧ in, out ∈ Channel(Value)

Fill(i)

=^{Δ} ∧ ctl[i] = “empty” ∧ IsNext(pp, i) ∧ ctl′ = [ctl except ![i] = “full”] ∧ pp′ = [pp except ![i] = 1 − pp[i]] ∧ Comm(buf′[i], in) ∧ unchanged ⟨gg, out, UnB(i)⟩

Empty(i)

=^{Δ} ∧ ctl[i] = “full” ∧ IsNext(gg, i) ∧ ctl′ = [ctl except ![i] = “empty”] ∧ gg′ = [gg except ![i] = 1 − gg[i]] ∧ Comm(buf [i], out) ∧ unchanged ⟨pp, in, buf ⟩

NotProc(i)

=^{Δ} ∧ unchanged ⟨pp[i], gg[i], ctl[i], buf [i]⟩ ∧ IsNext(pp, i) ⇒ unchanged in ∧ IsNext(gg, i) ⇒ unchanged out

varN =^{Δ} ⟨pp, gg, ctl, buf , in, out ⟩

Φ_{N} =^{Δ}

∧ □TypeN ∧ ∀ i ∈ Z_{N} : ∧ (pp[i] = gg[i] = 0) ∧ (ctl[i] = “empty”) ∧ □[Fill(i) ∨ Empty(i) ∨ NotProc(i)]_{varN} ∧ WF_{varN} (Empty(i))

Π_{N}  =^{Δ} ∃ ∃ ∃ ∃ ∃ ∃ pp, gg, ctl : Φ_{N}

Figure 6: The TLA formula Π_{N} representing the N -process program. cesses. The variable in belongs to Buffer(i) only when IsNext(pp, i) equals true, and out belongs to Buffer(i) only when IsNext(gg, i) equals true. Action NotProc(i) characterizes steps of Buffer(i)’s environment, which is allowed to change in when IsNext(pp, i) equals false, and to change out when IsNext(gg, i) equals false. The subscript in □[…]_{varN} allows steps of the entire program’s environment that leave all the variables unchanged. It is semantically superfluous, since NotProc(i) already allows such steps, but the syntax of TLA requires some subscript.

3 The Proof

We now give a hierarchically structured proof that Π_{2} and Π_{N} are equivalent [4]. The proof is completely formal, meaning that each step is a mathematical formula. English is used only to explain the low-level reasoning. The entire proof could be carried down to a level at which each step follows from the simple application of formal rules, but such a detailed proof is more suitable for machine checking than human reading. Our complete proof, with “Q.E.D.” steps and low-level reasoning omitted, appears in Appendix A.

The correctness of the algorithm rests on simple properties of integers and of the mod operator. We need the following lemma, where the bit array Rep(m) used to represent the integer m is defined by

Rep(m) =^{Δ} [i ∈ Z_{N} ↦ if i < m mod 2N ≤ i + N then 1 else 0]

The lemma is proved in Appendix B. We assume throughout that N is a positive integer.

Lemma 1 If m ∈ N and i ∈ Z_{N} , then

1. IsNext(Rep(m), i) ≡ (i = m mod N )

2. IsNext(Rep(m), i) ⇒ Rep(m + 1) = [Rep(m) except ![i] = 1 − Rep(m)[i]]

For temporal reasoning, we use the following TLA rules from Figure 5 of [5].

Theorem Π_{2} ≡ Π_{N}

1a. Φ_{2} ≡ Φ_{2}^{u} b. Φ_{N} ≡ Φ_{N}^{u} 2a. Φ_{2}^{u} ≡ ∃ ∃ ∃ ∃ ∃ ∃ pp, gg, ctl : Φ_{2}^{h} b. Φ_{N}^{u} ≡ ∃ ∃ ∃ ∃ ∃ ∃ p, g : Φ_{N}^{h}

3. Φ_{2}^{h} ≡ Φ_{N}^{h}

4. Q.E.D.

Proof: Π_{2} ≡ ∃ ∃ ∃ ∃ ∃ ∃ p, g : Φ_{2}^{u}  step 1a and the definition of Π_{2} ≡ ∃ ∃ ∃ ∃ ∃ ∃ p, g, pp, gg, ctl : Φ_{2}^{h} step 2a ≡ ∃ ∃ ∃ ∃ ∃ ∃ p, g, pp, gg, ctl : Φ_{N}^{h} step 3 ≡ ∃ ∃ ∃ ∃ ∃ ∃ pp, gg, ctl, p, g : Φ_{N}^{h} simple logic ≡ ∃ ∃ ∃ ∃ ∃ ∃ pp, gg, ctl : Φ_{N}^{u}  step 2b ≡ Π_{N}  step 1b and the definition of Π_{N}

Figure 7: The high-level structure of the proof.

(This version of TLA2 generalizes the one in [5].)

STL2. ⊢ □F ⇒ F  STL3. ⊢ □□F ≡ □F
STL4. \frac{F ⇒ G}{□F ⇒ □G}  STL5. ⊢ □(F ∧ G) ≡ (□F ) ∧ (□G)
INV1. \frac{I ∧ [N ]_{f} ⇒ I′}{I ∧ □[N ]_{f} ⇒ □I} INV2. ⊢ □I ⇒ (□[N ]_{f} ≡ □[N ∧ I ∧ I′]_{f} )

TLA2. \frac{P ∧ (∀ i ∈ S : [A_{i}]_{fi} ) ⇒ Q ∧ [B]_{g}}{□P ∧ (∀ i ∈ S : □[A_{i}]_{fi} ) ⇒ □Q ∧ □[B]_{g}}

The high-level structure of the proof is shown in Figure 7. The proofs of steps 1–3, and the definitions of Φ_{2}^{u}, Φ_{N}^{u}, Φ_{2}^{h}, and Φ_{N}^{h}, are given in the following sections.

3.1 Step 1: Removing the Process Structure

Formulas Φ_{2}^{u} and Φ_{N}^{u} are defined in Figure 8. They can be thought of as uniprocess versions of the two algorithms. We obtained them by rewriting Φ_{2} and Φ_{N} as formulas with a single next-state relation, instead of as the conjunction of processes.

Step 1a is proved as follows.

1a. Φ_{2} ≡ Φ_{2}^{u}

1a.1. Type2 ⇒ ([Rcv]_{⟨p,buf ,in ⟩} ∧ [Snd]_{⟨g,out ⟩} ≡ [Rcv ∨ Snd]_{var2}) Proof: Given below.

var2 =^{Δ} ⟨p, g, buf , in, out ⟩

Φ_{2}^{u} =^{Δ} ∧ □Type2

∧ (p = 0) ∧ (g = 0)
∧ □[Rcv ∨ Snd]_{var2}
∧ WF_{⟨g,out ⟩}(Snd)

Φ_{N}^{u}

=^{Δ}
∧ □TypeN
∧ ∀ i ∈ Z_{N} : (pp[i] = gg[i] = 0) ∧ (ctl[i] = “empty”)
∧ □[∃ i ∈ Z_{N} : Fill(i) ∨ Empty(i)]_{varN}
∧ ∀ i ∈ Z_{N} : WF_{varN} (Empty(i))
Figure 8: Formulas Φ_{2}^{u} and Φ_{N}^{u}.

1a.2. □Type2 ⇒ (□[Rcv]_{⟨p,buf ,in ⟩} ∧ □[Snd]_{⟨g,out ⟩} ≡ □[Rcv ∨ Snd]_{var2})

Proof: Step 1a.1 and rule TLA2. 1a.3. Q.E.D.

Proof: Step 1a.2 and the definitions of Φ_{2} and Φ_{2}^{u}.

Step 1a.1 is proved by showing that Type2 implies

[Rcv]_{⟨p,buf ,in ⟩} ∧ [Snd]_{⟨g,out ⟩}

≡ by definition of [A]_{v} ∧ Rcv ∨ (⟨p, buf , in ⟩′ = ⟨p, buf , in ⟩) ∧ Snd ∨ (⟨g, out ⟩′ = ⟨g, out ⟩)

≡ by propositional logic ∨ Rcv ∧ (⟨g, out ⟩′ = ⟨g, out ⟩) ∨ Snd ∧ (⟨p, buf , in ⟩′ = ⟨p, buf , in ⟩) ∨ Rcv ∧ Snd ∨ (⟨g, out ⟩′ = ⟨g, out ⟩) ∧ (⟨p, buf , in ⟩′ = ⟨p, buf , in ⟩)

≡ ∨ Rcv  Rcv implies ⟨g, out ⟩′ = ⟨g, out ⟩ ∨ Snd  Snd implies ⟨p, buf , in ⟩′ = ⟨p, buf , in ⟩ ∨ false  Type2 ∧ Rcv implies p′ ≠ p, and Snd implies p′ = p ∨ var2′ = var2 ⟨v_{1}, …, v_{m} ⟩′ = ⟨v_{1}, …, v_{m} ⟩ iff (v′_{1} = v_{1}) ∧ … ∧ (v m^{′} = v_{m})

≡ [Rcv ∨ Snd]_{var2} by definition of [A]_{v}

All of the nontemporal steps in our proof can be reduced to this kind of algebraic manipulation. From now on, we just sketch such proofs and leave the detailed calculations to the reader.

The proof of step 1b is similar to that of step 1a, but it is a bit more difficult because it requires an invariant InvN , which asserts that the arrays pp and gg are representations of natural numbers.

InvN =^{Δ} (∃ m ∈ N : pp = Rep(m)) ∧ (∃ m ∈ N : gg = Rep(m))

1b. Φ_{N} ≡ Φ_{N}^{u}

1b.1a. Φ_{N} ⇒ □InvN

b. Φ_{N}^{u} ⇒ □InvN

Proof: Described below. 1b.2. TypeN ∧ InvN ⇒

[∃ i ∈ Z_{N} : Fill(i) ∨ Empty(i)]_{varN} ≡

∀ i ∈ Z_{N} : [Fill(i) ∨ Empty(i) ∨ NotProc(i)]_{varN} Proof: If i ≠ j , then TypeN implies that Fill(i) ∧ Fill(j ), Empty(i) ∧ Empty(j ), and Fill(i)∧Empty(j ) are all false; and TypeN ∧InvN implies Fill(i) ⇒ NotProc(j ) and Empty(i) ⇒ NotProc(j ). By Lemma 1.1, TypeN ∧ InvN implies (∀ i ∈ Z_{N} : NotProc(i)) ≡ (varN′ = varN ).

1b.3. □TypeN ∧ □InvN ⇒

□[∃ i ∈ Z_{N} : Fill(i) ∨ Empty(i)]_{varN} ≡

∀ i ∈ Z_{N} : □[Fill(i) ∨ Empty(i) ∨ NotProc(i)]_{varN} Proof: Step 1b.2 and rule TLA2.

1b.4 Q.E.D.

Proof: Steps 1b.1 and 1b.3 and the definitions of Φ_{N} and Φ_{N}^{u}.

Steps 1b.1a and 1b.1b are standard invariance properties; 1b.1a is proved as follows.

1b.1a Φ_{N} ⇒ □InvN

1b.1a.1 TypeN ∧ (∀ i ∈ Z_{N} : pp[i] = gg[i] = 0) ⇒ InvN

Proof: Rep(0) = [i ∈ Z_{N} ↦ 0]

1b.1a.2 ∧ InvN

∧ [TypeN ∧ (∀ i ∈ Z_{N} : Fill(i) ∨ Empty(i) ∨ NotProc(i))]_{varN} ⇒ InvN′ 1b.1a.2.1. InvN ∧ TypeN ∧ (i ∈ Z_{N} ) ∧ Fill(i) ⇒ InvN′ 1b.1a.2.2. InvN ∧ TypeN ∧ (i ∈ Z_{N} ) ∧ Empty(i) ⇒ InvN′ 1b.1a.2.3. InvN ∧ TypeN ∧ (∀ i ∈ Z_{N} : NotProc(i)) ⇒ InvN′ 1b.1a.2.4. InvN ∧ (varN′ = varN ) ⇒ InvN′ 1b.1a.2.5. Q.E.D.

Proof: Steps 1b.1a.2.1–1b.1a.2.4.

1b.1a.3.

∧ TypeN ∧ (∀ i ∈ Z_{N} : pp[i] = gg[i] = 0) ∧ □TypeN ∧ □[∀ i ∈ Z_{N} : Fill(i) ∨ Empty(i) ∨ NotProc(i)]_{varN} ⇒ □InvN Proof: Steps 1b.1a.1 and 1b.1a.2 and rules INV1 and INV2.

1b.1a.4. Q.E.D. Proof: Step 1b.1a.3 and rule TLA2, since (∀ i : [A_{i}]_{v}) ≡ [∀ i : A_{i}]_{v}.

Steps 1b.1a.2.1 and 1b.1a.2.2 are proved using Lemma 1.2; steps 1b.1a.2.3 and 1b.1a.2.4 follow because their hypotheses imply pp′ = pp and gg′ = gg. As indicated in the appendix, the proof of step 1b.1b is similar.

3.2 Step 2: Adding History Variables

Formulas Φ_{2}^{h} and Φ_{N}^{h} are defined in Figure 9, which also defines their safety parts, Φ_{2}^{hS} and Φ_{N}^{hS}. We obtained Φ_{2}^{h} by adding pp, gg, and ctl as history variables to Φ_{2}^{u}; and we obtained Φ_{N}^{h} by adding p and g as history variables to Φ_{N}^{u}. In general, adding an auxiliary variable a to a formula F means writing a formula F^{a} such that F ≡ ∃ ∃ ∃ ∃ ∃ ∃ a : F^{a}. A history variable is an auxiliary variable that records information from previous states. It is added by using the following lemma, which can be deduced from the results in [1]. Step 2 is easily proved by repeated application of this lemma.

Lemma 2 (History Variable) If h and h′ do not occur in Init, A_{i}, B_{j} , v, or f, and h′ does not occur in g_{i}, for all i ∈ I and j ∈ J , then

Init ∧ □[∃ i ∈ I : A_{i}]_{v} ∧ (∀ j ∈ J : WF_{v}(B_{j} ))
≡ ∃ ∃ ∃ ∃ ∃ ∃ h : ∧ Init ∧ (h = f ) ∧ □[∃ i ∈ I : A_{i} ∧ (h′ = g_{i})]_{⟨h,v ⟩} ∧ ∀ j ∈ J : WF_{v}(B_{j} )

3.3 Step 3: Equivalence of Φ_{2}^{h} and Φ_{N}^{h}

In the two-process algorithm, p and g are the actual internal variables, while pp, gg, and ctl are history variables. The situation is reversed in the N - process algorithm. Step 3 involves showing that the history variables of one algorithm behave like the internal variables of the other. Its proof uses the following formulas, where Inv will be shown to be an invariant of both Φ_{2}^{h} and Φ_{N}^{h}.

IsFull(g, p, i) =^{Δ} ∃ m ∈ N : (g ≤ m < p) ∧ (i = m mod N )

Inv =^{Δ} ∧ pp = Rep(p) ∧ gg = Rep(g) ∧ ctl = [i ∈ Z_{N} ↦ if IsFull(g, p, i) then “full” else “empty”] ∧ 0 ≤ p − g ≤ N

The high-level structure of the proof is:

Init =^{Δ} ∧ p = g = 0

∧ pp = gg = [i ∈ Z_{N} ↦ 0]
∧ ctl = [i ∈ Z_{N} ↦ “empty”]
Type =^{Δ} Type2 ∧ TypeN
var =^{Δ} ⟨pp, gg, ctl, p, g, buf , in, out ⟩

HRcv

=^{Δ}

∧ Rcv

∧ pp′ = [pp except ![p mod N ] = 1 − pp[p mod N ]] ∧ ctl′ = [ctl except ![p mod N ] = “full”] ∧ unchanged gg

HSnd

=^{Δ}

∧ Snd

∧ gg′ = [gg except ![g mod N ] = 1 − gg[g mod N ]] ∧ ctl′ = [ctl except ![g mod N ] = “empty”] ∧ unchanged pp

Φ_{2}^{hS}

=^{Δ}
∧ □Type
∧ Init
∧ □[HRcv ∨ HSnd]_{var}
Φ_{2}^{h} =^{Δ} Φ_{2}^{hS} ∧ WF_{⟨g,out ⟩}(Snd)

HFill(i)

=^{Δ}

∧ Fill(i) ∧ p′ = p + 1 ∧ unchanged g

HEmpty(i)

=^{Δ}

∧ Empty(i) ∧ g′ = g + 1 ∧ unchanged p

Φ_{N}^{hS}

=^{Δ}
∧ □Type
∧ Init
∧ □[∃ i ∈ Z_{N} : HFill(i) ∨ HEmpty(i)]_{var}
Φ_{N}^{h} =^{Δ} Φ_{N}^{hS} ∧ (∀ i ∈ Z_{N} : WF_{varN} (Empty(i)))
Figure 9: Formulas Φ_{2}^{h} and Φ_{N}^{h}.

3. Φ_{2}^{h} ≡ Φ_{N}^{h}

3.1a. Type ∧ Inv ⇒ (HRcv ≡ ∃ i ∈ Z_{N} : HFill(i))

b. Type ∧ Inv ⇒ (HSnd ≡ ∃ i ∈ Z_{N} : HEmpty(i)) 3.2. [Type ∧ Inv ∧ (HRcv ∨ HSnd)]_{var} ≡

[Type ∧ Inv ∧ (∃ i ∈ Z_{N} : HFill(i) ∨ HEmpty(i))]_{var} 3.3a. Φ_{2}^{hS} ⇒ □Inv

b. Φ_{N}^{hS} ⇒ □Inv 3.4. Φ_{2}^{hS} ≡ Φ_{N}^{hS} 3.5. □Inv ∧ Φ_{N}^{hS} ⇒ (WF_{⟨g,out ⟩}(Snd) ≡ (∀ i ∈ Z_{N} : WF_{varN} (Empty(i)))) 3.6. Q.E.D.

Proof: Immediate from steps 3.3–3.5.

Steps 3.1 and 3.2 are (nontemporal) action formulas. They make it intuitively clear why the two transformed formulas are equivalent. Step 3.1a is proved as follows.

3.1a. Type ∧ Inv ⇒ (HRcv ≡ ∃ i ∈ Z_{N} : HFill(i))

3.1a.1 Type ∧ Inv ⇒ (HRcv ≡ HFill(p mod N ))

3.1a.1.1. Type ∧ Inv ⇒ ((p − g ≠ N ) ≡ (ctl[p mod N ] = “empty”))

Proof: Arithmetic reasoning and the definition of IsFull.

3.1a.1.2. Type ∧ Inv ⇒ IsNext(pp, p mod N )

Proof: Lemma 1.1.

3.1a.1.3. Q.E.D.

Proof: Steps 3.1a.1.1 and 3.1a.1.2, and the definitions of HRcv and HFill.

3.1a.2 Type ∧ Inv ⇒ (HFill(p mod N ) ≡ (∃ i ∈ Z_{N} : HFill(i))) Proof: By Lemma 1.1, Type ∧ Inv implies IsNext(pp, p mod N ) and ¬IsNext(pp, i), if i ∈ Z_{N} and i ≠ (p mod N ).

3.1a.3 Q.E.D.

Proof: Steps 3.1a.1 and 3.1a.2.

As indicated in the appendix, the proof of 3.1b is analogous. Step 3.2 follows easily from step 3.1.

Step 3.3 asserts that Inv is an invariant of both formulas; its proof is a standard invariance argument.

3.3a. Φ_{2}^{hS} ⇒ □Inv

b. Φ_{N}^{hS} ⇒ □Inv

3.3.1. Init ⇒ Inv Proof: Rep(0) equals [i ∈ Z_{N} ↦ 0] and IsFull(0, 0, i) ≡ false, for all i ∈ Z_{N} .

3.3.2a. Inv ∧ [Type ∧ (HRcv ∨ HSnd)]_{var} ⇒ Inv′

b. Inv ∧ [Type ∧ (∃ i ∈ Z_{N} : HFill(i) ∨ HEmpty(i))]_{var} ⇒ Inv′

Proof: Given below. 3.3.3. Q.E.D.

Proof: Steps 3.3.1 and 3.3.2, and rules INV1 and INV2.

Step 3.3.2 asserts that the next-state actions leave Inv invariant. The proof of 3.3.2a is:

3.3.2a. Inv ∧ [Type ∧ (HRcv ∨ HSnd)]_{var} ⇒ Inv′

3.3.2a.1 Inv ∧ Type ∧ HRcv ⇒ Inv′ Proof: Assume Inv ∧ Type ∧ HRcv. Then Inv.1′ is immediate because p′ = p and pp′ = pp; Inv.2′ follows from Lemma 1.2; Inv.4′ follows from Inv.4, since HRcv implies p′ = p + 1, g′ = g, and p − g ≠ N ; and Inv.3′ holds because

IsFull(g′, p′, i) ≡ by definition of HRcv

IsFull(g, p + 1, i)

≡ by definition of IsFull

∃ m ∈ N : (g ≤ m < p + 1) ∧ (i = m mod N )

≡ by Rcv.1 and Inv.4

if i = p mod N then true else IsFull(g, p, i)

3.3.2a.2 Inv ∧ Type ∧ HSnd ⇒ Inv′

Proof: Similar to the proof of 3.3.2a.1. 3.3.2a.3 Inv ∧ (var′ = var) ⇒ Inv′

Proof: Immediate. 3.3.2a.4 Q.E.D.

Proof: Steps 3.3.2a.1–3.3.2a.3.

Step 3.3.2b follows from steps 3.3.2a and 3.2. This completes the proof of step 3.3.

Steps 3.4 and 3.5, assert the equivalence of the safety and liveness parts of the formulas, respectively. Step 3.4 follows from 3.3 and

□Type ∧ □Inv ⇒ □[HRcv ∨ HSnd]_{var} ≡ □[∃ i ∈ Z_{N} : HFill(i) ∨ HEmpty(i)]_{var}

which follows from step 3.2 and rule TLA2. Step 3.5 has the following high-level proof.

3.5. □Inv ∧ Φ_{N}^{hS} ⇒ (WF_{⟨g,out ⟩}(Snd) ≡ (∀ i ∈ Z_{N} : WF_{varN} (Empty(i))))

3.5.1. □Inv ∧ Φ_{N}^{hS} ⇒ (∀ i ∈ Z_{N} : WF_{varN} (Empty(i))) ≡ WF_{varN} (∃ i ∈ Z_{N} : Empty(i))

3.5.2. □Inv ∧ □Type ∧ □[HRcv ∨ HSnd]_{var} ⇒

WF_{⟨g,out ⟩}(Snd) ≡ WF_{varN} (∃ i ∈ Z_{N} : Empty(i))

3.5.3. Q.E.D.

Proof: Steps 3.5.1 and 3.5.2.

We first consider step 3.5.1. When writing TLA specifications, one often has to choose between asserting fairness of A_{1} ∨ … ∨ A_{m} and asserting fairness of each action A_{i}. The choice becomes a matter of taste when the resulting specifications are equivalent. This is the case if, whenever one of the A_{i} becomes enabled, a step of no other A_{j} can occur before the next A_{i} step. For weak fairness, the equivalence is a consequence of the following result, which can be derived from the TLA proof rules of [5].

Lemma 3 If

Enabled ⟨A_{i} ⟩_{v} ∧ □Inv ∧ □[N ∧ ¬A_{i}]_{v} ⇒ □¬Enabled ⟨A_{j} ⟩_{v}

for all i, j ∈ S with i ≠ j , then

□Inv ∧ □[N]_{v} ⇒ (WF_{v}(∃ i ∈ S : A_{i}) ≡ (∀ i ∈ S : WF_{v}(A_{i})))

We use this lemma to prove step 3.5.1.

3.5.1. □Inv ∧ Φ_{N}^{hS} ⇒

(∀ i ∈ Z_{N} : WF_{varN} (Empty(i))) ≡ WF_{varN} (∃ i ∈ Z_{N} : Empty(i))) 3.5.1.1. Φ_{N}^{hS} ⇒ □[∃ i ∈ Z_{N} : Fill(i) ∨ Empty(i)]_{varN}

Proof: TLA2, since HFill(i) ⇒ Fill(i) and HEmpty(i) ⇒ Empty(i).

3.5.1.2. ∧ i ∈ Z_{N}

∧ IsNext(gg, i) ∧ □(Inv ∧ Type) ∧ □[(∃ j ∈ Z_{N} : Fill(j ) ∨ Empty(j )) ∧ ¬Empty(i)]_{varN} ⇒ □IsNext(gg, i) Proof: By rules INV1 and INV2, since

Inv ∧ Type ∧ (Fill(j ) ∨ Empty(j )) ∧ ¬Empty(i)

implies gg′ = gg, for all i, j ∈ Z_{N} .

3.5.1.3. ∧ (i, j ∈ Z_{N} ) ∧ (i ≠ j )

∧ Enabled ⟨Empty(i)⟩_{varN} ∧ □(Inv ∧ Type) ∧ □[(∃ k ∈ Z_{N} : Fill(k) ∨ Empty(k)) ∧ ¬Empty(i)]_{varN} ⇒ □¬Enabled ⟨Empty(j )⟩_{varN} Proof: Step 3.5.1.2 and rule STL4, since Enabled ⟨Empty(i)⟩_{varN} implies IsNext(gg, i), and Lemma 1.1 implies

Inv ∧ Type ∧ IsNext(gg, i) ⇒ ¬IsNext(gg, j )

for all i, j ∈ Z_{N} with i ≠ j .

3.5.1.4. Q.E.D. Proof: Steps 3.5.1.1 and 3.5.1.3, and Lemma 3.

Finally, we prove 3.5.2, which completes the proof of the theorem.

3.5.2. □Inv ∧ □Type ∧ □[HRcv ∨ HSnd]_{var} ⇒

WF_{⟨g,out ⟩}(Snd) ≡ WF_{varN} (∃ i ∈ Z_{N} : Empty(i)) 3.5.2.1. Inv ∧ Type ∧ [HRcv ∨ HSnd]_{var} ⇒

⟨Snd ⟩_{⟨g,out ⟩} ≡ ⟨∃ i ∈ Z_{N} : Empty(i)⟩_{varN} Proof: By steps 3.1b and 3.2, since Inv ∧ Type ∧ [HRcv ∨ HSnd]_{var} implies ⟨Snd ⟩_{⟨g,out ⟩} ≡ HSnd, and

Inv ∧ Type ∧ [∃ i ∈ Z_{N} : HFill(i) ∨ HEmpty(i)]_{var} implies ⟨∃ i ∈ Z_{N} : Empty(i)⟩_{varN} ≡ (∃ i ∈ Z_{N} : HEmpty(i)).

3.5.2.2. □Inv ∧ □Type ∧ □[HRcv ∨ HSnd]_{var} ⇒

□◇⟨Snd ⟩_{⟨g,out ⟩} ≡ □◇⟨∃ i ∈ Z_{N} : Empty(i)⟩_{varN} Proof: □Inv ∧ □Type ∧ □[HRcv ∨ HSnd]_{var}

⇒ by 3.5.2.1 and rules STL5 and TLA2, since ⟨A⟩_{v} ≡ ¬[¬A]_{v}
□[¬Snd]_{⟨g,out ⟩} ≡ □[¬ ∃ i ∈ Z_{N} : Empty(i)]_{varN}
⇒ ¬□[¬Snd]_{⟨g,out ⟩} ≡ ¬□[¬ ∃ i ∈ Z_{N} : Empty(i)]_{varN}
⇒ by rules STL3, STL4, and STL5
□¬□[¬Snd]_{⟨g,out ⟩} ≡ □¬□[¬ ∃ i ∈ Z_{N} : Empty(i)]_{varN}
⇒ since ◇ ≡ ¬□¬
□◇¬[¬Snd]_{⟨g,out ⟩} ≡ □◇¬[¬ ∃ i ∈ Z_{N} : Empty(i)]_{varN}
⇒ since ⟨A⟩_{v} ≡ ¬[¬A]_{v}
□◇⟨Snd ⟩_{⟨g,out ⟩} ≡ □◇⟨∃ i ∈ Z_{N} : Empty(i))⟩_{varN}

3.5.2.3 □Inv ∧ □Type ∧ □[HRcv ∨ HSnd]_{var} ⇒

□◇¬Enabled ⟨Snd ⟩_{⟨g,out ⟩} ≡

□◇¬Enabled ⟨∃ i ∈ Z_{N} : Empty(i))⟩_{varN} Proof: Rules STL2 (which implies F ⇒ ◇F ), STL4, STL5, and TLA2, since by 3.5.2.1, Inv ∧ Type ∧ [HRcv ∨ HSnd]_{var} implies

Enabled ⟨Snd ⟩_{⟨g,out ⟩} ≡ Enabled ⟨∃ i ∈ Z_{N} : Empty(i))⟩_{varN}

3.5.2.4 Q.E.D.

Proof: Steps 3.5.2.2 and 3.5.2.3, since WF_{v}(A) is defined to equal □◇¬Enabled ⟨A⟩_{v} ∨ □◇⟨A⟩_{v}.

4 Further Remarks

We have proved the equivalence of two different representations of the ring buffer. This is not just an intellectual exercise; the ability to transform an algorithm into a completely different form is important for applying formal methods to real systems. Going from the two-process version to the N - process one reduces the internal state of each process from an unbounded number (p or g) to three bits (pp[i], gg[i], and ctl[i]). As explained in [3], such a transformation enables us to apply model checking to unboundedstate systems.

In retrospect, it is not surprising that programs with different numbers of processes can be equivalent. Multiprocess programs are routinely executed on single-processor computers by interleaving the execution of their processes. The transformation of Φ_{2} and Φ_{N} to Φ_{2}^{u} and Φ_{N}^{u} can be viewed as a formal description of this interleaving.

Using an interleaving representation makes the proof of equivalence a bit simpler, but it is not necessary. The equivalence of noninterleaving representations can be proved as follows. Let RcvNI and SndNI be the actions obtained from Rcv and Snd by removing the unchanged conjuncts and adding the conjunct unchanged UnB(p mod N ) to RcvNI . Replacing Rcv and Snd with RcvNI and SndNI in the definition of Π_{2} yields a noninterleaving representation of the two-process program. Similarly, we get a noninterleaving representation of the N -process program by replacing Fill(i) and Empty(i) with actions FillNI (i) and EmptyNi(i) that have no unchanged conjuncts except the one for UnB(i). In the proof of equivalence, formula Φ_{2}^{u} is changed by replacing its next-state action Rcv ∨ Snd with Rcv ∨Snd ∨(RcvNI ∧SndNI ), and Φ_{N}^{u} is changed by replacing its nextstate action with ∃ i ∈ Z_{N} : Fill(i) ∨ Empty(i) ∨ (FillNI (i) ∧ EmptyNI (i)). Formulas Φ_{2}^{h} and Φ_{N}^{h} are obtained by adding history variables to the new versions of Φ_{2}^{u} and Φ_{N}^{u}. The proof of equivalence is the same as before, except we have to consider the next-state actions’ extra disjuncts. These disjuncts represent the simultaneous sending and receiving of values.

Indivisible state changes are an abstraction; executing an operation of a real program takes time. In TLA, we can represent the concurrent execution of program operations either as successive steps, or as a single step. Which representation we choose is a matter of convenience, not philosophy. We have found that interleaving representations are usually, but not always, more convenient than noninterleaving ones for reasoning about algorithms.

A proof that two algorithms are equivalent can be turned into a derivation of one algorithm from the other. Our proof yields the following derivation, where each equivalence is obtained from the indicated proof step(s).

Π_{2} ≡ ∃ ∃ ∃ ∃ ∃ ∃ : p, g : Φ_{2}^{u}  1a
≡ ∃ ∃ ∃ ∃ ∃ ∃ p, g, pp, gg, ctl : Φ_{2}^{h}  2a

≡ ∃ ∃ ∃ ∃ ∃ ∃ p, g, pp, gg, ctl : Φ_{2}^{h} ∧ □Inv 3.3a
≡ ∃ ∃ ∃ ∃ ∃ ∃ pp, gg, ctl, p, g : Φ_{N}^{h} ∧ □Inv 3.4 and 3.5
≡ ∃ ∃ ∃ ∃ ∃ ∃ pp, gg, ctl, p, g : Φ_{N}^{h}  3.3b
≡ ∃ ∃ ∃ ∃ ∃ ∃ p, g : Φ_{N}^{u}  2b
≡ ∃ ∃ ∃ ∃ ∃ ∃ p, g : Φ_{N}^{u} ∧ □InvN  1b.1b
≡ ∃ ∃ ∃ ∃ ∃ ∃ p, g : Φ_{N} ∧ □InvN  1b.3
≡ Π_{N}  1b.1a

Our derivation uses rules of logic to rewrite formulas. In process algebra [6], analogous transformations are performed by applying algebraic laws. It would be interesting to compare a process-algebraic proof of equivalence of the two ring-buffer programs with our TLA proof.

A Proof of the Theorem

Theorem Π_{2} ≡ Π_{N}

1a. Φ_{2} ≡ Φ_{2}^{u} 1a.1. Type2 ⇒ ([Rcv]_{⟨p,buf ,in ⟩} ∧ [Snd]_{⟨g,out ⟩} ≡ [Rcv ∨ Snd]_{var2}) 1a.2. □Type2 ⇒ (□[Rcv]_{⟨p,buf ,in ⟩} ∧ □[Snd]_{⟨g,out ⟩} ≡ □[Rcv ∨ Snd]_{var2})

1b. Φ_{N} ≡ Φ_{N}^{u}

1b.1a. Φ_{N} ⇒ □InvN 1b.1a.1 TypeN ∧ (∀ i ∈ Z_{N} : pp[i] = gg[i] = 0) ⇒ InvN

1b.1a.2 ∧ InvN

∧ [TypeN ∧ (∀ i ∈ Z_{N} : Fill(i) ∨ Empty(i) ∨ NotProc(i))]_{varN}

⇒ InvN′

1b.1a.3.

∧ TypeN ∧ (∀ i ∈ Z_{N} : pp[i] = gg[i] = 0)

∧ □TypeN ∧ □[∀ i ∈ Z_{N} : Fill(i) ∨ Empty(i) ∨ NotProc(i)]_{varN}

⇒ □InvN

1b.1b. Φ_{N}^{u} ⇒ □InvN 1b.1b.1. TypeN ∧ (∀ i ∈ Z_{N} : pp[i] = gg[i] = 0) ⇒ InvN

1b.1b.2. ∧ InvN

∧ [TypeN ∧ (∃ i ∈ Z_{N} : Fill(i) ∨ Empty(i)]_{varN}

⇒ InvN′

1b.1b.3.

∧ TypeN ∧ (∀ i ∈ Z_{N} : pp[i] = gg[i] = 0)
∧ □TypeN ∧ □[∃ i ∈ Z_{N} Fill(i) ∨ Empty(i)]_{varN}
⇒ InvN′

1b.2. TypeN ∧ InvN ⇒

[∃ i ∈ Z_{N} : Fill(i) ∨ Empty(i)]_{varN} ≡

∀ i ∈ Z_{N} : [Fill(i) ∨ Empty(i) ∨ NotProc(i)]_{varN}

1b.3. □TypeN ∧ □InvN ⇒

□[∃ i ∈ Z_{N} : Fill(i) ∨ Empty(i)]_{varN} ≡

∀ i ∈ Z_{N} : □[Fill(i) ∨ Empty(i) ∨ NotProc(i)]_{varN}

2a. Φ_{2}^{u} ≡ ∃ ∃ ∃ ∃ ∃ ∃ pp, gg, ctl : Φ_{2}^{h} b. Φ_{N}^{u} ≡ ∃ ∃ ∃ ∃ ∃ ∃ p, g : Φ_{N}^{h}

3. Φ_{2}^{h} ≡ Φ_{N}^{h}

3.1a. Type ∧ Inv ⇒ (HRcv ≡ ∃ i ∈ Z_{N} : HFill(i))

3.1a.1 Type ∧ Inv ⇒ (HRcv ≡ HFill(p mod N ))

3.1a.1.1. Type ∧Inv ⇒ ((p −g ≠ N ) ≡ (ctl[p mod N ] = “empty”)) 3.1a.1.2. Type ∧ Inv ⇒ IsNext(pp, p mod N )

3.1a.2 Type ∧ Inv ⇒ (HFill(p mod N ) ≡ (∃ i ∈ Z_{N} : HFill(i)) 3.1b. Type ∧ Inv ⇒ (HSnd ≡ ∃ i ∈ Z_{N} : HEmpty(i))

3.1b.1 Type ∧ Inv ⇒ (HSnd ≡ HEmpty(g mod N )

3.1b.1.1. Type ∧ Inv ⇒ ((p − g ≠ 0) ≡ (ctl[g mod N ] = “empty”)) 3.1b.1.2. Type ∧ Inv ⇒ IsNext(gg, g mod N )

3.1b.1 Type ∧ Inv ⇒ (HEmpty(p mod N ) ≡ (∃ i ∈ Z_{N} : HEmpty(i)) 3.2. [Type ∧ Inv ∧ (HRcv ∨ HSnd)]_{var} ≡

[Type ∧ Inv ∧ (∃ i ∈ Z_{N} : HFill(i) ∨ HEmpty(i))]_{var} 3.3a. Φ_{2}^{hS} ⇒ □Inv

b. Φ_{N}^{hS} ⇒ □Inv 3.3.1. Init ⇒ Inv 3.3.2a. Inv ∧ [Type ∧ (HRcv ∨ HSnd)]_{var} ⇒ Inv′

3.3.2a.1 Inv ∧ Type ∧ HRcv ⇒ Inv′ 3.3.2a.2 Inv ∧ Type ∧ HSnd ⇒ Inv′ 3.3.2a.3 Inv ∧ (var′ = var) ⇒ Inv′

3.3.2b. Inv ∧ [Type ∧ (∃ i ∈ Z_{N} : HFill(i) ∨ HEmpty(i))]_{var} ⇒ Inv′ 3.4. Φ_{2}^{hS} ≡ Φ_{N}^{hS} 3.5. □Inv ∧ Φ_{N}^{hS} ⇒ (WF_{⟨g,out ⟩}(Snd) ≡ (∀ i ∈ Z_{N} : WF_{varN} (Empty(i))))

3.5.1. □Inv ∧ Φ_{N}^{hS} ⇒

(∀ i ∈ Z_{N} : WF_{varN} (Empty(i))) ≡ WF_{varN} (∃ i ∈ Z_{N} : Empty(i)) 3.5.1.1. Φ_{N}^{hS} ⇒ □[∃ i ∈ Z_{N} : Fill(i) ∨ Empty(i)]_{varN}

3.5.1.2. ∧ i ∈ Z_{N}

∧ IsNext(gg, i) ∧ □(Inv ∧ Type) ∧ □[(∃ j ∈ Z_{N} : Fill(j ) ∨ Empty(j )) ∧ ¬Empty(i)]_{varN} ⇒ □IsNext(gg, i)

3.5.1.3. ∧ (i, j ∈ Z_{N} ) ∧ (i ≠ j )

∧ Enabled ⟨Empty(i)⟩_{varN}

∧ □(Inv ∧ Type)

∧ □[(∃ k ∈ Z_{N} : Fill(k) ∨ Empty(k)) ∧ ¬Empty(i)]_{varN} ⇒ □¬Enabled ⟨Empty(j )⟩_{varN}

3.5.2. □Inv ∧ □Type ∧ □[HRcv ∨ HSnd]_{var} ⇒

WF_{⟨g,out ⟩}(Snd) ≡ WF_{varN} (∃ i ∈ Z_{N} : Empty(i)) 3.5.2.1. Inv ∧ Type ∧ [HRcv ∨ HSnd]_{var} ⇒

⟨Snd ⟩_{⟨g,out ⟩} ≡ ⟨∃ i ∈ Z_{N} : Empty(i)⟩_{varN}

3.5.2.2. □Inv ∧ □Type ∧ □[HRcv ∨ HSnd]_{var} ⇒

□◇⟨Snd ⟩_{⟨g,out ⟩} ≡ □◇⟨∃ i ∈ Z_{N} : Empty(i))⟩_{varN}

3.5.2.3 □Inv ∧ □Type ∧ □[HRcv ∨ HSnd]_{var} ⇒

□◇¬Enabled ⟨Snd ⟩_{⟨g,out ⟩} ≡

□◇¬Enabled ⟨∃ i ∈ Z_{N} : Empty(i))⟩_{varN}

B Proof of Lemma 1

Lemma 1 If m ∈ N and i ∈ Z_{N} , then

1. IsNext(Rep(m), i) ≡ (i = m mod N )

2. IsNext(Rep(m), i) ⇒ Rep(m + 1) = [Rep(m) except ![i] = 1 − Rep(m)[i]]

1. Rep(m + 1) = [Rep(m) except ![m mod N ] = 1 − Rep(m)[m mod N ]]

1.1. Case: (m +1) mod 2N = (m mod 2N ) + 1

Proof: It suffices to prove that Rep(m + 1)[j ] = if j = m mod N then 1 − Rep(m)[j ] else Rep(m)[j ]

for any j ∈ Z_{N} . The proof follows. 1.1.1. (j = m mod N ) ≡ (j = m mod 2N ) ∨ (j + N = m mod 2N )

Proof: Simple number theory. 1.1.2. If j = m mod N , then

(j < 1 + (m mod 2N ) ≤ j + N ) ≡ ¬(j < m mod 2N ≤ j + N ) Proof: Step 1.1.1 and simple arithmetic.

1.1.3. If j ≠ m mod N then

(j < 1 + (m mod 2N ) ≤ j + N ) ≡ (j < m mod 2N ≤ j + N ) Proof: Step 1.1.1 and simple arithmetic.

1.1.4. Q.E.D.

Proof: By 1.1.2, 1.1.3, and the definition of Rep.

1.2. Case: (m +1) mod 2N ≠ (m mod 2N ) + 1

Proof: The case assumption implies m mod 2N = 2N − 1, which implies

Rep(m)  = [i ∈ Z_{N} ↦ if i = N − 1 then 0 else 1]
Rep(m + 1) = [i ∈ Z_{N} ↦ 0]

1.3. Q.E.D.

Proof: Steps 1.1 and 1.2.

2. IsNext(Rep(m), i) ≡ (i = m mod N ) The proof is by induction on m. 2.1. Case: m = 0

Proof: Rep(0) = [j ∈ Z_{N} ↦ 0] and IsNext(Rep(0), i) ≡ (i = 0), for i ∈ Z_{N} .

2.2. Assume: IsNext(Rep(m), i) ≡ (i = m mod N ) Prove: IsNext(Rep(m + 1), i) ≡ (i = m + 1 mod N ) The result is trivial if N = 1. We assume N > 1. 2.2.1. (i = m mod N ) ⇒ (IsNext(Rep(m + 1), i) ≡ ¬IsNext(Rep(m), i))

Proof: i = m mod N implies IsNext(Rep(m + 1), i)

≡ by definition of IsNext
if i = 0 then Rep(m + 1)[0] = Rep(m + 1)[N − 1]
else Rep(m + 1)[i] ≠ Rep(m + 1)[i − 1]
≡ by step 1
if i = 0 then 1 − Rep(m)[0] = Rep(m)[N − 1]
else 1 − Rep(m)[i] ≠ Rep(m)[i − 1]
≡ ¬IsNext(Rep(m), i)

2.2.2. (i = m+1 mod N ) ⇒ (IsNext(Rep(m+1), i) ≡ ¬IsNext(Rep(m), i))

Proof: i = m + 1 mod N implies IsNext(Rep(m + 1), i)

≡ by definition of IsNext
if i = 0 then Rep(m + 1)[0] = Rep(m + 1)[N − 1]
else Rep(m + 1)[i] ≠ Rep(m + 1)[i − 1]
≡ by step 1, since N > 1 implies m + 1 mod N ≠ m mod N
if i = 0 then Rep(m)[0] = 1 − Rep(m)[N − 1]
else Rep(m)[i] ≠ 1 − Rep(m)[i − 1]
≡ ¬IsNext(Rep(m), i)

2.2.3. (i ≠ m mod N ) ∧ (i ≠ m + 1 mod N ) ⇒

IsNext(Rep(m + 1), i) ≡ IsNext(Rep(m), i) Proof: The hypothesis implies IsNext(Rep(m + 1), i)

≡ by definition of IsNext
if i = 0 then Rep(m + 1)[0] = Rep(m + 1)[N − 1]
else Rep(m + 1)[i] ≠ Rep(m + 1)[i − 1]
≡ by step 1
if i = 0 then Rep(m)[0] = Rep(m)[N − 1]
else Rep(m)[i] ≠ Rep(m)[i − 1]
≡ IsNext(Rep(m), i)

2.2.4. Q.E.D.

Proof: By 2.2.1–2.2.3 and the induction assumption.

2.3 Q.E.D.

Proof: By steps 2.1 and 2.2 and mathematical induction.

3. IsNext(Rep(m), i) ⇒ (Rep(m + 1) = [Rep(m) except ![i] = 1 − Rep(m)[i]]) Proof: Immediate from steps 1 and 2.

4. Q.E.D.

Proof: Steps 2 and 3.

References

[1] Martín Abadi, Leslie Lamport, and Stephan Merz. Refining specifications. To appear.

[2] C. A. R. Hoare. Communicating sequential processes. Communications of the ACM, 21(8):666–677, August 1978.

[3] R. P. Kurshan and Leslie Lamport. Verification of a multiplier: 64 bits and beyond. In Costas Courcoubetis, editor, Computer-Aided Verification, volume 697 of Lecture Notes in Computer Science, pages 166–179, Berlin, June 1993. Springer-Verlag. Proceedings of the Fifth International Conference, CAV’93.

[4] Leslie Lamport. How to write a proof. Research Report 94, Digital Equipment Corporation, Systems Research Center, February 1993. To appear in American Mathematical Monthly.

[5] Leslie Lamport. The temporal logic of actions. ACM Transactions on Programming Languages and Systems, 16(3):872–923, May 1994.

[6] R. Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, Heidelberg, New York, 1980.