A historical perspective of a paper published in 1977. The major contribution of that paper was its informal definitions of safety and liveness properties. It provided a method for proving invariance (a safety property) that was equivalent to ones in several papers published at about the same time—the most influential being the Owicki-Gries method.

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.

Hyperproperties generalize ordinary properties by expressing relations among multiple executions of a system. Self-composition has been used to reduce verifying that a system satisfies certain classes of Hyperproperties to verifying that a derived system satisfies an ordinary property. By describing systems and their properties in the temporal logic TLA, we use self-composition to handle a larger class of Hyperproperties that includes those we have seen that express security conditions. TLA tools are used to verify that high-level designs of industrial systems satisfy properties. Now, they can also verify that those systems satisfy these Hyperproperties. No prior knowledge of Hyperproperties or TLA is assumed.

No abstract available.

No abstract available.

Algorithms are different from programs and should not be described with programming languages. For example, algorithms are usually best described in terms of mathematical objects like sets and graphs instead of the primitive objects like bytes and integers provided by programming languages. +CAL is an algorithm language based on TLA+. A +CAL algorithm is translated to a TLA+ specification that can then be checked with the TLC model checker.

The distributed transaction commit problem requires reaching agreement on whether a transaction is committed or aborted. The classic Two-Phase Commit protocol blocks if the coordinator fails. Fault-tolerant consensus algorithms also reach agreement, but do not block whenever any majority of the processes are working. The Paxos Commit algorithm runs a Paxos consensus algorithm on the commit/abort decision of each participant to obtain a transaction commit protocol that uses 2 F + 1 coordinators and makes progress if at least F + 1 of them are working properly. Paxos Commit has the same stable-storage write delay, and can be implemented to have the same message delay in the fault-free case as Two-Phase Commit, but it uses more messages. The classic Two-Phase Commit algorithm is obtained as the special F = 0 case of the Paxos Commit algorithm.

It is well known that the consensus problem can be solved in a distributed system if, after some time T/sub S/, no process fails and there is some upper bound /spl delta/ on how long it takes to deliver a message. We know of no existing algorithm that guarantees consensus among N processes before time T/sub S/+O(N/spl delta/). We show that consensus can be achieved by time T/sub S/+O(/spl delta/).

Asynchronous algorithms for implementing a fault-tolerant distributed system, which can make progress despite the failure of any F processors, require 2F + 1 processors. Cheap Paxos, a variant of the Paxos algorithm, guarantees liveness under the additional assumption that the set of nonfaulty processors does not "jump around" too fast, but uses only F + 1 main processors that actually execute the system and F auxiliary processors that are used only to handle the failure of a main processor. The auxiliary processors take part in reconfiguring the system to remove the failed processor, after which they can remain idle until another main processor fails.

TLA (the temporal logic of actions) is a simple logic for describing and reasoning about concurrent systems. It provides a uniform way of specifying algorithms and their correctness properties, as well as rules for proving that one specification satisfies another. TLA+ is a formal specification language based on TLA, and TLC is a model checker for TLA+ specifications. TLA+ and TLC have been used to specify and check high-level descriptions of real, complex systems. Because TLA+ provides the full power of ordinary mathematics, it permits simple, straightforward specifications of the kinds of algorithms presented at PODC.

Most specification languages have a type system. Type systems are hard to get right, and getting them wrong can lead to inconsistencies. Set theory can serve as the basis for a specification language without types. This possibility, which has been widely overlooked, offers many advantages. Untyped set theory is simple and is more flexible than any simple typed formalism. Polymorphism, overloading, and subtyping can make a type system more powerful, but at the cost of increased somplexity, and such refinements can never attain the flexibility of having no types at all. Typed formalisms have advantages, too, stemming from the power of mechanical type checking. While types serve little purpose in hand proofs, they do help with mechanized proofs. In the absence of verificaiton, type checking can catch errors in specifications. It may be possible to have the best of both worlds by adding typing annotations to an untyped specification language. We consider only specification languages, not programming languages.

Recent archaeological discoveries on the island of Paxos reveal that the parliament functioned despite the peripatetic propensity of its part-time legislators. The legislators maintained consistent copies of the parliamentary record, despite their frequent forays from the chamber and the forgetfulness of their messengers. The Paxon parliament's protocol provides a new way of implementing the state machine approach to the design of distributed systems.

A multiprocess program executing on a modern multiprocessor must issue explicit commands to synchronize memory accesses. A method is proposed for deriving the necessary commands from a correctness proof of the underlying algorithm in a formalism based on temporal relations among operation executions.

We show how to specify components of concurrent systems. The specification of a system is the conjunction of its components' specifications. Properties of the system are proved by reasoning about its components. We consider both the decomposition of a given system into parts, and the composition of given parts to form a system.

