Leslie Lamport

Stephan Merz

Auxiliary Variables in TLA +

Auxiliary variables are often needed for verifying that an implementation is correct with respect to a higher-level specification. They augment the formal description of the implementation without changing its semantics-that is, the set of behaviors that it describes. This paper explains rules for adding history, prophecy, and stuttering variables to TLA + specifications, ensuring that the augmented specification is equivalent to the original one. The rules are explained with toy examples, and they are used to verify the correctness of a simplified version of a snapshot algorithm due to Afek et al.

Contents 1 Introduction

With state-based methods, checking that an implementation satisfies a higherlevel specification requires describing how the higher-level concepts in the specification are represented by the lower-level data structures of the implementation. This approach was first proposed in the domain of sequential systems by Hoare in 1972 [START_REF] Hoare | Proof of correctness of data representations[END_REF]. Hoare called the description an abstraction function. The generalization to concurrent systems was called a refinement mapping by Abadi and Lamport [START_REF] Abadi | The existence of refinement mappings[END_REF]. They observed that constructing a refinement mapping may require adding auxiliary variables to the implementation-variables that do not alter the behavior of the actual variables and need not be implemented.

This paper is about adding auxiliary variables to TLA + specifications. The ideas we present should be applicable to other state-based specification methods, but we make no attempt to translate them into those other methods. We hope that a future paper will present the basic ideas in a language-independent way and will contain soundness and completeness proofs. Our goal here is to teach engineers writing TLA + specifications how to add auxiliary variables when they need them.

We assume the reader can understand TLA + specifications. A basic understanding of refinement mappings will be helpful but isn't necessary. TLA + and refinement mappings are explained in the book Specifying Systems [START_REF] Lamport | Specifying Systems[END_REF] and in material listed on the TLA web page [START_REF] Lamport | TLA-temporal logic of actions[END_REF]. This is a long paper, in part because it contains 25 figures with actual TLA + specifications. The paper contains hyperlinks, and we recommend reading the pdf version on line. If you are doing that, you can download the source files for all the TLA + specifications described in this paper by clicking here. Otherwise, you can find the URL in the reference list [START_REF] Lamport | Auxiliary variables in TLA+[END_REF]. We expect that engineers will have to study the specifications carefully to learn how to add auxiliary variables to their specifications.

We explain three kinds of auxiliary variables: history, prophecy, and stuttering variables. History variables record information about the system's past behavior. They have been used since at least the 1970s [START_REF] Owicki | Verifying properties of parallel programs: An axiomatic approach[END_REF]. They were sometimes called "ghost" variables. Prophecy variables predict the future behavior of the system. They were introduced by Abadi and Lamport in 1991 [START_REF] Abadi | The existence of refinement mappings[END_REF]. The need for them was also implicit in an example presented in Herlihy and Wing's classic paper on linearizability [START_REF] Herlihy | Axioms for concurrent objects[END_REF]. We found the original prophecy variables very difficult to use in practice. The prophecy variables described here are new, and our experience with them so far indicates that they are reasonably easy to use in practice. Stuttering variables add "stuttering" steps-ones that leave the specification's actual variables unchanged. Abadi and Lamport originally used prophecy variables to add stuttering steps, but we have found it better to introduce stuttering steps with a separate kind of variable.

We will mostly ignore liveness and consider only safety specifications. The 3 canonical form of a TLA + specification consists of a safety specification of the form Init ∧ 2[Next ] vars conjoined with a liveness condition. An auxiliary variable is added by modifying the safety specification, but leaving the liveness condition unchanged. Liveness therefore poses no problem for auxiliary variables and is discussed only briefly.

Refinement Mappings

We will illustrate refinement mappings with a simple, useless example. A user presents a server with a sequence of integer inputs. The server responds to each input value i with one of the following outputs: Hi if i is the largest number input so far, Lo if it's the smallest number input so far, Both if it's both, and None if it's neither. We declare Hi, Lo, Both, and None in a constants statement. They are assumed not to be integers.

Specification MinMax 1

Our first specification appears in a module named MinMax 1. It describes the interaction of the user and the server with two variables: a variable x to hold an input or a response, and a variable turn that indicates whether it's the user's turn to input a value or the server's turn to respond. The specification also uses a variable y to hold the set of values input so far. The initial predicate is

Init ∆ = ∧ x = None ∧ turn = "input" ∧ y = {}
The next-state relation Next equals InputNum ∨ Respond where InputNum is the user's input action and Respond is the server's output action. The definition of InputNum is simple:

InputNum ∆ = ∧ turn = "input" ∧ turn ′ = "output" ∧ x ′ ∈ Int ∧ y ′ = y
To define the Respond action, we must first define operators setMax and setMin so that, for any finite nonempty set S of integers, setMax (S ) and setMin(S ) are the maximum and minimum element, respectively, of S . The definitions are:

setMax (S ) ∆ = choose t ∈ S : ∀ s ∈ S : t ≥ s setMin(S ) ∆ = choose t ∈ S : ∀ s ∈ S : t ≤ s
The definition of Respond is:

Respond ∆ = ∧ turn = "output" ∧ turn ′ = "input" ∧ y ′ = y ∪ {x } ∧ x ′ = if x = setMax (y ′ )
then if x = setMin(y ′ ) then Both else Hi else if x = setMin(y ′ ) then Lo else None Note that action InputNum is enabled iff turn equals "input", and action Respond is enabled iff turn equals "output". The complete specification is the formula

Spec ∆ = Init ∧ 2[Next ] vars
where vars is the tuple x , turn, y of variables. The module MinMax 1 we have written thus far is shown in Figure 1.

The Hiding Operator ∃ ∃ ∃ ∃ ∃ ∃

Recall that a behavior is a sequence of states, where a state is an assignment of values to all possible variables. For specification Spec of module MinMax 1, the interesting part of the state is the assignment of values to x , turn, and y.

Our specification allows all other variables to have any value at any state of any behavior.

The purpose of this specification is to describe the interaction of the user and the server. This interaction is described by the values of x and turn. The value of y is needed only to describe how the values of x and turn can change. We consider x and turn to be the externally visible or observable values of the specification and y to be an internal variable. A philosophically correct specification of our user/server system would allow only behaviors in which the values of x and turn are as specified by Spec, but would not constrain the value of y. We can write such a specification in terms of the temporal-logic operator ∃ ∃ ∃ ∃ ∃ ∃ . For any temporal formula F and variable v , the formula ∃ ∃ ∃ ∃ ∃ ∃ v : F is defined approximately as follows. A behavior σ satisfies ∃ ∃ ∃ ∃ ∃ ∃ v : F iff there exists a behavior τ satisfying F such that τ is identical to σ except for the values its states assign to v . The precise definition is more complicated because a temporal formula of TLA + may neither require nor prohibit stuttering steps, but we will use the approximate definition for now. The operator ∃ ∃ ∃ ∃ ∃ ∃ is much like the ordinary existential quantifier ∃ except that ∃ ∃ ∃ ∃ ∃ ∃ v : F asserts the existence not of a single value for v that makes F true but rather of a sequence of values, one for each state in the behavior, that makes F true on the behavior. This temporal existential quantifier ∃ ∃ ∃ ∃ ∃ ∃ satisfies most of the properties of ordinary quantification. For example, if the variable v does not occur in formula F , then ∃ ∃ ∃ ∃ ∃ ∃ v : F is equivalent to F . We sometimes read the formula ∃ ∃ ∃ ∃ ∃ ∃ v : F as "F with v hidden". The philosophically correct specification of the MinMax 1 system should consist of formula Spec with y hidden. The obvious way to write this specification is ∃ ∃ ∃ ∃ ∃ ∃ y : Spec . However, we can't do that for the following reason. Suppose 5 a module M defines exp to equal some expression. TLA + does not allow the expression {v ∈ exp : v 2 > 42} (2.1) to appear at any point in module M where v is already declared or defined. Since exp must be defined for the expression to have a meaning, this means that (2.1) is illegal if v is a declared variable that appears in the definition of exp. Similarly, the formula ∃ ∃ ∃ ∃ ∃ ∃ y : Spec is illegal because y appears in the definition of Spec. 1There are ways to write the formula Spec with v hidden in TLA + . The most convenient ones involve writing it in another module that instantiates module MinMax 1. Chapter 4 of Specifying Systems [START_REF] Lamport | Specifying Systems[END_REF] explains one way to do this. However, there's little reason to do it since the TLA + tools cannot check specifications written with ∃ ∃ ∃ ∃ ∃ ∃ . (The TLAPS proof system may eventually be able to reason about it.) Instead, we take the formula ∃ ∃ ∃ ∃ ∃ ∃ y : Spec to be an abbreviation for the formula ∃ ∃ ∃ ∃ ∃ ∃ y : [[Spec]] , where [[Spec]] is the formula obtained from Spec by expanding all definitions. Formula [[Spec]] contains only: TLA + primitives; the constants Hi, Lo, Both, and None; and the variables x , turn, and y. Thus ∃ ∃ ∃ ∃ ∃ ∃ y : Spec is meaningful in a context in which x and turn are declared variables. If used in a context in which y already has a meaning, we interpret ∃ ∃ ∃ ∃ ∃ ∃ y : Spec to be the formula obtained from ∃ ∃ ∃ ∃ ∃ ∃ y : [[Spec]] by replacing y everywhere with a new symbol.

What it means to expand all definitions in an expression is not as simple as it might seem. Consider the following definition:

NotUnique(a) ∆ = ∃i : i = a (2.2)
It's clear that the following theorem is true:

theorem ∀a : NotUnique(a) (2.3)
Now suppose we follow the definition of NotUnique with: constant i theorem NotUnique(i) (2.4) Theorem (2.3) obviously implies the theorem of (2.4). However, a naive expansion of the definition of NotUnique tells us that [[NotUnique(i)]] equals ∃i : i = i , which equals false. The problem is clear: the bound identifier i in the definition of NotUnique is not the same i as the one declared in the constant declaration. The following definition of NotUnique is equivalent to (2.2) NotUnique(a) ∆ = ∃jku : jku = a and with the naive expansion of this definition, [[NotUnique(i)]] equals the true formula ∃jku : jku = i of (2.4).

The easiest way to define the meaning of expanding all definitions in an expression is to consider (2.2) to define NotUnique(a) to equal something like ∃v 743 : v 743 = a , where v 743 is an identifier that cannot be used anywhere else. In general, every bound identifier in a definition is replaced by some unique identifier.

already declared. In such a language, ∃ ∃ ∃ ∃ ∃ ∃ y : Spec would be equivalent to ∃ ∃ ∃ ∃ ∃ ∃ w : Spec for any identifier w , which means it would be equivalent to Spec.

Recursive definitions are not a problem for complete expansion of definitions because in TLA + , a recursive definition is just an abbreviation for a non-recursive one. For example

f [i ∈ Nat ] ∆ = if i = 0 then 1 else i * f [i -1] is an abbreviation for f ∆ = choose f : f = [i ∈ Nat → if i = 0 then 1 else i * f [i -1]]
so the bound identifier f to the right of the " ∆ =" is not the same symbol as the f being defined. (A recursive operator definition is an abbreviation for a much more complicated ordinary definition.)

Specification MinMax 2

The specification of our system in module MinMax 1 uses the variable y to remember the set of all values that the user has input. Module MinMax 2 specifies the same user/server interaction that remembers only the smallest and largest values input so far, using the variables min and max . Representing the initial state, before any values have been input, is a little tricky. It would be simpler if the standard Integers module defined a value ∞ such that -∞ < i < ∞ for all integers i. So, we will write the spec pretending that it did. Afterwards, we'll describe how to obtain an actual TLA + spec.

The initial predicate of the specification is:

Init ∆ = ∧ x = None ∧ turn = "input" ∧ min = ∞ ∧ max = -∞
The user's InputNum action is the same as for the MinMax 1 specification, except it leaves min and max rather than y unchanged:

InputNum ∆ = ∧ turn = "input" ∧ turn ′ = "output" ∧ x ′ ∈ Int ∧ unchanged min, max
Here is the system's Respond action:

Respond ∆ = ∧ turn = "output" ∧ turn ′ = "input" ∧ min ′ = if x ≤ min then x else min ∧ max ′ = if x ≥ max then x else max ∧ x ′ = if x = max ′ then if x = min ′ then Both else Hi else if x = min ′ then Lo else None
As usual, the complete specification is

Spec ∆ = Init ∧ 2[Next ] vars
where this time vars is the tuple x , turn, min, max of variables.

To turn this into a TLA + specification, we replace ∞ and -∞ by two constants Infinity and MinusInfinity. In the definition of Respond , we replace x ≤ min and x ≥ max by IsLeq(x , min) and IsGeq(x , max ), where IsLeq and IsGeq are defined by

IsLeq(i, j ) ∆ = (j = Infinity) ∨ (i ≤ j ) IsGeq(i, j ) ∆ = (j = MinusInfinity) ∨ (i ≥ j )
These definitions must be preceded by declarations or definitions of Infinity and MinusInfinity. They can equal any values, except that they must not be equal and neither of them should be an integer-otherwise, the spec wouldn't mean what we want it to mean. We could declare Infinity and MinusInfinity in a constant declaration and then add an assume statement asserting that they aren't in Int . However, we prefer to define them like this:

Infinity ∆ = choose n : n / ∈ Int MinusInfinity ∆ = choose n : n / ∈ (Int ∪ {Infinity})
This completes module MinMax 2, which is shown in its entirety in Figure 2.

As before, we consider x and turn to be the externally visible variables, and min and max to be internal variables. The philosophically correct specification, which hides the internal variables min and max , is

∃ ∃ ∃ ∃ ∃ ∃ min, max : Spec . Of course, this is an abbreviation for ∃ ∃ ∃ ∃ ∃ ∃ min : (∃ ∃ ∃ ∃ ∃ ∃ max : Spec ), which is equivalent to ∃ ∃ ∃ ∃ ∃ ∃ max : (∃ ∃ ∃ ∃ ∃ ∃ min : Spec ).

The Relation Between the Two Specifications

Using the standard TLA + naming convention, we have given the two specifications the same name Spec. To distinguish them, let Spec 1 be the specification Spec of module MinMax 1 and Spec 2 be the Spec of module MinMax 2.

It should be clear that both specifications describe the same behavior of the external variables x and turn. This means that if we hide the internal variable y of Spec 1 and the internal variables min and max of Spec 2 , we should obtain equivalent specifications. More precisely, we expect to this to be true:

(∃ ∃ ∃ ∃ ∃ ∃ y : Spec 1 ) ≡ (∃ ∃ ∃ ∃ ∃ ∃ min, max : Spec 2 ) (2.5)
This formula is equivalent to the conjunction of these two formulas We verify (2.5) by separately verifying (2.6) and (2.7). We first consider (2.6). Formula (2.6) asserts of a behavior σ that if there exists some way of assigning values to y in the states of σ to make it satisfy Spec 1 , then σ satisfies ∃ ∃ ∃ ∃ ∃ ∃ min, max : Spec 2 . Since the variable y does not appear in ∃ ∃ ∃ ∃ ∃ ∃ min, max : Spec 2 , changing the values of y in the states of σ doesn't affect whether it satisfies that formula. This implies that to verify (2.6), it suffices to show that any behavior σ that satisfies Spec 1 also satisfies ∃ ∃ ∃ ∃ ∃ ∃ min, max : Spec 2 . In other words, to verify 10

