Specifying and Verifying Fault-Tolerant Systems

             Leslie Lamport_{lamport@src.dec.com} and Stephan Merz_{merz@src.dec.com}

Digital Equipment Corporation Systems Research Center

25 July 1994 minor correction: 14 October 1994

To appear in Proceedings of the Third International Symposium on Formal Techniques in Real Time and Fault Tolerant Systems, held 19–23 September 1994 in Lübeck, Germany.

Specifying and Verifying Fault-Tolerant Systems

Leslie Lamport and Stephan Merz

Digital Equipment Corporation, Systems Research Center

Abstract. We formally specify a well known solution to the Byzantine generals problem and give a rigorous, hierarchically structured proof of its correctness. We demonstrate that this is an engineering exercise, requiring no new scientific ideas.

1 Introduction

Assertional verification of concurrent systems began almost twenty years ago with the work of Ashcroft [4]. By the early 1980’s, the basic principles of formal specification and verification of concurrent systems were known [10, 12, 19]. More precisely, we had learned how to specify and verify those aspects of a system that can be expressed as the correctness of an individual execution. Faulttolerant systems are just one class of concurrent systems; they require no special techniques.

The most important problems that remain are in the realm of engineering, not science. Scientific ideas must be translated into engineering practice. We describe here what we believe to be a suitable framework for an engineering discipline of formal specification and verification.

The limited space provided by these proceedings, and the limited time and patience of the authors, have forced us to choose a simple example—the specification and hierarchical verification of a well known fault-tolerant algorithm. Our example is OM(1), the one-traitor “oral-message” solution to the Byzantine generals problem [16]. In this problem, there is a collection of generals—a commander and a set of lieutenants—who communicate with one another by message. Any of the generals, including the commander, may be a traitor. The commander must send an order to all the lieutenants so that (i) all loyal lieutenants agree on the same order o, and (ii) if the commander is loyal, then o is the order that she issued. Algorithm OM(1) satisfies these conditions if at most one of the generals is a traitor. We augment the traditional statement of the problem by requiring that all loyal generals choose their order within some fixed time after the start of the algorithm. A solution to the Byzantine generals problem lies at the heart of a fault-tolerant system in which faulty processors can exhibit completely arbitrary behavior.

This algorithm was formally specified and verified in 1983, in an appendix to a final report [20]. Even then, it was considered too straightforward an exercise to be worth writing up separately for publication. The specification and verification of fault-tolerant algorithms is not rocket science, but it is still not standard engineering practice. Most of the literature on verification concentrates on the underlying formalism and ignores the problem of defining a language for specifying real systems [11, 17, 18]. The literature on specification languages generally ignores the problem of reasoning formally about specifications of real systems [8, 9].

We address these practical issues by using existing tools: a precisely defined specification language and a hierarchical proof method. Section 2 contains the formal specifications of the problem and the algorithm. There are three specifications, a high-level problem specification, a mid-level specification of the algorithm at roughly the level of detail provided in [16], and a low-level specification that more realistically models message passing. Section 3 proves that each specification implements the next higher-level one. A correctness property of the high-level specification is also proved. Section 4 discusses the specifications and proofs.

2 The Formal Specifications

Our specifications are written in TLA^{+}, a complete specification language based on TLA, the Temporal Logic of Actions. The semantics of TLA is defined in terms of states and behaviors. A state is an assignment of values to variables, and a behavior is an infinite sequence of states. A TLA formula is interpreted as a boolean function on behaviors.

In TLA, a system is modeled by choosing variables whose values describe the system’s state, and an execution of the system is represented by a behavior. The system is specified by a TLA formula that is true of a behavior iff (if and only if) that behavior represents a correct execution of the system. A specification is a mathematical formula with precisely defined semantics. The correspondence between the real system and the mathematical formula lies in the interpretation of the formula’s variables. The free variables of the specification represent the system’s interface—the part of the system that is being specified. A description of TLA and its proof rules can be found in [13]. However, we try to explain the meaning of the TLA formulas in our specification well enough so they can be read with no prior knowledge of TLA.

Some formalisms describe systems in terms of events (often called actions) rather than states. An event in such a formalism corresponds to a change to the value of an interface variable in a TLA specification. The basic method of writing and reasoning about specifications is the same for event-based and state-based formalisms.

TLA^{+} provides a language for writing TLA specifications. In addition to the operators of TLA, it contains operators for defining and manipulating data structures and syntactic structures for handling large specifications. The first published description of TLA^{+} was in [15]. Since then, the following changes have been made to the language: (i) explicit specification of sorts is no longer required for definitions, (ii) the except construct (described below) has replaced the earlier syntax for the same operator, (iii) single square brackets have replaced double square brackets for record operators. (Record operators are not used here.) All of these changes preceded work on this particular example.

Some formulas in the specifications have been annotated with boxed numbers, such as ^{98} . A boxed number refers to the corresponding number in the margin of the text, such as the one on this line, which marks the point where the formula

98

is explained.

Our specifications provide a crash course in TLA^{+}, since they use almost all the basic syntactic features of the language and many of its predefined operators. Figures 21–23 at the end of this paper list all the syntactic constructs and predefined operators of TLA^{+}. Ones that are used in the specifications are annotated with pointers to the places in the text where they are explained.

2.1 The High-Level Specification

The high-level specification appears in Figure 1. It begins with a module named SpecParams. The module is the basic unit of a TLA^{+} specification. It is a col-

1

lection of declarations, definitions, assumptions, and theorems.

The import statement imports the contents of the modules FiniteSets and

2

Reals. This statement has almost the same effect as inserting the text of these modules into module SpecParams. The only difference is that when another module imports or includes module SpecParams, it does not obtain the definitions that SpecParams imported from modules FiniteSets and Reals.

Module FiniteSets defines IsFiniteSet(S) to equal true iff S is a finite set.

3

The module Reals defines the set Real of real numbers, with the zero element 0 and the usual operators +, ∗, <, and ≤ on real numbers. Our specification can be understood without knowing precisely how these imported operators are defined. For the reader who wants to see the formal definitions, we include module FiniteSets without further explanation in Figure 20, at the end of the paper. We omit module Reals. (Starting with the predefined module Naturals that defines the natural numbers, it takes fewer than fifty lines to define the set Real and all the operators on real numbers used in our specification.)

Returning to module SpecParams, we next encounter a parameters state-

4

ment, which declares the module’s parameters. The parameters are the free symbols of a module. All formulas defined in a module can be expressed in terms of its parameters and the built-in operators of TLA^{+}. There are two classes of module parameters, constants and variables. Constants are the rigid variables of

5

temporal logic; they represent quantities that are unchanged during a behavior. Variables are the flexible variables of temporal logic; they represent quantities that can change during the course of a behavior. The constant parameters of the specification are:

Cmdr The commander.

6

Lt The set of lieutenants. Order The set of all possible orders. Now_{0} The time at which the algorithm starts. Δ The maximum length of time it can take for the loyal generals to decide

on their values.

module SpecParams^{1}

import FiniteSets, Reals^{3}

parameters Cmdr, Lt, Order, Now_{0}, Δ^{6} : constant status, ord, now ^{7} : variable

assumption HiAssump^{11} =^{Δ} ∧ (IsFiniteSet(Lt)) ∧ (Cmdr ∉ Lt) ∧ “?” ∉ Order ∧ Now_{0} ∈ Real ∧ (Δ ∈ Real) ∧ (0 < Δ)

Gen^{13}  =^{Δ} Lt ∪ {Cmdr}

Loyal(g)^{13} =^{Δ} status[g] = “Loyal”

module HiLevel

import SpecParams, Reals, RealTime

LInit(g)^{20} =^{Δ} ∧ status[g] ∈ {“Loyal”, “Traitor”} ∧ Loyal(g) ⇒ (ord[g] = “?”)

CInit^{18}  =^{Δ} ∧ status[Cmdr] ∈ {“Loyal”, “Traitor”} ∧ Loyal(Cmdr) ⇒ (ord[Cmdr] ∈ Order)
Fail(g)^{19}  =^{Δ} status′[g] = “Traitor”

Choose(g)^{21} =^{Δ} ∧ Loyal(g) ∧ (ord[g] = “?”) ∧ ord′[g] ∈ Order ∧ ∀ h ∈ Gen : Loyal(h)′ ∧ (ord′[h] ≠ “?”) ⇒ (ord′[g] = ord′[h]) ∧ unchanged status[g]

var(g)^{18}  =^{Δ} ⟨ord[g], status[g]⟩
CSpec^{15}  =^{Δ} CInit ∧ □[Fail(Cmdr)]_{var(Cmdr)}

LSpec(g)^{20} =^{Δ} ∧ LInit(g) ∧ □[Choose(g) ∨ Fail(g)]_{var(g)} ∧ □(Loyal(g) ∧ (ord[g] = “?”) ⇒ (now ≤ Now_{0} + Δ))

Spec^{23}  =^{Δ} ∧ CSpec ∧ ∀ g ∈ Lt : LSpec(g) ∧ (now = Now_{0}) ∧ RT (⟨ord, status ⟩)

theorem

SpecGood^{25} =^{Δ} Spec ⇒ □ ∀ g ∈ Gen :

Loyal(g) ∧ (Now_{0} + Δ < now) ⇒ ∧ ord[g] ∈ Order ∧ ∀ h ∈ Gen : Loyal(h) ⇒ (ord[g] = ord[h])

Fig. 1. The high-level specification.

The variable parameters are:

status For each general g, the value of status[g] will be the string “Loyal” or

7

“Traitor”, denoting whether or not the general is loyal. (Strings, denoted by expressions of the form “ … ”, are a predefined data type of TLA^{+}.) The Byzantine generals problem is expressed in terms of which generals are loyal. In the formal specification, the state must describe which generals are loyal. Hence, we introduce the variable status.

ord For each general g, the value of ord[g] denotes the order chosen by general

g, or the string “?” if g has not yet chosen an order. now The variable now will be a real number that denotes the current time.

In our informal discussion, we describe the values that variables will have in a behavior that satisfies the specification. TLA is a typeless logic, which means that a variable can assume any value. (More precisely, for any value v and variable x, there is a state in which the value of x is v.) Thus, when we say that the value of status[g] will be a string, we mean that its value will be a string in every state of every behavior that satisfies the specification we are about to describe.

The lines are primarily decorative, though the second one serves

8

to delimit the assumption section.

An assumption section asserts assumptions about constant parameters. In

9

this module, there is a single assumption named HiAssump, which is defined to be the expression to the right of the =^{Δ} . In general, the symbol =^{Δ} denotes

10

that the identifier to its left is defined to equal the expression to its right. The formula HiAssump is the conjunction of four assertions:

11

1. Lt (the set of lieutenants) is a finite set that does not contain Cmdr.

2. “?” is not a possible order.

3. Now_{0} is a real number.

4. Δ is a positive real number.

TLA^{+} uses the notation that a list of expressions bulleted by ∧ denotes their

12

conjunction, and a list of expressions bulleted by ∨ denotes their disjunction. Indentation is used to eliminate parentheses.

Following the assumption section is a section consisting of two definitions. The constant operator Gen is defined to be the set of all generals—both the

13

lieutenants and the commander. The boolean operator Loyal is defined so that Loyal(x) equals true iff status[x] equals “Loyal”, for any x. (We care about the value of Loyal(x) only when x is an element of Gen.) Round parentheses denote application of an operator to its argument (or arguments). The symbol Loyal by itself, without an argument, is not a syntactically complete expression. Square brackets denote function application. Both status and status[e] are syntactically complete expressions that denote values, for any expression e.

The line ends the module.

14

The actual specification is contained in module HiLevel, which comes next. This module imports the modules SpecParams, Reals, and RealTime.

The RealTime module is used to express real-time properties. It is essentially the same module as in [15], which in turn used the definitions from [2].^{1} Specifying real-time properties is an engineering problem that is solved by applying standard methods. We will explain the operators in the RealTime module as they appear in our specification. The module is given in Figure 20.