Predicate-action diagrams, which are similar to standard state-transition diagrams, are precisely defined as formulas of TLA (the Temporal Logic of Actions). We explain how these diagrams can be used to describe aspects of a specification-and those descriptions then proved correct-even when the complete specification cannot be written as a diagram. We also use the diagrams to illustrate proofs.>

We describe a method for writing assumption/guarantee specifications of concurrent systems. We also provide a proof rule for reasoning about the composition of these systems. Specifications are written in TLA (the Temporal Logic of Actions), and all reasoning is performed within the logic. Our proof rule handles internal variables and both safety and liveness properties. 1 Introduction An open system is one that interacts with an environment that neither it nor its implementor controls. To deduce useful properties of a system, we must specify its environment. No system will exhibit its intended behavior in the presence of a su#ciently hostile environment. For example, a combinational circuit will not produce an output in the intended range if some input line, instead of having a 0 or a 1, has an improper voltage level of 1/2. The specification of the circuit's environment must rule out such improper inputs. An open system calls for an assumption/guarantee specification, asserting that...

Abstract Standard mathematical notation works well for short formulas, but not for the longer ones often written by computer scientists. Notations are proposed to make one or two-page formulas easier to read and reason about.

Traditional methods for specifying and reasoning about concurrent systems work for real-time systems. Using TLA (the temporal logic of actions), we illustrate how they work with the examples of a queue and of a mutual-exclusion protocol. In general, two problems must be addressed: avoiding the real-time programming version of Zeno's paradox, and coping with circularities when composing real-time assumption/guarantee specifications. Their solutions rest on properties of machine closure and realizability.

The temporal logic of actions (TLA) is a logic for specifying and reasoning about concurrent systems. Systems and their properties are represented in the same logic, so the assertion that a system meets its specification and the assertion that one system implements another are both expressed by logical implication. TLA is very simple; its syntax and complete formal semantics are summarized in about a page. Yet, TLA is not just a logician's toy; it is extremely powerful, both in principle and in practice. This report introduces TLA and describes how it is used to specify and verify concurrent algorithms. The use of TLA to specify and reason about open systems will be described elsewhere.

A rigorous modular specification method requires a proof rule asserting that if each component behaves correctly in isolation, then it behaves correctly in concert with other components. Such a rule is subtle because a component need behave correctly only when its environment does, and each component is part of the others' environments. We examine the precise distinction between a system and its environment, and provide the requisite proof rule when modules are specified with safety and liveness properties.

As an exercise in synchronization without mutual exclusion, algorithms are developed to implement both a monotonic and a cyclic multiple-word clock that is updated by one process and read by one or more other processes.

Refinement mappings are used to prove that a lower-level specification correctly implements a higher-level one. The authors consider specifications consisting of a state machine (which may be infinite-state) that specifies safety requirements and an arbitrary supplementary property that specifies liveness requirements. A refinement mapping from a lower-level specification S/sub 1/ to higher-level one S/sub 2/ is a mapping from S/sub 1/'s state space to S/sub 2/'s state space that maps steps of S/sub 1/'s state machine steps to steps of S/sub 2/'s state machine and maps behaviors allowed by S/sub 1/ to behaviors allowed by S/sub 2/. It is shown that under reasonable assumptions about the specifications, if S/sub 1/ implements S/sub 2/, then by adding auxiliary variables to S/sub 1/ one can guarantee the existence of a refinement mapping. This provides a completeness result for a practical hierarchical specification method.>

Article Free Access Share on A lattice-structured proof of a minimum spanning Authors: Jennifer L. Welch Laboratory for Computer Science, Massachusetts Institute of Technology Laboratory for Computer Science, Massachusetts Institute of TechnologyView Profile , Leslie Lamport Digital Equipment Corporation, Systems Research Center Digital Equipment Corporation, Systems Research CenterView Profile , Nancy Lynch Laboratory for Computer Science, Massachusetts Institute of Technology Laboratory for Computer Science, Massachusetts Institute of TechnologyView Profile Authors Info & Claims PODC '88: Proceedings of the seventh annual ACM Symposium on Principles of distributed computingJanuary 1988 Pages 28–43https://doi.org/10.1145/62546.62552Published:01 January 1988Publication History 12citation368DownloadsMetricsTotal Citations12Total Downloads368Last 12 Months13Last 6 weeks0 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF

When explicit control predicates rather than dummy variables are used, the Owicki-Gries method for proving safety properties of concurrent programs can be strengthened, making it easier to construct the required program annotations.

A new solution to the mutual exclusion problem is presented that, in the absence of contention, requires only seven memory accesses. It assumes atomic reads and atomic writes to shared registers.