(∃ ∃ ∃ ∃ ∃ ∃ y : Spec 1 ) ⇒ (∃ ∃ ∃ ∃ ∃ ∃ min, max : Spec 2 ) (2.6) (∃ ∃ ∃ ∃ ∃ ∃ min, max : Spec 2 ) ⇒ (∃ ∃ ∃ ∃ ∃ ∃ y : Spec 1 ) (2.7) module MinMax 2 extends Integers, Sequences constants Lo, Hi, Both, None assume {Lo, Hi, Both, None} ∩ Int = {} Infinity ∆ = choose n : n / ∈ Int MinusInfinity ∆ = choose n : n / ∈ (Int ∪ {Infinity}) IsLeq(i, j ) ∆ = (j = Infinity) ∨ (i ≤ j ) IsGeq(i, j ) ∆ = (j = MinusInfinity) ∨ (i ≥ j ) variables x , turn, min, max vars ∆ = x , turn, min, max Init ∆ = ∧ x = None ∧ turn = "input" ∧ min = Infinity ∧ max = MinusInfinity InputNum ∆ = ∧ turn = "input" ∧ turn ′ = "output" ∧ x ′ ∈ Int ∧ unchanged min, max Respond ∆ = ∧ turn = "output" ∧ turn ′ = "input" ∧ min ′ = if IsLeq(x , min) then x else min ∧ max ′ = if IsGeq(x , max ) then x else max ∧ x ′ = if x = max ′ then if x = min ′ then Both else Hi else if x = min ′ then Lo else None Next ∆ = InputNum ∨ Respond Spec ∆ = Init ∧ 2[Next ] vars
(2.6), it suffices to verify

Spec 1 ⇒ (∃ ∃ ∃ ∃ ∃ ∃ min, max : Spec 2 ) (2.8)
To verify (2.8), we must show that for any behavior σ that satisfies Spec 1 , there exists a way of assigning values to the variables min and max in the states of σ that makes the resulting behavior satisfy Spec 2 . A standard way of doing that is to find explicit expressions min and max such that, if in each state of a behavior we assign to the variables min and max the values of min and max in that state, then the resulting behavior satisfies Spec 2 . We do this by showing that any behavior satisfying Spec 1 satisfies the formula obtained by substituting min for min and max for max in Spec 2 . Let's write that formula [[Spec 2 ]], emphasizing that we must expand all definitions in Spec 2 before substituting min for min and max for max . So, we verify (2.8) by verifying

Spec 1 ⇒ [[Spec 2 ]] (2.9)
We can write formula [[Spec 2 ]] (or more precisely, a formula equivalent to it) in module MinMax 1 as follows. We first add the statement

M ∆ = instance MinMax 2 with min ← min, max ← max
For every defined symbol def in module MinMax 2, this statement defines M !def to be equivalent to [[def ]], the formula whose definition is obtained by substituting min for min and max for max in the formula obtained by expanding all definitions in the definition of def in MinMax 2. 2 This instance statement therefore defines M !Spec to be equivalent to [[Spec 2 ]], allowing us to write (2.9) in module MinMax 1 as the theorem:

theorem Spec ⇒ M !Spec
We can write a TLA + proof of this theorem and check it with the TLAPS theorem prover. We can also have TLC check this theorem by creating a model for module MinMax 1 with specification Spec that substitutes a finite set of integers for Int and checks the property M !Spec. But before we can do that, we have to determine what the expressions min and max are in the instance statement.

Formula (2.9) asserts that in a behavior σ satisfying Spec 1 , if in each state of σ we assign to min and max the values of min and max in that state, then the resulting behavior satisfies Spec 2 . One way of thinking about this is that in a behavior satisfying Spec 1 , the values of min and max simulate the values that Spec 2 requires min and max to assume.

A little thought reveals that min and max should be defined as indicated in this statement: Of course, we need to define Infinity and MinusInfinity before we can write that statement. They should be defined to be the same values as in MinMax 2, so we just copy the definitions from that module into module MinMax 1. We have added the statements in Figure 3 to the bottom of the module in Figure 1 2

Infinity ∆ = choose n : n / ∈ Int MinusInfinity ∆ = choose n : n / ∈ (Int ∪ {Infinity}) M ∆ = instance MinMax 2 with min ← if y = {} then Infinity else setMin(y), max ← if y = {} then MinusInfinity else setMax (y)

.5 Refinement In General

In general, we have two specs: Spec 1 with variables x 1 , . . . , x m , y 1 , . . . , y n , and Spec 2 with variables x 1 , . . . , x m , z 1 , . . . , z p . For compactness let x denote x 1 , . . . , x m , let y denote y 1 , . . . , y n and let z denote z 1 , . . . , z p . We consider x to be the externally visible variables of both specifications, and we consider y and z to be internal variables.

The specifications with their internal variables hidden are written ∃ ∃ ∃ ∃ ∃ ∃ y : Spec 1 and ∃ ∃ ∃ ∃ ∃ ∃ z : Spec 2 . To verify that ∃ ∃ ∃ ∃ ∃ ∃ y : Spec 1 implements ∃ ∃ ∃ ∃ ∃ ∃ z : Spec 2 , we must show that for each behavior satisfying Spec 1 , there is some way to assign values of the variables z in each state so that the resulting behavior satisfies Spec 2 . We do that by explicitly specifying those values of z in terms of the values of x and y. More precisely, for each z i we define an expression z i in terms of the variables x and y and show that Spec 1 implements [[Spec 2 ]], the specification obtained by expanding all definitions in Spec 2 and substituting z 1 ← z 1 , . . . , z p ← z p in the resulting formula. This substitution is called a refinement mapping; and if Spec 1 implements [[Spec 2 ]], then we say that Spec 1 implements Spec 2 under the refinement mapping.

The assertion that Spec 1 implements Spec 2 under the refinement mapping z 1 ← z 1 , . . . , z p ← z p can be expressed in TLA + as follows. Suppose Spec 1 is formula Spec1 in a module named Mod 1, and Spec 2 is formula Spec2 in a module named Mod 2. (Spec1 and Spec2 can be the same identifier.) For some identifier Id , we add the following statement to Mod 1:

3 Id ∆ = instance Mod 2 with z 1 ← z 1 , . . . , z p ← z p
The assertion that Spec 1 implements Spec 2 under the refinement mapping can then be expressed in module Mod 1 by the following theorem:

theorem Spec1 ⇒ Id !Spec2
This theorem asserts that in any behavior satisfying Spec 1 , the values of the expressions z i are values that Spec 2 permits the variables z i to have. The shape of the theorem makes it explicit that in TLA + , implementation is implication. The correctness of the theorem can be checked (but seldom completely verified) with TLC for module Mod 1 having Spec1 as the specification and Id !Spec2 as the temporal property to be checked.

As we will see, it is sometimes the case that ∃ ∃ ∃ ∃ ∃ ∃ y : Spec 1 implements ∃ ∃ ∃ ∃ ∃ ∃ z : Spec 2 but there does not exist a refinement mapping under which Spec 1 implements Spec 2 . In that case, it is almost always possible to construct the necessary refinement mapping by adding auxiliary variables to Spec 1 . Adding auxiliary variables a to the specification Spec 1 means finding a specification Spec a

1 such that ∃ ∃ ∃ ∃ ∃ ∃ a : Spec a 1 is equivalent to Spec 1 . Showing that ∃ ∃ ∃ ∃ ∃ ∃ y, a : Spec a 1 implements ∃ ∃ ∃ ∃ ∃ ∃ z : Spec 2 shows that ∃ ∃ ∃ ∃ ∃ ∃ y : Spec 1 implements ∃ ∃ ∃ ∃ ∃ ∃ z : Spec 2 , since ∃ ∃ ∃ ∃ ∃ ∃ y, a : Spec a 1 equals ∃ ∃ ∃ ∃ ∃ ∃ y : ∃ ∃ ∃ ∃ ∃ ∃ a : Spec a 1 which is equivalent to ∃ ∃ ∃ ∃ ∃ ∃ y : Spec 1 .
Even though we can't define the expressions z i in terms of x and y, we may be able to define them in terms of x, y, and a.