Importing SpecParams provides module HiLevel with the specification parameters and the definitions of Gen and Loyal. Importing SpecParams does not import the modules FiniteSets and Reals that it in turn imports.

Instead of reading module HiLevel in sequence, we examine next the temporal formula CSpec, which specifies the commander. This formula has the canonical

15

form Init ∧ □[Next]_{v} for a process specification^{2}, where

Init is a predicate—a Boolean expression made from constants and variables. It

describes the initial state of the process’s variables. Next is an action—a boolean expression made from constants, variables, and

primed variables. It describes all steps (pairs of successive states) that can change the process’s variables. In an action, unprimed variables denote values in the first (starting) state and primed variables denote values in the second (final) state.

v is a state function—a nonboolean expression made from constants and variables. It is usually a tuple that describes all components of the process’s state.

The formula [Next]_{v} denotes Next ∨ (v′ = v), so it represents a step that is

16

either a Next step or one that leaves v (and hence all variables in the tuple v) unchanged. The temporal operator □ means always, so Init ∧ □[Next]_{v} is true

17

for a behavior (infinite sequence of states) iff the first state satisfies Init and every successive pair of states is either a Next step or leaves v unchanged.

The commander’s state is described by ord[Cmdr] and status[Cmdr], which are the components of the tuple var(Cmdr). (In TLA^{+}, tuples are enclosed in

18

angle brackets ⟨…⟩.) The initial condition CInit asserts that

1. The commander’s status is either “Loyal” or “Traitor”.

2. If her status is “Loyal”, then her order is an element of Order. The symbol ⇒ denotes logical implication. It has lower precedence (binds more loosely) than any other boolean operator.

The commander’s next-state relation is Fail(Cmdr), which asserts that the new

19

value of status[Cmdr] is “Traitor”. This allows any step that ends in a state with status[Cmdr] equal to “Traitor”. Such a step can change ord[Cmdr] to any value. Thus, the formula CSpec is satisfied by any behavior that either (i) consists of an infinite number of states with status[Cmdr] = “Loyal” and ord[g] = o, for some o in Order, or (ii) starts with a finite (possibly empty) sequence of such

1 The definition of VTimer in the RealTime module of [15] contains a typographical

error; the correct definition appears in [2] and Figure 20. 2 Since real-time conditions are used to specify progress, there are no fairness condi-

tions in our processes.

states and ends with an infinite sequence of states in which status[Cmdr] equals “Traitor” and ord[Cmdr] assumes completely arbitrary values.

The formula CSpec describes only the values assumed by ord[Cmdr] and status[Cmdr]. It makes no assertion about any other part of the state—such as the value of the variable now, or of ord[g] for g different from Cmdr, or of a variable foo that might be introduced later.

The formula LSpec(g) is the specification of lieutenant g. It is the conjunction

20

of two formulas. The first asserts that LInit(g) holds initially and that each step is a Choose(g) step, a Fail(g) step, or a step that leaves lieutenant g’s state unchanged. The initial predicate LInit(g) asserts that (i) status[g] has a correct value, and (ii) if g is loyal, then ord[g] equals “?”, denoting that g has not yet chosen an order. A Choose(g) step is one in which

21

1. In the starting a state, g is loyal and has not yet chosen an order. (Any step taken by a traitorous general can be interpreted as a Fail step.)

2. In the final state, g has chosen an order.

3. For every general h that, in the final state, is loyal and has chosen an order, the order that h has chosen is the same as the one that g has chosen.

4. g’s status does not change, which by (1) implies that he is still loyal in the final state. The formula unchanged f is an abbreviation for f′ = f .

22

The second conjunct of LSpec(g) is of the form □P, for a predicate P. Such a formula asserts of a behavior that P is true in every state. In this case, the formula asserts that if g is loyal and has not chosen an order, then now is at most Now_{0} + Δ. In other words, it asserts that if now is greater than Now_{0} + Δ and g is loyal, then he must have chosen an order. Since we interpret now as the current time, the second conjunct of LSpec(g) asserts that if g is loyal, then he must choose an order by time Now_{0} + Δ.

The formula Spec is the complete high-level specification. It asserts

23

1. The commander’s specification CSpec.

2. The specification LSpec(g), for each lieutenant g.

3. now = Now_{0}, which means that the current time initially (at the start of the algorithm) equals Now_{0}.

4. Formula RT (⟨ord, status ⟩). Module RealTime defines formula RT (v) to as-

24

sert that (a) now is a monotonically nondecreasing real number and (b) steps that change now leave v unchanged. Thus, RT (⟨ord, status ⟩) asserts that (a) now changes the way we expect time to change, and (b) ord and status do not change when now does. Thus, in steps that change ord and status, the value of now is the same in the initial and final state. Intuitively, this means that we are considering changes to ord and status to happen instantaneously.

Formula Spec is the high-level specification. This means that we consider a behavior to represent a correct execution of the algorithm iff it satisfies Spec. A specification is therefore a definition, and a definition cannot be right or wrong. However, a specifications can fail to capture our intent. To gain confidence in a specification, we can prove theorems about it. Such theorems usually have the form Spec ⇒ Prop, which asserts that every behavior satisfying the specification Spec also satisfies the property Prop. Module HiLevel asserts such a theorem, named SpecGood. This theorem states that, in any behavior satisfying Spec, it

25

is always the case that, for any general g, if g is loyal and the time is later than Now_{0} + Δ, then g has chosen an order and his order is the same as that of every other loyal general. In other words, every loyal general chooses an order by time Now_{0} + Δ, and that order is the same as any other loyal general’s order. All theorems are proved in Section 3.

2.2 The Mid-Level Specification

The mid-level specification describes Algorithm OM(1) of [16], an “oral-message” Byzantine agreement algorithm that works in the presence of at most one traitor. It is a two-round algorithm. In the first round, the commander sends her message to all lieutenants. In the second round, each lieutenant relays the message he received to all other lieutenants. A lieutenant chooses his order by applying a majority function to the values that he has received. The only requirements on this majority function are (i) if the same order o is received from all but one of the other generals, then o is chosen, and (ii) all lieutenants use the same majority function.

This informal description is essentially the one given in [16]. It contains several tacit assumptions—for example, that every lieutenant receives a value in the first round, even if the commander is a traitor. The formal specification makes these assumptions explicit.

Module MidLevelParams of Figure 2 declares the following new parameters

26

that are used in the mid-level specification.

rcvd For each lieutenant g, the order that g receives directly from the commander is recorded in rcvd[g][g], and the relayed order that g receives from each other lieutenant h is recorded in rcvd[g][h]. Thus, for each lieutenant g, the value of rcvd[g] will be a function whose domain is the set Lt of lieutenants. If lieutenant g is loyal, then before any orders have been sent, rcvd[g][h] will equal “?”, for all lieutenants h.

Majority The majority function. More precisely, Majority is an operator with a single argument. We care about the value of Majority(f ) only when f is a function from Lt to the set Order of orders.

δ The maximum delay between when an order is sent and when it is received. This delay applies both to the sending of orders by the commander and to the relaying of orders by the lieutenants. (The delay δ includes the time needed to decide to send an order.)

ϵ The maximum time it takes a lieutenant to make a decision. In this specification, the only decision he has to make is to choose an order once he has received all the relayed orders.

Assumption MidAssump makes the following assertion about the constant pa-

27

rameters.

module MidLevelParams

import SpecParams, Reals export^{29} MidLevelParams, SpecParams, Reals parameters rcvd^{26} : variable

Majority( ), δ, ϵ^{26} : constant

assumption MidAssump^{27} =^{Δ} ∧ (δ ∈ Real) ∧ (ϵ ∈ Real) ∧ (2 ∗ δ + ϵ ≤ Δ) ∧ ∀ f ∈ [Lt → Order]^{28} : ∧ Majority(f ) ∈ Order ∧ ∀ o ∈ Order : (∃ h ∈ Lt : ∀ g ∈ Lt \ {h} : f [g] = o) ⇒ (Majority(f ) = o)

Fig. 2. Module MidLevelParams.

1. δ and ϵ are real numbers such that 2 ∗ δ + ϵ is at most Δ.

2. For any function f that maps lieutenants to orders: 1. Majority(f ) is an order.

2. If o is an order such that f [g] equals o for every lieutenant except some lieutenant h, then Majority(f ) equals o.

The expression [Lt → Order] denotes the set of all functions f with domain

28

Lt such that f [g] ∈ Order, for all g ∈ Lt.

The export statement causes the named definitions to be imported by any mod-

29

ule that imports MidLevelParams. A module name stands for all definitions from that module. (Omitting the export statement would be equivalent to writing export MidLevelParams.)

Module MidLevel in Figure 3 defines the formula Spec to be the mid-level specification. It first imports two other modules. Importing MidLevelParams imports all its parameters, including the ones it imported from SpecParams.

The include statement incorporates the definitions from module HiLevel,

30

with all defined symbols prefixed by “Hi.”; for example, a definition of Hi.var is included that makes Hi.var(h) equal to ⟨ord[h], status[h]⟩. Parameters of an included module are instantiated by expressions. In the absence of explicit instantiation (described below), a parameter is instantiated by the symbol of the same name. Thus, the parameter Cmdr of HiLevel is instantiated by Cmdr (a parameter of MidLevel, obtained via the import statement); the parameter ord of HiLevel is instantiated by ord; etc. When a module is included, its assumptions (with the appropriate instantiations) must be provable from the assumptions and definitions of the including module. Thus, assumption Hi.HiAssump, the assumption of the included module HiLevel, must be provable from the assumptions and definitions of module MidLevel. This assumption follows trivially from assumption HiLevel, which is imported from module MidLevelParams, which in turn imports it from module SpecParams.

module MidLevel

import MidLevelParams, RealTime include HiLevel as Hi^{30} LInit(g)^{32} =^{Δ} ∧ Hi.LInit(g) ∧ Loyal(g) ⇒ (rcvd[g] = [h ∈ Lt ↦ “?”]) Issue(g)^{34} =^{Δ} ∧ Loyal(g) ∧ rcvd[g][g] = “?” ∧ ∃ o ∈ Order : ∧ rcvd′[g] = [rcvd[g] except ![g] = o] ∧ Loyal(Cmdr) ⇒ (o = ord[Cmdr]) ∧ unchanged ⟨ord[g], status[g]⟩ Relay(g, h)^{35} =^{Δ} ∧ Loyal(g) ∧ rcvd[g][h] = “?” ∧ ∃ o ∈ Order : ∧ rcvd′[g] = [rcvd[g] except ![h] = o] ∧ Loyal(h) ⇒ (o = rcvd[h][h]) ∧ unchanged ⟨ord[g], status[g]⟩ Choose(g) =^{Δ} ∧ Loyal(g) ∧ ord[g] = “?” ∧ ∀ h ∈ Lt : rcvd[g][h] ≠ “?” ∧ ord′[g] = Majority(rcvd[g]) ∧ unchanged ⟨rcvd[g], status[g]⟩ Next(g)^{33} =^{Δ} Issue(g) ∨ (∃ h ∈ Lt \ {g} : Relay(g, h)) ∨ Choose(g) ∨ Hi.Fail(g)^{36} var(g) =^{Δ} ⟨ord[g], rcvd[g], status[g]⟩ LSpec(g) =^{Δ} ∧ LInit(g) ∧ □[Next(g)]var(g)^{32} ∧ □(Loyal(g) ∧ (rcvd[g][g] = “?”) ⇒ (now ≤ Now_{0} + δ))^{37} ∧ ∀ h ∈ Lt \ {g} : □(Loyal(g) ∧ (rcvd[g][h] = “?”) ⇒ (now ≤ Now_{0} + 2 ∗ δ))^{37} ∧ ∃ ∃ ∃ ∃ ∃ ∃ t : ∧ VTimer(t, Choose(g), ϵ, var(g)) ∧ MaxTimer(t)^{38}

Spec^{31} =^{Δ} ∧ Hi.CSpec ∧ ∀ g ∈ Lt : LSpec(g) ∧ now = Now_{0} ∧ RT (⟨ord, rcvd, status ⟩) OneTraitor ^{40} =^{Δ} ∃ h ∈ Gen : ∀ g ∈ Gen \ {h} : Loyal(g) theorem