A novel formal theory of concurrent systems that does not assume any atomic operations is introduced. The execution of a concurrent program is modeled as an abstract set of operation executions with two temporal ordering relations: “precedence” and “can causally affect”. A primitive interprocess communication mechanism is then defined. In Part II, the mutual exclusion is expressed precisely in terms of this model, and solutions using the communication mechanism are given.

The theory developed in Part I is used to state the mutual exclusion problem and several additional fairness and failure-tolerance requirements. Four “distributed” N -process solutions are given, ranging from a solution requiring only one communication bit per process that permits individual starvation, to one requiring about N ! communication bits per process that satisfies every reasonable fairness and failure-tolerance requirement that we can conceive of.

The formal correspondence between an implementation and its specification is examined. It is shown that existing specifications that claim to describe priority are either vacuous or else too restrictive to be implemented in some reasonable situations. This is illustrated with a precisely formulated problem of specifying a first-come-first-served mutual exclusion algorithm, which it is claimed cannot be solved by existing methods.

A constraint is a relation among program variables that is maintained throughout execution. Type declarations and a very general form of aliasing can be expressed as constraints. A proof system based upon the interpretation of Hoare triples as temporal logic formulas is given for reasoning about programs with constraints. The proof system is shown to be sound and relatively complete, and example program proofs are given.

Algorithms are described for maintaining clock synchrony in a distributed multiprocess system where each process has its own clock. These algorithms work in the presence of arbitrary clock or process failures, including “two-faced clocks” that present different values to different processes. Two of the algorithms require that fewer than one-third of the processes be faulty. A third algorithm works if fewer than half the processes are faulty, but requires digital signatures.

This paper presents an algorithm by which a process in a distributed system determines a global state of the system during a computation. Many problems in distributed systems can be cast in terms of the problem of detecting global states. For instance, the global state detection algorithm helps to solve an important class of problems: stable property detection. A stable property is one that persists: once a stable property becomes true it remains true thereafter. Examples of stable properties are “computation has terminated,” “ the system is deadlocked” and “all tokens in a token ring have disappeared.” The stable property detection problem is that of devising algorithms to detect a given stable property. Global state detection can also be used for checkpointing.

This is an edited transcript of a talk given at last year's conference. To preserve the flavor of the talk and the questions, I have done very little editing—mostly eliminating superfluous words and phrases, correcting especially atrocious grammar, and making the obvious changes needed when replacing slides by figures. The tape recorder was not functioning for the first few minutes, so I had to recreate the beginning of the talk.

An informal description is given of three fault-tolerant clock-synchronization algorithms. These algorithms work in the presence of arbitrary kinds of failure, including “two-faced” clocks. Two of the algorithms are derived from Byzantine Generals solutions.

A general method is described for implementing a distributed system with any desired degree of faulttolerance.Instead of relying upon explicit timeouts, processes execute a simple clock-driven algorithm.Reliable clock synchronization and a solution to the Byzantine Generals Problem are assumed.

Generalized Hoare Logic is a formal logical system for deriving invariance properties of programs.It provides a uniform way to describe a variety of methods for reasoning about concurrent programs, including noninterference, satisfaction, and cooperation proofs.We describe a simple recta-rule of the Generalized Hoare Logic--the Decomposition Principle--and show how all these methods can be derived using it.

A method is presented that permits assertional reasoning about a concurrent program even though the atomicity of the elementary operations is left unspecified. It is based upon a generalization of the dynamic logic operator [α]. The method is illustrated by verifying the mutual exclusion property for a two-process version of the bakery algorithm.

The Byzantine Generals Problem requires processes to reach agreement upon a value even though some of them may fad.It is weakened by allowing them to agree upon an "incorrect" value if a failure occurs.The transaction eormmt problem for a distributed database Js a special case of the weaker problem.It is shown that, like the original Byzantine Generals Problem, the weak version can be solved only ff fewer than one-third of the processes may fad.Unlike the onginal problem, an approximate solution exists that can tolerate arbaranly many failures.

Concurrent Program ModulesA method for specifying program modules in a concurrent program is described.It is based upon temporal logic, but uses new kinds of temporal assertions to make the specifications simpler and easier to understand.The semantics of the specifications is described informally, and a sequence of examples are given culminating in a specification of three modules comprising the alternating-bit communication protocol.A formal semantics is given in the appendix.