We will define three kinds of auxiliary variables: history variables that remember what happened in the past, prophecy variables that predict what will happen in the future, and stuttering variables that add stuttering steps (ones that don't change x and y). Let us return to the notation of Section 2.4, so Spec 1 is specification Spec of module MinMax 1 and Spec 2 is specification Spec of module MinMax 2. We observed that ∃ ∃ ∃ ∃ ∃ ∃ y : Spec 1 and ∃ ∃ ∃ ∃ ∃ ∃ min, max : Spec 2 are equivalent, meaning that each implements (implies) the other. We found a refinement mapping under which Spec 1 implements Spec 2 . To prove the converse implication, we want to find a refinement mapping under which Spec 2 implements Spec 1 . This means defining an expression y in terms of the variables x , turn, min, and max such that the values of x , turn, and y in any behavior allowed by Spec 1 are values of x , turn, and y allowed by Spec 2 .

In a behavior of Spec 1 , the value of y is the set of all values input by the user. However, in a behavior of Spec 2 , the variables min and max record only the smallest and largest input values. There is no way to reconstruct the set of all values input from the variables of MinMax 2. So, there is no refinement mapping under which Spec 2 implements Spec 1 . To solve this problem, we write another spec Spec h 2 that is the same as Spec 2 , except that it also constrains the behavior of another variable h. More precisely, if we hide h in Spec h 2 , then we get a specification that's equivalent to Spec 2 . Expressed mathematically, this means ∃ ∃ ∃ ∃ ∃ ∃ h : Spec h 2 is equivalent to Spec 2 . The initial predicate and next-state action of Spec h 2 are the same as those of Spec 2 , except they also describe the values that h may assume. In particular, the value of h records information about previous values of the variable x , but does not affect the current or future values of x or any of the other variables turn, min, and max of Spec 2 . Thus ∃ ∃ ∃ ∃ ∃ ∃ h : Spec h 2 is equivalent to Spec 2 . We call h a history variable.

We write Spec h 2 as follows in a TLA + module MinMax 2H . The module begins with the statement extends MinMax 2 that simply imports all the declarations and definitions from MinMax , defining Spec to be the specification we are calling Spec 2 . The module declares the variable h and defines the initial predicate InitH of Spec h 2 by

InitH ∆ = Init ∧ (h = { })
The next-state action NextH is defined to equal InputNumH ∨ RespondH where InputNumH and RespondH are defined as follows:

InputNumH ∆ = ∧ InputNum ∧ h ′ = h RespondH ∆ = ∧ Respond ∧ h ′ = h ∪ {x }
The specification Spec h 2 is the following formula defined in the module:

SpecH ∆ = InitH ∧ 2[NextH ] varsH
where varsH equals vars, h . (Because vars equals x , turn, min, max , we can also define varsH to equal x , turn, min, max , h ; the two definitions give equivalent expressions unchanged varsH .)

It's easy to see that this specification asserts that h is always equal to the set of all values that the user has input thus far, which is exactly what Spec 1 asserts about y. Therefore, Spec h 2 implements Spec 1 under the refinement mapping 14

module MinMax 2H extends MinMax 2 variable h varsH ∆ = vars, h InitH ∆ = Init ∧ (h = {}) InputNumH ∆ = ∧ InputNum ∧ h ′ = h RespondH ∆ = ∧ Respond ∧ h ′ = h ∪ {x } NextH ∆ = InputNumH ∨ RespondH SpecH ∆ = InitH ∧ 2[NextH ] varsH M ∆ = instance MinMax 1 with y ← h theorem SpecH ⇒ M ! Spec Figure 4: Module MinMax2H.
y ← h-that is, with y equal to the expression h. We express this in module MinMax 2H by

M ∆ = instance MinMax 1 with y ← h theorem SpecH ⇒ M ! Spec
The complete module MinMax 2H is in Figure 4 3

.2 Disjunctive Representation

The generalization from the MinMax example is intuitively clear. We add a history variable h to a specification by conjoining h = exp Init to its initial predicate and (h ′ = exp A ) to each subaction A of its next-state action, where expression exp Init can contain the spec's variables and each expression exp A can contain the spec's variables, both primed and unprimed, and h (unprimed). To make this precise, we have to state exactly what a subaction is. In general, there may be many different ways to define the subactions of a next-state action. In defining SpecH in module MinMax 2H , we took InputNum and Respond to be the subactions of the next-state action Next of MinMax 2. However, we can also consider Next itself to be a subaction of Next . We can do this and get an equivalent specification SpecH by defining NextH as follows:

NextH ∆ = ∧ Next ∧ ∨ (turn = "input") ∧ (h ′ = h) ∨ (turn = "output") ∧ (h ′ = h ∪ {x })
The two specifications are equivalent because the two definitions of NextH are equivalent. Their equivalence is asserted by adding the following theorem to module MinMax 2H . The TLAPS proof system easily checks its by proof.

theorem NextH = ∧ InputNum ∨ Respond ∧ ∨ (turn = "input") ∧ (h ′ = h) ∨ (turn = "output") ∧ (h ′ = h ∪ {x }) by def NextH , Next , InputNumH , RespondH , InputNum, Respond
To define what a subaction is, we introduce the concept of a disjunctive representation. A disjunctive representation of a formula N is a way of writing N in terms of subactions A 1 , . . . , A m using only the operators ∨ and ∃k ∈ K , for some identifiers k and expressions K . For example, consider the formula:

B ∨ C ∨ D ∨ (∃i ∈ S , j ∈ T : (∃q ∈ U : E ) ∨ (∃r ∈ W : F )) (3.1)
where B , C , D , E , and F can be any formulas. Here is one of the 36 possible disjunctive representations of formula (3.1), where each boxed formula is a subaction:

B ∨ C ∨ D ∨ (∃i ∈ S , j ∈ T : (∃q ∈ U : E ) ∨ (∃r ∈ W : F ))
In other words, this disjunctive representation of (3.1) has the four subactions B , C ∨ D , ∃q ∈ U : E , and F . Each subaction of a disjunction representation has a context, which is a pair k; K , where k is an n-tuple of identifiers and K is an n-tuple of expressions, for some n. The contexts of the subactions in the disjunctive representation of (3.1) defined above are:

subaction context B C ∨ D ∃q ∈ U : E i, j ; S , T F i, j , r ; S , T , W
We let ∃ i, j ; S , T be an abbreviation for ∃i ∈ S , j ∈ T and similarly for ∀ i, j ; S , T . The generalization of this example should be clear. The tuple of identifiers in the context of a subaction A are all the bound identifiers of existential quantifiers within whose scope A lies. 4 If k; K is the empty context ; , we let ∃ k; K : F and ∀ k; K : F equal F .

We can now define precisely what it means to add a history variable to a specification The definition is contained in the hypothesis of this theorem:

Equivalence of Next-State Actions

When adding an auxiliary variable, it is often useful to rewrite a specification Spec-that is, to replace Spec with a different but equivalent formula. This is most often done by rewriting the next-state action Next , which is done by rewriting one or more of the subactions in a disjunctive representation of Next . We now consider when we can replace a subaction A in a disjunctive representation of Next by the subaction B . We can obviously replace A by B if A and B are equivalent formulas. However, this is often too stringent a requirement. For example, the two actions

(x ′ = if y ≥ 0 then x + y else x -y) ∧ (y ′ = y) (x ′ = if y > 0 then x + y else x -y) ∧ (y ′ = y)
are not equivalent. However, they are equivalent if y is a number. Thus, we can replace one by the other in the next-state action if y ∈ Int is an invariant of the specification. The generalization of this observation is:

Theorem 2 (Subaction Equivalence)
Let A be a subaction with context k; K in a disjunctive representation of the next-state action of a specification Spec with tuple vars of variables, let Inv be an invariant of Spec, and let B be an action satisfying:

Inv ⇒ ∀ k; K : A ≡ B (3.2)
Then Spec is equivalent to the specification obtained by replacing A with B in the next-state action's disjunctive representation. Formula (3.2) is an action formula, so it can be proved with TLAPS but cannot be checked with TLC.

TLC can check directly that two specifications are equivalent by checking that each specification implies the other. To check that specification Spec implies a specification SpecB , just run TLC with a model having Spec as the behavioral specification and SpecB as the property to be checked. If one spec is obtained by a simple modification of the other, it should suffice to use small models. But in that case, it should not be hard to prove (3.2) with TLAPS, where Inv is a simple type invariant.

Discussion of History Variables

As our example, we showed that specifications MinMax 1 and MinMax 2 are equivalent. In practice, we rarely care about checking equivalence of specifications. We almost always want to show that a specification S satisfies some property P, which means that S implies P. For example, S ⇒ 2Inv asserts that Inv is an invariant of S. In (2.6) and (2.7), the property P is, like S, a complete system specification.

The most general form of correctness that TLC can check is that one specification implies another. For example, the assertion that Inv is an invariant of a specification S with tuple vars of variables is equivalent to the assertion that S implies the specification

Inv ∧ 2[Inv ′ ≡ Inv ] vars
We often want to show that a specification S implies a higher-level, more abstract specification T . The standard way of doing this is to find a refinement mapping that expresses the values of T 's variables as functions of the values of S's variables. This can't be done if specification T remembers in its state information that is forgotten by S. In that case, we show that S implies T by adding a history variable h to S to obtain the specification S h , and we find a refinement mapping to show S h implies T . Since ∃ ∃ ∃ ∃ ∃ ∃ h : S h is equivalent to S, this shows that S implies T .

One can argue that T is not a good higher-level specification if it keeps information about the past that doesn't have to be kept by its implementation S. 18 However, sometimes that information about the past can simplify the higherlevel specification. We may also add a history variable to a specification S so we can state the property we want to show that it satisfies, even if we aren't explicitly constructing a refinement mapping. For example the property that S requires one kind of action to occur before another can be expressed as an invariant if we add a history variable that remembers when actions have occurred. Because it's a history variable, it doesn't have to be implemented in the system being specified-that is, in the actual hardware or software. Only the variables of S must be implemented.

Liveness

A natural liveness requirement for our MinMax specs is that every input should produce an output. This requirement is added to both specifications by conjoining the fairness requirement WF vars (Respond ) to the formula Spec. (It is just a peculiarity of our example that the fairness requirements are exactly the same in both specifications.) Let us call the resulting specifications LSpec.

The two specifications are still equivalent when the internal variables are hidden. Formula (2.5), and hence formulas (2.6) and (2.7), remain true if we replace Spec 1 and Spec 2 by LSpec 1 and LSpec 2 , respectively-where LSpec 1 and LSpec 2 are formulas LSpec of MinMax 1 and MinMax 2, respectively. We verify (2.6) the same as before by verifying the theorem LSpec ⇒ M !LSpec of module MinMax 1. To verify (2.7), we need to add a history variable h to LSpec 2 rather than to Spec 2 . We now drop the subscripts; all the formulas we write will be ones defined in MinMax 2 or MinMax 2H .

To add a history variable to the specification LSpec, we add a history variable to its safety part and then conjoin the liveness part of LSpec. The resulting specification is defined in module MinMax 2H by

HLSpec ∆ = HSpec ∧ WF vars (Respond )
The equivalence of LSpec and ∃ ∃ ∃ ∃ ∃ ∃ h : HLSpec follows from the equivalence of Spec and ∃ ∃ ∃ ∃ ∃ ∃ h : HSpec by this argument:

1. Spec ∧ WF vars (Respond ) ≡ ( ∃ ∃ ∃ ∃ ∃ ∃ h : HSpec ) ∧ WF vars (Respond ) Proof: Because Spec is equivalent to ∃ ∃ ∃ ∃ ∃ ∃ h : HSpec . 2. ( ∃ ∃ ∃ ∃ ∃ ∃ h : HSpec ) ∧ WF vars (Respond ) ≡ ∃ ∃ ∃ ∃ ∃ ∃ h : (HSpec ∧ WF vars (Respond )) Proof: For any formulas F and G, if h does not occur in G, then (∃ ∃ ∃ ∃ ∃ ∃ h : F ) ∧ G is equivalent to ∃ ∃ ∃ ∃ ∃ ∃ h : (F ∧ G) . 3. Q.E.D.
Proof: By definition of LSpec and HLSpec, 1 and 2 imply that LSpec

is equivalent to ∃ ∃ ∃ ∃ ∃ ∃ h : HLSpec .
What we have done for this example generalizes in the obvious way. For a specification written in the canonical form

Init ∧ 2[Next ] vars ∧ L
with L a liveness condition, we add a history variable by adding it just to the safety part, keeping the same liveness condition. This method of adding a history variable to a specification with liveness produces unusual specifications. In our example, if we expand the definition of HSpec, we see that specification HLSpec equals

InitH ∧ 2[NextH ] varsH ∧ WF vars (Respond )
This spec is unusual because it contains a fairness condition on the action Respond that is not a subaction of the next-state relation NextH . Such specs can be weird. However, specs obtained in this way by adding a history variable are not. Because (i) a Respond action is enabled iff a RespondH action is and (ii) a NextH step is a Respond step iff it is a RespondH step, specification HLSpec is equivalent to the normal specification:

InitH ∧ 2[NextH ] varsH ∧ WF varsH (RespondH ) (3.3)
In general, if Spec h is obtained from a specification Spec by adding a history variable h, then replacing a fairness requirement on a subaction A by the same fairness requirement on A h produces a specification equivalent to Spec h .

The unusual nature of specification HLSpec affects neither the TLC model checker nor our ability to reason about the specification. The same refinement mapping as before shows that HLSpec implements MinMax 1 with the added fairness condition when internal variables are hidden.

Prophecy Variables

As we have observed, the fundamental task of verification is to show that the specification Spec 1 of an implementation satisfies a specification Spec 2 of what the implementation is supposed to do. A history variable remembers the past. It is needed to find a refinement mapping to show that Spec 1 implements Spec 2 when Spec 2 remembers previous events longer than it has to. A prophecy variable is one that predicts the future. It is needed to find a refinement mapping to show that Spec 1 implements Spec 2 when Spec 2 makes decisions before it has to.

One-Prediction Prophecy Variables

We begin by showing how to add a simple prophecy variable that makes a single prediction at a time. Suppose a disjunctive representation of the next-state relation contains a subaction A such that

A ⇒ ( ∃i ∈ Π : Pred A (i) ) (4.1) 20
for some expression Pred A (i) and constant set Π. Formula (4.1) is equivalent to

A ≡ A ∧ ( ∃i ∈ Π : Pred A (i) ) (4.2)
which means that any A step is an A ∧ Pred A (i) step for some i in Π. We introduce a one-prediction prophecy variable p whose value is an i for which the next A step is an A ∧ Pred A (i) step-if there is a next A step. (There could be more than one such i, since we don't require Pred A (i) ∧ Pred A (j ) to equal false if i = j .) We give p that meaning by replacing the subaction A with a subaction A p defined by

A p ∆ = A ∧ Pred A (p) ∧ Setp (4.3)
where Setp determines the value of p ′ .

To ensure that adding the prophecy variable p allows all the behaviors of the other variables that the original spec does, we must ensure that p can always have any value in Π. We do this by initializing p to an arbitrary element of Π and changing p only by setting it to any arbitrary element of Π. Thus we modify the spec's initial predicate Init to equal Init ∧ (p ∈ Π) and we let Setp equal p ′ ∈ Π, so

A p ∆ = A ∧ Pred A (p) ∧ (p ′ ∈ Π) (4.4)
For another subaction A of the next-state relation whose effect is not being predicted by p, we let A p leave the prediction unchanged, so it is defined simply as:

A p ∆ = A ∧ (p ′ = p) (4.5)
We illustrate this with a simple example: a system in which integers are sent and received, where sending an integer i is represented by setting the variable x to i, and receiving a value is represented by setting x to a value NotInt that is not an integer. Our specification SendInt 2 has the receiving action set an internal variable z to the next value to be sent. (The initial value of z is the first value to be sent.) This simple specification is in Figure 5.

Of course, we can describe the behavior of the variable x even more simply, without using any internal variable. Such a specification is in module SendInt 1 of Figure 6. Let Spec 1 and Spec 2 be the formulas Spec of modules SendInt 1 and SendInt 2, respectively. It should be obvious that Spec 1 is equivalent to

∃ ∃ ∃ ∃ ∃ ∃ z : Spec 2 . To verify (∃ ∃ ∃ ∃ ∃ ∃ z : Spec 2 )
⇒ Spec 1 , we just have to verify Spec 2 ⇒ Spec 1 , which TLC easily checks for a model that substitutes a finite set of integers for Int . We now show how to verify Spec 1 ⇒ (∃ ∃ ∃ ∃ ∃ ∃ z : Spec 2 ) . There is obviously no refinement mapping under which Spec 1 implements Spec 2 . Such a refinement mapping would be an expression z involving only the variable x so that z is the value of z in any state satisfying Spec 2 . This is 21

module SendInt 2 extends Integers NotInt ∆ = choose n : n / ∈ Int variable x , z Init ∆ = ∧ x = NotInt ∧ z ∈ Int Send ∆ = ∧ x = NotInt ∧ x ′ = z ∧ z ′ = NotInt Rcv ∆ = ∧ x ∈ Int ∧ x ′ = NotInt ∧ z ′ ∈ Int Next ∆ = Send ∨ Rcv Spec ∆ = Init ∧ 2[Next ] x , z Figure 5: Specification SendInt 2. module SendInt 1 extends Integers NotInt ∆ = choose n : n / ∈ Int variable x Init ∆ = x = NotInt Send ∆ = ∧ x = NotInt ∧ x ′ ∈ Int Rcv ∆ = ∧ x ∈ Int ∧ x ′ = NotInt Next ∆ = Send ∨ Rcv Spec ∆ = Init ∧ 2[Next ] x Figure 6: Specification SendInt1
impossible, since z could equal any integer in a state in which x equals NotInt , so there is no way to express its value as a function of the value of x . The variable z of SendInt 2 is used to predict the value to be sent before it actually is sent. To be able to define the value of z for a refinement mapping, we add a prophecy variable p to SendInt 1 that predicts what the next value to be sent is. The prophecy variable p must predict the value sent by action Send of SendInt 1. Therefore SendP must have the form of (4.4). A little thought shows that p makes the right prediction if we take Pred Send (p) to equal x ′ = p. Since TLA + doesn't allow identifiers to have subscripts we write PredSend instead of Pred Send and define

PredSend (i) ∆ = x ′ = i Condition (4.1) becomes Send ⇒ ∃i ∈ Π : PredSend (i)
which is obviously true by definition of Send , if we let Π equal Int . Writing Pi instead of Π and SendP instead of Send p , we make the definitions:

Pi ∆ = Int SendP ∆ = Send ∧ PredSend (p) ∧ (p ′ ∈ Pi)
(We could of course simply write Int instead of Pi, but writing Pi will help us understand what's going on.)

For the receive action, Rcv p should have the form (4.5).

In a behavior of SendInt 2, when x equals NotInt , the value of z is the next value sent; and when x equals an integer (the value sent), then z equals NotInt . Therefore, if SpecP is the specification obtained from specification Spec of SendInt 1 by adding the prophecy variable p, then SpecP implements the specification Spec of SendInt 2 under this refinement mapping:

z ← if x = NotInt then p else NotInt
Note that SpecP predicts the next value to be sent even before the SendInt 2 specification does-when the previous value is sent rather than when it is received. Although it's not necessary, we'll see later how we could defer the prediction until the Rcv action is executed.

The complete specification is contained in module SendInt 1P in Figure 7. Observe that we defined PredSend before the declaration of p to ensure that PredSend is not defined in terms of p.

The module's theorem asserts that SpecP implements formula Spec of SendInt 2 under the refinement mapping defined above. It can be checked with TLC by creating a model with temporal specification SpecP and having it check the temporal property SI 2!Spec. The model will have to substitute a finite set of integers for Int . The specification is very simple and doesn't depend on any properties of integers, so substituting a set with a few numbers will ensure that we didn't make a mistake.

module SendInt 1P extends SendInt 1 Pi ∆ = Int PredSend (i) ∆ = x ′ = i variable p varsP ∆ = x , p InitP ∆ = Init ∧ (p ∈ Pi) SendP ∆ = Send ∧ PredSend (p) ∧ (p ′ ∈ Pi) RcvP ∆ = Rcv ∧ (p ′ = p) NextP ∆ = SendP ∨ RcvP SpecP ∆ = InitP ∧ 2[NextP ] varsP SI 2 ∆ = instance SendInt 2 with z ← if x = NotInt then p else NotInt theorem SpecP ⇒ SI 2 ! Spec

One-Prediction Prophecy Variables in General

We generalize our description of a one-prediction prophecy variable in two ways. First, we can allow a prophecy variable to make predictions about more than one action by replacing more than one subaction A of a disjunctive representation by an action A p of the form (4.3). If we do this for subactions A 1 , A 2 , . . . , then the value of p makes a prediction about the next step to occur that is an A 1 or A 2 or . . . step. We can express this a little more elegantly by generalizing (4.3) to allow Setp to depend on A and then letting each action A of the disjunctive representation be replaced with an action A p defined by

A p ∆ = A ∧ Pred A (p) ∧ Setp A (4.6)
For an action A about which no prediction is being made, Pred A (p) is the expression true. We can then replace (4.4) and (4.5) by defining Setp A to be one of the following:

(a) Setp A ∆ = p ′ = p (b) Setp A ∆ = p ′ ∈ Π (4.7)
where possibility (a) is allowed only if Pred A (p) is the expression true (so p is making no prediction about A). This is more general because it allows an action that doesn't use the prediction made by p to make a new prediction.

Our second generalization is needed to handle subactions of a disjunctive representation having a nonempty context. For a subaction A with context k; K , condition (4.1) contains the identifiers k. That condition need only hold for values of those identifiers in the corresponding set in K. Thus (4.1) can be generalized to

∀ k; K : A ⇒ (∃i ∈ Π : Pred A (i)) (4.8)
Condition (4.8) is a condition on pairs of states. It needn't hold for all pairs of states, only for pairs of states that can occur in a behavior satisfying the original specification Spec. We can therefore replace (4.8) by the requirement5

Spec ⇒ 2[ ∀ k; K : A ⇒ (∃i ∈ Π : Pred A (i) )] vars (4.9)
TLC can check this condition with a model having the temporal formula Spec as its behavioral spec and

2[∀ k; K : A ⇒ ( ∃i ∈ Π : Pred A (i) )] vars
as a property to be checked.

Prophecy Array Variables

Our next example is based on one created by Martín Abadi [START_REF] Abadi | The prophecy of undo[END_REF]. It is similar to our SendInt specifications in that a sender sends a value v to a receiver with a Send action that sets the variable x to v , and the receiver receives the value by resetting x . Instead of sending integers, the values sent are elements of an unspecified constant set Data, and we let the initial value of x be a value NonData not in Data. A variable y contains a set of values to be sent. Those values are chosen by a Choose action, which adds a new data element to y. The high-level specification is formula Spec in module SendSet of Figure 8. We consider the variable x to be externally visible and y to be internal.

Our implementation adds to the specification of SendSet an undo operation that removes elements from y. Abadi reports that this example is a highly simplified abstraction of a real system in which the implementation contains an undo operation not present in the specification.

The implementation specification is formula SpecU in module SendSetUndo of Figure 9. Its initial predicate is the same as the initial predicate of the specification Spec of module SendSet , and its next-state action NextU is the same as the next-state action Next of that module except it allows Undo(S ) steps that remove from y an arbitrarily chosen non-empty subset S of y. It's clear that the specifications Spec of module SendSet and SpecU of module SendSetUndo allow the same behaviors of the variable x . Hence, ∃ ∃ ∃ ∃ ∃ ∃ y : Spec and ∃ ∃ ∃ ∃ ∃ ∃ y : SpecU are equivalent. It's easy to show that Spec implements SpecU under the identity refinement mapping in which y is defined to equal y, since NextU allows all steps allowed by Next . This implies that ∃ ∃ ∃ ∃ ∃ ∃ y : Spec implies ∃ ∃ ∃ ∃ ∃ ∃ y : SpecU . To construct a refinement mapping under which SpecU implements Spec, we must define y so that it contains a data value d iff that value is going to be sent by a Send step rather than being removed from y by an Undo step. This involves predicting, when d is added to y, whether it will later be sent or "undone".

module SendSet constant Data NonData ∆ = choose d : d / ∈ Data variables x , y vars ∆ = x , y Init ∆ = (x = NonData) ∧ (y = {}) Choose ∆ = ∧ ∃ d ∈ Data \ y : y ′ = y ∪ {d } ∧ x ′ = x Send ∆ = ∧ x = NonData ∧ x ′ ∈ y ∧ y ′ = y \ {x ′ } Rcv ∆ = ∧ x ∈ Data ∧ x ′ = NonData ∧ y ′ = y Next ∆ = Choose ∨ Send ∨ Rcv Spec ∆ = Init ∧ 2[Next ] vars Figure 8: Specification SendSet. module SendSetUndo extends SendSet Undo(S ) ∆ = ∧ y ′ = y \ S ∧ x ′ = x NextU ∆ = Next ∨ (∃ S ∈ (subset y) : Undo(S )) SpecU ∆ = Init ∧ 2[NextU ] vars
We add a prophecy array variable p to SpecU that makes this prediction, setting p[d ] to either "send" or "undo" when d is added to y. So, we define our set Pi of possible predictions by

Pi ∆ = {"send", "undo"}
The value of p in every state will be a function with domain equal to the set y, with p[d ] ∈ Pi for all d ∈ y. In other words p ∈ [y → Pi] will be an invariant of the spec SpecUP obtained by adding the prophecy variable p. The variable p is therefore making a predication p[d ] for every d in y, so p is making an array of prophecies. (This is a "dynamic" array, because the value of y can change.)

We now define the specification SpecUP . As with a one-prediction prophecy variable, we obtain the next-state relation of SpecUP by replacing each subaction A in a disjunctive representation of the next-state relation with a new action A p . Instead of defining A p as in (4.6), we define it to equal

A p ∆ = A ∧ Pred A (p) ∧ (p ′ ∈ NewPSet A ) (4.10)
for suitable expressions Pred A (p) and NewPSet A . We need a condition corresponding to condition (4.9) for a one-prediction prophecy variable to assert that there is a possible value of p that makes Pred A (p) true. With an array prophecy variable, p is no longer an element of Pi but a function in [Dom → Pi] for some domain Dom that can change. In our example, Dom equals y. To make the generalization to an arbitrary spec easier, we define Dom to equal y and write Dom instead of y where appropriate. For our example, we can replace (4.9) with

SpecU ⇒ 2[∀ k; K : A ⇒ ( ∃f ∈ [Dom → Π] : Pred A (f ) )] vars (4.11)
where k; K is the context of A. (Remember that for the empty context ; , we define ∀ ; : F to equal F , for any formula F .)

We now define the formulas Pred A and NewPSet A for the disjunctive representation of NextU with subactions Choose, Send , Rcv , and Undo(S ). The context of the first three subactions is empty; the context of Undo(S ) is S ; subset y .

The variable p does not make any prediction about the Choose action, so Pred Choose (p) should equal true. The action adds an element d to its domain, 27 so Choose p must allow p ′ [d ] to equal any element of Pi. For any element d in the domain Dom of p, the value of p[d ] can be left unchanged. Our definitions of Pred Choose (p) and NewPSet Choose (p) are then

PredChoose(p) ∆ = true NewPSetChoose(p) ∆ = { f ∈ [Dom ′ → Pi] : ∀ d ∈ Dom : f [d ] = p[d ] }
The prophecy variable p should predict that if the next action is a Send action, then it sends a value d in Dom such that p[d ] = "send". The value sent by the action is x ′ , so we define

PredSend (p) ∆ = p[x ′ ] = "send"
The Send action removes the sent element d from Dom, thus erasing the prediction p made about d . The value of p[d ] is left unchanged for all other elements d in Dom. Thus NewPSet Send (p) is defined as follows to be a set consisting of a single function

NewPSetSend (p) ∆ = { [d ∈ Dom ′ → p[d ]] }
No prediction is made about the Rcv action, and it doesn't change Dom, so we have:

PredRcv (p) ∆ = true NewPSetRcv (p) ∆ = {p}
The Undo(S ) p action should be enabled only when p has predicted that all the elements in S will not be sent-in other words, when ∀d ∈ S : p[d ] = "undo" is true. Since the identifier S appears in this formula, it must be an argument of the definition of Undo(S ) p . Thus, we define

PredUndo(p, S ) ∆ = ∀d ∈ S : p[d ] = "undo"
The Undo(S ) action removes from Dom all the elements for which p made a prediction about Undo(S )-namely, all the elements of S . We can define NewPSet Undo(S ) the same way we defined PSetSend Send , without explicitly mentioning S :

NewPSetUndo(p) ∆ = { [d ∈ Dom ′ → p[d ]] }
We can now declare the variable p and define the specification SpecUP by defining the initial predicate InitUP and defining the next-state relation NextUP in terms of the subactions A p , using (4.10). The complete specification is in module SendSetUndoP shown in Figure 10. Note that the initial value of p is the unique function whose domain is the empty set. We could write that function as [d ∈ {} → exp] for any expression exp-for example, 42. However, it's easier to write that function as (the empty sequence). We can now define the refinement mapping under which SpecUP implements specification Spec of module SendSet . The refinement mapping defines y to equal the set of elements d in y with p[d ] = "send". We thus add to the module 28 We should also check that condition (4.11) holds for each subaction A. To do this, we need to create a model with specification SpecU and have TLC check the property:

module SendSetUndoP extends SendSetUndo Pi ∆ = {"send", "undo"} Dom ∆ = y PredChoose(p) ∆ = true NewPSetChoose(p) ∆ = {f ∈ [Dom ′ → Pi] : ∀ d ∈ Dom : f [d ] = p[d ]} PredSend (p) ∆ = p[x ′ ] = "send" NewPSetSend (p) ∆ = {[d ∈ Dom ′ → p[d ]]} PredRcv (p) ∆ = true NewPSetRcv (p) ∆ = {p} PredUndo(p, S ) ∆ = ∀ d ∈ S : p[d ] = "undo" NewPSetUndo(p) ∆ = {[d ∈ Dom ′ → p[d ]]} variable p varsP ∆ = vars, p InitUP ∆ = Init ∧ (p = ) ChooseP ∆ = Choose ∧ PredChoose(p) ∧ (p ′ ∈ NewPSetChoose(p)) SendP ∆ = Send ∧ PredSend (p) ∧ (p ′ ∈ NewPSetSend (p)) RcvP ∆ = Rcv ∧ PredRcv (p) ∧ (p ′ ∈ NewPSetRcv (p)) UndoP (S ) ∆ = Undo(S ) ∧ PredUndo(p, S ) ∧ (p ′ ∈ NewPSetUndo(p)) NextUP ∆ = ChooseP ∨ SendP ∨ RcvP ∨ (∃ S ∈ subset y : UndoP (S )) SpecUP ∆ = InitUP ∧ 2[NextUP ] varsP
2[ ∧ Choose ⇒ ∃ f ∈ [Dom → Pi] : PredChoose(f ) ∧ Send ⇒ ∃ f ∈ [Dom → Pi] : PredSend (f ) ∧ Rcv ⇒ ∃ f ∈ [Dom → Pi] : PredRcv (f ) 29 ∧ ∀ S ∈ subset y : Undo(S ) ⇒ ∃ f ∈ [Dom → Pi] : PredUndo(f , S ) ] vars
However, there is a problem in doing this. TLC will not allow a model for module SendSetUndoP to have behavior specification SpecU because that spec doesn't describe the behavior of the variable p. We can solve this problem by modifying the specification-temporarily inserting "======" into the module before the declaration of p and then creating the necessary model. Alternatively, we can move all the definitions before the declaration of p into module SendSetUndo and check the condition in a model for that spec. This is inelegant because those definitions aren't part of the SendSetUndo specification. The proper solution is to move those definitions from SendSetUndoP and put them in a new module that extends SendSetUndo and is extended by SendSetUndoP . We can then check that the condition is satisfied using a model for that specification that has behavior spec SpecU . We won't bother doing this, instead putting them in module SendSetUndoP .

Recall that in the SendInt example of Section 4.1, the one-prediction prophecy variable we used predicted the next value to be sent when the previous value was sent, while the specification SendInt 2 didn't choose the next value to be sent until the previous value was received. We can use an array prophecy variable to defer the prediction until it's needed. We let the domain Dom of p initially contain a single element-let's take that element to be "on". We let the Send action set Dom to the empty set, and we let the Rcv action set Dom to {"on"}.

Prophecy Data Structure Variables

It is easy to generalize from the SendSet example to an arbitrary prophecyarray variable. However, it is useful to generalize still further from an array to an arbitrary data structure. These prophecy data structure variables are the most general ones that we consider. We propose them as the standard way of defining prophecy variables in TLA + , and we have created a module with definitions that simplify adding these prophecy variables. Both single-prophecy variables and prophecy array variables are easily expressed as special cases.

As our example of a prophecy data structure variable, we modify the specification SendSet , in which a set of items to be sent is chosen, to a specification SendSeq in which a sequence of items is chosen. The value of the variable y is changed from a set of data items to a sequence of data items. The next item to be sent is the one at the head of y, and each value chosen is appended to the tail of y. The specification is in module SendSeq, shown in Figure 11.

For our implementation, we add an undo action that removes an arbitrary element from the sequence y. The specification is in module SendSeqUndo of module SendSeq extends Sequences, Integers As before, we want to show that specification SendU of module SendSeqUndo implements ∃ ∃ ∃ ∃ ∃ ∃ y : Spec , where Spec is the specification of module SendSeq. Again, we need to add a prophecy variable p that predicts whether each element of y will be sent or "undone". We do this by having p be an element of Seq({"send", "undo"}) that has the same length as y. The Choose p action should append either "send" or "undo" to the tail of p, the Send p action should remove the head of p, and the Undo(i) action should remove the i th element of p.

constant Data NonData ∆ = choose v : v / ∈ Data variables x , y vars ∆ = x , y Init ∆ = (x = NonData) ∧ (y = ) Choose ∆ = ∧ ∃ d ∈ Data : y ′ = Append (y, d ) ∧ x ′ = x Send ∆ = ∧ x = NonData ∧ y = ∧ x ′ = Head (y) ∧ y ′ = Tail (y) Rcv ∆ = ∧ x ∈ Data ∧ x ′ = NonData ∧ y ′ = y Next ∆ = Choose ∨ Send ∨ Rcv Spec ∆ = Init ∧ 2[Next ] vars
As we did for the SendSet example, we write a module SendSeqUndoP that extends SendSeqUndo. In it, we define the formulas Pred A (p) of (4.10) for each of the subactions Choose, Send , Rcv , and Undo(i). The definitions are: We now need to define the expression NewPSet A of (4.10) for each of these subactions.

PredChoose(p) ∆ = true PredSend (p) ∆ = p[1] = "send" PredRcv (p) ∆ = true PredUndo(p, i) ∆ = p[i] = "undo" module SendSeqUndo extends SendSeq RemoveEltFrom(i, seq) ∆ = [j ∈ 1 . . (Len(seq) -1) → if j < i then seq[j ] else seq[j + 1]] Undo(i) ∆ = ∧ y ′ = RemoveEltFrom(i, y) ∧ x ′ = x NextU ∆ = Next ∨ (∃ i ∈ 1 . . Len(y) : Undo(i)) SpecU ∆ = Init ∧ 2[NextU ] vars
Since a sequence of length n is a function with domain 1 . . n, the value of p is a function-just as in SendSetUndoP above. This time its domain Dom is the set 1 . . Len(y). However, in that example, if d is in the domain Dom of p in two successive states, then p[d ] represents the same prediction in both states. This isn't true in the current example. If s → t is a Send step and Len(p) > 1 in state s, then the prediction made by p [START_REF] Abadi | The existence of refinement mappings[END_REF] in state s is the prediction made by p [START_REF] Abadi | The prophecy of undo[END_REF] in state t . If s → t is an Undo(i) step and j > i, the prediction made by p[j ] in state s is the prediction made by p[j -1] in state t .

In general, an action A defines a correspondence between some elements in the domain Dom of p and elements in the domain Dom ′ of p ′ . For example, for the Send action, each element i > 1 in Dom corresponds to the element i - To express formally a correspondence between elements of Dom and Dom ′ , we introduce the concept of a partial injection. A partial function from a set U to a set V is a function from a subset of U to V . In other words, it is an element of [D → V ] for some subset D of U . (Remember that U is a subset of itself.) An injection is a function that maps different elements in its domain to different values. In other words, a function f is an injection iff for all a and b in

domain f , if a = b then f [a] = f [b]. The set of all partial injections from U to V is defined in TLA + by PartialInjections(U , V ) ∆ = let PartialFcns ∆ = union {[D → V ] : D ∈ subset U } in {f ∈ PartialFcns : ∀ a, b ∈ domain f : (a = b) ⇒ (f [a] = f [b])}
DomInjChoose ∆ = [d ∈ Dom → d ] DomInjSend ∆ = [i ∈ 2 . . Len(y) → i -1] DomInjRcv ∆ = [d ∈ Dom → d ] DomInjUndo(i) ∆ = [j ∈ 1 . . Len(y) \ {i} → if j < i then j else j -1]
For the prophecy array variable described in Section 4.3 above, the function DomInj A maps each element d in Dom that is also in Dom ′ to itself. Thus, for each subaction A used in defining a prophecy array variable, we can define

DomInj A ∆ = [d ∈ Dom ∩ Dom ′ → d ] A function f such that f [x ] =
x for all x ∈ domain f is called an identity function. For convenience, the Prophecy module defines IdFcn(S ) to be the identify function with domain S . But we won't bother using it here. The Prophecy module also defines EmptyFcn to be the (unique) function whose domain is the empty set.

Let us return to our prophecy data structure example. For a subaction A, we can define NewPSet A in terms of DomInj A and the subset PredDom A of Dom, which consists of the elements in Dom such that p[d ] makes a prediction about A. We define these sets PredDom A in module SendSeqUndoP for our four subactions as follows:

PredDomChoose ∆ = {} PredDomSend ∆ = {1} PredDomRcv ∆ = {} PredDomUndo(i) ∆ = {i}
(Since PredDom Undo(i) depends on the identifier i in its context, we must define PredDomUndo to have a parameter.)

We can define NewPSet A to equal the set of all functions q in [Dom ′ → Π] such that for every element d in Dom that is not in PredDom A and has a corresponding element DomInj A [d ] in Dom ′ , the value of q on that corresponding element equals p[d ]. More precisely, NewPSet A equals:

{ q ∈ [Dom ′ → Π] : ∀d ∈ (domain DomInj A ) \ PredDom A : q[DomInj A [d ]] = p[d ] }
We encapsulate definitions like this in a module Prophecy. We find it most convenient to make this a constant module with constant parameters Pi, Dom, and DomPrime. This module is meant to be instantiated with the parameter Pi instantiated by Π, with the parameter Dom instantiated by the appropriate state function Dom, and with DomPrime instantiated by Dom ′ . The following definition from module Prophecy allows us to define NewPSet A (p) to equal NewPSet (p, DomInj A , PredDom A ) :

NewPSet (p, DomInj , PredDom) ∆ = { q ∈ [DomPrime → Pi] : ∀ d ∈ (domain DomInj ) \ PredDom : q[DomInj [d ]] = p[d ] }
For each action in A in our disjunctive decomposition of NextU , we have written the definitions of Pred A , DomInj A , and PredDom A . This allows us to define NewPSet A , and therefore, by (4.10), to define A p . The following operator ProphAction from the Prophecy module allows us to write A p as ProphAction(A, p, p ′ , DomInj A , PredDom A , Pred A ) :

ProphAction(A, p, pPrime, DomInj , PredDom, Pred ( ))

∆ = A ∧ Pred (p) ∧ (pPrime ∈ NewPSet (p, DomInj , PredDom))
In module SendSeqUndoP , we can define

ChooseP ∆ = ProphAction(Choose, p, p ′ , DomInjChoose, PredDomChoose, PredChoose)
The definitions of SendP and RcvP are similar. However, there is a problem with the definition of Undo(i) p , which we write as UndoP (i). Operator ProphAction requires its last argument, which represents Pred A , to be an operator with a single argument. However, we defined PredUndo to have two arguments: p and its context identifier i. Since we are defining UndoP (i), the fifth argument has to be an operator Op so that Op(p) equals PredUndo(p, i). So, we should define:

UndoP (i) ∆ = let Op(j ) ∆ = PredUndo(j , i) in ProphAction(Undo(i), p, p ′ , DomInjUndo(i), PredDomUndo(i), Op)
Using the TLA + lambda construct (added since Specifying Systems was published), this can also be written as:

UndoP (i) ∆ = ProphAction( Undo(i), p, p ′ , DomInjUndo(i), PredDomUndo(i), lambda j : PredUndo(j , i) )
It's now straightforward to complete our definition of specification SpecUP . Doing so, gathering up the definitions made or implied so far, and rearranging them a bit, we get the beginning of module SendSeqUndoP shown in Figure 13. Finally, we have to define the refinement mapping under which SpecUP implements specification Spec of module SendSeq. The idea is simple: we let y be the subsequence of y containing only those elements for which the corresponding element of the sequence p equals "send". The following formal definition is a bit tricky. It uses a local recursive definition of an operator R such that if yseq is any sequence and pseq is a sequence of the same length, then R(yseq, pseq) is the subsequence of yseq that contains yseq[i] iff pseq[i] equals "send".

∆ = [d ∈ Dom → d ] PredChoose(p) ∆ = true PredDomSend ∆ = {1} DomInjSend ∆ = [i ∈ 2 . . Len(y) → i -1] PredSend (p) ∆ = p[1] = "send" PredDomRcv ∆ = {} DomInjRcv ∆ = [d ∈ Dom → d ] PredRcv (p) ∆ = true PredDomUndo(i) ∆ = {i} DomInjUndo(i) ∆ = [j ∈ 1 . . Len(y) \ {i} → if j < i then j else j -1] PredUndo(p, i) ∆ = p[i] = "undo" variable p varsP ∆ = vars, p InitUP ∆ = Init ∧ (p ∈ [Dom → Pi]) ChooseP ∆ = ProphAction(Choose, p, p ′ , DomInjChoose, PredDomChoose, PredChoose) SendP ∆ = ProphAction(Send , p, p ′ , DomInjSend , PredDomSend , PredSend ) RcvP ∆ = ProphAction(Rcv , p, p ′ , DomInjRcv , PredDomRcv , PredRcv ) UndoP (i) ∆ = ProphAction(Undo(i), p, p ′ , DomInjUndo(i), PredDomUndo(i), lambda j : PredUndo(j , i)) NextUP ∆ = ChooseP ∨ SendP ∨ RcvP ∨ (∃ i ∈ 1 . . Len(y) : UndoP (i)) SpecUP ∆ = InitUP ∧ 2[NextUP ] varsP
yBar ∆ = let recursive R( , ) R(yseq, pseq) ∆ = if yseq =
then yseq else if Head (pseq) = "send" then Head (yseq) • R(Tail (yseq), Tail (pseq)) else R(Tail (yseq), Tail (pseq)) in R(y, p)

We then instantiate module SendSeq and state as follows the theorem asserting that SpecUP implements formula Spec of that model under the refinement mapping.

SS

Checking the Definitions

We have shown how to define a specification Spec p for an arbitrary specification Spec by defining a state function Dom and, for every subaction A of a disjunctive representation of the next-state action of Spec, defining Pred A , DomInj A , and PredDom A . These definitions must satisfy certain conditions to ensure that ∃ ∃ ∃ ∃ ∃ ∃ p : Spec p is equivalent to Spec. We now state those conditions.

The first condition is (4.11). The Prophecy module defines this operator:

ExistsGoodProphecy(Pred ( )) ∆ = ∃ q ∈ [Dom → Pi] : Pred (q)
For a subaction A with an empty context, we can write (

∀q, r ∈ [Dom → Pi] : (∀d ∈ PredDom A : q[d ] = r [d ]) ⇒ (Pred A (q) = Pred A (r ))
In addition to this requirement, to ensure that our formulas make sense, we also make the obvious requirement that PredDom A is a subset of Dom. The following definition appears in module Prophecy.

IsPredDom(PredDom, Pred ( )) Remembering that the condition on PredDom A needs to hold only for A steps in a behavior satisfying the specification, we can express it for an action A with an empty context as:

∆ = ∧ PredDom ⊆ Dom ∧ ∀ q, r ∈ [Dom → Pi] : (∀ d ∈ PredDom : q[d ] = r [d ]) ⇒ (Pred (q) = Pred (r )) Condition ∆ = ∧ ProphCondition(Choose,
Spec ⇒ 2[A ⇒ IsPredDom(PredDom A , Pred A )] vars
Because the second argument of IsPredDom is an operator argument, we again need to use a local definition or a lambda expression to express the condition if the subaction A has a nonempty context. For example, here is how we can express it for the Undo(i) subaction in our SendSeq example using a local definition:

2[ ∀ i ∈ Dom : Undo(i) ⇒ let Op(p) ∆ = PredUndo(p, i) in IsPredDom(PredDomUndo, Op) ] vars
Here is how it is written with a lambda expression:

2[ ∀ i ∈ Dom : Undo(i) ⇒ IsPredDom( PredDomUndo, lambda p : PredUndo(p, i) ) ] vars
The following definition from module Prophecy allows us to combine the three conditions.

ProphCondition(A, DomInj , PredDom, Pred ( ))

∆ = A ⇒ ∧ ExistsGoodProphecy(Pred ) ∧ IsDomInj (DomInj ) ∧ IsPredDom(PredDom, Pred )
Using this definition, the requirements on the definitions are expressed for specification SendSeqUndo in Figure 14. We encounter the same problem here that we encountered in checking condition (4.11) for the SendSet example. We would like to put these requirements 38 in module SendSetUndoP (Figure 10), right before the declaration of the variable p. However, TLC can't check the theorem in a model for that specification because SpecU does not specify the values of variable p. We can either move all the definitions that are now in SendSetUndoP before the declaration of p into a separate module, put them at the end of module SendSetUndo, or end the module before the declaration of p by adding "=====" when checking the condition.

You should check these conditions when adding a prophecy variable. They provide a good way to debug your definitions, before you try checking that the specification with prophecy variable implements the desired specification.

Liveness

As with our other auxiliary variables, we add a prophecy variable to the safety part of a specification, but we keep the liveness part the same. As we remarked in Section 3.5, this produces unusual specifications in which the liveness property can assert a fairness condition about an action that isn't a subaction of the next-state action.

For history variables, although the form of the specifications is unusual, the specifications are not. This is not the case for prophecy variables. If Spec has a liveness condition, the specification Spec p obtained from it by adding a prophecy variable can be weird. As an example, suppose that in the SendInt specifications of Section 4.1, instead of taking Pi to equal Int , we let it equal Int ∪ {∞} for some value ∞ / ∈ Int . Everything we did would work exactly as before, and the theorem at the end of module SendInt 1P in Figure 7 would still be true. If a SendP step set p ′ to ∞, predicting that the next value to be sent is ∞, then the system would simply halt (stutter forever) before the next SendP step because Send ∧ PredSend (∞) equals false. Now suppose we add a liveness condition WF vars (Next ) to our SendInt specifications, requiring that they never halt. We would then have

SpecP ∆ = InitP ∧ 2[NextP ] varsP ∧ WF vars (Next )
This formula SpecP implies that infinitely many Next steps must occur, so a behavior can't halt. The weak fairness conjunct therefore requires that SpecP not set p ′ to ∞. This is weird. The liveness property WF vars (Next ) doesn't just require that something must eventually happen; it also prevents something (setting p to ∞) from ever happening. The technical term for this weirdness is that the formula SpecP is not machine closed [START_REF] Abadi | The existence of refinement mappings[END_REF], which means that its liveness property affects safety as well as liveness.

Non-machine closed specs should never be used to describe how a system works. You can't understand how to implement a system if the next-state action doesn't describe what it can and cannot do next. In extremely rare cases, a nonmachine closed high-level spec is the best way to describe what a system should 39 do, rather than how it should do it. You are very unlikely to encounter such a situation in practice.

While the non-machine closed spec we get by adding a prophecy variable to a spec with liveness can be weird, this weirdness causes no problem. We don't have to implement SpecP . We use it only to check the correctness of Spec; and the presence of the liveness property makes no difference in what we do. With our modified SendInt specifications, we can check that SpecP implies SI 2!Spec exactly as we did before.

Stuttering Variables

Adding Stuttering Steps to a Simple Action

Suppose Spec 1 is a specification of a (24-hour) clock that displays only the hour-a specification we can write as

Spec 1 ∆ = (h = 0) ∧ 2[h ′ = (h + 1) % 24] h (5.1)
Let Spec 2 be this specification of an hour-minute clock:

Spec 2 ∆ = ∧ (h = 0) ∧ (m = 0) ∧ 2[ ∧ m ′ = (m + 1) % 60 ∧ h ′ = if m ′ = 0 then (h + 1) % 24 else h ] h,m (5.2)
If we ignore the variable m in Spec 2 , then we get a clock that displays only the hour. Thus, ∃ ∃ ∃ ∃ ∃ ∃ m : Spec 2 should be equivalent to Spec 1 . (The 59 steps each hour that change only m are stuttering steps that are allowed by Spec 1 .) It's easy to see that Spec 2 implies Spec 1 , so ∃ ∃ ∃ ∃ ∃ ∃ m : Spec 2 implies Spec 1 . There is no refinement mapping with which we can prove that Spec 1 implies ∃ ∃ ∃ ∃ ∃ ∃ m : Spec 2 . To construct the necessary refinement mapping we need to add an auxiliary variable s to Spec 1 to obtain a specification Spec s 1 that adds 59 steps that change only s to each step that increments h. Such an auxiliary variable is called a stuttering variable because it changes Spec 1 only by requiring it to add steps that leave the variable h of Spec 1 unchanged.

To add such a variable s to a specification Spec to form Spec s , we let the next-state action of Spec s take "normal" steps that satisfy the next-state action of Spec when s equals ⊤ (usually read "top"), which is some value that is not a positive integer. The value of s in the initial state equals ⊤. When s is set to a positive integer, the specification Spec s allows only stuttering steps that decrement s, leaving the variables of Spec unchanged. When s counts down to zero, it is set equal to ⊤ again. We add these stuttering steps before and/or after steps of some particular subaction of the next-state action. Here, we assume that this is a "simple" subaction, meaning that its context is empty.

Suppose we want the specification Spec s to add stuttering steps to each step of a particular subaction. We replace each subaction A by the action A s defined as follows. For each A other than that particular subaction, we define A s by:

A s ∆ = (s = ⊤) ∧ A ∧ (s ′ = s) (5.3)
To add initVal stuttering steps after a step of an action A, for a positive integer initVal (whose value may depend on the variables of Spec), we define

A s ∆ = if s = ⊤ then A ∧ (s ′ = initVal ) else ∧ vars ′ = vars ∧ s ′ = if s = 1 then ⊤ else s -1
We can generalize this by replacing the set of natural numbers with an arbitrary set Σ having a well-founded partial order ≺ with smallest element ⊥ (read "bottom") 6 , letting initVal be an arbitrary element of Σ, replacing s = 1 with s = ⊥, and replacing s -1 by decr (s) for some operator decr such that decr (s) ≺ s for all s ∈ Σ. The generalization is:

A s ∆ = if s = ⊤ then A ∧ (s ′ = initVal ) else ∧ vars ′ = vars ∧ s ′ = if s = ⊥ then ⊤ else decr (s) (5.4)
We can add initVal stuttering steps before an A step, rather than after it, as follows. The stuttering steps should only be taken when they can be followed by an A step, which is the case only when an A step is enabled. Remembering that enabled A is the state predicate that is true iff an A step is enabled, the stuttering steps can be added with this definition of A s :

A s ∆ = ∧ enabled A ∧ if s = ⊥ then A ∧ (s ′ = ⊤) else ∧ vars ′ = vars ∧ s ′ = if s = ⊤ then initVal else decr (s) (5.5)
We could generalize (5.4) and (5.5) to allow putting stuttering steps both before and after an A step. We won't bother to do this because it is probably seldom needed, and it wouldn't be significantly simpler than adding two separate stuttering variables.

Adding Stuttering Steps to Multiple Actions

To generalize what we did in the preceding section, we first consider how to add stuttering steps before or after an action A that may have a nonempty context. We assume that the set Σ, its ⊥ element, and the operator decr do not depend on the values of the context variables. (This should be true in most real examples.) However, initVal may depend on them. We therefore must make sure that initVal is evaluated with the values of the context variables for which the action A is "executed". This is no problem for stuttering steps added after the A step, where A s is defined by (5.4). (Since the stuttering steps do nothing but decrement the value of s, it makes no difference for which value of the context variables A s is "executed" when s = ⊤.) However, it is a problem for stuttering steps added before an A step, where A s is defined by (5.5).

To solve the problem for A s defined by (5.5), we let the non-⊤ values of s be records with a val component that equals the value of s described in (5.5), and a ctxt component that equals the tuple of values of the context when initVal is evaluated. In other words, ctxt is set by the else clause in the second conjunct of (5.5). The condition that s.ctxt equals the values of the context variables is added as a conjunct to the then clause to make sure that A is executed only in that context. The precise definition is given below.

We often need to add stuttering steps before or after more than one subaction of the next-state action. We could do that by adding separate stuttering variables, or we could introduce a stuttering array variable. However, because the stuttering steps we add to an action all occur immediately before or after that subaction, we can add them all with the same stuttering variable s. Stuttering steps can be added to each such subaction with its own set Σ and hence its own values of initVal and ⊥ and of the operator decr . We just let the value of s indicate the action to which the stuttering steps are being added. We do this by adding to the non-⊤ values of s an additional id component that identifies the action for which the stuttering steps are being added. The component is set when s is first set to a non-⊤ value, and execution of the new subaction A s is enabled when s = ⊤ only if s.id equals the identifier of A.

We write the three definitions (5.3), (5.4), and (5.5) in TLA + using the three operators NoStutter , PostStutter , and PreStutter , respectively, shown in Figure 15. The module should be instantiated by substituting the new stuttering variable for s and the tuple of variables of the original specification for vars. It defines ⊤, which is written top, to be a value that is different from the values assigned to s by PostStutter and PreStutter actions (and that TLC knows is different from those values). The other values in (5.4) and (5.5) are provided by the following arguments to PostStutter and PreStutter .

A

The action to which stuttering steps are being added.

id An identifier to distinguish that action A from other actions to which stuttering steps are added. We like to let it be the name of 42

module Stuttering top ∆ = [top → "top"] variables s, vars NoStutter (A) ∆ = (s = top) ∧ A ∧ (s ′ = s) PostStutter (A, actionId , context , bot , initVal , decr ( )) ∆ = if s = top then ∧ A ∧ s ′ = [id → actionId , ctxt → context , val → initVal ] else ∧ s.id = actionId ∧ unchanged vars ∧ s ′ = if s.val = bot then top else [s except ! .val = decr (s.val )]
PreStutter (A, enabled , actionId , context , bot , initVal , decr ( ))

∆ = if s = top then ∧ enabled ∧ unchanged vars ∧ s ′ = [id → actionId , ctxt → context , val → initVal ] else ∧ s.id = actionId ∧ if s.val = bot then ∧ s.ctxt = context ∧ A ∧ s ′ = top else ∧ unchanged vars ∧ s ′ = [s except ! .val = decr (s.val )]
Figure 15: The beginning of the Stuttering module.

the action (which is a string).

bot

The ⊥ (smallest) element of Σ.

initVal The value we have been calling by that name.

decr The operator we have been calling by that name. It must take a single argument.

enabled A formula that should be equivalent to enabled A. We can often find such a formula that TLC can evaluate much more efficiently than enabled A. You can use TLC to check that enabled is equivalent to enabled A by checking that enabled ≡ enabled A is an invariant of the original specification.

context The tuple of context identifiers of A. (You can use i instead of a 1-tuple i .) The context argument is used in the PostStutter 43

MayPostStutter (A, actionId , context , bot , initVal , decr ( )) ∆ = if s = top then ∧ A ∧ s ′ = if initVal = bot then s else [id → actionId , ctxt → context , val → initVal ] else ∧ s.id = actionId ∧ unchanged vars ∧ s ′ = if decr (s.val ) = bot then top else [s except ! .val = decr (s.val )] MayPreStutter (A, enabled , actionId , context , bot , initVal , decr ( )) ∆ = if s = top then ∧ enabled ∧ if initVal = bot then A ∧ (s ′ = s) else ∧ unchanged vars ∧ s ′ = [id → actionId , ctxt → context , val → decr (initVal )] else ∧ s.id = actionId ∧ if s.val = bot then ∧ s.ctxt = context ∧ A ∧ s ′ = top else ∧ unchanged vars ∧ s ′ = [s except ! .val = decr (s.val )]
Figure 16: The end of the Stuttering module.

action only to set the ctxt component of s. This component may be used in defining refinement mappings.

Note that PostStutter and PreStutter add at least one stuttering step, adding exactly one such step if initVal = bot . It is often more convenient to use operators that add one fewer stuttering step. These are the operators MayPostStutter and MayPreStutter defined in the Stuttering module as shown in Figure 16. Unlike the original definitions, the actions they define do not execute any stuttering step when initVal equals bot . As a simple example, let formula Spec be defined as in Figure 17 to equal the hour clock specification of (5.1). Let us suppose that a module HourMin defines a formula Spec to equal the hour-minute clock specification Spec 2 of (5.2). To construct a refinement mapping under which the hour clock specification implements the hour-minute clock specification, we add 59 stuttering steps before 44 module Hour extends Integers each Next step of the hour-clock specification. The obvious way to do that is to let Σ be the set 1 . . 59 ordered by < , with ⊥ equal to 1 and initVal equal to 59. However, our refinement mapping becomes simpler if we use the reverse ordering > of 1 . . 59, with ⊥ equal to 59 and initVal equal to 1. The refinement mapping can then define m to equal 0 when s = ⊤ and s.val when s = ⊤.

variable h Init ∆ = h = 0 Next ∆ = h ′ = (h + 1) % 24 Spec ∆ = Init ∧ 2[Next ] h
We use the operator PreStutter of the Stuttering module to define Next s . We instantiate that module with vars equal to h and with s equal to the stuttering variable, which we also call s. For the arguments of PreStutter , observe that:

• Next is always enabled, so enabled Next equals true.

• Since we are adding stuttering steps to only one action, it doesn't matter what constant we choose for the actionId argument.

• Next , which is the only subaction in the trivial disjunctive representation of Next , has a null context. We can therefore let the context argument be any constant.

We therefore add the following to the end of module Hour .

vars ∆ = h variable s instance Stuttering InitS ∆ = Init ∧ (s = top) NextS ∆ = PreStutter (Next , true, "Next", " ", 59, 1, lambda j : j + 1) SpecS ∆ = InitS ∧ 2[NextS ] vars, s HM ∆ = instance HourMin with m ← if s = top then 0 else s.val theorem SpecS ⇒ HM ! Spec
TLC can easily check this theorem.

Correctness of Adding a Stuttering Variable

How do we check that adding a stuttering variable using the operators of the Stuttering module produces a specification Spec s such that ∃ ∃ ∃ ∃ ∃ ∃ s : Spec s is equivalent to the original specification Spec? The construction ensures that each behavior of Spec s is obtained by adding stuttering steps to a behavior of Spec, so ∃ ∃ ∃ ∃ ∃ ∃ s : Spec s implies Spec. It can fail to be equivalent to Spec only if it either adds an infinite sequence of stuttering steps, or if we have used an incorrect enabled argument for PreStutter . It will be equivalent to Spec if the following conditions are satisfied for every use of the PostStutter and PreStutter operators, with arguments named as above, for some constant set Σ:

1. For every σ in Σ, the sequence of values σ, decr (σ), decr (decr (σ)), . . . is contained in Σ and eventually reaches bot .

2. initVal is in Σ.

enabled is equivalent to enabled A [for PreStutter only]

Condition 1 is a condition only on the constants Σ, bot , and decr . It can be written as StutterConstantCondition(Σ, bot , decr ) using the following definition from the Stuttering module:

StutterConstantCondition(Sigma, bot , decr ( )) ∆ = let InverseDecr (S ) ∆ = {sig ∈ Sigma \ S : decr (sig) ∈ S } R[n ∈ Nat ] ∆ = if n = 0 then {bot } else let T ∆ = R[n -1] in T ∪ InverseDecr (T ) in Sigma = union {R[n] : n ∈ Nat }
This condition can be checked by TLC by putting it into an assume statement or else putting it in the Evaluate Constant Expression field of a model's Model Checking Results page. In either case, the model must replace Nat by a 0 . . n for a (sufficiently large) integer n, and Σ must also be replaced with a finite set if it is infinite. The Stuttering module defines AltStutterConstantCondition to be equivalent to StutterConstantCondition if Σ is finite, and it doesn't require redefining Nat .

The last two conditions are ones that need only hold for behaviors of Spec. They can be stated formally as follows, where A is a subaction with context k; K :

Spec ⇒ 2[∀ k; K : A ⇒ (initVal ∈ Σ)] vars (5.6) Spec ⇒ 2(∀ k; K : enabled ≡ enabled A) (5.7)
TLC can check them in the obvious way.

Adding Infinite Stuttering

The type of stuttering variable we have been describing adds a finite number of stuttering steps before or after a step of a subaction. There is another type of stuttering variable that adds an infinite number of stuttering steps not associated with an action. You are unlikely ever to have to use one, but we include it for completeness.

Suppose we want to find a refinement mapping under which a spec Spec 1 that allows only halting behaviors implements a spec Spec 2 that allows behaviors in which externally visible variables stop changing, but internal variables keep changing forever. We obviously can't do that, because if all the variables of Spec 1 stop changing, then no expression defined in terms of those variables can keep changing forever. None of the methods we have described thus far for adding an auxiliary variable a to Spec 1 can help us, because they all have the property that if every behavior allowed by Spec 1 halts, then so does every behavior allowed by Spec a 1 . It's hard to devise a practical example in which this problem would arise. One possibility is for Spec 2 to have a server perform internal actions looking for user input that may never arrive, while in Spec 1 the server just waits for input. Although unlikely to arise, the problem is easy to solve, so we briefly sketch a solution.

The solution is to add a stuttering variable that is required to stutter forever. Let Spec equal Init ∧ 2[Next ] vars and let UC be the stuttering action unchanged vars . Since [Next ] vars equals Next ∨ UC , we can write Spec as Init ∧ 2[Next ∨ UC ] vars . We can therefore add the subaction UC to any disjunctive representation of Next . We add a history variable s as described in Section 3, using a disjunctive representation containing the subaction UC . This defines an action A s for every subaction A and produces the specification Init s ∧ 2[Next s ] vars,s . (We choose UC s so it implies s ′ = s.) We then define Spec s to equal

Init s ∧ 2[Next s ] vars,s ∧ WF vars,s (UC s )
Since enabled UC s equals true, the fairness requirement WF vars,s (UC s ) implies that infinitely many UC s steps occur. These are steps that leave the variables in vars unchanged, changing only s. Since we have added s as a history variable, ∃ ∃ ∃ ∃ ∃ ∃ s : Init s ∧ 2[Next s ] vars,s is equivalent to Spec. Since any TLA + spec allows stuttering steps, this implies that ∃ ∃ ∃ ∃ ∃ ∃ s : Spec s is equivalent to Spec.

Liveness

Liveness poses no problem when adding a stuttering variable. As with other auxiliary variables, we obtain Spec s by adding the stuttering variable to the safety part of Spec and then conjoining to it the liveness conjunct of Spec. (This 47 is true as well for the kind of stuttering variable described in Section 5.4, where Spec s contains a liveness conjunct.)

Although Spec s may have an unusual form, it isn't weird. If Spec is machine closed then Spec s is also machine closed. However, putting it into a standard form with fairness conditions only on subactions of Next s is not as simple as it is for history variables.

The Snapshot Problem

We now consider an example of using auxiliary variables to show that an algorithm satisfies its specification. Our example is based on an algorithm of Afek et al. [START_REF] Afek | Atomic snapshots of shared memory[END_REF]. Their algorithm implements what they call a single-writer atomic snapshot memory, which will call simply a snapshot object. Their algorithm implements a snapshot object using an unbounded amount of storage. They also present a second algorithm that uses a bounded amount of storage and implements a more general type of object, but we restrict ourselves to their first, simpler algorithm. Moreover, we consider only a simplified version of this simpler algorithm; their algorithm can be checked by adding the same auxiliary variables used for the simplified version.

Linearizability

A snapshot algorithm is used to implement an atomic read of an array of memory registers, each of which can be written by a different process. Its specification is a special case of a linearizable specification of a data object-a concept introduced by Herlihy and Wing [START_REF] Herlihy | Axioms for concurrent objects[END_REF].

A data object, also called a state machine, executes commands from user processes. It is described by an initial state of the object and an operator Apply, where Apply(i, cmd , st ) describes the output and new state of the object that results from process i executing command cmd when the object has state st . It is specified formally by these declared constants: constants Procs, Commands( ), Outputs( ), InitObj , Apply( , , )

They have the following meanings:

Procs

The set of processes.

Commands(i)

The set of commands that process i can issue.

Outputs(i)

The set of outputs the commands issued by process i can produce.

InitObj

The initial state of the object.

Apply(i, cmd , st ) A record with output and newState fields describing the result of process i executing command cmd when the object is in state st .

A linearizable implementation of the data object is one in which the state of the object is internal, the only externally visible actions being the issuing of the command and the return of its output. More precisely, a process i executes a command cmd with a BeginOp(i, cmd ) step, followed by a DoOp(i) step that modifies the state of the object, followed by an EndOp(i) step. The BeginOp and EndOp steps are externally visible, meaning that they modify externally visible variables (and perhaps internal variables), while the DoOp step modifies only internal variables-including an internal variable describing the state of the object.

To simplify the specification, we assume that the sets of commands and of outputs are disjoint. We can then use a single externally visible variable interface, letting BeginOp(i, cmd ) set interface [i] to the command cmd and letting EndOp(i) set it to the command's output. We also introduce an internal variable istate to hold the internal state of the processes-needed to remember, while a process is executing a command, whether or not it has performed the DoOp step and, if it has, what output was produced. We do this by letting BeginOp(i, cmd ) set istate [i] to cmd , and letting DoOp(i) set it to the command's output. Here is the definition of the next-state action and its subactions.

BeginOp(i, cmd

) ∆ = ∧ interface[i] ∈ Outputs(i) ∧ interface ′ = [interface except ! [i] = cmd ] ∧ istate ′ = [istate except ! [i] = cmd ] ∧ object ′ = object DoOp(i) ∆ = ∧ interface[i] ∈ Commands(i) ∧ istate[i] = interface[i] ∧ let result ∆ = Apply(i, interface[i], object ) in ∧ object ′ = result .newState ∧ istate ′ = [istate except ! [i] = result .output ] ∧ interface ′ = interface EndOp(i) ∆ = ∧ interface[i] ∈ Commands(i) ∧ istate[i] ∈ Outputs(i) ∧ interface ′ = [interface except ! [i] = istate[i]] ∧ unchanged object , istate Next ∆ = ∃ i ∈ Procs : ∨ ∃ cmd ∈ Commands(i) : BeginOp(i, cmd ) ∨ DoOp(i) ∨ EndOp(i)
Initially, interface[i] and istate[i] equal some output, for each i. We let that 49 module Linearizability constants Procs, Commands( ), Outputs( ), InitOutput ( ),

ObjValues, InitObj , Apply( , , )

assume equal InitOutput (i) for some constant operator InitOutput . We also add a fairness requirement to imply that any command that has begun (with a BeginOp step) eventually completes (with an EndOp step). The complete specification (with the action definitions above elided) is in module Linearizability, shown in Figure 18. Any particular linearizable object can be specified by instantiating the module with the appropriate constants. The module includes an assumption named LinearAssumps, to check that the instantiated constants satisfy the properties they should for the module to specify a linearizable object. To state all those properties, the specification introduces a constant ObjValues to describe the set of all possible states of the object. This set could be defined to equal the following rather complicated expression. Trying to understand it provides a good lesson in set theory.

LinearAssumps ∆ = ∧ InitObj ∈ ObjValues ∧ ∀ i ∈ Procs : InitOutput (i) ∈ Outputs(i) ∧ ∀ i ∈ Procs : Outputs(i) ∩ Commands(i) = {} ∧ ∀ i ∈ Procs,
Init ∆ = ∧ object = InitObj ∧ interface = [i ∈ Procs → InitOutput (i)] ∧ istate = [i ∈ Procs → InitOutput (i)] BeginOp(i, cmd ) ∆ = . . . DoOp(i) ∆ = . . . EndOp(i) ∆ = . . . Next ∆ = . . . SafeSpec ∆ = Init ∧ 2[Next ] vars
let ApplyProcTo(i, S )

∆ = {Apply(i, cmd , x ).newState : x ∈ S , cmd ∈ Commands(i)} ApplyTo(S ) ∆ = union {ApplyProcTo(i, S ) : i ∈ Procs} ApplyITimes[i ∈ Nat ] ∆ = if i = 0 then {InitObj } else ApplyTo(ApplyITimes[i -1]) in union {ApplyITimes[i] : i ∈ Nat }

The Linearizable Snapshot Specification

By a snapshot object, we mean what Afek et al. [START_REF] Afek | Atomic snapshots of shared memory[END_REF] called an atomic snapshot memory. In a snapshot object, the processes are either readers or writers.

Reader and writer should be thought of as roles; the same physical process can act as both a reader and a writer. A snapshot object is an array of registers, one per writer. A write operation writes a value to the writer's register and produces as output some fixed value that is not a possible register value. A read operation has a single command that produces the object's state (an array of register values) as output and leaves that state unchanged. The specification declares four constants: the sets Readers and Writers of reader and writer processes; the set RegVals of possible register values; and a value InitRegVal in RegVals that is the initial value of a register. We call the snapshot object a memory and use different names for some of the parameters of the Linearizability module, including MemVals and InitMem for ObjValues and InitObj . We define NotMemVal be the single reader command and NotRegVal to be the single write command output. The complete specification is in module LinearSnapshot of Figure 19. (The assume is added at the end of the module so TLC will check that the assumption LinearAssumps of module Linearizability is true under the instantiation.)

The Simplified Afek et al. Snapshot Algorithm

The snapshot algorithm of Afek et al. uses an internal variable imem whose value is an array with imem[i] a pair consisting of the value of the i th register and an integer whose value is the number of times the register has been written. It assumes that the entire pair can be read and written atomically.

A write operation writes the register value cmd in the obvious way, the

DoOp(i) action setting imem[i] to cmd , imem[i][2] + 1 .
A read operation first performs the following scan procedure:

It reads all the elements imem[i] once, in any order. It then reads them a second time, again in any order. If it reads the same values both times for all i, it outputs the array of register values it read.

module LinearSnapshot constants Readers, Writers, RegVals, InitRegVal If the values obtained for each element imem[i] by the two reads are not all the same, so the scan procedure does not produce an output, then the procedure is repeated. The scan procedure is repeated again and again until it produces an output.

assume ∧ Readers ∩ Writers = {} ∧ InitRegVal ∈ RegVals Procs ∆ = Readers ∪ Writers MemVals ∆ = [Writers → RegVals] InitMem ∆ = [i ∈ Writers → InitRegVal ] NotMemVal ∆ = choose v : v / ∈ MemVals NotRegVal ∆ = choose v : v / ∈ RegVals Commands(i) ∆ = if i ∈ Readers then {NotMemVal } else RegVals Outputs(i) ∆ = if i ∈ Readers then MemVals else {NotRegVal } InitOutput (i) ∆ = if i ∈ Readers then InitMem else NotRegVal Apply(i, cmd , obj ) ∆ = if i ∈ Readers then [newState → obj , output → obj ] else [newState → [obj except ! [i] = cmd ], output → NotRegVal ]
The actual algorithm has an alternative method of producing an output that can be used when it has read three different values for imem [i], for some writer i. By using this method, termination of the read is assured. However, for simplicity, we use an algorithm that keeps performing the scan procedure until it succeeds in producing an output. Thus, a read need never terminate, so the algorithm does not satisfy the liveness requirement of a snapshot algorithm-52 namely, it does not satisfy the weak fairness requirement of the DoOp(i) action for a reader i. However, it does satisfy the safety requirement. The correctness of the complete algorithm (including liveness) can be verified by essentially the same method used for our simplified version; but the complete algorithm is more complicated, so the refinement mapping is more complicated and model checking takes longer. We therefore consider only the simplified algorithm.

To specify the algorithm in TLA + , we declare the same constants Readers, Writers, RegVals, and InitRegVal and make the same definitions of MemVals, InitMem, NotMemVal , and NotRegVal as in module LinearSnapshot above. We also define:

IRegVals ∆ = RegVals × Nat IMemVals ∆ = [Writers → IRegVals] InitIMem ∆ = [i ∈ Writers → InitRegVal , 0 ]
We declare five variables, with the following meanings: BeginWr (i, cmd )

∆ = ∧ interface[i] = NotRegVal ∧ wrNum ′ = [wrNum except ! [i] = wrNum[i] + 1] ∧ interface ′ = [interface except ! [i] = cmd ] ∧ unchanged imem, rdVal 1, rdVal 2 DoWr (i) ∆ = ∧ interface[i] ∈ RegVals ∧ imem[i][2] = wrNum[i] ∧ imem ′ = [imem except ! [i] = interface[i], wrNum[i] ] 53
∧ unchanged interface, wrNum, rdVal 1, rdVal 2

EndWr (i) ∆ = ∧ interface[i] ∈ RegVals ∧ imem[i][2] = wrNum[i] ∧ interface ′ = [interface except ! [i] = NotRegVal ] ∧ unchanged imem, wrNum, rdVal 1, rdVal 2
The BeginRd (i) action is straightforward.

BeginRd (i) ∆ = ∧ interface[i] ∈ MemVals ∧ interface ′ = [interface except ! [i] = NotMemVal ] ∧ unchanged imem, wrNum, rdVal 1, rdVal 2
The definitions of the actions that perform the scan procedure use the following definition. We define AddToFcn(f , x , v ) to be the function g obtained from the function f by adding x to its domain and defining g[x ] to equal v . Using operators defined in the TLC module, it can be defined to equal f @@(x : > v ). However, it's easy enough to define it directly as:

AddToFcn(f , x , v ) ∆ = [y ∈ (domain f ) ∪ {x } → if y = x then v else f [y]]
Using AddToFcn, we define the Rd 1 action that performs the scan's first read of imem and the Rd 2 action that performs its second read.

Rd 1(i) ∆ = ∧ interface[i] = NotMemVal ∧ ∃ j ∈ Writers \ domain rdVal 1[i] : rdVal 1 ′ = [rdVal 1 except ! [i] = AddToFcn(rdVal 1[i], j , imem[j ])] ∧ unchanged interface, imem, wrNum, rdVal 2 Rd 2(i) ∆ = ∧ interface[i] = NotMemVal ∧ domain rdVal 1[i] = Writers ∧ ∃ j ∈ Writers \ domain rdVal 2[i] : rdVal 2 ′ = [rdVal 2 except ! [i] = AddToFcn(rdVal 2[i], j , imem[j ])] ∧ unchanged interface, imem, wrNum, rdVal 1
Finally, we define TryEndRd (i) to be an action that is enabled when the reader's scan operation has completed. It compares the values read by the two sets of reads and, if they are equal, it performs the EndOp for the read. Otherwise, it enables the next scan to begin.

TryEndRd (i) ∆ = ∧ interface[i] = NotMemVal ∧ domain rdVal 1[i] = Writers ∧ domain rdVal 2[i] = Writers 54 ∧ if rdVal 1[i] = rdVal 2[i] then interface ′ = [interface except ! [i] = [j ∈ Writers → rdVal 1[i][j ][1]]] else interface ′ = interface ∧ rdVal 1 ′ = [rdVal 1 except ! [i] = ] ∧ rdVal 2 ′ = [rdVal 2 except ! [i] = ] ∧ unchanged imem, wrNum
The complete specification is in module AfekSimplified , shown in Figure 20 with the action definitions above elided.

Another Snapshot Specification

The algorithm in module AfekSimplified satisfies the safety specification in LinearSnapshot , but we now show that it does not implement that safety specification under any refinement mapping. Let Spec A be the algorithm's specification and let SSpec L be the specification SafeSpec of LinearSnapshot . We assume there is a refinement mapping mem ← mem and istate ← istate under which Spec A implements SSpec L and obtain a contradiction. Let F be the formula obtained from a formula F of module LinearSnapshot by replacing mem with mem and istate with istate. Consider a behavior satisfying Spec A that begins with the following three sequences of steps.

∆ = [Writers → RegVals] InitMem ∆ = [i ∈ Writers → InitRegVal ] NotMemVal ∆ = choose v : v / ∈ MemVals NotRegVal ∆ = choose v : v / ∈ RegVals IRegVals ∆ = RegVals × Nat IMemVals ∆ = [Writers → IRegVals] InitIMem ∆ = [i ∈ Writers → InitRegVal , 0 ] variables imem, interface, wrNum, rdVal 1, rdVal 2 vars ∆ = imem, interface, wrNum, rdVal 1, rdVal 2 Init ∆ = ∧ imem = InitIMem ∧ interface = [i ∈ Readers ∪ Writers → if i ∈ Readers then InitMem else NotRegVal ] ∧ wrNum = [i ∈ Writers → 0] ∧ rdVal 1 = [i ∈ Readers → ] ∧ rdVal 2 = [i ∈ Readers → ] BeginWr (i, cmd ) ∆ = . . . DoWr (i) ∆ = . . . EndWr (i) ∆ = . . . BeginRd (i) ∆ = . . . AddToFcn(f , x , v ) ∆ = . . . Rd 1(i) ∆ = . . . Rd 2(i) ∆ = . . . TryEndRd (i) ∆ = . . . Next ∆ = ∨ ∃ i ∈ Readers : BeginRd (i) ∨ Rd 1(i) ∨ Rd 2(i) ∨ TryEndRd (i) ∨ ∃ i ∈ Writers : ∨ ∃ cmd ∈ RegVals : BeginWr (i, cmd ) ∨ DoWr (i) ∨ EndWr (i) Spec ∆ = Init ∧ 2[Next ] vars Figure 20: Module AfekSimplified Since v 1 = v 2
, this is a contradiction, showing that the refinement mapping cannot exist. This behavior of Spec A is allowed by ∃ ∃ ∃ ∃ ∃ ∃ mem, istate : SSpec L , since we can choose values of mem and istate for which SSpec L is satisfied-namely, values for which the DoRd (i) step occurs before the DoWr (j ) step. However, choosing those values requires knowing what steps occur after the DoWr (j ) step. The linearizability specification SSpec L chooses the value returned by a read sooner than it has to. This tells us that to find a refinement mapping that shows Spec A implements ∃ ∃ ∃ ∃ ∃ ∃ mem, istate : SSpec L , we must add a prophecy variable to Spec A . Instead of adding a prophecy variable to Spec A , we write a new snapshot specification Spec NL that allows the same externally visible behaviors as specification Spec L of LinearSnapshot ; and whose safety specification SSpec NL allows the same visible behaviors as SSpec L . However, in Spec NL we make a reader wait as long as possible before choosing its output value. We can then find a refinement mapping to show that Spec A implements SSpec NL without using a prophecy variable.

We will still need a prophecy variable to show that SSpec NL allows the same externally visible behavior as SSpec L . The advantage of introducing Spec NL is that the specification of what an algorithm is supposed to do is generally much simpler than the algorithm. Prophecy variables are the most complicated kind of auxiliary variables, and it is easier to add one to a high-level specification than to a lower-level algorithm. (This same idea of modifying the high-level specification to avoid adding a prophecy variable to the algorithm can be applied to the queue example of Herlihy and Wing [START_REF] Herlihy | Axioms for concurrent objects[END_REF].)

Specification Spec NL records in its internal state all values of the memory mem that a read operation is allowed to return. The EndRd operation nondeterministically chooses one of those values as its output. Its internal state therefore remembers much more about what happened in the past than a reasonable implementation would. This means that defining a refinement mapping under which an algorithm implements Spec NL will require adding a history variable to the algorithm's spec. Adding a history variable is much easier than adding a prophecy variable.

We The BeginWr command is essentially the same as in LinearSnapshot .

BeginWr (i, cmd ) ∆ = ∧ interface[i] = NotRegVal ∧ interface ′ = [interface except ! [i] = cmd ] ∧ wstate ′ = [wstate except ! [i] = cmd ] ∧ unchanged mem, rstate
The BeginRd (i) command, which sets rstate[i] to a one-element sequence containing the current value of mem, is:

BeginRd (i) ∆ = ∧ interface[i] ∈ MemVals ∧ interface ′ = [interface except ! [i] = NotMemVal ] ∧ rstate ′ = [rstate except ! [i] = mem ] ∧ unchanged mem, wstate
The writer executes a DoWr that is the same as in LinearSnapshot , except that it also appends the new value of mem to the end of rstate[j ] for every reader j currently executing a read operation.

DoWr (i) ∆ = ∧ interface[i] ∈ RegVals ∧ wstate[i] = interface[i] ∧ mem ′ = [mem except ! [i] = interface[i]] ∧ wstate ′ = [wstate except ! [i] = NotRegVal ] ∧ rstate ′ = [j ∈ Readers → if rstate[j ] = then else Append (rstate[j ], mem ′ )] ∧ interface ′ = interface
A reader i has no internal actions, only the externally visible BeginRd (i) and EndRd (i) actions. Its EndRd (i) action outputs an arbitrarily chosen element of rstate [i].

EndRd (i) ∆ = ∧ interface[i] = NotMemVal ∧ ∃ j ∈ 1 . . Len(rstate[i]) : interface ′ = [interface except ! [i] = rstate[i][j ]] ∧ rstate ′ = [rstate except ! [i] = ] ∧ unchanged mem, wstate
The writer's EndWr action is essentially the same as in LinearSnapshot .

EndWr (i) ∆ = ∧ interface[i] ∈ RegVals ∧ wstate[i] = NotRegVal ∧ interface ′ = [interface except ! [i] = wstate[i]] ∧ unchanged mem, rstate, wstate
The complete module, minus the action definitions above, is in Figure 21.

module NewLinearSnapshot extends Integers, Sequences constants Readers, Writers, RegVals, InitRegVal For compactness, in the following discussion we let:

assume ∧ Readers ∩ Writers = {} ∧ InitRegVal ∈ RegVals InitMem ∆ = [i ∈ Writers → InitRegVal ] MemVals ∆ = [Writers → RegVals] NotMemVal ∆ = choose v : v / ∈ MemVals NotRegVal ∆ = choose v : v / ∈
= ∧ mem = InitMem ∧ interface = [i ∈ Readers ∪ Writers → if i ∈ Readers then InitMem else NotRegVal ] ∧ rstate = [i ∈ Readers → ] ∧ wstate = [i ∈ Writers → NotRegVal ] BeginRd (i) ∆ = . . . BeginWr (i, cmd ) ∆ = . . . DoWr (i) ∆ = . . . EndRd (i) ∆ = . . . EndWr (i) ∆ = . . . Next ∆ = ∨ ∃ i ∈ Readers : BeginRd (i) ∨ EndRd (i) ∨ ∃ i ∈ Writers : ∨ ∃ cmd ∈ RegVals : BeginWr (i, cmd ) ∨ DoWr (i) ∨ EndWr (i) SafeSpec ∆ = Init ∧ 2[Next ] vars Fairness ∆ = ∧ ∀ i ∈ Readers : WF vars (EndRd (i)) ∧ ∀ i ∈ Writers : WF vars (DoWr (i)) ∧ WF vars (EndWr (i)) Spec ∆ = Init ∧ 2[Next ] vars ∧ Fairness
S L ∆ = ∃ ∃ ∃ ∃ ∃ ∃ mem, istate : Spec L S NL ∆ = ∃ ∃ ∃ ∃ ∃ ∃ mem, rstate, wstate : Spec NL
Specifications S L and S NL are equivalent. However, our goal is to prove that Spec A implements S L , for which it suffices to show that it implements specification S NL and that S NL implements S L . So, we won't bother showing equivalence of the two specs; we just show here that S NL implements S L . We show in Section 6.6 below that Spec A implements S NL .

To show that S NL implements S L , we add to Spec NL a prophecy variable p then a stuttering variable s to obtain a specification Spec ps NL such that ∃ ∃ ∃ ∃ ∃ ∃ s, p : Spec ps NL is equivalent to Spec NL . We then show that ∃ ∃ ∃ ∃ ∃ ∃ s, p : Spec ps NL implements S L by showing that Spec ps NL implements Spec L under a suitable refinement mapping mem ← mem, istate ← istate.

The two auxiliary variables we add to Spec NL have the following functions:

p A prophecy variable that predicts for each reader i which element of the sequence of memory values rstate[i] will be chosen as the output.

s A stuttering variable that adds:

• A single stuttering step after a BeginRd (i) step if p[i] predicts that the read will return the current value of memory. The refinement mapping will be defined so that stuttering step will be a DoRd (i). • Stuttering steps after a DoWr (i) step that will implement the DoRd (j ) step of every current read operation that returns the value of mem immediately after the DoWr (i) step.

Both these variables are added in a single module named NewLinearSnapshotPS .

Adding the Prophecy Variable

The prophecy variable p is a prophecy data structure variable as described in Section 4.4. Its domain Dom is the set of readers that are currently executing a read, which can be described as the set of readers i such that rstate[i] is a nonempty sequence. The value of p[i] is a positive integer that predicts which element of the list rstate[i] will be chosen as the output. This value can be arbitrarily large, since arbitrarily many writes can occur during a read operation, so Π is the set Nat \ {0}. A prediction is made for reader i when the element i is added to Dom, which is done by a BeginRd (i) step. The prediction is used by the IEndRd (i, j ) action, allowing it to be performed only if p[i] has predicted that the j th item in the sequence rstate[i] will be output. The definitions of Pred A , PredDom A , and DomInj A for the subactions A are given along with the beginning of the module in Figure 22. The module next defines the temporal formula Condition, which should be implied by Spec. There follows the definition of the specification SpecP obtained by adding the prophecy variable p to Spec. TLC can check that Condition is implied by Spec, which implies that ∃ ∃ ∃ ∃ ∃ ∃ p : SpecP is equivalent to Spec. These definitions appear in Figure 23.

Adding the Stuttering Variable

The module next adds the stuttering variable s to SpecS . We need to add a single stuttering step after a BeginRdP (i) step iff the reader will output the current value of mem, which is the case iff the step sets p[i] to 1. We also need to add a stuttering step after DoWrP (i) for every currently reading reader j for which p[j ] predicts that the value of mem that the step appends to rstate[j ] is the one that the read will output. These steps are added by letting the values of s.val be subsets of readers, ordered by the subset relation, with the decrement operation removing an element from the set chosen with the choose operator.

The specification SpecPS obtained by adding the stuttering variable s to SpecP is defined in the part of module NewLinearSnapshotPS shown in Figure 24. 61 The two theorems at the beginning are conditions (5.6) for adding the stuttering steps to BeginRdP (i) and DoWrP (i) steps. They can be checked by temporarily ending the module immediately after those theorems and running TLC on a model having SpecP as its specification. Two assume statements have been added to check the constant conditions on the arguments of the MayPostStutter operators used to add those stuttering steps.

The Refinement Mapping

Let's again use the abbreviations Spec L for formula Spec of LinearSnapshot and Spec PS for formula SpecPS of module NewLinearSnapshot . We now define the state functions mem and istate such that Spec PS implements Spec L under the refinement mapping mem ← mem, istate ← istate. We want writer actions of Spec L to be simulated by the corresponding writer actions of Spec PS . Hence, we let mem equal mem and we let istate[i] equal wstate [i] for every writer i. The problem is defining istate[i] for readers i.

In Spec L , for any process i not executing a read or write, istate[i] equals interface [i]. Hence, we can define istate[i] to equal interface[i] for any reader i not currently reading. We now consider the case when i is currently reading, which is true iff rstate[i] = , which implies p[i] is a positive integer. There are two possibilities: p[i] = 1 In this case, the DoRd (i) step of Spec L is simulated by the stuttering step added to BeginRd (i). The DoRd (i) step changes istate[i] from NotMemVal to the memory value to be output, so istate[i] should equal rstate[i] [START_REF] Abadi | The prophecy of undo[END_REF] when rstate[i] = , except after the BeginRd (i) step and before the stuttering step added immediately after it.

p[i] > 1 In this case, the DoRd (i) step of Spec L is simulated by one of the stuttering steps added to the DoWr (j ) step for the writer that appends the p[i] th element to rstate [i]. We let it be the stuttering step that removes i from s.val , so istate[i] equals NotMemVal until p[i] ≤ Len(rstate [i]) and it's not the case that i is an element of s.val while some writer is performing a stuttering step added after its DoWr step.

The definition of istate, under the name istateBar , appears near the end of the module, shown in Figure 25. The theorems at the end of the module can be checked with TLC. In fact, TLC checks that SpecPS satisfies property LS !Spec by checking that the safety part of SpecPS satisfies both (a) the safety part of LS !Spec and (b) the property that the liveness part of SpecPS implies the liveness part of LS !Spec. Therefore, having TLC check that SpecPS satisfies LS !Spec checks both theorems.

AfekSimplified Implements NewLinearSnapshot

We now finish checking the correctness of the algorithm Spec A of AfekSimplified by showing that it implements ∃ ∃ ∃ ∃ ∃ ∃ mem, rstate, wstate : SSpec NL , where SSpec NL is the safety specification of NewLinearSnapshot . As we suggested in Section 6.4, finding a refinement mapping to show this requires adding a history variable to Spec A that captures the information remembered by SSpec NL in the variable rstate. This is straightforward. We just add a history variable h such that h[i] is changed by BeginRd (i), DoWr (i), and an ending TryEndRdH

EndWrH (i) ∆ = EndWr (i) ∧ (h ′ = h) BeginRdH (i) ∆ = ∧ BeginRd (i) ∧ h ′ = [h except ! [i] = memBar ] Rd 1H (i) ∆ = Rd 1(i) ∧ (h ′ = h) Rd 2H (i) ∆ = Rd 2(i) ∧ (h ′ = h) TryEndRdH (i) ∆ = ∧ TryEndRd (i) ∧ h ′ = if rdVal 1[i] = rdVal 2[i] then [h except ! [i] = ] else h NextH ∆ = ∨ ∃ i ∈ Readers : BeginRdH (i) ∨ Rd 1H (i) ∨ Rd 2H (i) ∨ TryEndRdH (i) ∨ ∃ i ∈ Writers : ∨ ∃ cmd ∈ RegVals : BeginWrH (i, cmd ) ∨ DoWrH (i) ∨ EndWrH (i) SpecH ∆ = InitH ∧ 2[NextH ] varsH

===

  choose t ∈ S : ∀ s ∈ S : t ≥ s setMin(S ) ∆ = choose t ∈ S : ∀ s ∈ S : t ≤ s constants Lo, Hi, Both, None assume {Lo, Hi, Both, None} ∩ Int = {} variables x , turn, y vars ∆ = x , turn, yInit ∆ = ∧ x = None ∧ turn = "input" ∧ y = {} InputNum ∆ = ∧ turn = "input" ∧ turn ′ = "output" ∧ x ′ ∈ Int ∧ y ′ = y Respond ∆ = ∧ turn = "output" ∧ turn ′ = "input" ∧ y ′ = y ∪ {x } ∧ x ′ = if x = setMax (y ′ ) then if x = setMin(y ′ ) then Both else Hi else if x = setMin(y ′ ) then Lo else None Next ∆ InputNum ∨ Respond Spec ∆ Init ∧ 2[Next ] vars

Figure 1 :

 1 Figure 1: Module MinMax 1.

Figure 2 :

 2 Figure 2: Module MinMax 2.

Figure 3 :

 3 Figure 3: Additions to module MinMax 1.

1

 1 Equivalence of MinMax 1 and MinMax 2

Figure 7 :

 7 Figure 7: Specification SendInt1P

Figure 9 :

 9 Figure 9: Specification SendSetUndo.

Figure=

  Figure 10: Specification SendSetUndoP

Figure 11 :

 11 Figure 11: Specification SendSeq

Figure 12 :

 12 Figure 12: Specification SendSeqUndo

  1 of Dom ′ . The formula p ′ ∈ NewPSet A in (4.10) should ensure that if an element d of Dom ′ either corresponds to an element c of Dom that makes a prediction about A or else does not correspond to any element of Dom, then p ′ [d ] can assume any value in Π; but if d corresponds to an element c of Dom that make no prediction about A, then p ′ [d ] equals p[c]. Instead of defining the formulas NewPSet A directly, we will define them in terms of the correspondence between elements of Dom and Dom ′ made by A and the set of elements d in Dom for which p[d ] makes a prediction about A.

For

  each subaction A, we define a partial injection DomInj A from Dom to Dom ′ such that an element c of Dom corresponds to an element d of Dom ′ iff c is in the domain of DomInj A and d = DomInj A [c]. Here are the definitions for the four subactions, which are put in module SendSeqUndoP :

instance

  Prophecy with DomPrime ← Dom ′ PredDomChoose ∆ = {} DomInjChoose

Figure 13 :

 13 Figure13: The specification of SpecUP.

∆=

  instance SendSeq with y ← yBar theorem SpecUP ⇒ SS ! Spec TLC can check this theorem in the usual way.

Figure 14 :

 14 Figure 14: Action requirements for specification SendSeqUndo.

Figure 17 :

 17 Figure 17: The hour clock specification.

Fairness∆=

  Figure 18: Module Linearizability.

Figure 19 :

 19 Figure 19: Module LinearSnapshot.

Figure 21: Module NewLinearSnapshot 6 . 5

 65 Figure 21: Module NewLinearSnapshot

==

  Figure 22: Module NewLinearSnapshotPS, part 1.

Figure 25 :

 25 Figure 25: Module NewLinearSnapshotPS, part 4.

=

  (i) action (one executed with rdVal 1[i] = rdVal 2[i]) the same way rstate[i] is changed by the corresponding BeginRd (i), DoWr (i), and EndRd (i) action of SSpec NL .The specification SpecH , obtained by adding the history variable h to specification Spec of module AfekSimplified , is defined in module AfekSimplified as shown in Figure26. The definition should be easy to understand by comparing the definition of the initial predicate InitH and of the actions in the module to the corresponding definitions in module NewLinearSnapshot . Note that the action definitions use memBar where the corresponding action definitions in NewLinearSnapshot use mem. The module defines memBar to equal the mem-66module AfekSimplifiedH extends AfekSimplified , Sequences variable h varsH ∆ = vars, h InitH ∆ Init ∧ (h = [i ∈ Readers → ]) memBar ∆ = [i ∈ Writers → imem[i][1]] BeginWrH (i, cmd ) ∆ = BeginWr (i, cmd ) ∧ (h ′ = h) DoWrH (i) ∆ = ∧ DoWr (i) ∧ h ′ = [j ∈ Readers → if h[j ] = then else Append (h[j ], memBar ′ )]

Figure 26 :

 26 Figure 26: Beginning of module AfekSimplifiedH.

  Theorem 1 (History Variable) Let Spec equal Init ∧ 2[Next ] vars and let Spec h equal Init h ∧ 2[Next h ] vars h , where: The hypotheses of this theorem are purely syntactic ones: conditions on the definitions of Init h , Next h , and vars h plus conditions on what variables and identifiers may appear in exp Init and exp A . By a variable or identifier appearing in an expression exp, we mean that it appears in the expression [[exp]] obtained by expanding all definitions if exp. (See the discussion of definition expansion on page 7.)

	• Init h equals Init ∧ (h = exp Init ), for some expression exp Init that may
	contain the specification's (unprimed) variables.
	• Next h is obtained from Next by replacing each subaction A of a disjunctive
	representation of Next with A ∧ (h ′ = exp A ) , for some expression exp A
	that may contain primed and unprimed specification variables, identifiers
	in the context of A, and constant parameters.
	• vars h equals vars, h
	Then Spec is equivalent to ∃ ∃ ∃ ∃ ∃ ∃ h : Spec h .

  The only condition we require of DomInj A is that it be a partial function from Dom to Dom ′ . This is expressed as IsDomInj (DomInj A ) using this definition from module Prophecy As with the ExistsGoodProphecy condition, it needs to hold only for A steps in a behavior satisfying the specification Spec. Hence the general requirement on DomInj

	IsDomInj (DomInj )

4.11) as

Spec ⇒ 2[A ⇒ (ExistsGoodProphecy(Pred A )] vars (Remember that the Prophecy module will be instantiated with the appropriate expression substituted for Dom.) To see how this definition is used if A has a non-empty context, here is how condition is (4.11) is expressed for the subaction UndoP (i) of specification SpecU in our SendSeq example:

SpecU ⇒ 2[ ∀ i ∈ Dom : Undo(i) ⇒ ExistsGoodProphecy(lambda p : PredUndo(p, i)) ] vars ∆ = DomInj ∈ PartialInjections(Dom, DomPrime) A for an action A with context k; K is Spec ⇒ 2[∀ k; K : A ⇒ IsDomInj (DomInj A )]

vars Because IsDomInj does not have an operator argument, no local definition or lambda expression is needed even if the context is nonempty. For example, if A is subaction Undo(i) of specification SpecU of the SendSeq example, this condition is written: ∀i ∈ Dom : Undo(i) ⇒ IsDomInj (DomInjUndo(i)) Finally, we need a condition on PredDom A . Remember that PredDom A should equal the set of elements d of Dom such that p[d ] is making predictions about A. Actually, it suffices that PredDom A contain all such elements. (It may contain other elements as well.) This is equivalent to the requirement that any element not in PredDom A does not make a prediction about A. Making a prediction about A means affecting the value of Pred A , so not making a prediction means not affecting its value. Thus, p[d ] does not make a prediction about A iff setting p[d ] to any value in Π does not change the value of Pred A . You should be able to convince yourself that the value of Pred A does not depend on the value of p[d ] for any d not in PredDom A iff the following formula is true:

  DomInjChoose, PredDomChoose, PredChoose) ∧ ProphCondition(Send , DomInjSend , PredDomSend , PredSend )

	∧ ProphCondition(Rcv ,	DomInjRcv ,	PredDomRcv ,	PredRcv )
	∧ ∀ i ∈ Dom :
	ProphCondition(Undo(i), DomInjUndo(i), PredDomUndo(i),
	lambda p : PredUndo(p, i))
	theorem SpecU ⇒ 2[Condition] vars

  interface : The same as in LinearSnapshot . imem : Like mem in LinearSnapshot , except imem[i] is an ordered pair in RegVals × Nat , the first component representing mem[i] and the second the number of times mem[i] has been written. The initial value of imem is initially InitIMem. wrNum : A function with domain Writers, where wrNum[i] is the number of BeginWr (i) steps that have been taken. rdVal 1, rdVal 2 : They are functions such that rdVal 1[i] and rdVal 2[i] describe the values read so far by reader i in the two reads of the scan procedure. Both rdVal 1[i] and rdVal 2[i] are functions whose domain is the set of writers j for which the first or second read of imem[j ] has been performed, mapping each such j to the value read. They are set initially to the empty function (the function with empty domain), which we write .

	The writer actions are straightforward. Note that because wrNum[i] counts
	the number of BeginWr (i, cmd ) steps and imem[i][2] is set to wrNum[i] by
	the DoWr (i), the EndWrite(i) action should be enabled and DoWr (i) disabled
	when imem[i][2] equals wrNum[i].

  The behavior satisfies SSpec L , so this sequence of actions must start with a BeginRd (i) step, contain a DoRd (i) step, and end with an EndRd (i) step. The reader has not determined the value to be output by the read command until it

	module AfekSimplified
	extends Integers
	constants Readers, Writers, RegVals, InitRegVal
	MemVals

1. Reader i does a BeginRd (i) step, completes its first scan (so domain rdVal 1[i] equals Writers) and begins its second scan by reading imem[j ] = v 1 , 0 for some writer j and v 1 in RegVals (so

domain rdVal 2[i] equals {j } and rdVal 2[i][j ] equals v 1 , 0 ).

2. Writer j then does a complete write operation, writing a new value v 2 different from v 1 .

3. Reader i completes its second scan, executes its TryEndRd (i) action, finding rdVal 2[i] equal to rdVal 1[i], and completing the read operation by setting interface[i] to a value M with M [j ] = v 1 . has finished its second scan, so the DoRd (i) step must occur in sequence 3. The three steps of the write of v 2 by writer j occur in sequence 2, so the DoWr (j ) step for that write must occur in that sequence, therefore preceding the DoRd (i) step. Hence, the LinearSnapshot spec implies that the DoRd (i) step must set istate[i][j ] to v 2 . However in the last step of 3, the reader sets the value of interface[i][j ] to v 1 , which implies that the DoRd (i) step set istate[i][j ] to v 1 . 55

  write specification Spec NL (and SSpec NL ) in module NewLinearSnapshot . It has the same declarations of Readers, Writers, RegVals, and InitRegVal and the same definitions of MemVals, InitMem, NotMemVal , and NotRegVal as in module LinearSnapshot . It has the same variables interface and mem as module LinearSnapshot , plus these two internal variables:The first element of rstate[i] is therefore the value mem had when the BeginRd (i) step occurred. The value of rstate[i] is the empty sequence when i is not executing a read operation.

wstate A function with domain Writers such that the value wstate[i] is the same as the value of istate[i] in LinearSnapshot , for each writer i. rstate A function with domain Readers so that, for each reader i currently executing a read operation, rstate[i] is the sequence of values that mem has assumed thus far while the operation has been executing. 57

  Dom ′ 60It is most convenient to define p in terms of a disjunctive representation in which EndRd (i) is decomposed into ∃ j ∈ 1 . . Len(rstate[i]) : IEndRd (i, j ) , where IEndRd can be defined by: NotMemVal∧ interface ′ = [interface except ! [i] = rstate[i][j ]] ∧ rstate ′ = [rstate except ! [i] = ] ∧ unchanged mem, wstateWe could make the change in our original specification NewLinearSnapshot , but instead we define a new next-state action Nxt that is equivalent to Next :Readers : ∨ BeginRd (i) ∨ ∃ j ∈ 1 . . Len(rstate[i]) : IEndRd (i, j ) ∨ ∃ i ∈ Writers : ∨ ∃ cmd ∈ RegVals : BeginWr (i, cmd ) ∨ DoWr (i) ∨ EndWr (i)It's easy to see that Nxt is equivalent to formula Next of NewLinearSnapShot , and TLAPS can easily check this proof.

	IEndRd (i, j )
	Nxt

Module NewLinearSnapshotPS therefore begins

extends NewLinearSnapshot Pi ∆ = Nat \ {0} Dom ∆ = {r ∈ Readers : rstate[r ] = } instance Prophecy with DomPrime ← ∆ = ∧ interface[i] = ∆ = ∨ ∃ i ∈ theorem Next = Nxt by def Next , Nxt , EndRd , IEndRd

There are languages for writing math precisely that allow expression (2.1) even if v is

Note that the declared constants Hi, Lo, Both, and None of module MinMax 2 have been implicitly instantiated by the constants of the same name declared in MinMax 1.

If Mod2 has declared constants, then the statement must also specify expressions to be substituted for those constants. A substitution of the form id ← id for an identifier id can be omitted from the with clause.

Everything we do extends easily to handle unbounded quantification if we pretend that the unbounded quantifiers ∃v and ∀v are written ∃v ∈ Ω and ∀v ∈ Ω, and we define e ∈ Ω to equal true for every expression e. Since unbounded quantification seldom occurs in specifications, we will not discuss this further.

Formula (4.9) does not imply that (4.8) is true for stuttering steps that are allowed by A. It can be shown that this doesn't matter, and condition (4.9) is strong enough.

This means that ⊥ ≺ σ for all σ ∈ Σ, and any decreasing chain σ 1 ≻ σ 2 ≻ . . . of elements in Σ must be finite.

The rest of the refinement mapping is defined at the end of the module, shown in Figure 27. It substitutes h for rstate. The expression wstateBar is substituted for wstate. To understand it, remember that in SSpec NL , the value of wstate[i] for a writer i is NotRegVal except between a BeginWr (i, cmd ) action and a DoWr (i) action, when it equals interface[i] (which equals cmd ).

The theorem was checked by TLC in about 10 hours on a circa 2012 laptop, using a model with: two readers, two writers, and two register values; symmetry of readers and writers (register values aren't symmetric because IntRegVal equals one of them); a state constraint limiting each writer to at most three writes; and two worker threads.