MidCorrect^{40} =^{Δ} (□OneTraitor) ∧ Spec ⇒ Hi.Spec Fig. 3. Module MidLevel

11

Formula Spec is the specification of the mid-level algorithm. It is similar to

31

the specification Spec of module HiLevel, consisting of the conjunction of four formulas that assert: (i) the specification Hi.CSpec of the commander included from module HiLevel, (ii) formula LSpec(g), for every lieutenant g, (iii) now is initially equal to Now_{0}, and (iv) formula RT (⟨ord, rcvd, status ⟩). As explained in Section 2.1, RT (⟨ord, rcvd, status ⟩) asserts that now behaves the way we expect it to and that ord, rcvd, and status change instantaneously. The rest of the specification involves the definition of LSpec(g), the specification of lieutenant g. Formula LSpec(g) is the conjunction of four formulas, which we describe in turn.

The first conjunct of LSpec(g) has the canonical form Init ∧ □[Next]_{v} ex-

32

plained in Section 2.1. The initial predicate LInit(g) asserts (i) the initial condition Hi.LInit(g) on status[g] and ord[g] and (ii) that rcvd[g] is a function with domain Lt such that rcvd[g][h] equals “?” for every h in Lt. In general, the construct [x ∈ S ↦ exp(x)] denotes the function f with domain S such that f [x] = exp(x) for all x in S. The next-state relation Next(g) is the disjunction

33

of four actions:

Issue(g) Represents the sending of an order by the commander to lieutenant g.

34

It is enabled iff g is loyal and rcvd[g][g] equals “?”, denoting that g has not yet received an order from the commander. The action sets rcvd[g][g] to an order that, if the commander is loyal, is actually her order. The notation [f except ![x] = exp] denotes a function f̂ that is the same as f except that f̂[x] equals exp.

∃ h ∈ Lt\{g} : Relay(g, h) Asserts that a Relay(g, h) step occurs, for some lieu-

35

tenant h other than g. Such a step represents the relaying of an order from h to g. If h is loyal, then the relayed order is rcvd[h][h].

Hi.Fail(g) As described above, an action taken when g is or becomes a traitor.

36

It allows arbitrary changes to ord[g] and rcvd[g] (and all variables other than status[g]).

Choose(g) The action in which g chooses his order by applying Majority to his array rcvd[g] of relayed values.

The final three conjuncts of LSpec(g) place timing bounds on when g’s actions must occur. The second conjunct asserts that (it is always true that) if g is loyal

37

and rcvd[g][g] equals “?”, then now is at most Now_{0} + δ. If g is loyal, rcvd[g][g] equals “?” iff an Issue(g) step has not occurred. Thus, this conjunct asserts that, if g is loyal, then an Issue(g) step must occur by time Now_{0} + δ. Similarly, the third conjunct asserts that, if g is loyal, then a Relay(g, h) step must occur by time Now_{0} + 2 ∗ δ.

The final conjunct of LSpec(g) places a timing bound on the Choose(g) action, using the temporal formulas VTimer and MaxTimer, defined in module

38

RealTime. These formulas were introduced in [2] and used again in [15] as a general method for specifying real-time bounds. If A is an action and v a state function such that any A step changes v, and if t is a variable that does not occur in A or v, then the formula VTimer(t, A, ϵ, v) ∧ MaxTimer(t) asserts that A cannot be enabled for more than ϵ time units before the next A step occurs.

12

The temporal existential quantifier ∃ ∃ ∃ ∃ ∃ ∃ t essentially hides the variable t. Thus, the

39

fourth conjunct of LSpec(g) asserts that, if lieutenant g is loyal, then a Choose(g) step must occur within ϵ time units of when he has received an order from the commander and from all other lieutenants.

Finally, the module asserts the correctness of the mid-level algorithm. The

40

predicate OneTraitor asserts of a state that there is at most one traitorous general. Theorem MidCorrect asserts that, for any behavior, if (i) there is always at most one traitorous general and (ii) formula Spec holds, then formula Hi.Spec holds. In other words, this theorem asserts that, in the presence of at most one traitor, the mid-level specification implements the high-level specification.

2.3 The Low-Level Specification

In the mid-level specification, a value is transferred from the commander to a lieutenant in a single step, and is relayed from one lieutenant to another in a single step. In the low-level specification, we model the way values are transmitted over communication channels. This requires adding timeouts to detect if a traitorous general fails to send a message.

The specification uses module TimedChannel of Figure 4, which provides

41

generic definitions for describing the transmission of values over a channel. This module imports module Sequences to define operators on sequences. In TLA^{+}, an n-tuple ⟨v_{1}, …, v_{n} ⟩ is a function whose domain is the set {1, …, n} of nat-

42

ural numbers, where ⟨v_{1}, …, v_{n} ⟩[i] equals v_{i}, for 1 ≤ i ≤ n. The Sequences module represents sequences as tuples. The module is given without explanation in Figure 20. It defines the usual operators Head, Tail, and ∘ (concatenation) on sequences.

Module TimedChannel has two variable parameters:

43

src The interface at the sender’s end of the channel. It will be a pair whose first element is a sequence of values and whose second element is either 0 or 1.

dest The interface at the receiver’s end of the channel. It will be a pair whose first element is a sequence of values and whose second element is either 0 or 1.

(The purpose of the second components of src and dest is explained below.) The module has a single constant parameter τ, which is a real number that represents the maximum time required to transmit one value.

The sending of a value v is initiated by a Send(v) step, which appends v

44

to the tail of src[1] and complements src[2]—changing its value from 0 to 1 or vice-versa. Receipt of the value v occurs with a Rcv(v) step, which is enabled iff v is the head of the sequence dest[1]. A Rcv(v) step removes v from the head of dest[1] and complements dest[2].

The transmission of a value from one end of the channel to the other is

45

modeled by a Tmt step, which moves an element from the head of src[1] to the tail of dest[1].

module TimedChannel^{41}

import Sequences, Reals, RealTime parameters src, dest^{43} : variable

τ ^{47} : constant

assumption Assump =^{Δ} (τ ∈ Real) ∧ (0 < τ)

Send(v)^{44} =^{Δ} src′ = ⟨src[1] ∘ ⟨v ⟩, 1 − src[2]⟩ Rcv(v)^{44} =^{Δ} ∧ (dest[1] ≠ ⟨ ⟩) ∧ (v = Head(dest[1])) ∧ dest′ = ⟨Tail(dest[1]), 1 − dest[2]⟩

Tmt^{45}  =^{Δ} ∧ src[1] ≠ ⟨ ⟩ ∧ src′ = ⟨Tail(src[1]), src[2]⟩ ∧ dest′ = ⟨dest[1] ∘ ⟨Head(src[1])⟩, dest[2]⟩

ext^{48}  =^{Δ} ⟨src[2], dest[2]⟩

Spec^{46} =^{Δ} ∧ (src = ⟨⟨ ⟩, 0⟩) ∧ □[Tmt ∨ ∃ v : Send(v)]_{src} ∧ (dest = ⟨⟨ ⟩, 0⟩) ∧ □[Tmt ∨ ∃ v : Rcv(v)]_{dest} ∧ ∃ ∃ ∃ ∃ ∃ ∃ t : VTimer(t, Tmt, τ, ⟨src, dest ⟩) ∧ MaxTimer(t)^{47}

Fig. 4. Module TimedChannel.

Formula Spec is the specification of the timed channel. A behavior satisfies

46

this formula iff the variables src and dest behave the way they should for a timed channel. The formula has three conjuncts. The first describes the sequence of values assumed by src. Initially, src[1] is the empty sequence and src[2] equals 0; every step that changes src is a Tmt step or a Send(v) step, for some v. The second conjunct similarly describes the sequence of values assumed by dest. The third conjunct asserts the real-time requirement. As explained in Section 2.2, the conjunct asserts that Tmt cannot remain enabled for more than τ time units

47

before the next Tmt step occurs. Thus, this conjunct asserts that, when src[1] is nonempty, values are moved from it to dest[1] at the rate of at least one every τ time units.

We now come to ext, the pair consisting of the second components of src and

48

dest, and the explanation of what those second components are for. The channel specification Spec allows arbitrary values to be sent “spontaneously”, and it allows those values to be received at arbitrary times. This specification is used by conjoining it with specifications of a sender and receiver that constrain when Send and Rcv actions occur. The sender’s specification will describe when Send actions can occur and what values they can send; the receiver’s specification will describe when Rcv actions can occur. The sender’s and receiver’s specifications must also allow the channel’s internal Tmt steps. They allow such steps by allowing any step that leave ext unchanged; Spec implies that any such step must be a Tmt step.

Module LowLevelParams in Figure 5 begins the specification of the low-level

module LowLevelParams

import SpecParams, MidLevelParams, Reals export SpecParams, MidLevelParams, Reals, LowLevelParams, Hi, Mid, TC^{52} parameters in, out, sent^{49} : variable

τ ^{50} : constant

assumption LowAssump =^{Δ} (τ ∈ Real) ∧ (0 < τ) ∧ (τ + 3 ∗ ϵ ≤ δ)

include HiLevel as Hi include MidLevel as Mid include TimedChannel as TC (g, h) with src ← out[g][h], dest ← in[h][g]^{51}

AllBut(func, g)^{53} =^{Δ} [h ∈ Lt \ {g} ↦ func[h]]

NotSent(g, h)  =^{Δ} sent[g][h] = “No”
ext(g)^{54}  =^{Δ} [h ∈ Lt ↦ TC (g, h).ext]

Fig. 5. Module LowLevelParams.

algorithm itself. The module imports the two higher-level … Params modules and declares three new variable parameters:

in The state function in[h][g] represents the receiver’s end (dest) of the chan-

49

nel from g to h. out The state function out[g][h] represents the sender’s end (src) of the channel

from g to h. sent The value of sent[g][h], which will be either “Yes” or “No”, records whether

or not general g has sent a value to lieutenant h. For each general g, sent[g] will be a function with domain Lt.

The constant parameter τ has the same meaning as in module TimedChannel.

50

The module next asserts assumption LowAssump, which relates τ to δ and ϵ. The module also asserts assumptions HiAssump and MidAssump, which are imported with modules SpecParams and MidLevelParams, respectively.

Module LowLevelParams then includes modules HiLevel and MidLevel, and includes a parameterized copy of module TimedChannel. The latter include

51

statement incorporates all the definitions from module TimedChannel prefixed with “TC (g, h).”, and with the indicated instantiations of the parameters src and dest. For example, it includes the definition

TC (g, h).Tmt =^{Δ} ∧ out[g][h][1] ≠ ⟨ ⟩ ∧ out[g][h]′ = ⟨Tail(out[g][h][1]), out[g][h][2]⟩ ∧ in[h][g]′ = ⟨in[h][g][1] ∘ ⟨Head(out[g][h][1])⟩, in[h][g][2]⟩

The export statement exports all these included definitions, as well as the ones

52

from the imported modules and the definitions made in the LowLevelParams module itself.

Finally, the module makes three definitions. If func is a function with domain

53

Lt, then AllBut(func, g) is the restriction of func to the domain Lt \ {g}, the set of all lieutenants other than g. The state function ext(g) is the array of ext

54

tuples for each channel interface at lieutenant g. Thus, a step that leaves ext(g) unchanged allows Tmt steps for all the channels to and from g, but allows no Send or Rcv actions on those channels.

The definitions of the predicates and actions used in the final specification appear in module LowLevelActions of Figure 6. (Normally, one would combine this module with module LowLevel; we have split the specification to keep each module less than one page long.)

The section following the import statement specifies the initial predicate

55

CInit and next-state action CNext of the commander. (The heading is a comment, distinguished by its upright font.) The commander can either do a Hi.Fail step (any step that ends with status[Cmdr] = “Traitor”) or send her order to some lieutenant g with a CSend(g) step. A CSend(g) step is enabled iff the commander is loyal and has not yet sent her order to g; it sends the order and changes sent[g] to indicate that the order was sent.