Reliable computer systems must handle malfunctioning components that give conflicting information to different parts of the system.This situation can be expressed abstractly in terms of a group of generals of the Byzantine army camped with their troops around an enemy city.Communicating only by messenger, the generals must agree upon a common battle plan.However, one or more of them may be traitors who will try to confuse the others.The problem is to find an algorithm to ensure that the loyal generals will reach agreement.It is shown that, using only oral messages, this problem is solvable if and only if more than two-thirds of the generals are loyal; so a single traitor can confound two loyal generals.With unforgeable written messages, the problem is solvable for any number of generals and possible traitors.Applications of the solutions to reliable computer systems are then discussed.

A liveness property asserts that program execution eventually reaches some desirable state.While termination has been studied extensively, many other liveness properties are important for concurrent programs.A formal proof method, based on temporal logic, for deriving liveness properties is presented.It allows a rigorous formulation of simple informal arguments.How to reason with temporal logic and how to use safety (invariance) properties in proving liveness is shown.The method is illustrated using, first, a simple programming language without synchronization primitives, then one with semaphores.However, it is applicable to any programming language.

Pnueli [15] has recently introduced the idea of using temporal logic [18] as the logical basis for proving correctness properties of concurrent programs. This has permitted an elegant unifying formulation of previous proof methods. In this paper, we attempt to clarify the logical foundations of the application of temporal logic to concurrent programs. In doing so, we will also clarify the relation between concurrency and nondeterminism, and identify some problems for further research.In this paper, we consider logics containing the temporal operators "henceforth" (or "always") and "eventually" (or "sometime"). We define the semantics of such a temporal logic in terms of an underlying model that abstracts the fundamental concepts common to almost all the models of computation which have been used. We are concerned mainly with the semantics of temporal logic, and will not discuss in any detail the actual rules for deducing theorems.We will describe two different temporal logics for reasoning about a computational model. The same formulas appear in both logics, but they are interpreted differently. The two interpretations correspond to two different ways of viewing time: as a continually branching set of possibilities, or as a single linear sequence of actual events. The temporal concepts of "sometime" and "not never" ("not always not") are equivalent in the theory of linear time, but not in the theory of branching time -- hence, our title. We will argue that the logic of linear time is better for reasoning about concurrent programs, and the logic of branching time is better for reasoning about nondeterministic programs.The logic of linear time was used by Pnueli in [15], while the logic of branching time seems to be the one used by most computer scientists for reasoning about temporal concepts. We have found this to cause some confusion among our colleagues, so one of our goals has been to clarify the formal foundations of Pnueli's work.The following section gives an intuitive discussion of temporal logic, and Section 3 formally defines the semantics of the two temporal logics. In Section 4, we prove that the two temporal logics are not equivalent, and discuss their differences. Section 5 discusses the problems of validity and completeness for the temporal logics. In Section 6, we show that there are some important properties of the computational model that cannot be expressed with the temporal operators "henceforth" and "eventually", and define more general operators.

The problem addressed here concerns a set of isolated processors, some unknown subset of which may be faulty, that communicate only by means of two-party messages. Each nonfaulty processor has a private value of information that must be communicated to each other nonfaulty processor. Nonfaulty processors always communicate honestly, whereas faulty processors may lie. The problem is to devise an algorithm in which processors communicate their own values and relay values received from others that allows each nonfaulty processor to infer a value for each other processor. The value inferred for a nonfaulty processor must be that processor's private value, and the value inferred for a faulty one must be consistent with the corresponding value inferred by each other nonfaulty processor. It is shown that the problem is solvable for, and only for, n ≥ 3 m + 1, where m is the number of faulty processors and n is the total number. It is also shown that if faulty processors can refuse to pass on information but cannot falsely relay information, the problem is solvable for arbitrary n ≥ m ≥ 0. This weaker assumption can be approximated in practice using cryptographic methods.

Many large sequential computers execute operations in a different order than is specified by the program. A correct execution is achieved if the results produced are the same as would be produced by executing the program steps in order. For a multiprocessor computer, such a correct execution by each processor does not guarantee the correct execution of the entire program. Additional conditions are given which do guarantee that a computer correctly executes multiprocess programs.

A new, nonassertional approach to proving multiprocess program correctness is described by proving the correctness of a new algorithm to solve the mutual exclusion problem. The algorithm is an improved version of the bakery algorithm. It is specified and proved correct without being decomposed into indivisible, atomic operations. This allows two different implementations for a conventional, nondistributed system. Moreover, the approach provides a sufficiently general specification of the algorithm to allow nontrivial implementations for a distributed system as well.

The inductive assertion method is generalized to permit formal, machine-verifiable proofs of correctness for multiprocess programs. Individual processes are represented by ordinary flowcharts, and no special synchronization mechanisms are assumed, so the method can be applied to a large class of multiprocess programs. A correctness proof can be designed together with the program by a hierarchical process of stepwise refinement, making the method practical for larger programs. The resulting proofs tend to be natural formalizations of the informal proofs that are now used.