# Prophecy Made Simple

Leslie Lamport, Stephan Merz

► To cite this version:

Leslie Lamport, Stephan Merz. Prophecy Made Simple. ACM Transactions on Programming Languages and Systems (TOPLAS), 2022, 44 (2), pp.1-27. 10.1145/3492545. hal-03636686

HAL Id: hal-03636686

https://inria.hal.science/hal-03636686

Submitted on 11 Apr 2022

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>
# Prophecy Made Simple

LESLIE LAMPORT, Microsoft Research, USA

STEPHAN MERZ, University of Lorraine, CNRS, Inria, LORIA, France

Prophecy variables were introduced in the article "The Existence of Refinement Mappings" by Abadi and Lamport. They were difficult to use in practice. We describe a new kind of prophecy variable that we find much easier to use. We also reformulate ideas from that article in a more mathematical way.

CCS Concepts: • Software and its engineering → Formal software verification; • Theory of computation → Modal and temporal logics; Logic and verification; Program verification;

Additional Key Words and Phrases: Formal specification, state machine, refinement, auxiliary variable

## ACM Reference format:

Leslie Lamport and Stephan Merz. 2022. Prophecy Made Simple. *ACM Trans. Program. Lang. Syst.* 44, 2, Article 6 (April 2022), 27 pages.

https://doi.org/10.1145/3492545

## 1 INTRODUCTION

Refinement mappings are used to verify that one specification implements another. They generalize to systems the concept of abstraction function, introduced by Hoare to define what it means for one input/output relation to implement another [13]. Refinement mappings are a central concept in extending Floyd-Hoare state-based reasoning to concurrent systems. They are crucial to making verification of those systems tractable, whether verification is by rigorous proof or model checking.

"The Existence of Refinement Mappings" by Abadi and Lamport [2] has become a standard reference for verifying implementation with refinement mappings in state-based formalisms. That article, henceforth called ER, was mostly a synthesis of work that had been done in the preceding decade or so. It was well known that being able to construct a refinement mapping often requires adding to a specification a history variable that remembers information from previous states. The major new concept ER introduced was prophecy variables that predict future states, which may also be required to define a refinement mapping. ER showed that refinement mappings can always be found by adding history and prophecy variables for specifications satisfying certain conditions.

The prophecy variables defined by ER were elegant, looking like history variables with time running backward. In practice, they turned out to be difficult to use because reasoning backward from the future is hard. Defining the prophecy variable needed to verify implementation was challenging even in simple examples. We were never able to do it for realistic examples. Here, we describe a new kind of prophecy variable that we find easier to understand and to use because it involves

Authors' address: L. Lamport, Microsoft Research, 14820 NE 36th St, Redmond, WA 98052; S. Merz, University of Lorraine, CNRS, Inria Nancy Grand Est, 615 rue du Jardin Botanique, 54600 Villers-lès-Nancy, France; email: stephan.merz@inria.fr.

<figure><img src="image_2.png" /></figure>

This work is licensed under a Creative Commons Attribution International 4.0 License.

© 2022 Copyright held by the owner/author(s).

0164-0925/2022/04-ART6 $15.00

https://doi.org/10.1145/3492545
reasoning forward from the present. It makes simple examples simple and realistic examples not
too hard.

We were motivated to take a fresh look at prophecy variables by a paper of Abadi [1]. It describes techniques to make ER's prophecy variables easier to use, but we found those techniques hard to understand and prophecy variables still too hard to use. Soon after ER was written, TLA was developed. It allowed us to express the concepts developed in ER mathematically, so a specification is a formula and implementation is implication. It also gave us a new way to think about prophecy.

TLA is a linear-time temporal logic. A formula in such a logic is a predicate on sequences of states. In other temporal logics, formulas are built from predicates on states. TLA formulas are built from actions, which are predicates on pairs of states. This makes it easy to write as TLA formulas the state-machine specifications on which ER is based. Earlier temporal logics could also express actions, but not as conveniently as TLA. They therefore did not lead one to think in terms of actions.

Thinking in terms of actions led us quickly to the simple idea of letting the value of a prophecy variable predict which one of a set of actions will be the next one satisfied by a pair of successive states. For example, if each of the actions describes the sending of a different message, the value of the prophecy variable predicts which message is the next one to be sent. It was easy to generalize this idea to a prophecy variable that makes multiple predictions—even infinitely many.

In addition to explaining our new prophecy variables, we recast the concepts from ER in terms of temporal logic formulas. TLA is an obvious logic to use since it was devised for representing state machines, but the concepts should be applicable to any state-based formalism. We assume no prior knowledge of TLA or of ER. For readers who are familiar with ER, we point out the correspondence between our definitions and those of ER.

Sections 2, 3, and 4.1 explain how specifications are written, what it means for one specification to implement another, refinement mappings, and history variables. They correspond to Sections 2, 3, and 5.1 of ER. The rest of Section 4 explains prophecy variables and stuttering variables, which provide part of the functionality of ER's prophecy variables. Section 5 sketches how a prophecy variable can be used to verify that a concurrent algorithm implements the specification of a linearizable object [10]. Our method should be useful for verifying linearizable specifications of other systems.

Section 6 shows that existential quantification over constants, an operation present in TLA and some other temporal logics, can be used to predict the future. When used in this way, we call it a prophecy constant. Section 7 presents completeness results stating that the refinement mapping required to verify an implementation can always, in theory, be obtained by adding history and stuttering variables and either prophecy constants or our prophecy variables—without assuming the conditions required by ER’s prophecy variables. In practice, prophecy constants and prophecy variables complement each other. A concluding section compares our prophecy variables to others inspired by ER.

Our exposition is as informal as we can make it while trying to be rigorous. TLA⁺ is a complete specification language based on TLA [17]. Most of what we describe here has been explained in excruciating detail for TLA⁺ users [18]. It is easy to write our examples in TLA⁺, and their correctness has been checked with the TLA⁺ tools. Since the examples are written somewhat informally here, we cannot be sure that they have no errors.

## 2 PRELIMINARIES

### 2.1 States, Behaviors, and Specifications

Following Turing and ER, we model the execution of a discrete system as a sequence of states, which we call a *behavior*. For mathematical simplicity, we define a state to be an assignment of
values to all possible variables. Think of a behavior as representing a history of the entire universe. We specify a system as a predicate on behaviors, which is satisfied by those behaviors that represent a history in which the system executes the way it should. Traditional verification methods consider only behaviors that represent possible executions of a system. We consider all behaviors, where a behavior is any sequence of states, and a state is any assignment of any values to variables.

Only a finite number of variables are relevant to a system; the system's specification allows behaviors in which other variables can have any values. For example, if we represent its display with the variable *hr*, a 12-hour clock that displays the hour is satisfied by behaviors of the form

$$[hr : 12], [hr : 1], [hr : 2], \dots, \tag{1}$$

where $[hr : i]$ can be any state that assigns the value $i$ to $hr$. We call each pair of successive states in a behavior a step of the behavior. A state of ER corresponds to an assignment of values to only the variables of the specification.

Common sense dictates that a specification of an hour clock should not say that the clock has no alarm, or no radio, or no display showing minutes. However, between any two steps that change the value of $hr$, a behavior representing a universe in which our hour clock also displays minutes must contain 59 steps in which the minute display changes and the value of $hr$ remains the same. Therefore, in addition to allowing behaviors of the form (1), a specification of an hour clock must allow steps in which the value of $hr$ does not change.