The next section defines the initial condition and the normal actions for a

56

lieutenant. The Issue and Relay actions represent the receipt of an order from the commander or another lieutenant, respectively. The Send action is the one in which a lieutenant sends an order on a channel.

The following section gives the definitions of a lieutenant’s two timeout ac-

57

tions. An IssueTimeout(g) step can occur if lieutenant g has not received an order from the commander by time Now_{0} + τ + 2 ∗ ϵ. A RelayTimeout(g, h) step can occur if g has not received a relayed order from lieutenant h by time Now_{0} + 2 ∗ τ + 5 ∗ ϵ. These timeouts are needed to ensure progress if a traitorous general fails to send an order.

Action LNext(g) is the next-state action of lieutenant g.

58

Finally, module LowLevel in Figure 7 imports the preceding two modules and defines the complete low-level specification Spec.

The state functions cvar and lvar(g) are the tuples of variables of the com-

59

mander and lieutenant g, respectively.

The formula EMax(g, A) asserts that action A cannot be enabled for more

60

than ϵ time units before the next A step occurs (assuming that an A step changes lvar(g)).

Formula CSpec is the commander’s specification. The second conjunct asserts

61

that, for every lieutenant g, a CSend(g) step must occur within ϵ seconds of when it becomes enabled. If the commander is loyal, then action CSend(g) is enabled initially and remains enabled until she sends g her order. Thus, the second conjunct asserts that a loyal commander must send her order to every lieutenant within ϵ time units of the start of the algorithm.

Formula LSpec(g) is the specification of lieutenant g. The last four conjuncts

62

express the requirements that, if loyal, he must execute each of his actions within

module LowLevelActions

import LowLevelParams, RealTime

CInit =^{Δ} ∧ Hi.CInit ∧ Loyal(Cmdr) ⇒ (sent[Cmdr] = [h ∈ Lt ↦ “No”])The commander.^{55}

CSend(g) =^{Δ} ∧ Loyal(Cmdr) ∧ NotSent(Cmdr, g) ∧ TC (Cmdr, g).Send(ord[Cmdr]) ∧ sent′[Cmdr] = [sent[Cmdr] except ![g] = “Yes”] ∧ unchanged ⟨\begin{matrix}in[Cmdr], AllBut(out[Cmdr], g), ord[Cmdr], \\ status[Cmdr]⟩ \end{matrix} CNext =^{Δ} Hi.Fail(Cmdr) ∨ ∃ g ∈ Lt : CSend(g)

LInit(g) =^{Δ} ∧ Mid.LInit(g) ∧ Loyal(g) ⇒ (sent[g] = [h ∈ Lt ↦ “No”])  Lieutenant g.^{56}

Issue(g) =^{Δ} ∧ Loyal(g) ∧ (rcvd[g][g] = “?”) ∧ ∃ o ∈ Order : ∧ TC (Cmdr, g).Rcv(o) ∧ rcvd′[g] = [rcvd[g] except ![g] = o] ∧ unchanged ⟨ord[g], AllBut(in[g], Cmdr), out[g], status[g], sent[g]⟩ Send(g, h) =^{Δ} ∧ Loyal(g) ∧ (rcvd[g][g] ≠ “?”) ∧ NotSent(g, h) ∧ TC (g, h).Send(rcvd[g][g]) ∧ sent′[g] = [sent[g] except ![h] = “Yes”] ∧ unchanged ⟨ord[g], rcvd[g], in[g], AllBut(out[g], h), status[g]⟩ Relay(g, h) =^{Δ} ∧ Loyal(g) ∧ (rcvd[g][h] = “?”) ∧ ∃ o ∈ Order : ∧ TC (h, g).Rcv(o) ∧ rcvd′[g] = [rcvd[g] except ![h] = o] ∧ unchanged ⟨ord[g], AllBut(in[g], h), out[g], status[g], sent[g]⟩ Choose(g) =^{Δ} Mid.Choose(g) ∧ unchanged ⟨in[g], out[g]⟩

IssueTimeout(g) =^{Δ} ∧ Loyal(g) ∧ (rcvd[g][g] = “?”) ∧ Now_{0} + τ + 2 ∗ ϵ < now ∧ ∃ o ∈ Order : rcvd′[g] = [rcvd[g] except ![g] = o] ∧ unchanged ⟨ord[g], in[g], out[g], status[g], sent[g]⟩ Timeout actions.^{57}

RelayTimeout(g, h) =^{Δ} ∧ Loyal(g) ∧ (rcvd[g][h] = “?”) ∧ Now_{0} + 2 ∗ τ + 5 ∗ ϵ < now ∧ ∃ o ∈ Order : rcvd′[g] = [rcvd[g] except ![h] = o] ∧ unchanged ⟨ord[g], in[g], out[g], status[g]⟩ LNext(g)^{58} =^{Δ} ∨ Issue(g) ∨ Choose(g) ∨ IssueTimeout(g) ∨ ∃ h ∈ Lt \ {g} : Send(g, h) ∨ Relay(g, h) ∨ RelayTimeout(g, h) ∨ Hi.Fail(g)

Fig. 6. Module LowLevelActions.

module LowLevel

import LowLevelParams, LowLevelActions

cvar =^{Δ} ⟨ord[Cmdr], ext(Cmdr), status[Cmdr], sent[Cmdr]⟩  State functions.^{59}

lvar(g) =^{Δ} ⟨ord[g], rcvd[g], ext(g), status[g], sent[g]⟩

EMax(g, A)^{60} =^{Δ} ∃ ∃ ∃ ∃ ∃ ∃ t : VTimer(t, A, ϵ, lvar(g)) ∧ MaxTimer(t) Temporal formulas.

CSpec^{61} =^{Δ} ∧ CInit ∧ □[CNext]_{cvar} ∧ ∀ g ∈ Lt : EMax(Cmdr, CSend(g)) LSpec(g)^{62} =^{Δ} ∧ LInit(g) ∧ □[LNext(g)]_{lvar(g)} ∧ EMax(g, Issue(g)) ∧ EMax(g, IssueTimeout(g)) ∧ EMax(g, Choose(g)) ∧ ∀ h ∈ Lt \ {g} : ∧ EMax(g, Send(g, h)) ∧ EMax(g, Relay(g, h)) ∧ EMax(g, RelayTimeout(g, h)) Spec^{63} =^{Δ} ∧ CSpec ∧ ∀ g ∈ Lt : LSpec(g) ∧ ∀ g, h ∈ Gen : TC (g, h).Spec ∧ now = Now_{0} ∧ RT (⟨ord, rcvd, in, out, status, sent ⟩) theorem LowCorrect =^{Δ} Spec ⇒ Mid.Spec

Fig. 7. Module LowLevel.

ϵ time units of when he can.

Finally, the complete specification Spec has five conjuncts: (i) the specifica-

63

tion of the commander, (ii) the specifications of the lieutenants, (iii) the specifications of all the communication channels, (iv) the specification of the starting time, and (v) the usual RT formula.

3 The Proofs

We now describe how the theorems asserted in the specifications above are proved. The key to moving proofs from the realm of mathematics into engineering practice is hierarchical structuring. We use the method of structuring proofs introduced in [14]. The conventions used in this method are described as they appear.

A hierarchically structured proof is a sequence of steps, each with a proof. The proof of a step is either a short paragraph or calculation, or else a hierarchically structured proof. The idea is to make the unstructured “leaf” proofs sufficiently easy to check that they are highly unlikely to be wrong. We indicate how proofs of our theorems are carried down to the level at which each leaf proof consists of simple expansion of definitions and propositional logic. Such simple proofs are easy to check mechanically; most steps in our proofs can be checked with the TLP verification system [7].

3.1 Proof of Theorem SpecGood

Figure 8 is the high-level proof of theorem SpecGood, consisting of the level-one steps and the proof of the final step. The Let construct introduces definitions local to the proof. We use a hierarchical numbering convention for denoting parts of formulas, adding numbers to bulleted lists of conjuncts and disjuncts. Thus, Inv(g, h).3 is the formula Loyal(g) ∧ (ord[g] … Δ). We extend this convention to quantified formulas, so if F is the formula ∃ x : P(x), then F (y) denotes the formula P(y). We use this convention for formulas defined in the specifications even when the conjuncts and disjuncts are not explicitly numbered. Thus, with the definition if Issue from module MidLevel (Figure 3), Issue(h).2(p).1 denotes the formula rcvd′[h] = [rcvd[h] except ![h] = p].

Theorem SpecGood is of the form Spec ⇒ □P, for a state predicate P. If Spec were of the canonical form Init∧□[N ]_{v}, then this would be a completely standard proof using the method first described by Ashcroft [4]: find a state predicate I (the invariant) such that (i) Init implies I , (ii) I implies P, and (iii) I ∧ [N ]_{v} implies I′. (This TLA formulation of the proof method is more transparent than its original description as a method for reasoning about programs.) Since Spec is written as the conjunction of formulas in canonical form, along with formulas of the form □Q, our proof involves a simple generalization of Ashcroft’s method.

The Q.E.D. in step ⟨1⟩5 stands for the goal to be proved—in this case, the theorem itself. In the proof, curly braces enclose the justification of the implication or equivalence. Each step in this chain of implications and equivalence follows from simple substitution and application of standard rules.

Let: Good(g) =^{Δ} Loyal(g) ∧ (Now_{0} + Δ < now) ⇒ ∧ ord[g] ∈ Order ∧ ∀ h ∈ Gen : Loyal(h) ⇒ (ord[g] = ord[h])

Theorem Spec ⇒ □(∀ g ∈ Gen : Good(g))

Let: Inv(g, h) =^{Δ} 1.∧ Loyal(g) ⇒ ord[g] ∈ Order ∪ {“?”} 2.∧ Loyal(g) ∧ Loyal(h) ∧ (ord[g] ≠ “?”) ∧ (ord[h] ≠ “?”) ⇒ (ord[g] = ord[h]) 3.∧ Loyal(g) ∧ (ord[g] = “?”) ⇒ (now ≤ Now_{0} + Δ)

CInv =^{Δ} Loyal(Cmdr) ⇒ (ord[Cmdr] ∈ Order) ⟨1⟩1. Assume: g, h ∈ Lt

Prove: LSpec(g) ∧ LSpec(h) ⇒ □Inv(g, h) ⟨1⟩2. Assume: g ∈ Lt

Prove: LSpec(g) ∧ CSpec ⇒ □Inv(g, Cmdr) ⟨1⟩3. CSpec ⇒ □CInv ⟨1⟩4. CInv ∧ (∀ g ∈ Lt : ∀ h ∈ Gen : Inv(g, h)) ⇒ (∀ g ∈ Gen : Good(g)) ⟨1⟩5. Q.E.D.

Proof: Spec ⇒ {By the definition of Spec.} CSpec ∧ (∀ g, h ∈ Lt : LSpec(g) ∧ LSpec(h)) ⇒ {By ⟨1⟩1, ⟨1⟩2, and ⟨1⟩3.} □CInv ∧ (∀ g, h ∈ Lt : □Inv(g, h) ∧ □Inv(g, Cmdr)) ≡ {By the temporal logic rule that □ distributes over conjunction.} □(CInv ∧ (∀ g, h ∈ Lt : Inv(g, h) ∧ Inv(g, Cmdr)) ⇒ {⟨1⟩4, the definition of Gen, and the temporal logic rule (P ⇒ Q) ⊢ (□P ⇒ □Q).} □(∀ g ∈ Gen : Good(g))

Fig. 8. The high-level structure of the proof of theorem SpecGood

To finish the proof, we must now prove statements ⟨1⟩1–⟨1⟩4. The proof of ⟨1⟩4 involves simple predicate logic and will not be discussed. The proofs of ⟨1⟩1, ⟨1⟩2, and ⟨1⟩3 are similar; we consider only ⟨1⟩1.

The first-level proof of ⟨1⟩1 appears in Figure 9. The rule that underlies the proof is that proving I ∧ A ⇒ I′ allows us to infer I ∧ □A ⇒ □I , where I is a predicate and A an action. This is an RTLA [13] rule, where RTLA is a logic that is like TLA except that □A is an RTLA formula for any action A, not just for actions A of the form [N ]_{v}. In RTLA, temporal quantification (the operator ∃ ∃ ∃ ∃ ∃ ∃) can be applied only to a TLA formula, not to an arbitrary RTLA formula. All TLA proof rules are valid for RTLA.

To complete the proof of ⟨1⟩1, we must prove ⟨2⟩1 and ⟨2⟩2. Step ⟨2⟩1 follows from the definitions by simple predicate logic. The proof of ⟨2⟩2 is shown in Figure 10. The proof goal is first transformed into an Assume/Prove form, so the new goal becomes simply Inv(g, h)′. Inside the proof, these four assumptions are referred to as assumption ⟨2⟩:1–⟨2⟩:4.

Since Inv(g, h) is the conjunction of the formulas Inv(g, h).1, Inv(g, h).2, and Inv(g, h).3, the next level of the proof (steps ⟨3⟩1–⟨3⟩4) is immediate. The

⟨1⟩1. Assume: g, h ∈ Lt Prove: LSpec(g) ∧ LSpec(h) ⇒ □Inv(g, h)

Let: T (g) =^{Δ} Loyal(g) ∧ (ord[g] = “?”) ⇒ (now ≤ Now_{0} + Δ) ⟨2⟩1. LInit(g) ∧ LInit(h) ∧ T (g) ⇒ Inv(g, h)

⟨2⟩2. ∧ Inv(g, h)

∧ [Choose(g) ∨ Fail(g)]_{var(g)} ∧ [Choose(h) ∨ Fail(h)]_{var(h)} ∧ T (g)′ ⇒ Inv(g, h)′

⟨2⟩3. Q.E.D.

Proof:

LSpec(g) ∧ LSpec(h)

⇒ {By definition of LSpec and T .}

∧ LInit(g) ∧ LInit(h) ∧ □[Choose(g) ∨ Fail(g)]_{var(g)} ∧ □[Choose(h) ∨ Fail(h)]_{var(h)} ∧ □T (g)

⇒ {Using the RTLA rule ⊢ □P ≡ P ∧ □P′, for any predicate P.}

∧ LInit(g) ∧ LInit(h) ∧ T (g) ∧ □[Choose(g) ∨ Fail(g)]_{var(g)} ∧ □[Choose(h) ∨ Fail(h)]_{var(h)} ∧ □T (g)′

⇒ {By ⟨2⟩1.}

∧ Inv(g, h) ∧ □[Choose(g) ∨ Fail(g)]_{var(g)} ∧ □[Choose(h) ∨ Fail(h)]_{var(h)} ∧ □T (g)′

⇒ {Using the rule that □ distributes over ∧.}

∧ Inv(g, h) ∧ □([Choose(g) ∨ Fail(g)]_{var(g)} ∧ [Choose(h) ∨ Fail(h)]_{var(h)} ∧ T (g)′)

⇒ {By ⟨2⟩2 and the RTLA Rule (I ∧ A ⇒ I′) ⊢ (I ∧ □A ⇒ □I ), for

any predicate I and action A.} □Inv(g, h)

Fig. 9. The high-level structure of the proof of step ⟨1⟩1 from Figure 8.

⟨2⟩2. ∧ Inv(g, h)

∧ [Choose(g) ∨ Fail(g)]_{var(g)} ∧ [Choose(h) ∨ Fail(h)]_{var(h)} ∧ T (g)′ ⇒ Inv(g, h)′

Proof: By propositional logic, it suffices to: Assume: 1. Inv(g, h)

2. [Choose(g) ∨ Fail(g)]_{var(g)}

3. [Choose(h) ∨ Fail(h)]_{var(h)}
4. T (g)′

Prove: Inv(g, h)′ ⟨3⟩1. Inv(g, h).1′

Proof: By definition of Inv(g, h).1′ and propositional logic, it suffices to: Assume: Loyal(g)′ Prove: ord′[g] ∈ Order ∪ {“?”} ⟨4⟩1. Case: unchanged var(g)

Proof: Assumption ⟨2⟩:1, Case Assumption ⟨4⟩, and the definition of Inv, since unchanged var(g) implies ord′[g] = ord[g].

⟨4⟩2. Case: Choose(g)

Proof: Case Assumption ⟨4⟩, since Choose(g).2 =^{Δ} ord′[g] ∈ Order. ⟨4⟩3. Case: Fail(g)

Proof: Case Assumption ⟨4⟩ and Assumption ⟨3⟩ lead to a contradiction, since Fail(g) implies ¬Loyal(g)′ by definition of Fail and Loyal.

⟨4⟩4. Q.E.D.

Proof: By propositional logic from ⟨4⟩1, ⟨4⟩2, ⟨4⟩3, and Assumption ⟨2⟩:2, since [A]_{v} =^{Δ} A ∨ (unchanged v).

⟨3⟩2. Inv(g, h).2′ ⟨3⟩3. Inv(g, h).3′ ⟨3⟩4. Q.E.D.

Proof: ⟨3⟩1, ⟨3⟩2, ⟨3⟩3, and the definition of Inv.

Fig. 10. The proof of step ⟨2⟩2 from Figure 9.

proof of ⟨3⟩1 is given; the proofs of ⟨3⟩2 and ⟨3⟩3 are analogous.

The goal, Inv(g, h).1′ is deduced from assumptions ⟨2⟩:1 and ⟨2⟩:2. Since assumption ⟨2⟩:2 is a disjunction, we do a proof by cases. The statement Case: S is equivalent to Assume: S, Prove: Q.E.D.

3.2 Proof of Theorem MidCorrect

Theorem MidCorrect asserts that (□OneTraitor) ∧ Spec implies Hi.Spec. It is trivial to prove that Spec implies Hi.Spec.1 and Hi.Spec.3, so the problem is proving Hi.Spec.2 and Hi.Spec.4. Proving Hi.Spec.2 requires proving Hi.LSpec(g).1 and Hi.LSpec(g).2 for each lieutenant g.

The high-level structure of the proof of theorem MidCorrect appears in Figure 11. Steps ⟨1⟩2 and ⟨1⟩4 prove Hi.LSpec(g).1 and Hi.LSpec(g).2, respectively, and ⟨1⟩5 proves Hi.Spec.4. Steps ⟨1⟩1 and ⟨1⟩3 establish useful invariants.

Theorem (□OneTraitor) ∧ Spec ⇒ Hi.Spec

Let:

Inv(g, l)

=^{Δ}

Loyal(g) ⇒ 1.∧ (Domain rcvd[g] = Lt) 2.∧ (rcvd[g][l] ≠ “?”) ⇒ (rcvd[g][l] ∈ Order) 3.∧ Loyal(Cmdr) ∧ (rcvd[g][g] ∈ Order) ⇒ (rcvd[g][g] = ord[Cmdr])

4.∧ Loyal(l) ∧ (rcvd[g][l] ∈ Order) ⇒ (rcvd[g][l] = rcvd[l][l]) 5.∧ (ord[g] ≠ “?”) ⇒ ∧ ord[g] = Majority(rcvd[g]) ∧ ∀ h ∈ Lt : rcvd[g][h] ≠ “?”

TInv(g)

=^{Δ}
1.∧ now ∈ Real
2.∧ Loyal(g) ∧ (ord[g] = “?”) ∧ (∀ h ∈ Lt : rcvd[g][h] ≠ “?”) ⇒ (now ≤ Now_{0} + 2δ + ϵ)

⟨1⟩1. Assume: g, l ∈ Lt

Prove: Hi.CSpec ∧ LSpec(g) ∧ LSpec(l) ⇒ □Inv(g, l) ⟨1⟩2. Assume: g ∈ Lt

Prove: □OneTraitor ∧ LSpec(g) ∧ (∀ h, l ∈ Lt : □Inv(h, l)) ⇒ Hi.LSpec(g).1 ⟨1⟩3. Assume: g ∈ Lt

Prove: (now = Now_{0}) ∧ RT (⟨ord, rcvd, status ⟩) ∧ LSpec(g) ∧ (∀ h ∈ Lt : □Inv(g, h)) ⇒ □TInv(g)

⟨1⟩4. Assume: g ∈ Lt

Prove: LSpec(g) ∧ □TInv(g) ⇒ Hi.LSpec(g).2 ⟨1⟩5. RT (⟨ord, rcvd, status ⟩) ⇒ RT (⟨ord, status ⟩) ⟨1⟩6. Q.E.D.

⟨2⟩1. (□OneTraitor) ∧ Spec ⇒ Hi.Spec.1

Proof: Trivial, since Spec.1 is the same as Hi.Spec.1. ⟨2⟩2. (□OneTraitor) ∧ Spec ⇒ Hi.Spec.2

Proof: By ⟨1⟩1–⟨1⟩4 and the definitions of Spec and Hi.Spec, since Spec.2 equals ∀ l ∈ Lt : LSpec(l), and Hi.Spec.2 equals ∀ g ∈ Lt : Hi.LSpec(g).

⟨2⟩3. (□OneTraitor) ∧ Spec ⇒ Hi.Spec.3

Proof: Trivial, since Spec.3 is the same as Hi.Spec.3. ⟨2⟩4. (□OneTraitor) ∧ Spec ⇒ Hi.Spec.4

Proof: By ⟨1⟩5 and the definitions of Spec and Hi.Spec. ⟨2⟩5. Q.E.D.

Proof: ⟨2⟩1–⟨2⟩4 and the definition of Hi.Spec.

Fig. 11. The high-level structure of the proof of theorem MidCorrect ⟨1⟩2. Assume: g ∈ Lt

Prove: (□OneTraitor) ∧ LSpec(g) ∧ (∀ h, l ∈ Lt : □Inv(h, l))

⇒ Hi.LSpec(g).1

⟨2⟩1. LInit(g) ⇒ Hi.LInit(g)

Proof: By definition of LInit(g). ⟨2⟩2. OneTraitor′ ∧ (∀ h, l ∈ Lt : Inv(h, l) ∧ Inv(h, l)′) ∧ [Next(g)]_{var(g)}

⇒ [Hi.Choose(g) ∨ Hi.Fail(g)]_{Hi.var(g)} …

⟨2⟩3. Q.E.D.

Proof:

(□OneTraitor) ∧ LSpec(g) ∧ (∀ h, l ∈ Lt : □Inv(h, l))

⇒ {By definition of LSpec(g).}

(□OneTraitor) ∧ LInit(g) ∧ □[Next(g)]_{var(g)} ∧ (∀ h, l ∈ Lt : □Inv(h, l))

⇒ {By simple RTLA reasoning.}

LInit(g) ∧ □(\begin{matrix}OneTraitor′ \\ ∧ (∀ h, l ∈ Lt : Inv(h, l) ∧ Inv(h, l)′) ∧ [Next(g)]_{var(g)}) \end{matrix}

⇒ {By ⟨2⟩1, ⟨2⟩2 and simple RTLA reasoning.}

Hi.LInit(g) ∧ □[Hi.Choose(g) ∨ Hi.Fail(g)]_{Hi.var(g)}

⇒ {By definition of Hi.LSpec(g)}

Hi.LSpec(g).1.

Fig. 12. The proof of step ⟨1⟩2 from Figure 11, with the proof of ⟨2⟩2 elided.

Step ⟨1⟩1 is an invariance proof of the kind we have already seen in the proof of theorem SpecGood. Its proof is omitted.

We consider now the proof of ⟨1⟩2, which appears in Figure 12. The key step is ⟨2⟩2, whose proof is in Figure 13. Since Hi.var(g) is a subtuple of var(g), it is obvious that unchanged ⟨var(g)⟩ implies unchanged ⟨Hi.var(g)⟩. The proof demonstrates that every step of the mid-level specification, which is a Next(g) step, is a [Hi.Choose(g) ∨ Hi.Fail(g)]_{Hi.var(g)} step—that is, a step allowed by the high-level specification. (This is sometimes called proving step simulation.)

Formally, the first level in the proof of ⟨2⟩2 is a case split on the disjuncts of [Next(g)]_{var(g)}. The only hard case is Choose(g), which we prove implies Hi.Choose(g). (In other words, we prove that a mid-level Choose(g) step implements a high-level Hi.Choose(g) step.) The next-level proof of this case is obtained by separately proving Hi.Choose(g).1, …, Hi.Choose(g).4. The only hard parts are steps ⟨4⟩2 and ⟨4⟩3. The proof of ⟨4⟩2 is given in Figure 14; the proof of ⟨4⟩3 is omitted.

Step ⟨1⟩3 is a property of the same form as theorem SpecGood. However, there is a temporal quantifier ∃ ∃ ∃ ∃ ∃ ∃ in LSpec(g). Figure 15 indicates how this quantifier is handled. We first define LSpecT (g, t) to be LSpec(g) with the quantifier removed, and define the invariant TInvT (g, t).^{3} The heart of the proof, step ⟨2⟩1, asserts an ordinary invariance property with no temporal quantifiers; its proof is omitted. Steps ⟨2⟩3 and ⟨2⟩4 show how the quantifier is “put back into

3 If r and s are elements of Real, then r ≤ t ≤ s means (t ∈ Real) ∧ (r ≤ t) ∧ (t ≤ s).

⟨2⟩2. OneTraitor′ ∧ (∀ h, l ∈ Lt : Inv(h, l) ∧ Inv(h, l)′) ∧ [Next(g)]_{var(g)}

⇒ [Hi.Choose(g) ∨ Hi.Fail(g)]_{Hi.var(g)} Proof: By propositional logic, it suffices to: Assume: 1. OneTraitor′

2. ∀ h, l ∈ Lt : Inv(h, l) ∧ Inv(h, l)′ 3. [Next(g)]_{var(g)}

Prove: [Hi.Choose(g) ∨ Hi.Fail(g)]_{Hi.var(g)} ⟨3⟩1. Case: Issue(g)

Proof: By definition, Issue(g).3 equals unchanged Hi.var(g). ⟨3⟩2. Case: ∃ h ∈ Lt \ {g} : Relay(g, h)

Proof: By propositional logic, it suffices to prove that (h ∈ Lt) ∧ Relay(g, h) implies unchanged Hi.var(g), which follows from the definitions of Relay(g, h) and Hi.var(g).

⟨3⟩3. Case: Choose(g)

⟨4⟩1. Loyal(g) ∧ (ord[g] = “?”)

Proof: Choose(g).1, which holds by Case Assumption ⟨3⟩. ⟨4⟩2. ord′[g] ∈ Order

… ⟨4⟩3. ∀ h ∈ Gen : Loyal(h)′ ∧ (ord′[h] ≠ “?”) ⇒ (ord′[g] = ord′[h])

… ⟨4⟩4. unchanged status[g]

Proof: Choose(g).4, which holds by Case Assumption ⟨3⟩. ⟨4⟩5. Q.E.D.

Proof: ⟨4⟩1–⟨4⟩4 imply Hi.Choose(g). ⟨3⟩4. Case: Hi.Fail(g)

Proof: Immediate. ⟨3⟩5. Case: unchanged var(g)

Proof: By definition, Hi.var(g) is a subsequence of var(g). ⟨3⟩6. Q.E.D.

Proof: ⟨3⟩1–⟨3⟩5 and the definition of Next(g).

Fig. 13. The proof of step ⟨2⟩2 from Figure 12, with the proofs of ⟨4⟩2 and ⟨4⟩3 elided.

⟨4⟩2. ord′[g] ∈ Order

⟨5⟩1. rcvd[g] ∈ [Lt → Order]

⟨6⟩1. Domain rcvd[g] = Lt Proof: ⟨4⟩1 and Inv(g, g).1, which holds by Assumption ⟨1⟩ and Assumption ⟨2⟩:2.

⟨6⟩2. ∀ h ∈ Lt : rcvd[g][h] ≠ “?”

Proof: Choose(g).2, which holds by Assumption ⟨3⟩. ⟨6⟩3. ∀ h ∈ Lt : rcvd[g][h] ∈ Order

Proof: ⟨6⟩2 and Inv(g, h).2, which holds by ⟨4⟩1, Assumption ⟨1⟩, and Assumption ⟨2⟩:2.

⟨6⟩4. Q.E.D.

Proof: ⟨6⟩1 and ⟨6⟩3. ⟨5⟩2. Q.E.D.

Proof: Choose(g).3 (which holds by Assumption ⟨3⟩), ⟨5⟩1, and Assumption MidAssump.2.

Fig. 14. The proof of step ⟨4⟩2 from Figure 13.

the formula” using simple reasoning. Formally, we are using the following two rules, which are valid if x does not occur free in G:

\frac{F (x) ⇒ G}{(∃ ∃ ∃ ∃ ∃ ∃ x : F (x)) ⇒ G} ⊢ (∃ ∃ ∃ ∃ ∃ ∃ x : F (x) ∧ G) ≡ (∃ ∃ ∃ ∃ ∃ ∃ x : F (x)) ∧ G

This proof strategy will be familiar to anyone who has done rigorous proofs in ordinary first-order logic.

The proof of step ⟨1⟩4 is a simple matter of deducing (□P_{1}) ∧ (□P_{2}) ∧ (□P_{3}) ⇒ □Q from P_{1} ∧ P_{2} ∧ P_{3} ⇒ Q, where □P_{1} and □P_{2} are LSpec(g).2 and LSpec(g).3, respectively. The proof of step ⟨1⟩5 uses the same basic strategy as the proof of ⟨1⟩2, but is much simpler. The formal proofs of these steps are omitted.

3.3 Proof of Theorem LowCorrect

The high-level proof of theorem LowCorrect appears in Figure 16. As in the proof of theorem MidCorrect, we first prove the implication with the quantifiers removed from the hypothesis, and then add the quantifiers in the final step.

The proof of the final step, ⟨1⟩6, is shown in Figure 17. To prove step ⟨2⟩2, we use the same reasoning as before to add the quantifiers. The proof of step ⟨2⟩3 makes use of a TLA proof rule that is analogous to the rule

⊢ (∀ y : ∃ x : F (x)) ≡ (∃ x : ∀ y : F (x(y)))

of higher-order logic. In a formalism like TLA^{+} that includes set theory, functions are ordinary values, and this rule can be stated in first-order logic as

⊢ (∀ y ∈ S : ∃ x : F (x)) ≡ (∃ x : ∀ y ∈ S : F (x[y]))

⟨1⟩3. Assume: g ∈ Lt

Prove: (now = Now_{0}) ∧ RT (⟨ord, rcvd, status ⟩) ∧ LSpec(g)

∧ (∀ h ∈ Lt : □Inv(g, h)) ⇒ □TInv(g)

Let: LSpecT (g, t) =^{Δ} LSpec(g).1 ∧ LSpec(g).2 ∧ LSpec(g).3 ∧ LSpec(g).4(t)

TInvT (g, t) =^{Δ} 1.∧ now ∈ Real 2.∧ Loyal(g) ∧ (ord[g] = “?”) ∧ (∀ h ∈ Lt : rcvd[g][h] ≠ “?”) ⇒ (now ≤ t ≤ Now_{0} + 2δ + ϵ)

⟨2⟩1. (now = Now_{0}) ∧ RT (⟨ord, rcvd, status ⟩) ∧ LSpecT (g, t)

∧ (∀ h ∈ Lt : □Inv(g, h)) ⇒ □TInvT (g, t) …

⟨2⟩2. (now = Now_{0}) ∧ RT (⟨ord, rcvd, status ⟩) ∧ LSpecT (g, t)

∧ (∀ h ∈ Lt : □Inv(g, h)) ⇒ □TInv(g) Proof: ⟨2⟩1 and simple temporal reasoning, since TInvT (g, t) implies TInv(g).

⟨2⟩3. (∃ ∃ ∃ ∃ ∃ ∃ t : (now = Now_{0}) ∧ RT (⟨ord, rcvd, status ⟩) ∧ LSpecT (g, t)

∧ (∀ h ∈ Lt : □Inv(g, h))) ⇒ □TInv(g) Proof: ⟨2⟩2, since t does not occur free in □TInv(g).

⟨2⟩4. Q.E.D.

Proof: ⟨2⟩3, since ∃ ∃ ∃ ∃ ∃ ∃ t : ∧ (now = Now_{0}) ∧ RT (⟨ord, rcvd, status ⟩) ∧ LSpecT (g, t) ∧ ∀ h ∈ Lt : □Inv(g, h))