We define a *stuttering* step of a specification to be one in which both states assign the same values to the specification's variables. Two behaviors are said to be *stuttering equivalent* for a specification iff (if and only if) they both have the same sequence of non-stuttering steps. We often don't mention the specification when it is clear from context. We write only specifications that are *stuttering insensitive*, meaning that if two behaviors are stuttering equivalent, then one satisfies the specification iff the other does. All behaviors are infinite. An execution in which a system stops is represented by a behavior ending in an infinite sequence of stuttering steps of its specification. (The rest of the universe needn't also stop.)

An event $e$ in an event-based formalism corresponds to a step that satisfies some predicate $E$ on pairs of states. If the events are generated by transitions in an underlying state machine, then transitions that produce no event correspond to stuttering steps. In a purely event-based formalism, special “nothing happened” events correspond to stuttering steps.

Writing stuttering-insensitive specifications allows a simple definition of implementation (also called refinement). We say that a specification $S_1$ implements a specification $S_2$ iff every behavior satisfying $S_1$ also satisfies $S_2$. When predicates on behaviors are formulas in a temporal logic, $S_1$ implements $S_2$ means that the formula $S_1 \Rightarrow S_2$ is valid (satisfied by all behaviors).

## 2.2 State Machines

Following Turing, ER, and common programming languages, we write our specifications in terms of state machines. A state machine is specified with two formulas: a predicate *Init* on states that describes the possible initial states and a predicate *Next* on pairs of states that describes how the state can change. We call a predicate *A* on pairs of states an *action*, and we call a step satisfying *A* an *A step*. For a function *f* on states, we define UC *f* to be the action satisfied by a step iff it leaves the value of *f* unchanged. We enclose tuples in angle brackets $\langle \rangle$.

Let $x$ be the list $x_1, \dots, x_n$ of all variables of the specification. Then UC $\langle x \rangle$ is the action satisfied only by steps that leave all the variables $x$ unchanged—that is, stuttering steps. The state machine specified by *Init* and *Next* is satisfied by a behavior $s_1, s_2, \dots$ iff

*SM1.* $s_1$ satisfies *Init*, and

*SM2.* For all $i$, the step $s_i$, $s_{i+1}$ satisfies *Next* $\lor$ UC $\langle x \rangle$.
The disjunct UC $\langle x \rangle$ in SM2 ensures that the specification is stuttering insensitive. The predicate on behaviors described by SM1 and SM2 is written in TLA as this formula:

$$ \mathit{Init} \land \Box[\mathit{Next}]_{\langle x \rangle}, \qquad (2) $$

where $\Box$ is the temporal logic forever operator and $[Next]_f$ is an abbreviation for $Next \lor (UC f)$.

In TLA, an action is written as an ordinary mathematical formula that may contain primed and unprimed variables. Unprimed variables refer to the values of the variables in the first state of a pair of states, and primed variables refer to their values in the second state. (An action with no primed variables is a predicate on states.) Thus, UC $\langle x \rangle$ equals $\langle x' \rangle = \langle x \rangle$, which is equivalent to $(x'_1 = x_1) \land \dots \land (x'_n = x_n)$. (Priming an expression means priming all its variables.) Our hour-clock specification can be written in TLA as

$$ (hr = 12) \land \Box[hr' = \mathbf{if} \ hr = 12 \ \mathbf{then} \ 1 \ \mathbf{else} \ hr + 1]_{\langle hr \rangle}. $$

(The angle brackets in the subscript $\langle hr \rangle$ can be omitted.) A specification of the form (2) allows behaviors in which, at some point, the values of the variables $x$ never again change—that is, in our example, behaviors in which the clock halts. Allowing halting is a feature, not a problem. Formula (2) expresses a safety property. If we want the system also to satisfy a liveness property<fnref n="1" /> $L$, we specify it as

$$ \mathit{Init} \land \Box[\mathit{Next}]_{\langle x \rangle} \land L. \qquad (3) $$

Letting $L$ be the TLA weak fairness formula $WF_{\langle x \rangle}(Next)$ makes Formula (3) assert that the state machine never halts in a state in which a non-stuttering step is possible. For the hour clock, this implies that the clock never stops. The precise meaning of WF is irrelevant.

Safety and liveness properties are verified differently, so it is best to keep them separate in a specification. The liveness property $L$ plays no part in defining our prophecy variables, so we don't care how $L$ is written. We don't even require it to be a liveness property. Following ER, we call $L$ a supplementary property.

## 2.3 Internal Variables

Specifying a system with a state machine often requires the use of variables that do not represent the actual state of the system but serve to describe how that state changes. We call the variables describing the system's state external variables, and we call the additional variables internal variables. In our specifications, we want to hide the internal variables, leaving only the external variables visible.

In a linear-time temporal logic, we hide a variable $y$ in a formula $\mathcal{F}$ with the temporal existential quantifier $\exists$. The approximate definition is that $\exists y : \mathcal{F}$ is true of a behavior $\sigma$ iff there exist assignments of values to $y$ in the states of $\sigma$ (a separate assignment for each state of $\sigma$) that make the resulting behavior satisfy $\mathcal{F}$. This definition is wrong because it doesn't ensure that $\exists y : \mathcal{F}$ is stuttering insensitive. The correct definition is that $\sigma$ satisfies $\exists y : \mathcal{F}$ iff there is a behavior $\tau$ stuttering equivalent for $\mathcal{F}$ to $\sigma$ and assignments of values to $y$ that make $\tau$ satisfy $\mathcal{F}$. For a list $y$ of variables $y_1, \dots, y_m$, we define $\exists y : \mathcal{F}$ to equal $\exists y_1 : \dots \exists y_m : \mathcal{F}$.

We generalize the form (3) of a specification $S$ to $\exists y : IS$, where

$$ IS \stackrel{\Delta}{\equiv} \mathit{Init} \land \Box[\mathit{Next}]_{\langle x,y \rangle} \land L, \qquad (4) $$

<footnote n="1">¹The definitions of safety and liveness can be found elsewhere [4]; they are not needed here.</footnote>
$$
\begin{align*}
\mathcal{A} &\triangleq \exists \mathit{num}, \mathit{sum} : \mathcal{IA} \\
\mathcal{IA} &\triangleq \mathit{Init}_{\mathcal{A}} \wedge \Box [\mathit{Next}_{\mathcal{A}}]_{\langle \mathit{in}, \mathit{out}, \mathit{num}, \mathit{sum} \rangle} \\
\mathit{Init}_{\mathcal{A}} &\triangleq (\mathit{in} = \mathit{rdy}) \wedge (\mathit{out} = \mathit{num} = \mathit{sum} = 0) \\
\mathit{Next}_{\mathcal{A}} &\triangleq \mathit{Input}_{\mathcal{A}} \vee \mathit{Output}_{\mathcal{A}} \\
\mathit{Input}_{\mathcal{A}} &\triangleq (\mathit{in} = \mathit{rdy}) \wedge (\mathit{in}' \in \mathit{Int}) \wedge \mathit{UC} \langle \mathit{out}, \mathit{num}, \mathit{sum} \rangle \\
\mathit{Output}_{\mathcal{A}} &\triangleq \\
& \quad (\mathit{in} \neq \mathit{rdy}) \wedge (\mathit{in}' = \mathit{rdy}) \\
& \quad \wedge (\mathit{sum}' = \mathit{sum} + \mathit{in}) \wedge (\mathit{num}' = \mathit{num} + 1) \\
& \quad \wedge (\mathit{out}' = \mathit{sum}' / \mathit{num}')
\end{align*}
$$

<caption>Fig. 1. The definition of specification $\mathcal{A}$.</caption>

and x and y are lists of variables that may appear in Init, Next, and L. The external variables x are assumed to be different from the internal variables y. We call IS the internal specification of S.

## 3 IMPLEMENTATION AND REFINEMENT MAPPINGS

We explain refinement mappings with an example consisting of a specification $\mathcal{A}$, a specification $\mathcal{B}$ that implements $\mathcal{A}$, and a refinement mapping that can be used to verify $\mathcal{B} \Rightarrow \mathcal{A}$.

### 3.1 Specification $\mathcal{A}$

Specification $\mathcal{A}$ describes a system that receives as input a sequence of integers and, after receipt of each integer, outputs the average of all the integers received thus far. Receipt of an integer $i$ is represented by the value of the variable *in* changing from the special value *rdy* to $i$, where we assume *rdy* is not a number. Producing an output is represented by the value of *in* changing back to *rdy* and the value of *out* being set to the output. Initially, *in* = *rdy* and *out* = 0. Here is the beginning of a behavior that satisfies $\mathcal{A}$:

$$
\begin{align}
& [in : \text{rdy}, out : 0], [in : 3, out : 0], [in : \text{rdy}, out : 3], \tag{5} \\
& [in : -2, out : 3], [in : \text{rdy}, out : \frac{1}{2}], \dots \nonumber
\end{align}
$$

$\mathcal{A}$ is defined to equal $\exists \mathit{sum}, \mathit{num} : \mathcal{IA}$, where *num* is the number of outputs that have been produced and *sum* is the sum of the inputs that produced the most recent output. Here is a behavior satisfying $\mathcal{IA}$, which shows that behavior (5) satisfies $\mathcal{A}$:

$$
\begin{align*}
& [in : \text{rdy}, out : 0, num : 0, sum : 0], \tag{6} \\
& [in : 3, out : 0, num : 0, sum : 0], \\
& [in : \text{rdy}, out : 3, num : 1, sum : 3], \\
& [in : -2, out : 3, num : 1, sum : 3], \\
& [in : \text{rdy}, out : \frac{1}{2}, num : 2, sum : 1], \dots
\end{align*}
$$

The complete specification $\mathcal{A}$ is defined in Figure 1, where *Int* is the set of all integers. A step satisfies the action $\mathit{Next}_{\mathcal{A}}$ iff it is an $\mathit{Input}_{\mathcal{A}}$ step or an $\mathit{Output}_{\mathcal{A}}$ step. An $\mathit{Input}_{\mathcal{A}}$ step represents the receipt of an input and an $\mathit{Output}_{\mathcal{A}}$ step represents the production of an output.

### 3.2 Specification $\mathcal{B}$

Specification $\mathcal{B}$ is a different way of writing the same specification as $\mathcal{A}$. Instead of variables that record the number of inputs and their sum, the internal specification $\mathcal{IB}$ has a single internal
$$
\begin{align*}
\mathcal{B} &\triangleq \exists \text{seq} : \mathcal{IB} \\
\mathcal{IB} &\triangleq \text{Init}_\mathcal{B} \wedge \Box [\text{Next}_\mathcal{B}]_{(\text{in},\text{out},\text{seq})} \\
\text{Init}_\mathcal{B} &\triangleq (\text{in} = \text{rdy}) \wedge (\text{out} = 0) \wedge (\text{seq} = \langle \rangle) \\
\text{Next}_\mathcal{B} &\triangleq \text{Input}_\mathcal{B} \lor \text{Output}_\mathcal{B} \\
\text{Input}_\mathcal{B} &\triangleq \begin{array}{@{}l@{}} (\text{in} = \text{rdy}) \wedge (\text{in}' \in \text{Int}) \\ \qquad \wedge (\text{seq}' = \text{Append}(\text{seq}, \text{in}')) \wedge (\text{out}' = \text{out}) \end{array} \\
\text{Output}_\mathcal{B} &\triangleq \begin{array}{@{}l@{}} (\text{in} \neq \text{rdy}) \wedge (\text{in}' = \text{rdy}) \\ \qquad \wedge (\text{out}' = \text{Sum}(\text{seq})/\text{Len}(\text{seq})) \wedge (\text{seq}' = \text{seq}) \end{array}
\end{align*}
$$

<caption>Fig. 2. The definition of specification $\mathcal{B}$.</caption>

variable seq that records the entire sequence of inputs received so far. Specification $\mathcal{B}$ has the same form as $\mathcal{A}$, except its action $\text{Input}_\mathcal{B}$ appends the value being input to seq, and its $\text{Output}_\mathcal{B}$ action outputs the average of the numbers in the sequence seq.

To write $\mathcal{B}$, we introduce some notation for sequences. As mentioned above, we enclose sequences in angle brackets, so $\langle \rangle$ is the empty sequence. We define $\text{Len}(\text{sq})$ to equal the length of sequence $\text{sq}$ and $\text{Append}(\text{sq}, e)$ to be the sequence obtained by appending $e$ to the end of sequence $\text{sq}$, so $\text{Len}(\langle 3, 1 \rangle)$ equals 2 and $\text{Append}(\langle 3, 1 \rangle, 42)$ equals $\langle 3, 1, 42 \rangle$. We also define $\text{Sum}(\text{sq})$ to be the sum of the elements of $\text{sq}$, so $\text{Sum}(\langle 3, 1, 42 \rangle)$ equals 46 (which equals $3+1+42$) and $\text{Sum}(\langle \rangle)$ equals 0. Specification $\mathcal{B}$ is defined in Figure 2.

## 3.3 Implementation and a Refinement Mapping

To show $\mathcal{B} \Rightarrow \mathcal{A}$, we must show $(\exists \text{seq} : \mathcal{IB}) \Rightarrow \mathcal{A}$. The quantifier $\exists$ obeys the same rules as the quantifier $\exists$ of ordinary math. By those rules, since seq is not a variable of $\mathcal{A}$, to show $(\exists \text{seq} : \mathcal{IB}) \Rightarrow \mathcal{A}$ it suffices to show $\mathcal{IB} \Rightarrow \mathcal{A}$.

For any state $s$, let $s[[\text{num} \leftarrow u, \text{sum} \leftarrow v]]$ be the state that is the same as $s$ except that it assigns the value $u$ to variable `num` and the value $v$ to variable `sum`. Since $\mathcal{A}$ equals $\exists \text{num}, \text{sum} : \mathcal{IA}$, to show $\mathcal{IB} \Rightarrow \mathcal{A}$, it suffices to assume that a behavior $s_1, s_2, \dots$ satisfies $\mathcal{IB}$ and find sequences of values $\overline{\text{num}}_1, \overline{\text{num}}_2, \dots$ and $\overline{\text{sum}}_1, \overline{\text{sum}}_2, \dots$ such that the behavior

$$s_1[[\text{num} \leftarrow \overline{\text{num}}_1, \text{sum} \leftarrow \overline{\text{sum}}_1]], s_2[[\text{num} \leftarrow \overline{\text{num}}_2, \text{sum} \leftarrow \overline{\text{sum}}_2]], \dots$$

satisfies $\mathcal{IA}$. We are free to let each $\overline{\text{num}}_i$ and $\overline{\text{sum}}_i$ depend on the entire behavior $s_1, s_2, \dots$. However, we are going to make them depend only on the state $s_i$. We do that by finding expressions $\overline{\text{num}}$ and $\overline{\text{sum}}$, containing only the variables `in`, `out`, and `seq` of $\mathcal{IB}$, and let $\overline{\text{num}}_i$ and $\overline{\text{sum}}_i$ be the values of these expressions in state $s_i$.

More precisely, if $u$ and $v$ are expressions (formulas that need not be Boolean valued), then let $s[[\text{num} \leftarrow u, \text{sum} \leftarrow v]]$ be the state that is the same as $s$ except that it assigns to the variables `num` and `sum` the values of $u$ and $v$ in state $s$, respectively. To show $\mathcal{IB} \Rightarrow \exists \text{num}, \text{sum} : \mathcal{IA}$, it suffices to find expressions $\overline{\text{num}}$ and $\overline{\text{sum}}$, containing only the (unprimed) variables of $\mathcal{IB}$, such that:

RM. If a behavior $s_1, s_2, \dots$ satisfies $\mathcal{IB}$, then the behavior

$$s_1[[\text{num} \leftarrow \overline{\text{num}}, \text{sum} \leftarrow \overline{\text{sum}}]], s_2[[\text{num} \leftarrow \overline{\text{num}}, \text{sum} \leftarrow \overline{\text{sum}}]], \dots$$

satisfies $\mathcal{IA}$.
From conditions SM1 and SM2 of Section 2.2 and the definitions of $\mathcal{IA}$ and $\mathcal{IB}$, we see that RM is implied by:

RM1. For any state $s$, if $s$ satisfies $Init_B$, then $s[[num \leftarrow \overline{num}, sum \leftarrow \overline{sum}]]$ satisfies $Init_A$.

RM2. For any states $s$ and $t$, if step $s$, $t$ satisfies $Next_B \lor UC \langle in, out, seq \rangle$, then the pair of states

$$s[[num \leftarrow \overline{num}, sum \leftarrow \overline{sum}]], t[[num \leftarrow \overline{num}, sum \leftarrow \overline{sum}]]$$

satisfies $Next_A \lor UC \langle in, out, num, sum \rangle$.

Because $\overline{num}$ and $\overline{sum}$ contain only the variables $in$, $out$, and $seq$ of $\mathcal{IB}$, if the step $s$, $t$ satisfies $UC \langle in, out, seq \rangle$, then the step

$$s[[num \leftarrow \overline{num}, sum \leftarrow \overline{sum}]], t[[num \leftarrow \overline{num}, sum \leftarrow \overline{sum}]]$$

satisfies $UC \langle in, out, num, sum \rangle$. Therefore, RM2 is automatically satisfied if the step $s$, $t$ satisfies $UC \langle in, out, seq \rangle$. This means we can simplify RM2 to:

RM2. For any states $s$ and $t$, if the step $s$, $t$ satisfies $Next_B$, then the pair of states

$$s[[num \leftarrow \overline{num}, sum \leftarrow \overline{sum}]], t[[num \leftarrow \overline{num}, sum \leftarrow \overline{sum}]]$$

satisfies $Next_A \lor UC \langle in, out, num, sum \rangle$.

Let's consider RM1. Since $Init_A$ is the formula

$$(in = rdy) \land (out = num = sum = 0),$$

the state $s[[num \leftarrow \overline{num}, sum \leftarrow \overline{sum}]]$ satisfies $Init_A$ iff state $s$ satisfies

$$(in = rdy) \land (out = \overline{num} = \overline{sum} = 0). \qquad (7)$$

This is the formula obtained by substituting the expression $\overline{num}$ for the variable $num$ and the expression $\overline{sum}$ for the variable $sum$ in the formula $Init_A$. Let's call that formula

$$Init_A \text{ with } num \leftarrow \overline{num}, sum \leftarrow \overline{sum}.$$

RM1 asserts that every state satisfying $Init_B$ satisfies (7). Therefore, it is equivalent to

$$\text{RM1. } Init_B \Rightarrow (Init_A \text{ with } num \leftarrow \overline{num}, sum \leftarrow \overline{sum}).$$

As a sanity check on this condition, observe that because the variables in expressions $\overline{num}$ and $\overline{sum}$ are variables of $Init_B$, and the other variables $in$ and $out$ of $Init_A$ are also variables of $Init_B$, the formula $(Init_A \text{ with } \dots)$ in RM1 contains only variables in $Init_B$. Therefore, RM1 asserts that $Init_B$ implies a formula containing only variables of $Init_B$.

Applying the same reasoning to RM2, we see that RM2 is equivalent to

$$\text{RM2. } Next_B \Rightarrow (Next_A \text{ with } num \leftarrow \overline{num}, sum \leftarrow \overline{sum}) \lor UC \langle in, out, \overline{num}, \overline{sum} \rangle.$$

Substituting an expression like $\overline{num}$ for $num$ in $Next_A$ means replacing $num'$ by $\overline{num'}$. The expression $\overline{num'}$ represents the value of $\overline{num}$ in the second state of a step. It is the expression obtained by priming all the variables in $\overline{num}$.

The substitutions $num \leftarrow \overline{num}$, $sum \leftarrow \overline{sum}$ of expressions containing variables of $\mathcal{IB}$ for the internal variables of $\mathcal{IA}$ are what we call a refinement mapping. In ER, a state of $\mathcal{IA}$ or $\mathcal{IB}$ would be an assignment of values to that specification's variables. The mapping from states of $\mathcal{IB}$ to states of $\mathcal{IA}$ that maps $s$ to $s[[num \leftarrow \overline{num}, sum \leftarrow \overline{sum}]]$ is what ER calls a refinement mapping. Thinking of refinement mappings in terms of formulas instead of states is better when writing proofs, since proofs are written with formulas.
## 3.4 Finding the Refinement Mapping

Let's now find the expressions $num$ and $sum$ for the actual formulas defined in Figures 1 and 2 that satisfy RM1 and RM2. RM2 asserts that a step satisfying $Next_B$ simulates a step satisfying $Next_A$ or a stuttering step, where the values of $num$ and $sum$ are simulated by the values of $num$ and $sum$. In this simulation, the variables $in$ and $out$ are simulated by themselves. This implies that an $Input_B$ step must simulate an $Input_A$ step, leaving $num$ and $sum$ unchanged, and an $Output_B$ step must simulate an $Output_A$ step. So, we should verify RM2 by verifying these two formulas:

$$ \mathit{Input}_B \Rightarrow (\mathit{Input}_A \ \mathbf{with} \ \mathit{num} \leftarrow \overline{\mathit{num}}, \ \mathit{sum} \leftarrow \overline{\mathit{sum}}), \quad (8) $$

$$ \mathit{Output}_B \Rightarrow (\mathit{Output}_A \ \mathbf{with} \ \mathit{num} \leftarrow \overline{\mathit{num}}, \ \mathit{sum} \leftarrow \overline{\mathit{sum}}). \quad (9) $$

It's pretty clear that, after an output step, $num$ should equal $Len(seq)$ and $sum$ should equal $Sum(seq)$. Since $in$ equals $rdy$ after an $Output_A$ step, this leads to the following definitions:

$$ \overline{\mathit{num}} \triangleq \mathbf{if} \ in = \mathit{rdy} \ \mathbf{then} \ \mathit{Len}(seq) \ \mathbf{else} \ \mathit{Len}(\mathit{Front}(seq)), \\ \overline{\mathit{sum}} \triangleq \mathbf{if} \ in = \mathit{rdy} \ \mathbf{then} \ \mathit{Sum}(seq) \ \mathbf{else} \ \mathit{Sum}(\mathit{Front}(seq)), $$

where $Front(sq)$ is defined to equal the sequence consisting of the first $Len(sq) - 1$ elements of sequence sq, and $Front(\langle \rangle)$ is defined to equal $\langle \rangle$.

It's easy to verify RM1, which asserts

$$ (in = \mathit{rdy}) \land (out = 0) \land (seq = \langle \rangle) \Rightarrow (in = \mathit{rdy}) \land (out = \overline{\mathit{num}} = \overline{\mathit{sum}} = 0). $$

It's not hard to verify Formula (8), since $Input_B$ implies $Front(seq') = seq$. Equation (9) may also appear valid, but it's not. For example, there's no way to show that Formula (9) is true if $in' = 42$ and $seq = \langle \mathit{rdy} \rangle$, since we don't know what $Sum(\langle \mathit{rdy} \rangle)$ and $Sum(\langle \mathit{rdy}, 42 \rangle)$ equal.

It may seem obvious that $seq$ can't equal $\langle \mathit{rdy} \rangle$, but why can't it? Nothing in Formula (9) or Figure 2 asserts that $seq$ doesn't equal $\langle \mathit{rdy} \rangle$. What is true is that the value of $seq$ can't equal $\langle \mathit{rdy} \rangle$ in any state of any behavior satisfying $IB$. To show implementation, we don't have to show that RM2 is true for all pairs of states. It need only be true for reachable states, which are states that can occur in a behavior satisfying $IB$. In fact, every reachable state of $IB$ satisfies the following formula $Inv$:

$$ \mathit{Inv} \triangleq (in \in \mathit{Int} \cup \{\mathit{rdy}\}) \land (out \in \mathit{Int}) \land (seq \in \mathit{Int}^*) \land ((in \neq \mathit{rdy}) \Rightarrow (seq \neq \langle \rangle) \land (in = \mathit{Last}(seq))), $$

where $Int^*$ is the set of finite sequences of integers and $Last(sq)$ denotes the last element of a non-empty sequence sq. A formula that is true in every reachable state of a specification is called an invariant of the specification. In temporal logic, the formula $\Box \mathit{Inv}$ is satisfied by a behavior iff every state of the behavior satisfies $Inv$. Therefore, the assertion that $Inv$ is an invariant of $IB$ is expressed by $IB \Rightarrow \Box \mathit{Inv}$.

Since $Inv$ contains only variables of $IB$, its value is left unchanged by steps that leave those variables unchanged. To show that $Inv$ is an invariant of $IB$, by induction it suffices to show:

1. $\mathit{Init}_B \Rightarrow \mathit{Inv}$,

2. $\mathit{Inv} \land \mathit{Next}_B \Rightarrow \mathit{Inv}'$.
(Remember that $Inv'$ is the formula obtained by priming all the variables in $Inv$.) Because $Inv$ is an invariant of $IB$, instead of showing RM2, we need only show:

$$ \begin{array}{l} \mathit{Inv} \wedge \mathit{Inv}' \wedge \mathit{Next}_g \Rightarrow \qquad (10) \\ \qquad (\mathit{Next}_A \ \mathbf{with} \ \mathit{num} \leftarrow \overline{\mathit{num}}, \ \mathit{sum} \leftarrow \overline{\mathit{sum}}) \lor \ \mathit{UC}(\mathit{in}, \mathit{out}, \overline{\mathit{num}}, \overline{\mathit{sum}}). \end{array} $$

We leave this to the reader.

Proving invariance by proving I1 and I2 underlies all state-based methods for proving correctness, including the Floyd-Hoare [9, 12] and Owicki-Gries [21] methods. ER avoids the explicit use of invariants by restricting a specification's set of states to ones that satisfy the needed invariant.

## 3.5 Generalization

We now generalize what we have done in this section to arbitrary specifications $S_1$ and $S_2$, with external variables $x$, defined by

$$ \begin{align} \mathit{IS}_1 &\triangleq \mathit{Init}_1 \wedge \Box[\mathit{Next}_1]_{(x,y)} \wedge L_1, \tag{11} \\ \mathit{IS}_2 &\triangleq \mathit{Init}_2 \wedge \Box[\mathit{Next}_2]_{(x,z)} \wedge L_2, \\ \mathit{S}_1 &\triangleq \exists \mathit{y} : \mathit{IS}_1 \quad \mathit{S}_2 \triangleq \exists \mathit{z} : \mathit{IS}_2, \end{align} $$

where the lists $y$ and $z$ of internal variables of $S_1$ and $S_2$ contain no variables of $x$. To verify $S_1 \Rightarrow S_2$, we first define a state predicate $Inv$, with variables in $x$ and $y$, and show it is an invariant of $IS_1$ by showing:

I1. $\mathit{Init}_1 \Rightarrow \mathit{Inv}$,

I2. $\mathit{Inv} \wedge \mathit{Next}_1 \Rightarrow \mathit{Inv}'$.

Then, if $z$ is the list $z_1, \dots, z_m$ of variables, we find expressions $\overline{z_1}, \dots, \overline{z_m}$ with variables $x$ and $y$ and show the following, where $z \leftarrow \overline{z}$ means $z_1 \leftarrow \overline{z_1}, \dots, z_m \leftarrow \overline{z_m}$:

RM1. $\mathit{Init}_1 \Rightarrow (\mathit{Init}_2 \ \mathbf{with} \ z \leftarrow \overline{z})$,

RM2. $\mathit{Inv} \wedge \mathit{Inv}' \wedge \mathit{Next}_1 \Rightarrow ((\mathit{Next}_2 \ \mathbf{with} \ z \leftarrow \overline{z}) \lor \mathit{UC}(\mathbf{x}, \overline{z}))$,

RM3. $\mathit{Init}_1 \wedge \Box[\mathit{Next}_1]_{(x,y)} \wedge L_1 \Rightarrow (L_2 \ \mathbf{with} \ z \leftarrow \overline{z})$.

When RM1-RM3 hold, we say that $IS_1$ implements $IS_2$ under the refinement mapping $z \leftarrow \overline{z}$.

## 4 AUXILIARY VARIABLES

Sometimes, one specification implements another, but there does not exist a refinement mapping that shows it. For example, while we showed above that $\mathcal{B}$ implies $\mathcal{A}$, the two specifications are actually equivalent. However, $\mathcal{IA}$ does not implement $\mathcal{IB}$ under any refinement mapping because there is no way to define $\overline{\mathit{seq}}$ in terms of the variables of $\mathcal{A}$.

To show $\mathcal{A} \Rightarrow \mathcal{B}$, we construct a specification $\mathcal{A}^a$ from $\mathcal{A}$ containing an additional variable $a$ such that $\mathcal{A}$ is equivalent to $\exists a : \mathcal{A}^a$, and we show $\mathcal{A}^a \Rightarrow \mathcal{B}$. This shows $\mathcal{A} \Rightarrow \mathcal{B}$, assuming that $a$ is not an (external) variable of $\mathcal{B}$. Constructing $\mathcal{A}^a$ such that $\exists a : \mathcal{A}^a$ is equivalent to $\mathcal{A}$ is called adding the auxiliary variable $a$ to $\mathcal{A}$. We define three kinds of auxiliary variables: history, prophecy, and stuttering variables.

Let specification $S$ have internal specification $IS$ defined by Formula (4). We define $S^a$ to equal $\exists \mathit{y} : IS^a$ and define

$$ \mathit{IS}^a \triangleq \mathit{Init}^a \wedge \Box[\mathit{Next}^a]_{(x,y,a)} \wedge L, \qquad (12) $$

where $\mathit{Init}^a$ and $\mathit{Next}^a$ are obtained from $\mathit{Init}$ and $\mathit{Next}$ by adding specifications of the initial value of $a$ and how $a$ changes. To show that $S^a$ is obtained by adding $a$ as an auxiliary variable—that is, $\exists a : S^a$ is equivalent to $S$—we show that $\exists a : \mathit{IS}^a$ is equivalent to $\mathit{IS}$. Since $\mathit{IS}^a$ and
IS have the same supplementary property L, it suffices to show their equivalence with L removed. That is, we only have to show that if we hide the variable a, the state machines of ISª and IS are equivalent. This requires verifying two conditions:

AV1. Any behavior satisfying SM1 and SM2 for ISª satisfies them for IS.

AV2. From any behavior σ satisfying SM1 and SM2 for IS, we can obtain a behavior σª satisfying SM1 and SM2 for ISª by adding stuttering steps and assigning new values to the variable a in the states of the resulting behavior.

For all our auxiliary variables, Initª is defined by

$$Init^a \stackrel{\Delta}{\equiv} Init \wedge J, \qquad (13)$$

where J is an expression containing the variables x, y, and a. To define Nextª, we write Next as a disjunction of elementary actions, where we consider existential quantification to be a disjunction. For example, if U, V, and W(i) are actions, we can consider the elementary actions of

$$U \lor V \lor \exists i \in Int : W(i) \qquad (14)$$

to be U, V, and all W(i) with i ∈ Int. (We could also consider U ∨ V and ∃i ∈ Int : W(i) to be the elementary actions of Formula (14).) We define Nextª by replacing every elementary action A of Next with an action Aª. For history and prophecy variables, Aª is defined by letting

$$A^a \stackrel{\Delta}{\equiv} A \wedge B, \qquad (15)$$

where B is an action containing the variables x, y, and a (which may appear primed or unprimed), and letting a be left unchanged by stuttering steps of IS. Condition AV1 is implied by Formulas (13) and (15). Condition AV2 is implied by:

AX. For any behavior s₁, s₂, ... satisfying SM1 and SM2 for IS, there exists a behavior sª₁, sª₂, ... such that each sªᵢ is the same as sᵢ except for the value it assigns to a, and (1) sª₁ satisfies Initª and (2) for each elementary action A and each step sᵢ, sᵢ₊₁ that satisfies A, the step sªᵢ, sªᵢ₊₁ satisfies Aª.

We can show that history and prophecy variables satisfy AX. Stuttering variables can be shown to satisfy AV1 and AV2 directly.

Inspired by Abadi [1], we explain prophecy variables in terms of examples in which a specification with an undo action reverses the effect of some other action implements the same specification without the undo action. However, there is nothing about undo that makes our prophecy variables work especially well. We find them just as easy to use on other kinds of examples.

## 4.1 History Variables

We use a history variable h to show A ⇒ B. A history variable stores information from the current and previous states. To be able to find a refinement mapping that shows IAh ⇒ ∃seq : IB, we let h record the sequence of values input thus far. The initial value of h should obviously be the empty sequence, so we define

$$Init_{\mathcal{A}}^h \stackrel{\Delta}{\equiv} Init_{\mathcal{A}} \wedge (h = \langle \rangle).$$

The elementary actions of NextA are InputA and OutputA. We let InputA append the new input value to h and OutputA leave h unchanged:

$$Input_{\mathcal{A}}^h \stackrel{\Delta}{\equiv} Input_{\mathcal{A}} \wedge (h' = Append(h, in')), $$

$$Output_{\mathcal{A}}^h \stackrel{\Delta}{\equiv} Output_{\mathcal{A}} \wedge (h' = h).$$
Finally, we define

$$
\begin{align*}
\mathit{Next}_{\mathcal{A}}^h &\triangleq \mathit{Input}_{\mathcal{A}}^h \vee \mathit{Output}_{\mathcal{A}}^h, \\
\mathcal{IA}^h &\triangleq \mathit{Init}_{\mathcal{A}}^h \wedge \Box[\mathit{Next}_{\mathcal{A}}^h]_{(\mathit{in}, \mathit{out}, \mathit{sum}, \mathit{num}, \mathit{h})}, \\
\mathcal{A}^h &\triangleq \exists \mathit{sum}, \mathit{num} : \mathcal{IA}^h.
\end{align*}
$$

Condition AX is satisfied because, for any behavior $s_1, s_2, \dots$ satisfying SM1 and SM2 for $\mathcal{IA}$, we can inductively define the required states $s_i^h$ as follows: The value of $h$ in $s_1^h$ is determined by the condition $h = (\cdot)$ . For each $i$, a nonstuttering step $s_i$, $s_{i+1}$ is a step of one of the two elementary actions, and we let $s_{i+1}^h$ assign to $h$ the value of $h'$ determined by the $h' = \dots$ condition of that action. For a stuttering step, $h' = h$.

To show $\mathcal{A}^h \Rightarrow \mathcal{B}$, we let $\underline{seq}$ equal $h$; that is, we use the refinement mapping $seq \leftarrow h$. We must find an invariant $\mathit{Inv}$ of $\mathcal{IA}^h$ and show:

$$
\begin{align}
\mathit{Init}_{\mathcal{A}}^{h} &\Rightarrow (\mathit{Init}_{\mathcal{B}} \ \mathbf{with} \ \mathit{seq} \leftarrow h), \tag{16} \\
\mathit{Inv} \wedge \mathit{Inv}' \wedge \mathit{Input}_{\mathcal{A}}^{h} &\Rightarrow (\mathit{Input}_{\mathcal{B}} \ \mathbf{with} \ \mathit{seq} \leftarrow h), \nonumber \\
\mathit{Inv} \wedge \mathit{Inv}' \wedge \mathit{Output}_{\mathcal{A}}^{h} &\Rightarrow (\mathit{Output}_{\mathcal{B}} \ \mathbf{with} \ \mathit{seq} \leftarrow h). \nonumber
\end{align}
$$

This is a standard exercise in assertional reasoning. Formula (16) implies RM1 and RM2, which
imply $\mathcal{A}^h \Rightarrow \mathcal{B}$.

The generalization to an arbitrary internal specification (Formula (4)) is simple. We define

$$
\mathit{Init}^h \triangleq \mathit{Init} \wedge (h = f),
$$

where $f$ is an expression that can contain the variables $x$ and $y$. For an elementary action $A$ of
$\mathit{Next}$, we define

$$
A^h \triangleq A \wedge (h' = F),
$$

where $F$ is an expression that can contain the variables $x$ and $y$, both unprimed and primed, and the unprimed variable $h$. The general verification of AX is essentially the same as for our example. (If a step satisfies more than one elementary action, the value of $h'$ determined by $A^h$ for any of those actions can be used.)

4.2 Simple Prophecy Variables

We now consider a specification *C* that models implementing *A* with speculative execution, where an input can either produce an output or else be “undone” by resetting *in* to rdy without changing any other variables. Such a specification cannot implement *A*, which requires that every input produces an output. However, it does model a specification *Ã* that is the same as *A* except with the variable *in* hidden.

We therefore let $\tilde{\mathcal{A}}$ equal $\exists in : \mathcal{A}$, which equals $\exists in, num, sum : \mathcal{IA}$. Thus, $\tilde{\mathcal{A}}$ is the same as $\mathcal{A}$ except we consider input actions to be internal to the system. We define $\mathcal{C}$ to be the same as $\tilde{\mathcal{A}}$, except that after an input is received, the input action can be undone, setting $in$ to rdy, without producing any output for that input. The definition of $\mathcal{C}$ is in Figure 3.

Since *out* is the only external variable, it's clear that *C* allows the same externally visible behaviors as *Ã*. An *Input*<sub>*A*</sub> step followed by an *Undo*<sub>*C*</sub> step produces no change to *out*, so viewed externally they're just stuttering steps. It's obvious that *Ã* implements *C* because *IA* implies *IC*. (A behavior allowed by *IA* is allowed by *IC* because *IC* does not require that any *Undo*<sub>*C*</sub> steps occur.) However, we can't show *C* ⇒ *Ã* with a refinement mapping, even by adding history variables.

We can verify that *C* implements *Ã* by adding a prophecy variable *p* to *C* and showing that *IC*<sup>*p*</sup> implements *IA* under a refinement mapping. The variable *p* predicts whether or not an
$$
\begin{align*}
C &\triangleq \exists \mathit{in}, \mathit{num}, \mathit{sum} : \mathcal{IC} \\
\mathcal{IC} &\triangleq \mathit{Init}_{\mathcal{A}} \wedge \Box[\mathit{Next}_{C}]_{\langle \mathit{out}, \mathit{in}, \mathit{num}, \mathit{sum} \rangle} \\
\mathit{Next}_{C} &\triangleq \mathit{Next}_{\mathcal{A}} \lor \mathit{Undo}_{C} \\
\mathit{Undo}_{C} &\triangleq (\mathit{in} \neq \mathit{rdy}) \wedge (\mathit{in}' = \mathit{rdy}) \wedge \mathit{UC} \langle \mathit{out}, \mathit{num}, \mathit{sum} \rangle
\end{align*}
$$

<caption>Fig. 3. The definition of specification C.</caption>

$$
\begin{align*}
C^p &\triangleq \exists \mathit{in}, \mathit{num}, \mathit{sum} : \mathcal{IC}^p \\
\mathcal{IC}^p &\triangleq \mathit{Init}_C^p \wedge \Box[\mathit{Next}_C^p]_{\langle \mathit{out}, \mathit{in}, \mathit{num}, \mathit{sum}, p \rangle} \\
\mathit{Init}_C^p &\triangleq (p \in \{\mathit{do}, \mathit{undo}\}) \wedge \mathit{Init}_A \\
\mathit{Next}_C^p &\triangleq \mathit{Input}_A^p \lor \mathit{Output}_A^p \lor \mathit{Undo}_C^p \\
\mathit{Input}_C^p &\triangleq (p' = p) \wedge \mathit{Input}_A \\
\mathit{Output}_C^p &\triangleq (p = \mathit{do}) \wedge (p' \in \{\mathit{do}, \mathit{undo}\}) \wedge \mathit{Output}_A \\
\mathit{Undo}_C^p &\triangleq (p = \mathit{undo}) \wedge (p' \in \{\mathit{do}, \mathit{undo}\}) \wedge \mathit{Undo}_C
\end{align*}
$$

<caption>Fig. 4. The definition of specification $C^p$.</caption>

input value will be output. More precisely, its value predicts whether the next $Output_A \lor Undo_C$
step will be an $Output_A$ step or an $Undo_C$ step. The initial predicate makes the first prediction.
The next prediction is made after the currently predicted $Output_A$ or $Undo_C$ step occurs. The
specification $C^p$ is defined in Figure 4.

The value of the prophecy variable *p* is always either do or undo. Initially, *p* can have either of those values. If *p* equals do, then the next *Output*<sub>*A*</sub> or *Undo*<sub>*C*</sub> step must be an *Output*<sub>*A*</sub> step; it must be an *Undo*<sub>*C*</sub> step if *p* equals undo. In either case, after that step is taken, *p* is set to either do or undo. Condition AX is satisfied because for any behavior *s*<sub>1</sub>, *s*<sub>2</sub>, ... satisfying *IC*, there is a corresponding behavior *s*<sub>1</sub><sup>*p*</sup>, *s*<sub>2</sub><sup>*p*</sup>, ... satisfying *IC*<sup>*p*</sup> in which *p* always makes the correct prediction.

It's not hard to see that $\mathcal{IC}^p$ implements $\mathcal{IA}$ under this refinement mapping:

$$
in \leftarrow \mathbf{if} p = \mathbf{undo} \ \mathbf{then} \ rdy \ \mathbf{else} \ in, \ num \leftarrow num, \ sum \leftarrow sum.
$$

The generalization from this example is straightforward. Suppose the next-state action *Next* is the disjunction of elementary actions that include a set of actions *A*<sub>*i*</sub> for *i* in some set *P*. A simple prophecy variable *p* that predicts for which *i* the next *A*<sub>*i*</sub> step occurs is obtained by:

(1) Conjoining $p \in P$ to the initial predicate $\mathit{Init}$,

(2) Replacing each $A_i$ by $(p = i) \wedge (p' \in P) \wedge A_i$,

(3) Replacing each other elementary action *B* by (*p* = *p*) ∧ *B*.

Generalizations of simple prophecy variables and of the prophecy variables described in Sec-
tions 4.4 and 4.5 are discussed in Section 4.6.

The examples we use to illustrate prophecy variables are unrealistically simple because input
steps are internal. This makes it possible to define the necessary refinement mappings using the
stuttering variables introduced in Section 4.7 instead of prophecy variables. We have no reason to
believe stuttering variables can replace prophecy variables in any realistic example.
## 4.3 Predicting the Impossible

What if we obtain $S^p$ by adding a prophecy variable $p$ in this way to a specification $S$, and $p$ makes a prediction that cannot be fulfilled? This would appear to cause unsoundness, because it seems that $\exists p : S^p$ and $S$ couldn't be equivalent. But they would be equivalent, and understanding why helps understand our prophecy variables. Let's consider an especially egregious example. Define $S$ by

$$S \stackrel{\Delta}{\equiv} (x = 0) \wedge \Box[x' = x + 1]_{\langle x \rangle}.$$

Since $x' = x + 1$ equals $(x' = x + 1) \lor \text{FALSE}$, we can rewrite this as

$$S \stackrel{\Delta}{\equiv} (x = 0) \wedge \Box[(x' = x + 1) \lor \text{FALSE}]_{\langle x \rangle}.$$

Following the procedure above, we add a prophecy variable $p$ that predicts if the next non-stuttering step (i.e., the next $(x' = x + 1) \lor \text{FALSE}$ step) is an $x' = x + 1$ step or a FALSE step:

$$ \begin{align*} S^p &\stackrel{\Delta}{\equiv} \mathit{Init}^p \wedge \Box[\mathit{Next}^p]_{\langle x, p \rangle}, \\ \mathit{Init}^p &\stackrel{\Delta}{\equiv} (p \in \{\mathit{go}, \mathit{stop}\}) \wedge \mathit{Init}, \\ \mathit{Next}^p &\stackrel{\Delta}{\equiv} ((p = \mathit{go}) \wedge (x' = x + 1) \wedge (p' \in \{\mathit{go}, \mathit{stop}\})) \\ &\phantom{\stackrel{\Delta}{\equiv} ((} \lor ((p = \mathit{stop}) \wedge \text{FALSE}) \wedge (p' \in \{\mathit{go}, \mathit{stop}\})). \end{align*} $$

If $p$ ever becomes equal to stop, then no further $\mathit{Next}^p$ step is possible (since no step can satisfy FALSE), at which point the behavior must consist entirely of stuttering steps. In other words, the behavior describes a system that has stopped. But that's fine because $S$ allows such behaviors. If we don't want $S$ to allow such halting behaviors, we must conjoin to it a supplementary property such as $\mathit{WF}_{\langle x \rangle}(x' = x + 1)$. In that case, $S^p$ becomes

$$\mathit{Init}^p \wedge \Box[\mathit{Next}^p]_{\langle x, p \rangle} \wedge \mathit{WF}_{\langle x \rangle}(x' = x + 1). \quad (17)$$

The conjunct $\mathit{WF}_{\langle x \rangle}(x' = x + 1)$ implies that a behavior must keep taking steps that increment $x$. Formula (17) thus rules out any behavior in which $p$ ever equals stop, and therefore the formula $\exists p : S^p \wedge \mathit{WF}_{\langle x \rangle}(x' = x + 1)$ is equivalent to $S \wedge \mathit{WF}_{\langle x \rangle}(x' = x + 1)$.

Readers who find this equivalence puzzling may be confusing the next-state action FALSE with the specification FALSE. The specification FALSE is satisfied by no behavior; the specification $\Box[\text{FALSE}]_{\langle x \rangle}$ allows any behavior in which the value of $x$ never changes.

Readers who find the specification (17) weird are not confused. It is weird. In the terminology introduced by ER, it is weird because it is not machine closed. (Machine closure is explained in ER; it originally appeared under the name feasibility [5].) Except in rare cases, system specifications should be machine closed. However, a specification obtained by adding a prophecy variable is not meant to specify a system. It is used only to verify the system. Its weirdness is harmless.

## 4.4 A Sequence of Prophecies

We generalize a simple prophecy variable that makes a single prediction to one that makes a sequence of consecutive predictions. As an example, let $\mathcal{D}$ be the specification that is the same as $\mathcal{A}$ except instead of alternating between input and output actions, it maintains a queue $\mathit{inq}$ of unprocessed input values. An input action appends a value to the end of $\mathit{inq}$, and an output action removes the value at the head of the queue and changes $\mathit{sum}$, $\mathit{num}$, and $\mathit{out}$ as in our previous specifications. An input action can be performed anytime, but an output action can occur only when $\mathit{inq}$ is not empty. The definition of $\mathcal{D}$ is in Figure 5, where for any nonempty sequence $\mathit{sq}$ of values, $\mathit{Head}(\mathit{sq})$ is the first element of $\mathit{sq}$ and $\mathit{Tail}(\mathit{sq})$ is the sequence obtained from $\mathit{sq}$ by removing its first element, with $\mathit{Tail}(\langle \rangle) = \langle \rangle$.
$$ \mathcal{D} \stackrel{\Delta}{\equiv} \exists \mathit{inq}, \mathit{num}, \mathit{sum} : \mathcal{ID} $$

$$ \mathcal{ID} \stackrel{\Delta}{\equiv} \mathit{Init}_{\mathcal{D}} \wedge \Box[\mathit{Next}_{\mathcal{D}}]_{\langle \mathit{inq}, \mathit{out}, \mathit{num}, \mathit{sum} \rangle} $$

$$ \mathit{Init}_{\mathcal{D}} \stackrel{\Delta}{\equiv} (\mathit{inq} = \langle \rangle) \wedge (\mathit{out} = \mathit{num} = \mathit{sum} = 0) $$

$$ \mathit{Next}_{\mathcal{D}} \stackrel{\Delta}{\equiv} \mathit{Input}_{\mathcal{D}} \vee \mathit{Output}_{\mathcal{D}} $$

$$ \mathit{Input}_{\mathcal{D}} \stackrel{\Delta}{\equiv} \exists n \in \mathit{Int} : (\mathit{inq}' = \mathit{Append}(\mathit{inq}, n)) \wedge \mathit{UC}(\langle \mathit{out}, \mathit{num}, \mathit{sum} \rangle) $$

$$ \begin{aligned} \mathit{Output}_{\mathcal{D}} \stackrel{\Delta}{\equiv} & (\mathit{inq} \neq \langle \rangle) \wedge (\mathit{inq}' = \mathit{Tail}(\mathit{inq})) \\ & \wedge (\mathit{sum}' = \mathit{sum} + \mathit{Head}(\mathit{inq})) \wedge (\mathit{num}' = \mathit{num} + 1) \\ & \wedge (\mathit{out}' = \mathit{sum}' / \mathit{num}') \end{aligned} $$

<caption>Fig. 5. The definition of specification $\mathcal{D}$.</caption>

$$ \mathcal{E} \stackrel{\Delta}{\equiv} \exists \mathit{inq}, \mathit{num}, \mathit{sum} : \mathcal{IE} $$

$$ \mathcal{IE} \stackrel{\Delta}{\equiv} \mathit{Init}_{\mathcal{D}} \wedge \Box[\mathit{Next}_{\mathcal{E}}]_{\langle \mathit{inq}, \mathit{out}, \mathit{num}, \mathit{sum} \rangle} $$

$$ \mathit{Next}_{\mathcal{E}} \stackrel{\Delta}{\equiv} \mathit{Next}_{\mathcal{D}} \vee \mathit{Undo}_{\mathcal{E}} $$

$$ \mathit{Undo}_{\mathcal{E}} \stackrel{\Delta}{\equiv} (\mathit{inq} \neq \langle \rangle) \wedge (\mathit{inq}' = \mathit{Tail}(\mathit{inq})) \wedge \mathit{UC}(\langle \mathit{out}, \mathit{sum}, \mathit{num} \rangle) $$

<caption>Fig. 6. The definition of specification $\mathcal{E}$.</caption>

$$ \mathcal{E}^p \stackrel{\Delta}{\equiv} \exists \mathit{inq}, \mathit{num}, \mathit{sum} : \mathcal{IE}^p $$

$$ \mathcal{IE}^p \stackrel{\Delta}{\equiv} \mathit{Init}_{\mathcal{E}}^p \wedge \Box[\mathit{Next}_{\mathcal{E}}^p]_{\langle \mathit{inq}, \mathit{out}, \mathit{num}, \mathit{sum}, p \rangle} $$

$$ \mathit{Init}_{\mathcal{E}}^p \stackrel{\Delta}{\equiv} (p = \langle \rangle) \wedge \mathit{Init}_{\mathcal{D}} $$

$$ \mathit{Next}_{\mathcal{E}}^p \stackrel{\Delta}{\equiv} \mathit{Input}_{\mathcal{E}}^p \vee \mathit{Output}_{\mathcal{E}}^p \vee \mathit{Undo}_{\mathcal{E}}^p $$

$$ \mathit{Input}_{\mathcal{E}}^p \stackrel{\Delta}{\equiv} (\exists d \in \{\mathit{do}, \mathit{undo}\} : p' = \mathit{Append}(p, d)) \wedge \mathit{Input}_{\mathcal{D}} $$

$$ \mathit{Output}_{\mathcal{E}}^p \stackrel{\Delta}{\equiv} (\mathit{Head}(p) = \mathit{do}) \wedge (p' = \mathit{Tail}(p)) \wedge \mathit{Output}_{\mathcal{D}} $$

$$ \mathit{Undo}_{\mathcal{E}}^p \stackrel{\Delta}{\equiv} (\mathit{Head}(p) = \mathit{undo}) \wedge (p' = \mathit{Tail}(p)) \wedge \mathit{Undo}_{\mathcal{E}} $$

<caption>Fig. 7. The definition of specification $\mathcal{E}^p$.</caption>

As for our previous example, we implement $\mathcal{D}$ with a specification $\mathcal{E}$, which also contains an undo action that throws away the first input in $\mathit{inq}$ instead of processing it. It is specified in Figure 6.

To define a refinement mapping under which $\mathcal{E}$ implements $\mathcal{D}$, we add a prophecy variable whose value is a sequence of predictions, each one predicting whether the corresponding value of $\mathit{inq}$ will be processed by an output action or thrown away by an undo action. Each prediction is made when the value is added to $\mathit{inq}$ by an input action. The prediction is forgotten when the predicted action occurs. The definition of $\mathcal{E}^p$ is in Figure 7.

For sequences $\mathit{vsq}$ and $\mathit{dsq}$ of the same length, let $\mathit{OnlyDo}(\mathit{vsq}, \mathit{dsq})$ be the subsequence of $\mathit{vsq}$ consisting of all the elements for which the corresponding element of $\mathit{dsq}$ equals $\mathit{do}$. For example:

$$ \mathit{OnlyDo}(\langle 3, 2, 1, 4, 7 \rangle, \langle \mathit{do}, \mathit{undo}, \mathit{undo}, \mathit{do}, \mathit{undo} \rangle) = \langle 3, 4 \rangle. $$
$$ \mathcal{F} \stackrel{\Delta}{\equiv} \exists \text{inset}, \text{num}, \text{sum} : \mathcal{IF} $$

$$ \mathcal{IF} \stackrel{\Delta}{\equiv} \text{Init}_\mathcal{F} \wedge \Box[\text{Next}_\mathcal{F}]_{\langle \text{inset}, \text{out}, \text{num}, \text{sum} \rangle} $$

$$ \text{Init}_\mathcal{F} \stackrel{\Delta}{\equiv} (\text{inset} = \{\}\land(\text{out} = \text{num} = \text{sum} = 0)) $$

$$ \text{Next}_\mathcal{F} \stackrel{\Delta}{\equiv} (\exists n \in \text{Int} \setminus \text{inset} : \text{Input}_\mathcal{F}(n)) \lor (\exists n \in \text{inset} : \text{Output}_\mathcal{F}(n)) $$

$$ \text{Input}_\mathcal{F}(n) \stackrel{\Delta}{\equiv} (\text{inset}' = \text{inset} \cup \{n\}) \land \text{UC} \langle \text{out}, \text{num}, \text{sum} \rangle $$

$$ \begin{align*} \text{Output}_\mathcal{F}(n) &\stackrel{\Delta}{\equiv} (\text{inset}' = \text{inset} \setminus \{n\}) \\ &\qquad \land (\text{sum}' = \text{sum} + n) \land (\text{num}' = \text{num} + 1) \\ &\qquad \land (\text{out}' = \text{sum}' / \text{num}') \end{align*} $$

<caption>Fig. 8. The definition of specification $\mathcal{F}$.</caption>

Specification $\mathcal{IE}$ implements $\mathcal{ID}$ under this refinement mapping:

$$ \text{inq} \leftarrow \text{OnlyDo}(\text{inq}, p), \text{sum} \leftarrow \text{sum}, \text{num} \leftarrow \text{num}. $$

The generalization from this example is straightforward, if we take $p = \langle \rangle$ to mean that there is no prediction being made. Let the next-state action Next be the disjunction of elementary actions that include a set of actions $A_i$ for $i$ in a set $P$, and let $P^n$ be the set of all length $n$ sequences of elements of $P$. Here is how we add a prophecy variable $p$ that makes a sequence of predictions of the $i$ for which the next $A_i$ step occurs:

(1) Conjoin $p \in P^n$ to the initial predicate $\text{Init}$, for some $n \ge 0$. (Note that $p \in P^0$ is equivalent to $p = \langle \rangle$.)

(2) Replace each $A_i$ by $(p = \langle \rangle \lor \text{Head}(p) = i) \land (p' = \text{Tail}(p)) \land A_i$.

(3) Replace each other elementary action $B$ by either $(p' = p) \land B$ or $(\exists i \in P : p' = \text{Append}(p, i)) \land B$.

As with simple prophecy variables, AX is satisfied with the required behavior $s_1^p, s_2^p, \dots$ being one in which all the right predictions are made.

In our definition of $\mathcal{E}^p$, we could eliminate the $p = \langle \rangle$ of condition 2 from the definitions of $\text{Output}_\mathcal{E}^p$ and $\text{Undo}_\mathcal{E}^p$ because $\mathcal{IE}^p$ implies that $p$ is always the same length as $\text{inq}$, and $\text{Output}_\mathcal{D}$ and $\text{Undo}_\mathcal{D}$ both imply $\text{inq} \neq \langle \rangle$.

In condition 1, $n$ can even equal $\infty$, where $P^\infty$ is the set of all infinite sequences of elements of $P$. In that case, condition 3 requires replacing $B$ by $(p' = p) \land B$, since one cannot append an element to an infinite sequence. Such a prophecy variable, which makes infinitely many initial predictions that can unfold forever, is used in the completeness proof of Section 7.

## 4.5 A Set of Prophecies

Our next type of prophecy variable is one that makes a set of concurrent predictions. Our example specification $\mathcal{F}$ is similar to $\mathcal{D}$, except that instead of a queue $\text{inq}$ of inputs, it has an unordered set $\text{inset}$ of inputs. An output action can process any element of $\text{inset}$. Formula $\mathcal{F}$ is defined in Figure 8, where $\setminus$ is the set difference operator, so $\text{Int} \setminus \text{inset}$ is the set of all integers not in $\text{inset}$.

As before, we add an undo action that can throw away an element in $\text{inset}$ so it is not processed by an output action. The resulting specification $\mathcal{G}$ is defined in Figure 9.

To show that $\mathcal{G}$ implements $\mathcal{F}$, we add a prophecy variable $p$ whose value is always a function with domain $\text{inset}$. For any element $n$ of $\text{inset}$, $p(n)$ predicts whether that element will be undone or produce an output. To write the resulting specification $\mathcal{G}^p$, we need some notation for describing functions:
$$ \mathcal{G} \stackrel{\Delta}{\equiv} \exists \text{inset}, \text{num}, \text{sum} : \mathcal{IG} $$

$$ \mathcal{IG} \stackrel{\Delta}{\equiv} \mathrm{Init}_{\mathcal{F}} \wedge \Box[\mathrm{Next}_{\mathcal{G}}]_{\langle \mathrm{inset}, \mathrm{out}, \mathrm{num}, \mathrm{sum} \rangle} $$

$$ \mathrm{Next}_{\mathcal{G}} \stackrel{\Delta}{\equiv} \mathrm{Next}_{\mathcal{F}} \lor (\exists n \in \mathrm{inset} : \mathrm{Undo}_{\mathcal{G}}(n)) $$

$$ \mathrm{Undo}_{\mathcal{G}}(n) \stackrel{\Delta}{\equiv} (\mathrm{inset}' = \mathrm{inset} \setminus \{n\}) \wedge \mathrm{UC} \langle \mathrm{out}, \mathrm{sum}, \mathrm{num} \rangle $$

<caption>Fig. 9. The definition of specification $\mathcal{G}$.</caption>

$$ \mathcal{G}^p \stackrel{\Delta}{\equiv} \exists \text{inset}, \text{num}, \text{sum} : \mathcal{IG}^p $$

$$ \mathcal{IG}^p \stackrel{\Delta}{\equiv} \mathrm{Init}_{\mathcal{G}}^p \wedge \Box[\mathrm{Next}_{\mathcal{G}}^p]_{\langle \mathrm{inset}, \mathrm{out}, \mathrm{num}, \mathrm{sum}, p \rangle} $$

$$ \mathrm{Init}_{\mathcal{G}}^p \stackrel{\Delta}{\equiv} (p = \mathrm{EmptyFcn}) \wedge \mathrm{Init}_{\mathcal{F}} $$

$$ \mathrm{Next}_{\mathcal{G}}^p \stackrel{\Delta}{\equiv} (\exists n \in \mathrm{Int} \setminus \mathrm{inset} : \mathrm{Input}_{\mathcal{G}}^p(n)) \lor (\exists n \in \mathrm{inset} : \mathrm{Output}_{\mathcal{G}}^p(n) \lor \mathrm{Undo}_{\mathcal{G}}^p(n)) $$

$$ \mathrm{Input}_{\mathcal{G}}^p(n) \stackrel{\Delta}{\equiv} (\exists d \in \{\mathrm{do}, \mathrm{undo}\} : p' = \mathrm{Extend}(p, n, d)) \wedge \mathrm{Input}_{\mathcal{F}}(n) $$

$$ \mathrm{Output}_{\mathcal{G}}^p(n) \stackrel{\Delta}{\equiv} (p(n) = \mathrm{do}) \wedge (p' = \mathrm{Remove}(p, n)) \wedge \mathrm{Output}_{\mathcal{F}}(n) $$

$$ \mathrm{Undo}_{\mathcal{G}}^p \stackrel{\Delta}{\equiv} (p(n) = \mathrm{undo}) \wedge (p' = \mathrm{Remove}(p, n)) \wedge \mathrm{Undo}_{\mathcal{G}}(n) $$

<caption>Fig. 10. The definition of specification $\mathcal{G}^p$.</caption>

*EmptyFcn* The (unique) function whose domain is the empty set.

*Extend(f, v, w)* The function $\tilde{f}$ obtained from function *f* by adding *v* to its domain and defining $\tilde{f}(v)$ to equal *w*.

*Remove(f, v)* The function obtained from function *f* by removing *v* from its domain.

The specification $\mathcal{G}^p$ is defined in Figure 10. As before, AX holds with $s_1^p, s_2^p, \dots$ a behavior having all the right predictions. Specification $\mathcal{IG}^p$ implements $\mathcal{IF}$ under this refinement mapping:

$$ \mathrm{inset} \leftarrow \{n \in \mathrm{inset} : p(n) = \mathrm{do}\}, \mathrm{sum} \leftarrow \mathrm{sum}, \mathrm{num} \leftarrow \mathrm{num}, $$

which assigns to the variable *inset* of $\mathcal{IF}$ the subset of *inset* consisting of all elements *n* with *p(n)* = *do*.

The only nontrivial part of the generalization from this example to an arbitrary set of prophecies is that *p* should make no prediction for a value not in its domain. Usually, as in our example, the actions to which the prediction apply are not enabled for a value not in the domain of *p*. If that's not the case, then the condition conjoined to an action to enforce the prediction should equal *TRUE* if the prediction is being made for a value not in the domain of *p*.

## 4.6 Further Generalizations of Prophecy Variables

Prophecy variables making sequences and sets of predictions can be generalized to prophecy variables whose predictions are organized in any data structure—even an infinite one. The generalization is described in detail in [18]. The basic ideas are:

* A prediction predicts a value *i* for which the next step satisfying an action $\exists i \in P : A_i$ satisfies $A_i$. To add the prophecy variable, each $A_i$ is modified to enforce this prediction.
* An action or an initial condition that makes a prediction must allow any value *i* in *P* to be predicted.

* Any action may remove predictions and/or make new predictions. An action that fulfills a prediction must remove that prediction. Except for that requirement, actions may leave all predictions unchanged.

Whether a particular prophecy is made is often indicated by the data structure containing the prophecies. In the example of Section 4.5, whether a prediction is made for an integer *n* depends on whether *n* is in the domain of *p*. Sometimes it is convenient to indicate the absence of a prophecy by a special value none that is not an element of the set *P* of possible predictions. In the example of a simple prophecy variable in Section 4.2, we could let the *Output* and *Undo* actions remove the prophecy by setting *p* to none and have the *Input* action make the prophecy by setting *p* to do or undo. A none value is handled like the value $\langle \rangle$ of the prophecy sequence variables of Section 4.4.

## 4.7 Stuttering Variables

Usually, when $S_1$ implements $S_2$, specification $S_1$ takes more steps than $S_2$. Those extra steps simulate stuttering steps of $S_2$ under a refinement mapping. As an example, let $S_2$ have an internal variable *q*, whose value is a sequence, and an action *A* that sets *q* to *Tail*(*q*). Let *A* equal

$$E \wedge (q' = \text{Tail}(q)) \wedge \text{UC} \langle \mathbf{w} \rangle,$$

where *E* is an enabling condition that implies $q \neq \langle \rangle$, and $\mathbf{w}$ is the list of all internal and external variables of $S_2$ except *q*.

Let $S_1$ implement $S_2$ by representing *q* with an array variable *a*, where the value of *q* is the sequence of elements $a[0], ..., a[\text{Len}(*q*) - 1]$, and $a[j]$ equals a special value null for $j \ge \text{Len}(*q*)$. (We assume that *a* is a large enough array—perhaps infinite.) Let an *A* step of $S_2$ be implemented with a variable *i*, initially equal to 0, by steps setting $a[i]$ to $a[i + 1]$ for *i* equal to 0 through $\text{Len}(*q*) - 1$, the last step resetting *i* to 0. To show that $S_1$ implements $S_2$, we might use a refinement mapping in which an *A* step of $S_2$ is implemented by the first of those $\text{Len}(*q*)$ steps of $S_1$.

If *a* and *i* are internal variables of $S_1$, then $S_2$ should implement $S_1$. Since $S_1$ takes more steps than $S_2$ to implement an *A* step, defining a refinement mapping to show that $S_2$ implements $S_1$ requires an auxiliary variable that adds stuttering steps to $S_2$ that implement the additional steps taken by $S_1$. That variable must add $\text{Len}(*q*) - 1$ stuttering steps for each *A* step.

ER made their prophecy variables more complicated so they could add stuttering steps; we have long felt it was easier instead to use a new kind of auxiliary variable. We introduce a variable *s* that can add stuttering steps before and/or after an action, in this case the action *A*. An easy way to do it is to let the value of *s* be a natural number. Normally *s* equals 0; it is set to a positive integer to take stuttering steps, the value of *s* being the number of steps remaining. Let *Init* and *Next* be the initial predicate and next-state actions of $S_2$. We assume *Next* is written $A \lor B_1 \lor \dots \lor B_n$, where for each *j*, no step is both an *A* and $B_j$ step. We add the stuttering variable *s* to $S_2$ as follows to obtain the specification $S_2^s$ that adds $\text{Len}(*q*) - 1$ steps after each *A* step. The initial predicate $\text{Init}^s$ and next-state action $\text{Next}^s$ of $S_2^s$ are

$$\text{Init}^s \triangleq \text{Init} \wedge (s = 0) \qquad \text{Next}^s \triangleq A^s \lor B_1^s \lor \dots \lor B_n^s,$$

$$A^s \triangleq ((s = 0) \wedge (s' = \text{Len}(q) - 1) \wedge A) \lor ((s > 0) \wedge (s' = s - 1) \wedge \text{UC} \langle \mathbf{w}, q \rangle),$$

$$B_j^s \triangleq (s = s' = 0) \wedge B_j, \text{ for } j = 1, \dots, n.$$

Defining the refinement mapping under which $S_2^s$ implements $S_1$ is tricky. The reader can verify that if *A* were the only action that changed *q*, then the correct refinement mapping would include
these substitutions, where $q[k]$ equals the $k^{th}$ element of $q$:

$$ 
\begin{array}{l}
i \leftarrow iBar \\
a[j] \leftarrow \text{if } s = 0 \\
\quad \text{then if } j < \text{Len}(q) \quad \text{then } q[j+1] \quad \text{else null} \\
\quad \text{else if } j < iBar \quad \text{then } q[j+1] \\
\quad \quad \text{else if } j \le \text{Len}(q) \quad \text{then } q[j] \quad \text{else null} \\
\text{where } iBar \triangleq \text{ if } s = 0 \text{ then } 0 \text{ else } \text{Len}(q) + 1 - s.
\end{array}
$$

To add the $Len(q) - 1$ stuttering steps before every $A$ step, we just change the definition of $A^s$ to:

$$ 
\begin{aligned}
A^s \triangleq & ((s = 0) \land E \land (s' = \text{Len}(q) - 1) \land \text{UC}(\mathbf{w}, q)) \\
& \lor ((s > 1) \land (s' = s - 1) \land \text{UC}(\mathbf{w}, q)) \\
& \lor ((s = 1) \land (s' = 0) \land (q' = \text{Tail}(q)) \land \text{UC}(\mathbf{w})).
\end{aligned}
\quad (18)
$$

Finding a refinement mapping with this stuttering variable is another tricky exercise.

The generalizations that add $K$ stuttering steps before or after each $A$ step, for an arbitrary state function $K$ and action $A$, are straightforward. To add the steps after $A$, we modify the definition above by replacing $Len(q) - 1$ with $K$ and $w, q$ with the list of all variables of $S_2$. To add the stuttering steps before the $A$ step, we make one additional change to the corresponding definition of $A^s$: replacing $(q' = Tail(q)) \land UC(w)$ with $F$, where $F$ is an action such that $A \equiv E \land F$ and $F$ is enabled in every state in which $E$ is true.

We don't have to use natural numbers for counting stuttering states. We can add stuttering steps both before and after an action by using negative integers to count the steps after the action, counting up to 0-e.g., for an additional $J$ stuttering steps after action $A$, we can replace the last disjunct of Formula (18) by

$$ 
\begin{aligned}
& \lor ((s = 1) \land (s' = -J) \land (q' = Tail(q)) \land \text{UC}(\mathbf{w})) \\
& \lor ((s < 0) \land (s' = s + 1) \land \text{UC}(\mathbf{w}, q)).
\end{aligned}
$$

Often, we let $s$ take values that help define the refinement mapping. For example, suppose we want to take stuttering steps so the refinement mapping can implement an action by each process satisfying some condition. We can let $s$ always be a sequence of processes, where the empty sequence is the normal value of $s$, and counting down is done by $s' = Tail(s)$.

A single variable $s$ can be used to add stuttering steps before and/or after multiple actions. For example, we can let the normal value of $s$ be $\langle\rangle$, add stuttering steps to an action $A$ by letting $s$ assume values of the form $\langle“A”, i\rangle$ for a number $i$, and add stuttering steps to an action $B$ by letting $s$ assume values of the form $\langle“B”, q\rangle$ for $q$ a sequence of processes.

To handle the rare case when $S_1$ implements $S_2$ but it has internal behaviors that halt while the corresponding internal behaviors of $S_2$ must take additional steps, we add an infinite stuttering variable $s$ to $S_1$ that simply keeps changing forever. The formula $WF_{\langle s \rangle}(s' \neq s)$ asserts that there are infinitely many steps in which the value of $s$ changes.<fnref n="2" /> We add the auxiliary variable $s$ by conjoining to the supplementary property of $S_1$ the temporal logic tautology $\exists s : WF_{\langle s \rangle}(s' \neq s)$. An infinite stuttering variable is our only auxiliary variable that is added by modifying the supplementary property rather than the initial predicate and next-state action.

<footnote n="2">²We assume that variables can take more than one value.</footnote>
<figure><img src="image_3.png" /><figcaption>Fig. 11. The common prefix of behaviors $\sigma$ and $\tau$.</figcaption></figure>

## 5 VERIFYING LINEARIZABILITY

Linearizability has become a standard way of specifying an object shared by multiple processes [10]. A process's operation *Op* is described by a sequence of three steps: a *BeginOp* step that provides the operation's input, a *DoOp* step that performs the operation by reading and/or modifying the object, and an *EndOp* step that reports the operation's output. The *BeginOp* and *EndOp* steps are externally visible, meaning that they change external variables. The *DoOp* step is internal, meaning it modifies only internal variables.

We illustrate our use of auxiliary variables for verifying a linearizability specification with the atomic snapshot algorithm of Afek et al. [3]. Our discussion is informal; a precise exposition including formal TLA⁺ specifications is in [18]. The algorithm implements an array of memory registers accessed by a set of writer processes and a set of reader processes, with one register for each writer. A writer can perform *write* operations to its register. A reader can perform *read* operations that return a “snapshot” of the memory—that is, the values of all the registers.

We let *LinearSnap* be a linearizable specification of what a snapshot algorithm should do. It uses an internal variable *mem*, where *mem*(*w*) equals the value of writer *w*'s register. A *DoWrite* step modifies *mem*(*w*) for a single writer *w*. A single *DoRead* step reads the value of *mem*. Another internal variable maintains a process's state while it is performing an operation, including whether the *DoOp* action has been performed and, for a reader, what value of *mem* was read by *DoRead* and will be returned by *EndRead*. An external variable describes the *BeginOp* and *EndOp* actions.

We consider a simplified version of the Afek et al. snapshot algorithm we call *SimpleAfek*. It maintains an internal variable *imem*. A writer *w* writes a value *v* on its *i*th write by setting *imem*(*w*) to the pair ⟨*i*, *v*⟩. A reader does a sequence of reads of *imem*, each of those reads reading the values of *imem*(*w*) for all writers *w* in separate actions, executed in any order. If the reader obtains the same value of *imem* on two successive reads, it returns the obvious snapshot contained in that value of *imem*. If not, it keeps reading. *SimpleAfek* does not guarantee termination. The actual algorithm adds a way to have reading terminate after at most three reads and a way to replace the unbounded write numbers by a bounded set of values. The more complicated algorithm can be handled in the same way as *SimpleAfek*.

*SimpleAfek* implements *LinearSnap*, but constructing a refinement mapping to show that it does requires predicting the future. We show why with the following example, illustrated in Figures 11 to 13. There are two writers, named 1 and 2, and one reader. We describe two behaviors $\sigma$ and $\tau$ of *SimpleAfek* and consider how a refinement mapping maps steps of those behaviors to *DoRead* and *DoWrite* steps of *LinearSnap*. As shown in Figure 11, both behaviors begin in a state having $imem(1) = imem(2) = \langle 0, old \rangle$ for some value *old* and with the reader performing a *BeginRead* step (labeled *BR*) and beginning its sequence of reads of the complete array *imem* with individual reads obtaining the value $\langle 0, old \rangle$ for the first reads $Rd_1(1)$ of $imem(1)$ and $Rd_1(2)$ of $imem(2)$, as well as for the second read of $imem(1)$. Meanwhile, writer 1 performs a
<figure><img src="image_4.png" /><figcaption>Fig. 12. Suffix of behavior $\sigma$.</figcaption></figure>

<figure><img src="image_5.png" /><figcaption>Fig. 13. Suffix of behavior $\tau$.</figcaption></figure>

BeginWrite step $BW(new)$ of the value new. It then writes value new to imem(1), updating it to $\langle 1, new \rangle$, followed by an EndWrite step.

As illustrated in Figure 12, in behavior $\sigma$ the reader then completes its second read, finding $imem(2) = \langle 0, old \rangle$. Concurrently, writer 2 writes new to its register, the write of $imem(2)$ occurring after the second read of $imem(2)$. Since the first two reads see the same values of $imem$, the read completes and returns the snapshot with $mem(1) = mem(2) = old$. Because the reader obtained the snapshot before the writes, we have:

A. For behavior $\sigma$, the step of *SimpleAfek* that implements the *DoRead* step must precede the step that implements writer 1's *DoWrite* step.

As shown in Figure 13, in behavior $\tau$ the second read of $imem(2)$ is preceded by writer 2 updating $imem(2)$ to $\langle 1, new \rangle$. The reader then continues its operation, finding $imem(2) = \langle 1, new \rangle$. Because the first two reads obtained different values of $imem(2)$, the reader continues reading. Its third and fourth reads find $imem(1) = imem(2) = \langle 1, new \rangle$, so the read completes and returns the snapshot with $mem(1) = mem(2) = new$. Since that snapshot contains the value written by writer 1, we have:

B. For behavior $\tau$, the step of *SimpleAfek* that implements the *DoRead* step must follow the steps that implement the *DoWrite* steps of both writers.

Observations A and B imply that to handle the behavior $\sigma$ correctly, the refinement mapping must know that the current behavior is $\sigma$ and not $\tau$ before the two behaviors have diverged. This is possible only if something in the state predicts the future—i.e., only if we add a prophecy variable.

Linearizability provides a simple, uniform way of specifying data objects, but it provides little insight into what state must be maintained by an implementation. Whether this is a feature or a flaw depends on what the specification is used for. We present an equivalent snapshot specification *NewLinearSnap* that can make verifying correctness of an implementation easier. We verify that *SimpleAfek* implements *LinearSnap* by verifying that it implements *NewLinearSnap* and that *NewLinearSnap* implements *LinearSnap*.
In addition to the internal variable *mem* of *LinearSnap*, *NewLinearSnap* uses an internal variable *isnap* such that during a read operation by reader *r*, the value of *isnap(r)* is the sequence of values that *mem* had since the operation began. These values are the snapshots that *LinearSnap* allows the read to return. The *BeginRead* action sets *isnap(r)* to a one-element sequence containing the current value of *mem*. The writer actions are the same as in *LinearSnap*, except that a *DoWrite* action appends the new value of *mem* to *isnap(r)* for all readers *r* that have executed a *BeginRead* action but not the corresponding *EndRead*. The *EndRead* action of reader *r* returns a nondeterministically chosen element of the sequence *isnap(r)*. There is no *DoRead* action.

To verify that *SimpleAfek* implements *NewLinearSnap*, we add to it a history variable that has the same value as variable *isnap* of *NewLinearSnap*. Translating an understanding of why the algorithm is correct into an invariant of *SimpleAfek* and a refinement mapping under which it implements *NewLinearSnap* is then a typical exercise in assertional reasoning about concurrent algorithms, requiring no prophecy variable.

Although *NewLinearSnap* is equivalent to *LinearSnap*, to verify *SimpleAfek* we need only verify that it implements *LinearSnap*. This is done by first adding to it a prophecy variable *p* so that *p(r)* predicts which element of the sequence *isnap(r)* of snapshots will be chosen by the *EndRead* action of reader *r*. The value of *p(r)* is set to an arbitrary positive integer by *r*'s *BeginRead* action and is reset to none by its *EndRead* action.

If *p(r)* is set to 1, predicting that *r* will return the value *mem* had when the *BeginRead* step occurred, then the refinement mapping will cause the *DoRead* step of *LinearSnap* to occur right after the *BeginRead* step. If *p(r)* is set to a number greater than 1, predicting that *r* will return the value of *mem* after the (*p(r)* − 1)st *DoWrite* action since the read began, then the refinement mapping will cause the *DoRead* step to occur immediately after that *DoWrite* step. The step that implements the *DoRead* step of *LinearSnap* is added as follows as a stuttering step of *NewLinearSnap*.

We introduce a stuttering variable that adds a single stuttering step after *r*'s *BeginRead* action if *p(r)* = 1, and that adds stuttering steps after each *DoWrite* action—one stuttering step for every read *r* for which the write adds the *p(r)*th element to *isnap(r)*. To add the stuttering step after a *BeginRead* step, the stuttering variable simply counts down from 1. To add any necessary stuttering steps after a *DoWrite* step, it counts down using the set of readers whose *DoRead* the steps will simulate. Requiring the stuttering steps to simulate those *DoRead* steps of *LinearSnap* makes it clear how to define the refinement mapping.

The verification that *SimpleAfek* implements *LinearSnap*, which requires a prophecy variable, has been split into two steps: verifying that the intermediate specification *NewLinearSnap* implements *LinearSnap* and is implemented by *SimpleAfek*. Only the first step requires a prophecy variable. This approach can also be applied to an example in Herlihy and Wing's article defining linearizability [10]: an algorithm that implements a linearizable specification of a queue and requires predicting the future to construct a refinement mapping. The intermediate specification replaces the totally ordered queue of the original specification with a partially ordered set, where the partial order constrains which items may be dequeued. A refinement mapping showing that the new specification implements the original one can be defined using a prophecy variable that predicts the order in which items will be dequeued.

Verifying linearizability is an important problem. Liang and Feng devised a method for doing it [19], and Chakraborty et al. developed an elaborate theory just for proving linearizability of queue algorithms [6]. Our method of decomposing the verification has two obvious advantages. Adding a prophecy variable is not trivial—especially for complex algorithms. It is easier to add it to the simpler intermediate specification. Second, the same intermediate specification can be used for
$$Init_1 \stackrel{\Delta}{\equiv} x = 0 \qquad Next_1 \stackrel{\Delta}{\equiv} x' = x + 1$$

$$Stops \stackrel{\Delta}{\equiv} \diamond \Box [x' = x]_{\langle x \rangle}$$

$$S_1 \stackrel{\Delta}{=} Init_1 \wedge \Box [Next_1]_{\langle x \rangle} \wedge Stops$$

$$Init_2 \stackrel{\Delta}{=} (x = 0) \wedge (y \in Nat)$$

$$Next_2 \stackrel{\Delta}{=} (y > 0) \wedge (x' = x + 1) \wedge (y' = y - 1)$$

$$IS_2 \stackrel{\Delta}{=} Init_2 \wedge \Box [Next_2]_{\langle x,y \rangle}$$

$$S_2 \stackrel{\Delta}{=} \exists y : IS_2$$

<caption>Fig. 14. The definitions of specification $S_1$ and $S_2$.</caption>

multiple implementations. There is a third advantage that suggests the approach should be widely applicable: the intermediate specification is likely to be useful.

A specification might be written for implementors of a system or for its users. A specification written for implementors should not contain in its state information that is not needed by an implementation. The need for auxiliary variables to define a refinement mapping means that its state does contain unnecessary information. However, it could be a better specification for users. It's easier for a user to think of a queue as being totally ordered; an implementor should know that a partial order suffices. Writing an intermediate specification with no unnecessary state can be a useful part of the system-design process.

# 6 PROPHECY CONSTANTS

In addition to variables and constants like 0, a temporal logic formula can contain constant parameters. The sets of readers and writers in the *Simple Afek* specification are examples of constant parameters. Constant parameters can also be used to make predictions. Moreover, no new rules are required to use them in this way. The ordinary rules of logic suffice.

What we call a variable is called a *flexible variable* by logicians because its value can vary during the course of a behavior. They call a constant parameter a *rigid variable* because its value remains the same throughout a behavior. In addition to quantifiers over variables, temporal logic has quantifiers $\exists$ and $\forall$ over constant parameters. A behavior $\sigma$ satisfies the formula $\exists n : \mathcal{F}$ iff there is a value of the constant parameter $n$ (the same value in every state of $\sigma$) for which $\sigma$ satisfies $\mathcal{F}$. We let $\exists n \in P : \mathcal{F}$ equal $\exists n : (n \in P) \wedge \mathcal{F}$, where $P$ is a constant expression (one containing only constants and constant parameters) not containing $n$. The following simple rule of ordinary logic holds for any temporal logic formulas $\mathcal{F}$ and $\mathcal{G}$ and constant expression $P$.

**Elimination** To prove $(\exists n \in P : \mathcal{F}) \Rightarrow \mathcal{G}$, it suffices to assume $n \in P$ and prove $\mathcal{F} \Rightarrow \mathcal{G}$.

The following example from Section 5.2 of ER shows how this rule can be used to construct refinement mappings that require predicting the future, without adding a prophecy variable.

Specification $S_1$ is satisfied by behaviors that begin with $x = 0$, repeatedly increment $x$ by 1, and eventually stop (take only stuttering steps). It has no internal variables. Specification $S_2$ has external variable $x$ and internal variable $y$. Its internal specification is satisfied by behaviors that begin with $x = 0$ and $y$ any element of the set $Nat$ of natural numbers, take steps that increment $x$ by 1 and decrement $y$ by 1, and stop when $y = 0$. The TLA specifications of $S_1$ and $S_2$ are in Figure 14, where formula *Stops* asserts that the value of $x$ eventually stops changing.

Clearly $S_1$ and $S_2$ are equivalent, since both are satisfied by behaviors that increment $x$ a finite number of times (possibly 0 times) and then stop. ER observes that $S_1 \Rightarrow S_2$ cannot be verified
using their prophecy variables because $S_1$ doesn't satisfy a condition they call finite internal non-determinism. We can prove it using the $\exists$ Elimination rule.

Specification $S_1$ implies that the value of $x$ is bounded, which means that there is some natural number $n$ for which $x \le n$ is an invariant. This means that the following theorem is true:

$$S_1 \Rightarrow \exists n \in Nat : \Box(x \le n). \qquad (19)$$

Define $\mathcal{T}_1(n)$ to equal $S_1 \wedge \Box(x \le n)$. Formula (19) implies that $S_1$ equals $\exists n \in Nat : \mathcal{T}_1(n)$. By the $\exists$ Elimination rule, this implies that to prove $S_1 \Rightarrow S_2$, it suffices to assume $n \in Nat$ and prove $\mathcal{T}_1(n) \Rightarrow S_2$. This can be done with the refinement mapping $\bar{y} \leftarrow n - x$. The proof of $S_1 \Rightarrow S_2$ can be made completely rigorous in TLA and presumably in other temporal logics.

In general, we prove $S_1 \Rightarrow S_2$ by finding a formula $\mathcal{T}_1(n)$ such that $S_1$ implies $\exists n \in P : \mathcal{T}_1(n)$ for some constant set $P$, and we then prove $n \in P$ implies $\mathcal{T}_1(n) \Rightarrow S_2$. We can view this method in two ways. The first is that instead of proving $S_1 \Rightarrow S_2$ with a single refinement mapping, we prove $\mathcal{T}_1(n) \Rightarrow S_2$ by using a separate refinement mapping for each value of $n$. The second is that $n$ is a constant that predicts the value $x$ will have when the execution stops (stutters forever). We take the latter view and call $n$ a *prophecy constant*.

Prophecy constants are useful for predicting the infinite future—that is, making predictions that depend on the entire behavior. Section 6 of ER provides an example in which they cannot prove $S_1 \Rightarrow S_2$ with a refinement mapping because the supplementary property of $S_2$ implies that the initial value of an internal variable depends on whether the behavior terminates, violating a condition they call internal continuity. It is easy to find the refinement mapping by adding a prophecy constant that predicts if the behavior terminates—a prediction about the entire behavior.

The completeness results of the next section show that, in principle, we can use prophecy constants instead of prophecy variables, and vice versa. In practice, it seems that we should use prophecy variables to predict safety and prophecy constants to predict liveness. A prophecy variable is good for predicting which of multiple possibilities will be allowed to happen; a prophecy constant is good for predicting what will eventually happen.

“Prophecy constants” is just a new name for the bound rigid variables of a temporal logic. The observation that those bound variables can be used for defining refinement mappings appears not to have been published before. Hesselink’s eternity variables [11] are essentially a special case of prophecy constants, except based on reasoning directly about sequences of states using history variables rather than on temporal logic. Temporal logic was introduced to computer science by Pnueli to abstract that kind of reasoning [24].

# 7 THE EXISTENCE OF REFINEMENT MAPPINGS

We now present two completeness results. The first states that for any specification $S_1$ of the form $\exists y : Init \wedge \Box[Next]_{(x,y)} \wedge L$, if $S_1$ implements $S_2$, then we can add history, stuttering, and prophecy variables to $S_1$ to obtain an equivalent specification $S_1^a$ for which there exists a refinement mapping showing that $S_1^a$ implements $S_2$. The second result is the same except for prophecy constants rather than prophecy variables.

These results require only the assumption that the language for defining auxiliary variables and writing proofs is sufficiently expressive. (TLA$^+$ is such a language.) We first sketch the proof for prophecy constants. It is almost the same as Hesselink’s proof of completeness for eternity variables [11]. We then indicate how the proof is modified for prophecy variables. In the proofs, we let a specification’s state be an assignment of values to that specification’s variables, and we let a behavior of a specification be the sequence of specification states of a behavior satisfying the specification.
Let $IS_1$ and $IS_2$ be the internal specifications of $S_1$ and $S_2$. To simplify the proof, we assume that the next-state action $Next$ of $IS_1$ allows stuttering steps, replacing it by $Next \lor UC \langle \mathbf{x}, \mathbf{y} \rangle$ if necessary; and we assume $IS_1$ never halts, adding an infinite stuttering variable if it may halt.<fnref n="3" /> Let $IS_1^h$ be obtained from $IS_1$ by adding a history variable $h$ that initially equals 1 and is incremented by 1 with every $Next$ step. Letting $\sigma_{[i]}$ be the $i$th state of a behavior $\sigma$, specification $IS_1^h$ equals

$$ \exists \sigma \in P : IS_1^h \land \Box (\langle \mathbf{x}, \mathbf{y} \rangle = \sigma_{[h]}), $$

where $P$ is the set<fnref n="4" /> of all behaviors of $IS_1^h$. We define a refinement mapping using $\sigma$ as a prophecy constant.

Since $S_1$ implements $S_2$, for each $\sigma$ in $P$ there exists a behavior $f(\sigma)$ of $IS_2$ that $\sigma$ simulates. We define the refinement mapping for $\sigma$ so that it maps the state $\sigma_{[h]}$ in the behavior of $IS_1^h$ to the corresponding state $f(\sigma)_{[g]}$ of $IS_2$, for some $g$. In the absence of stuttering steps, $g$ would equal $h$. To define $g$ in general, we first make the externally visible steps $\sigma$ and $f(\sigma)$ match up by adding stuttering steps to $\sigma$ and/or $f(\sigma)$. Since our specifications are stuttering insensitive, we can choose $f$ so that $f(\sigma)$ already has the necessary stuttering steps. Since $\sigma$ is an arbitrary behavior of $IS_1$, we may have to add stuttering steps to it to make the externally visible steps of $\sigma$ match those of $f(\sigma)$. We do that by adding a stuttering variable $s$ to $IS_1^h$. We can then define $g$ to be a function of $h$, $s$, $\sigma$, and $f(\sigma)$.

We now show how to use a prophecy variable $p$ instead of the prophecy constant $\sigma$ to construct the refinement mapping. Let $IS_1^h$ be as above. Let $IS_1^{hj}$ be the specification obtained by adding a history variable $j$ to $IS_1^h$ whose value is the sequence of $IS_1$ states reached thus far during the current behavior of $IS_1^h$. Initially, $j$ contains a single element that equals the initial state of $IS_1$; and each $Next^h$ step appends the new $IS_1$ state to $j$. At any point during an execution of $IS_1^{hj}$, the value of $j$ is the part of the behavior of $IS_1$ executed thus far, and its length always equals $h$. We will define $p$ to be a prophecy variable whose value is an infinite sequence of $IS_1$ states, predicted to be the rest of the behavior whose prefix is the current value of $j$. Thus, the complete behavior $\sigma$ is a function of the current state. We can then define the necessary refinement mapping $g$ the same way we did for the prophecy constant $\sigma$.

To complete our proof sketch, we show how the prophecy variable $p$ is defined and how to define the behavior $\sigma$ of $IS_1$ as a function of the current values of $j$ and $p$. Let $\Sigma$ be any set of $IS_1$ states containing all its reachable states. We then define the specification $IS_1^{hjp}$ obtained by adding the prophecy variable $p$ to $IS_1^{hjp}$ as follows: the initial value of $p$ is any infinite sequence of elements of $\Sigma$, and the next-state action of $IS_1^{hjp}$ is

$$ Next^{hj} \land (Head(p) = \langle \mathbf{x}', \mathbf{y}' \rangle) \land (p' = Tail(p)). $$

The behavior $\sigma$ is defined to equal the concatenation of $j$ and $p$, which equals its initial value throughout a behavior of $IS_1^{hjp}$. Define a step of $\sigma$ to be a correct prediction if it satisfies the next-state relation of $IS_1$. If all the steps of $\sigma$ are correct predictions, then $\sigma$ is a behavior of $IS_1$. We can therefore define the required refinement mapping the same way we did for the prophecy constant $\sigma$. If $\sigma$ contains an incorrect prediction, then $IS_1^{hjp}$ halts (stutters forever) at the first incorrect prediction. Since $IS_1$ is assumed not to halt, this means $\sigma$ does not satisfy $IS_1$ and it doesn't

<footnote n="3">³This also allows us to avoid Hesselink's "preservation of quiescence" assumption.</footnote>

<footnote n="4">⁴In TLA⁺, it is easy to write a specification $IS_1^h$ in which $P$ is a collection that is “too large” to be a set—for example, a version of the Afek et al. algorithm in which a memory value can be any set, Russell’s paradox implying that the collection of all sets is not a set. We could remove the assumption that $P$ is a set by generalizing prophecy variables and constants to predict one among an arbitrary collection of possibilities, but there is no practical reason to do so. This assumption is built into many formalisms, including the one used by ER.</footnote>
matter how the refinement mapping is defined, since a proof that $S_1$ implements $S_2$ considers only behaviors satisfying $IS_1$.

These completeness proofs are based on embedding behavioral reasoning in state-based reasoning by recording behaviors in auxiliary variables. This is the same idea used in the first completeness result for assertional reasoning about concurrent specifications [22]. Such a completeness result is important because it shows that there are no inherent limitations to a proof method. However, it does not tell us anything about how to use the method in practice. For example, prophecy constants and prophecy variables are used differently, even though their completeness proofs are similar. Trying to mimic the reasoning used in these completeness proofs would simply place a state-based veneer over a behavioral proof. It would defeat the purpose of refinement mappings, which is to extend the Floyd-Hoare state-based assertional approach to concurrent systems.

# 8 CONCLUSION

Refinement means implementing a higher-level description of a program or system with a lower-level one. We know of two general methods of verifying refinement: refinement mappings, which we have described, and reduction. Reduction means obtaining a coarser-grained description (one with fewer atomic actions) from a finer-grained one by combining multiple atomic actions into a single action [20]. Reduction can be performed in TLA using refinement mappings [7].

ER and later uses of prophecy variables are based on assertional reasoning, introduced by Floyd [9] and Hoare [12]. The fundamental principle underlying this reasoning is that whether a program will do the correct thing in the future depends not on what it did in the past (or what it will do in the future), but on a property of its current state. For properties like invariance (including partial correctness) and termination that can be described in terms of the program's state, auxiliary variables are not necessary. They are needed only for refinement, which relate two specifications that may have different sets of states.

Much of the recent work uses prophecy variables based on a paradigm in which a *havoc* statement nondeterministically assigns to the variable an arbitrary element of some set of values, and a subsequent *assume* statement aborts execution if the “wrong” value was chosen. If the set of values is finite, this is a special case of an ER prophecy variable. Because it is a restricted type of ER variable, it is sound for an infinite set of values even though it doesn’t satisfy ER’s finite internal nondeterminism condition.

This *assume/havoc* approach is much like our simple prophecy variable, and it too is easier to use than an ER prophecy variable because it involves thinking forward to the future rather than backward from the future. However, like an ER prophecy variable, it predicts the future value of a variable. Our prophecy variables predict future events (action executions). This allows us easily to make predictions about structured sets of events, such as sequences. The prophecy variables of Zhang et al. [26] can predict a finite sequence of future values of a variable, but unlike predictions made with our prophecy sequences, their predictions cannot be modified. And sequences are just one kind of structure that can be put on our predictions.

Some recent work [8, 23] uses prophecy variables to assist in model checking, verifying that something eventually happens by adding a variable that predicts how many steps it takes for it to happen. They are verifying properties of state machines. Other recent work on prophecy variables [15, 19, 25, 26] uses Hoare triples to reason about programming-language code. Some of this work is for proving reduction [25]. The rest is for proving refinement (also called abstraction).

Being based on a programming language limits the power of methods. Reduction and refinement mappings are restricted to conform to the program structure. For example, it seems impossible for them to prove the equivalence (each refining the other) of two formulations of a simple *N*-process
producer-consumer algorithm—one using two processes and the other using *N* processes [16]. Because their expression languages have no way of describing the control state, these programming-language-based methods require history variables to prove even the simplest properties—for example, that the parallel composition of two atomic statements that each increment *x* by 1 is a program that increments *x* by 2. Moreover, they do not seem to be able to express, let alone verify, the rich variety of liveness conditions that arise in concurrency—for example, to distinguish between weakly and strongly fair semaphores.

We do not mean to denigrate programming languages and verification of programs written in them. Programs are what are executed on computers, and it is important to verify them. TLA is for describing and reasoning about algorithms, which are above the code level. Hoare famously said: "Inside every large program is a small program that is struggling to get out." That small program is what we call an algorithm [14]. TLA is for specifying and reasoning about those algorithms. TLA is simple because it is very close to its semantics. It is extremely expressive because it uses the full power of mathematics to describe an algorithm. The algorithm and the properties we prove about it are written in mathematics, the same language in which the proofs are written. There is no need for a special verification logic such as Hoare logic or separation logic. TLA is mathematics.

## REFERENCES

[1] Martín Abadi. 2015. The prophecy of undo. In *Fundamental Approaches to Software Engineering (Lecture Notes in Computer Science)*, Alexander Egyed and Ina Schaefer (Eds.), Vol. 9033. Springer, Berlin, 347–361.

[2] Martín Abadi and Leslie Lamport. 1991. The existence of refinement mappings. *Theoretical Computer Science* 82, 2 (May 1991), 253–284.

[3] Yehuda Afek, Hagit Attiya, Danny Dolev, Eli Gafni, Michael Merritt, and Nir Shavit. 1993. Atomic snapshots of shared memory. *Journal of the ACM* 40, 4 (Sept. 1993), 873–890.

[4] Bowen Alpern and Fred B. Schneider. 1985. Defining liveness. *Information Processing Letters* 21, 4 (Oct. 1985), 181–185.

[5] Krzysztof R. Apt, Nissim Francez, and Shmuel Katz. 1988. Appraising fairness in languages for distributed programming. *Distributed Computing* 2 (1988), 226–241.

[6] Soham Chakraborty, Thomas A. Henzinger, Ali Sezgin, and Viktor Vafeiadis. 2015. Aspect-oriented linearizability proofs. *Logical Methods in Computer Science* 11, 1 (2015), 1–33.

[7] Ernie Cohen and Leslie Lamport. 1998. Reduction in TLA. In *Concurrency Theory (CONCUR'98) (Lecture Notes in Computer Science)*, David Sangiorgi and Robert de Simone (Eds.), Vol. 1466. Springer-Verlag, 317–331.

[8] Byron Cook and Eric Koskinen. 2011. Making prophecies with decision predicates. In *Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'11)*, Thomas Ball and Mooly Sagiv (Eds.). ACM, 399–410.

[9] R. W. Floyd. 1967. Assigning meanings to programs. In *Proceedings of the Symposium on Applied Mathematics*, Vol. 19. American Mathematical Society, 19–32.

[10] Maurice P. Herlihy and Jeannette M. Wing. 1990. Linearizability: A correctness condition for concurrent objects. *ACM Transactions on Programming Languages and Systems* 12, 3 (Jan. 1990), 463–492.

[11] Wim H. Hesselink. 2005. Eternity variables to prove simulation of specifications. *ACM Transactions on Computational Logic* 6, 1 (2005), 175–201.

[12] C. A. R. Hoare. 1969. An axiomatic basis for computer programming. *Communications of the ACM* 12, 10 (Oct. 1969), 576–583.

[13] C. A. R. Hoare. 1972. Proof of correctness of data representations. *Acta Informatica* 1 (1972), 271–281.

[14] C. A. R. Hoare. 2019. (2019). Personal communication.

[15] Ralf Jung, Rodolphe Lepigre, Gaurav Parthasarathy, Marianna Rapoport, Amin Timany, Derek Dreyer, and Bart Jacobs. 2020. The future is ours: Prophecy variables in separation logic. *Proceedings of the ACM on Programming Languages* 4, POPL (2020), 45:1–45:32.

[16] Leslie Lamport. 1997. Processes are in the eye of the beholder. *Theoretical Computer Science* 179 (1997), 333–351.

[17] Leslie Lamport. 2003. *Specifying Systems*. Addison-Wesley, Boston. Also available at http://lamport.org.

[18] Leslie Lamport and Stephan Merz. 2017. Auxiliary Variables in TLA+. arXiv:1703.05121 (https://arxiv.org/abs/1703.05121). Also available, together with TLA⁺ specifications, at http://lamport.azurewebsites.net/tla/auxiliary/auxiliary.html.
[19] Hongjin Liang and Xinyu Feng. 2013. Modular verification of linearizability with non-fixed linearization points. In *ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'13)*, Hans-Juergen Boehm and Cormac Flanagan (Eds.). ACM, 459-470.

[20] Richard J. Lipton. 1975. Reduction: A method of proving properties of parallel programs. *Communications of the ACM* 18, 12 (Dec. 1975), 717-721.

[21] Susan Owicki and David Gries. 1976. Verifying properties of parallel programs: An axiomatic approach. *Communications of the ACM* 19, 5 (May 1976), 279-284.

[22] Susan Speer Owicki. 1975. *Axiomatic Proof Techniques for Parallel Programs*. Ph.D. Dissertation. Cornell University.

[23] Oded Padon, Jochen Hoenicke, Kenneth L. McMillan, Andreas Podelski, Mooly Sagiv, and Sharon Shoham. 2018. Temporal prophecy for proving temporal properties of infinite-state systems. In *2018 Formal Methods in Computer Aided Design (FMCAD'18)*, Nikolaj Bjørner and Arie Gurfinkel (Eds.). IEEE, 1-11.

[24] Amir Pnueli. 1977. The temporal logic of programs. In *Proceedings of the 18th Annual Symposium on the Foundations of Computer Science*. IEEE, 46-57.

[25] Shaz Qadeer, Ali Sezgin, and Serdar Tasiran. 2009. *Back and Forth: Prophecy Variables for Static Verification of Concurrent Programs*. Technical Report MSR-TR-2009-142. Microsoft.

[26] Zipeng Zhang, Xinyu Feng, Ming Fu, Zhong Shao, and Yong Li. 2012. A structural approach to prophecy variables. In *Theory and Applications of Models of Computation - 9th Annual Conference (TAMC'12), Proceedings (Lecture Notes in Computer Science)*, Manindra Agrawal, S. Barry Cooper, and Angsheng Li (Eds.), Vol. 7287. Springer, 61-71.

Received July 2020; revised June 2021; accepted October 2021