≡ {By definition of LSpecT .}

∃ ∃ ∃ ∃ ∃ ∃ t : ∧ (now = Now_{0}) ∧ RT (⟨ord, rcvd, status ⟩) ∧ LSpec(g).1 ∧ LSpec(g).2 ∧ LSpec(g).3 ∧ LSpec(g).4(t) ∧ ∀ h ∈ Lt : □Inv(g, h)

≡ {Because t occurs free only in LSpecT (g).4.}

∧ (now = Now_{0}) ∧ RT (⟨ord, rcvd, status ⟩) ∧ LSpec(g).1 ∧ LSpec(g).2 ∧ LSpec(g).3 ∧ ∃ ∃ ∃ ∃ ∃ ∃ t : LSpec(g).4(t) ∧ ∀ h ∈ Lt : □Inv(g, h)

≡ {By definition of LSpec.}

∧ (now = Now_{0}) ∧ RT (⟨ord, rcvd, status ⟩) ∧ LSpec(g) ∧ ∀ h ∈ Lt : □Inv(g, h)

Fig. 15. The proof of ⟨1⟩3 from Figure 11, with the proof of ⟨2⟩1 elided.

Theorem Spec ⇒ Mid.Spec

Let: qt, ct, t_{1}, t_{2}, t_{3}, t_{4}, t_{5}, t_{6} : variable TEMax(t, g, A) =^{Δ} VTimer(t, A, ϵ, lvar(g)) ∧ MaxTimer(t) CSpecT =^{Δ} 1.∧ CInit ∧ □[CNext]_{cvar} 2.∧ ∀ g ∈ Lt : TEMax(ct[g], Cmdr, CSend(g))

LSpecT (g) =^{Δ} 1.∧ LInit(g) ∧ □[LNext(g)]_{lvar(g)} 2.∧ TEMax(t_{1}[g], g, Issue(g)) 3.∧ TEMax(t_{2}[g], g, IssueTimeout(g)) 4.∧ TEMax(t_{3}[g], g, Choose(g)) 5.∧ ∀ h ∈ Lt \ {g} : ∧ TEMax(t_{4}[g][h], g, Send(g, h)) ∧ TEMax(t_{5}[g][h], g, Relay(g, h)) ∧ TEMax(t_{6}[g][h], g, RelayTimeout(g, h))

TCSpecT (g, h) =^{Δ} TC (g, h).Spec.1 ∧ TC (g, h).Spec.2 ∧ TC (g, h).Spec.3(qt[g][h])

CInv(g) =^{Δ} …

LInv(g, h) =^{Δ} …

⟨1⟩1. CSpec ⇒ Mid.Hi.CSpec ⟨1⟩2. Assume: g ∈ Lt

Prove:

∧ CSpecT ∧ LSpecT (g) ∧ TCSpecT (Cmdr, g) ∧ (now = Now_{0}) ∧ RT (⟨ord, rcvd, in, out, status, sent ⟩) ⇒ □CInv(g)

⟨1⟩3. Assume: 1. g, h ∈ Lt

2. g ≠ h

Prove:

∧ LSpecT (g) ∧ LSpecT (h) ∧ TCSpecT (g, h) ∧ (now = Now_{0}) ∧ RT (⟨ord, rcvd, in, out, status, sent ⟩) ∧ □CInv(g) ⇒ □LInv(g, h)

⟨1⟩4. Assume: g ∈ Lt

Prove: LSpec(g) ∧ □CInv(g) ∧ □(∀ h ∈ Lt \ {g} : LInv(h, g))

⇒ Mid.LSpec(g)

⟨1⟩5. RT (⟨ord, rcvd, in, out, status ⟩) ⇒ RT (⟨ord, rcvd, status ⟩) ⟨1⟩6. Q.E.D.

Fig. 16. The high-level proof of theorem LowCorrect.

(The range S is needed because the domain of a function must be a set.) If the ordinary existential quantifier ∃ is replaced by the temporal quantifier ∃ ∃ ∃ ∃ ∃ ∃, the rule remains sound in general only if S is finite.^{4}

We now return to the high-level proof of the theorem. The proof of step ⟨1⟩1 is simple and is omitted. The proofs of ⟨1⟩2 and ⟨1⟩3 are straightforward

4 The rule is unsound for an infinite set S because ∃ ∃ ∃ ∃ ∃ ∃ is defined so ∃ ∃ ∃ ∃ ∃ ∃ x : F is invariant under stuttering. It is sound for the operator ∃ ∃ ∃ ∃ ∃ ∃ of Manna and Pnueli [18], which does not preserve invariance under stuttering.

⟨1⟩6. Q.E.D.

⟨2⟩1. ∧ CSpec

∧ CSpecT

∧ ∀ g ∈ Lt : LSpecT (g)

∧ ∀ g, h ∈ Gen : TCSpecT (g, h)

∧ RT (⟨ord, rcvd, in, out, status, sent ⟩)

∧ now = Now_{0} ⇒ Mid.Spec

Proof: ⟨1⟩1–⟨1⟩5 and the definition of Mid.Spec.

⟨2⟩2. ∧ CSpec

∧ ∃ ∃ ∃ ∃ ∃ ∃ ct : CSpecT

∧ ∃ ∃ ∃ ∃ ∃ ∃ t_{1}, t_{2}, t_{3}, t_{4}, t_{5}, t_{6} : ∀ g ∈ Lt : LSpecT (g)

∧ ∃ ∃ ∃ ∃ ∃ ∃ qt : ∀ g, h ∈ Gen : TCSpecT (g, h) ∧ RT (⟨ord, rcvd, in, out, status, sent ⟩) ∧ now = Now_{0} ⇒ Mid.Spec

Proof: ⟨2⟩1, since ct occurs only in CSpecT , t_{1}, t_{2}, t_{3}, t_{4}, t_{5}, and t_{6} occur only in LSpecT (g), and qt occurs only in TCSpecT (g, h).

⟨2⟩3. 1. (∃ ∃ ∃ ∃ ∃ ∃ ct : CSpecT ) ≡ CSpec 2. (∃ ∃ ∃ ∃ ∃ ∃ t_{1}, t_{2}, t_{3}, t_{4}, t_{5}, t_{6} : ∀ g ∈ Lt : LSpecT (g)) ≡ ∀ g ∈ Lt : LSpec(g)

3. (∃ ∃ ∃ ∃ ∃ ∃ qt : ∀ g, h ∈ Gen : TCSpecT (g, h)) ≡ ∀ g, h ∈ Gen : TC (g, h).Spec Proof: Lt is finite by assumption HiAssump.1 from module SpecParams (imported via module MidLevel), and ∃ ∃ ∃ ∃ ∃ ∃ x : ∀ v ∈ S : F (x[v]) is equivalent to ∀ v ∈ S : ∃ ∃ ∃ ∃ ∃ ∃ x : F (x), for any finite set S and temporal operator F ( ).

⟨2⟩4. Q.E.D.

Proof: ⟨2⟩2, ⟨2⟩3, and the definition of Spec.

Fig. 17. The proof of step ⟨1⟩6 from Figure 16.

invariance arguments. The invariants, CInv(g) and LInv(g, h), are defined in Figure 18. Because the invariants are a bit long, the proofs of ⟨1⟩2 and ⟨1⟩3 are rather tedious; they are omitted.

Step ⟨1⟩4 introduces a new problem—proving an implication whose conclusion contains a ∃ ∃ ∃ ∃ ∃ ∃. We now examine its proof, which is outlined in Figure 19.

Step ⟨2⟩1 is an implication of the form we’ve seen before. The major part of its proof consists of proving step simulation. The proof is straightforward but tedious, taking about two pages.

Steps ⟨2⟩2 and ⟨2⟩3 have the form □P ⇒ □Q, which is proved by showing that P implies Q. These proofs are easy.

Step ⟨2⟩4 is where the ∃ ∃ ∃ ∃ ∃ ∃ appears in the conclusion. In first-order logic, one proves that F (x) implies ∃ y : G(x, y) by instantiating y—that is, finding an expression h(x) such that F (x) implies G(x, h(x)). The same technique is used with the temporal quantifier ∃ ∃ ∃ ∃ ∃ ∃, where the instantiation is called a refinement mapping [1]. To prove ⟨2⟩4, we must instantiate the timer variable t used to express the timing constraint on Mid.Choose. The instantiation is simple—we instantiate t with the timer variable for the low-level Choose action. Step ⟨3⟩1

Let: r(g, h) =^{Δ} if rcvd[g][h] = “?” then ⟨ ⟩ else ⟨rcvd[g][h]⟩ c(g, h) =^{Δ} in[h][g][1] ∘ out[g][h][1] cOrd(g) =^{Δ} r(g, g) ∘ c(Cmdr, g) lOrd(g, h) =^{Δ} r(g, h) ∘ c(h, g)

CInv(g) =^{Δ}

1.∧ Loyal(Cmdr) ∧ Loyal(g) ⇒ ∨ (cOrd(g) = ⟨ ⟩) ∧ NotSent(Cmdr, g) ∨ (cOrd(g) = ⟨ord[Cmdr]⟩) ∧ ¬NotSent(Cmdr, g)

2.∧ Loyal(g) ∧ (rcvd[g][g] = “?”) ⇒ ∀ h ∈ Lt : NotSent(g, h) 3.∧ Loyal(Cmdr) ∧ NotSent(Cmdr, g) ⇒ (now ≤ ct[g] ≤ Now_{0} + ϵ) 4.∧ Loyal(g) ∧ Loyal(Cmdr) ∧ (out[Cmdr][g][1] ≠ ⟨ ⟩) ⇒ (now ≤ qt[Cmdr][g] ≤ Now_{0} + τ + ϵ) 5.∧ Loyal(g) ∧ Loyal(Cmdr) ∧ (in[g][Cmdr][1] ≠ ⟨ ⟩) ⇒ (now ≤ t_{1}[g] ≤ Now_{0} + τ + 2 ∗ ϵ) 6.∧ Loyal(g) ∧ (rcvd[g][g] = “?”) ∧ (Now_{0} + τ + 2 ∗ ϵ < now) ⇒ (now ≤ t_{2}[g] ≤ Now_{0} + τ + 3 ∗ ϵ) 7.∧ now ∈ Real

LInv(g, h) =^{Δ}

1.∧ Loyal(g) ∧ Loyal(h) ⇒ ∨ (lOrd(h, g) = ⟨ ⟩) ∧ NotSent(g, h) ∨ (lOrd(h, g) = ⟨rcvd[g][g]⟩) ∧ ¬NotSent(g, h)

2.∧ Loyal(g) ∧ (rcvd[g][g] ≠ “?”) ∧ NotSent(g, h) ⇒ (now ≤ t_{4}[g][h] ≤ Now_{0} + τ + 4 ∗ ϵ) 3.∧ Loyal(g) ∧ Loyal(h) ∧ (out[g][h][1] ≠ ⟨ ⟩) ⇒ (now ≤ qt[g][h] ≤ Now_{0} + 2 ∗ τ + 4 ∗ ϵ) 4.∧ Loyal(g) ∧ Loyal(h) ∧ (in[h][g][1] ≠ ⟨ ⟩) ⇒ (now ≤ t_{5}[h][g] ≤ Now_{0} + 2 ∗ τ + 5 ∗ ϵ) 5.∧ Loyal(h) ∧ (rcvd[h][g] = “?”) ∧ (now > Now_{0} + 2 ∗ τ + 5 ∗ ϵ) ⇒ (now ≤ t_{6}[h][g] ≤ Now_{0} + 2 ∗ τ + 6 ∗ ϵ)

Fig. 18. The invariants for the proof of theorem LowCorrect.

⟨1⟩4. Assume: g ∈ Lt

Prove: LSpec(g) ∧ □CInv(g) ∧ □(∀ h ∈ Lt \ {g} : LInv(h, g))

⇒ Mid.LSpec(g)

⟨2⟩1. LSpec(g).1 ∧ □CInv(g) ∧ □(∀ h ∈ Lt \ {g} : LInv(h, g))

⇒ Mid.Init(g) ∧ □[Mid.Next(g)]_{Mid.var(g)} …

⟨2⟩2. □CInv(g) ⇒ □(Loyal(g) ∧ (rcvd[g][g] = “?”) ⇒ (now ≤ Now_{0} + δ))

… ⟨2⟩3. □LInv(h, g) ⇒ □(Loyal(g) ∧ (rcvd[g][h] = “?”) ⇒ (now ≤ Now_{0} + 2 ∗ δ))

… ⟨2⟩4.

□[LNext(g)]_{lvar(g)} ∧ EMax(g, Choose(g))

⇒ ∃ ∃ ∃ ∃ ∃ ∃ t : VTimer(t, Mid.Choose(g), ϵ, Mid.var(g)) ∧ MaxTimer(t) ⟨3⟩1. □[LNext(g)]_{lvar(g)} ∧ VTimer(t, Choose(g), ϵ, lvar(g))

⇒ VTimer(t, Mid.Choose(g), ϵ, Mid.var(g)) …

⟨3⟩2.

∧ □[LNext(g)]_{lvar(g)}

∧ VTimer(t, Choose(g), ϵ, lvar(g)) ∧ MaxTimer(t)

⇒ ∃ ∃ ∃ ∃ ∃ ∃ t : VTimer(t, Mid.Choose(g), ϵ, Mid.var(g)) ∧ MaxTimer(t) Proof: ⟨3⟩1.

⟨3⟩3.

∧ □[LNext(g)]_{lvar(g)}

∧ ∃ ∃ ∃ ∃ ∃ ∃ t : VTimer(t, Choose(g), ϵ, lvar(g)) ∧ MaxTimer(t)

⇒ ∃ ∃ ∃ ∃ ∃ ∃ t : VTimer(t, Mid.Choose(g), ϵ, Mid.var(g)) ∧ MaxTimer(t) Proof: ⟨3⟩2, since t does not occur free in □[LNext(g)]_{lvar(g)} or ∃ ∃ ∃ ∃ ∃ ∃ t : . . ..

⟨3⟩4. Q.E.D.

Proof: ⟨3⟩2 and the definition of EMax(g, Choose(g)). ⟨2⟩5. Q.E.D.

Proof: ⟨2⟩1–⟨2⟩4 and the definition of Mid.LSpec(g).

Fig. 19. The proof of step ⟨1⟩4 from Figure 16, with most steps elided.

has a familiar form, since VTimer(…) has the form Init ∧ □[Next]_{v}; its proof is simple.

The one remaining step in the high-level proof of the theorem is ⟨1⟩5. It is easy, and is omitted.

4 Discussion

Because the algorithm and its informal specification were well understood, writing the formal specifications was a straightforward exercise. As expected, we discovered small mistakes in the initial versions while writing the proofs. Our specifications were not subject to mechanical checking, so they probably still contain typographical errors. We would like to say that any such errors are minor, but with modern text editors and typesetting systems, one careless keystroke can produce major mistakes.

We have used a specification style different from our customary one. We usually write interleaving specifications, in which events in different processes are represented by separate steps [3]. Here, we have written noninterleaving specifications that allow individual steps which represent actions in two or more processes. For example, the formula Spec of module MidLevel allows behaviors in which a single step is both an Issue(g) step of lieutenant g and a Relay(h, g) step of a different lieutenant h. Writing noninterleaving specifications introduced no new problems.

Writing the proofs was also a straightforward exercise. As is typical when reasoning about real time, our specifications are safety properties; there are no liveness properties. When proving safety properties, creativity is required only in finding the invariants. With practice, writing invariants becomes second nature. The rest of the proof is a standard process of applying simple TLA proof rules and using the structure of the formulas to decompose the resulting proof obligations.

Writing this kind of proof is an exercise in organizing a complex structure. It is very much like programming; it is completely different from what mathematicians do when they write proofs. All the steps in our proof are mathematically trivial. Hierarchically structured proofs are long and tedious, but they are the only kind of hand proofs that can be trusted. There are no shortcuts. Short proofs are short because they gloss over details that have to be checked to avoid errors.

These proofs are amenable to mechanical verification. Most steps can be checked with the TLP verification system [7]. However, for this type of reasoning, which cannot be checked by finite-state methods, mechanical theorem proving still seems to be considerably more work than writing a hand proof. The hierarchical proof style makes it possible to reduce the probability of errors in hand proofs to an acceptable level.

Our specifications are written in TLA^{+}. The flexibility of TLA^{+} is indicated by the ease with which real-time properties are expressed, even though the language has no special primitives for time. We use the same RealTime module for specifying Byzantine generals that was used in [15] for specifying a gas burner. This kind of flexibility and modularity are characteristic of an engineering discipline.

Our proofs use the logic TLA. They are completely formal. Although most of the lower-level steps were omitted, the parts that we did present in detail show that all the proofs can be carried out to the level of simple propositional reasoning. The proofs are seamless. The theorems to be proved are mathematical formulas, and at each step we are proving a mathematical formula. There is no switching from programs to logic; there is no appeal to semantic understanding. Hierarchically decomposing a large problem into smaller ones by the use of simple mathematical rules is characteristic of an engineering discipline.

We believe that formal specification and proof is now feasible for high-level designs of real systems. They are not yet feasible for reasoning at the level of executable code, except in special applications or for small parts of a system. It may appear that it is difficult to reason about code because our specifications are logical formulas rather than programs. However, the primary issue is not one of language but of complexity. It is hard to reason about real programs because they are complicated. Formal reasoning is generally applied only to concurrent programs written in toy languages like CSP [8] and Unity [5]. A program in a toy language is no closer to a real program than is a TLA formula. Further work is needed before formal reasoning about executable code becomes routine.

References

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

2. Martín Abadi and Leslie Lamport. An old-fashioned recipe for real time. Research Report 91, Digital Equipment Corporation, Systems Research Center, 1992. An earlier version, without proofs, appeared in [6, pages 1–27].

3. Martín Abadi and Leslie Lamport. Conjoining specifications. Research Report 118, Digital Equipment Corporation, Systems Research Center, 1993. To appear in ACM Transactions on Programming Languages and Systems.

4. E. A. Ashcroft. Proving assertions about parallel programs. Journal of Computer and System Sciences, 10:110–135, February 1975.

5. K. Mani Chandy and Jayadev Misra. Parallel Program Design. Addison-Wesley, Reading, Massachusetts, 1988.

6. J. W. de Bakker, C. Huizing, W. P. de Roever, and G. Rozenberg, editors. Real-Time: Theory in Practice, volume 600 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, 1992. Proceedings of a REX Real-Time Workshop, held in The Netherlands in June, 1991.

7. Urban Engberg, Peter Grønning, and Leslie Lamport. Mechanical verification of concurrent systems with TLA. In Computer-Aided Verification, Lecture Notes in Computer Science, Berlin, Heidelberg, New York, June 1992. Springer-Verlag. Proceedings of the Fourth International Conference, CAV’92.

8. C. A. R. Hoare. Communicating Sequential Processes. Series in Computer Science. Prentice-Hall International, London, 1985.

9. Reino Kurki-Suonio. Operational specification with joint actions: Serializable databases. Distributed Computing, 6(1):19–37, 1992.

10. Simon S. Lam and A. Udaya Shankar. Protocol verification via projections. IEEE Transactions on Software Engineering, SE-10(4):325–342, July 1984.

11. Simon S. Lam and A. Udaya Shankar. Specifying modules to satisfy interfaces: A state transition system approach. Distributed Computing, 6(1):39–63, 1992.

12. Leslie Lamport. Specifying concurrent program modules. ACM Transactions on Programming Languages and Systems, 5(2):190–222, April 1983.

13. Leslie Lamport. The temporal logic of actions. Research Report 79, Digital Equipment Corporation, Systems Research Center, December 1991. To appear in ACM Transactions on Programming Languages and Systems.

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

15. Leslie Lamport. Hybrid systems in TLA^{+}. In Robert L. Grossman, Anil Nerode, Anders P. Ravn, and Hans Rischel, editors, Hybrid Systems, volume 736 of Lecture Notes in Computer Science, pages 77–102, Berlin, Heidelberg, 1993. Springer-Verlag.

16. Leslie Lamport, Robert Shostak, and Marshall Pease. The Byzantine generals problem. ACM Transactions on Programming Languages and Systems, 4(3):382– 401, July 1982.

17. Nancy Lynch and Mark Tuttle. Hierarchical correctness proofs for distributed algorithms. In Proceedings of the Sixth Symposium on the Principles of Distributed Computing, pages 137–151. ACM, August 1987.

18. Zohar Manna and Amir Pnueli. The Temporal Logic of Reactive and Concurrent Systems. Springer-Verlag, New York, 1991.

19. Jayadev Misra and K. Mani Chandy. Proofs of networks of processes. IEEE Transactions on Software Engineering, SE-7(4):417–426, July 1981.

20. Peter G. Neumann and Leslie Lamport. Highly dependable distributed systems. Technical report, SRI International, June 1983. Contract Number DAEA18-81-G-0062, SRI Project 4180.

module FiniteSets^{3}

import Naturals HasCardinality(n, S) =^{Δ} let Q =^{Δ} {i ∈ Nat : i < n} in ∧ n ∈ Nat ∧ ∃ f ∈ [Q → S] : ∧ ∀ s ∈ S : ∃ q ∈ Q : f [q] = s ∧ ∀ q1, q2 ∈ Q : (f [q1] = f [q2]) ⇒ (q1 = q2)

IsFiniteSet(S) =^{Δ} ∃ n ∈ Nat : HasCardinality(n, S)

module Sequences^{42}

import Naturals OneTo(n) =^{Δ} {i ∈ Nat : (1 ≤ i) ∧ (i ≤ n)} Len(s) =^{Δ} choose n : (n ∈ Nat) ∧ (Domain s) = OneTo(n)

Head(s) =^{Δ} s[1]

Tail(s) =^{Δ} [i ∈ OneTo(Len(s) − 1) ↦ s[i + 1]]

(s) ∘ (t) =^{Δ} [i ∈ OneTo(Len(s) + Len(t)) ↦ if i ≤ Len(s) then s[i] else t[i − Len(s)]]

module RealTime

import Reals parameters now : variable

∞ : constant

assumption

InfinityUnReal =^{Δ} ∞ ∉ Real RT (v)^{24} =^{Δ} ∧ now ∈ Real ∧ □[\begin{matrix}∧ now′ ∈ \{r ∈ Real : now < r\} \\ ∧ v′ = v ]_{now} \end{matrix}

VTimer(x, A, δ, v) =^{Δ} ∧ x = if Enabled ⟨A⟩_{v} then now + δ else ∞ ∧ □[x′ = if (Enabled ⟨A⟩_{v} )′ then if ⟨A⟩_{v} ∨ ¬Enabled ⟨A⟩_{v} then now′ + δ else x else ∞ ]_{⟨x ,v ⟩}

MaxTimer(x) =^{Δ} □[(x ≠ ∞) ⇒ (now′ ≤ x)]_{now} MinTimer(x, A, v) =^{Δ} □[A ⇒ (now ≥ x)]_{v}

Fig. 20. The modules FiniteSets, Sequences, and RealTime. assumption Begins a sequence of assumptions that must be true of the constant

parameters when the module is included in another module.^{9}

constant Specifies a parameter’s sort.^{5}

definitions Begins a sequence of definitions. This keyword may be omitted or replaced by one of the keywords action, boolean, constant, predicate, state function, temporal, or transition function to denote the sort of the symbols being defined.

export Specifies definitions visible to importing and including modules.^{29}

import Appends parameters, assumptions, definitions, and theorems of another module.^{2}

include … as … with Appends definitions, assumptions (as theorems), and theorems of another module, with instantiations for its parameters.^{30} ^{51}

module Begins a module.^{1}

parameters Declares the free parameters of a module.^{4}

theorem Begins a sequence of theorems. (They must be provable from the module’s assumptions and the rules of first-order logic, set theory, and TLA.)

variable Specifies a parameter’s sort.^{5}

=^{Δ} Defines an operator.^{10}

A mostly meaningless decoration that ends the scope of an assumption or theorem section.^{8}

Marks the end of a module.^{14}

Fig. 21. The syntactic keywords and symbols of TLA^{+}.

Predicate and Action Operators p′ [p true in final state of step] [A]_{e} [A ∨ (e′ = e)]^{16} ⟨A⟩_{e} [A ∧ (e′ ≠ e)] Enabled A [An A step is possible] unchanged e [e′ = e]^{22} A · B [Composition of actions]

Temporal Operators □F [F is always true]^{17} ◇F [Eventually: ¬□¬F ] WF_{e}(A) [Weak fairness: □◇⟨A⟩_{e} ∨ □◇¬Enabled A] SF_{e}(A) [Strong fairness: □◇⟨A⟩_{e} ∨ ◇□¬Enabled A] F ⇝ G [Leads to: □(F ⇒ ◇G)] ∃ ∃ ∃ ∃ ∃ ∃ x : F [Temporal existential quantification (hiding).]^{39}

Fig. 22. The nonconstant operators of TLA^{+}.

Logic true false ∧ ∨ ¬ ⇒ ≡ ∀ x : p ∃ x : p ∀ x ∈ S : p ∃ x ∈ S : p choose x : p [Equals some x satisfying p]

Sets = ≠ ∈ ∉ ∪ ∩ ⊆ \ [set difference] {e_{1}, …, e_{n}} [Set consisting of elements e_{i}] {x ∈ S : p} [Set of elements x in S satisfying p] {e : x ∈ S} [Set of elements e such that x in S] Subset S [Set of subsets of S] union S [Union of all elements of S]

Functions f [e] [Function application]^{13} Domain f [Domain of function f ] [x ∈ S ↦ e] [Function f such that f [x] = e for x ∈ S]^{32} [S → T ] [Set of functions f with f [x] ∈ T for x ∈ S]^{28} [f except ![e_{1}] = e_{2}] [Function f̂ equal to f except f̂[e_{1}] = e_{2}]^{34} [f except ![e] ∈ S] [Set of functions f̂ equal to f except f̂[e] ∈ S]

Records e.x [The x-component of record e] [x_{1} ↦ e_{1}, …, x_{n} ↦ e_{n}] [The record whose x_{i} component is e_{i}] [x_{1} : S_{1}, …, x_{n} : S_{n}] [Set of all records with x_{i} component in S_{i}] [r except !.x = e] [Record r̂ equal to r except r̂.x = e] [r except !.x ∈ S] [Set of records r̂ equal to r except r̂.x ∈ S]

Tuples e[i] [The i^{th} component of tuple e] ⟨e_{1}, …, e_{n} ⟩ [The n-tuple whose i^{th} component is e_{i}]^{42} S_{1} × … × S_{n} [The set of all n-tuples with i^{th} component in S_{i}]

Miscellaneous “c_{1} … c_{n}” [A literal string of n characters]^{7} if p then e_{1} else e_{2} [Equals e_{1} if p true, else e_{2}] case p_{1} → e_{1}, …, p_{n} → e_{n} [Equals e_{i} if p_{i} true] let x_{1} =^{Δ} e_{1} … x_{n} =^{Δ} e_{n} in e [Equals e in the context of the definitions] \begin{matrix}∧ & p_{1} \\ & … \\ ∧ & p_{n} \end{matrix} [the conjunction p_{1} ∧ … ∧ p_{n}] \begin{matrix}∨ & p_{1} \\ & … \\ ∨ & p_{n} \end{matrix} [the disjunction p_{1} ∨ … ∨ p_{n}]^{12}

Fig. 23. The constant operators of TLA^{+}.