Verification of distributed programs using representative interleaving sequences
Distributed ComputingPublished 1 September 1992
Shmuel Katz, Doron Peled
Citations74
SJR quartileQ1
SJR score0.81
SNIP1.21
Generate an AI Snapshot to get a quick, structured summary of this paper.
Study Snapshot
ObjectiveStudy objective
MethodsResearch methodology
PopulationPopulation studied
Sample sizeSample sizes
OutcomesStudy outcomes here
ResultsStudy results comes here
LimitationsResearch study limitations comes here
A concise AI-generated summary of the paper will appear here once you click Generate AI Snapshot.
TL;DR
A formal proof method for distributed programs that explicitly identifies equivalence classes of execution sequences which are equivalent up to permuting commutative operations using the temporal logic ISTL.
Abstract
We present a formal proof method for distributed programs. The semantics used to justify the proof method explicitly identifies equivalence classes of execution sequences which are equivalent up to permuting commutative operations. Each equivalence class is called an interleaving set or a run. The proof rules allow concluding the correctness of certain classes of properties for all execution sequences, even though such properties are demonstrated directly only for a subset of the sequences. The subset used must include a representative sequence from each interleaving set, and the proof rules, when applicable, guarantee that this is the case. By choosing a subset with appropriate sequences, simpler intermediate assertions can be used than in previous formal approaches. The method employs proof lattices, and is expressed using the temporal logic ISTL.
Keywords
Computer Science
ACM Transactions on Computer SystemsDistributed snapshots
2,439 Citations1985K. Mani Chandy, Leslie Lamport
Kommunikation mit Automaten
2,078 Citations1962C. A. Petri
The theory of automata is shown not capable of representing the actual physical flow of information in the solution of a recursive problem and a theory of communication is proposed that yields a means of representation that with equal rigor and simplicity accomplishes more than the theory of synchronous automata.
Communications of the ACMGuarded commands, nondeterminacy and formal derivation of programs
1,926 Citations1975Edsger W. Dijkstra
So-called “guarded commands” are introduced as a building block for alternative and repetitive constructs that allow nondeterministic program components for which at least the activity evoked, but possibly even the final state, is not necessarily uniquely determined by the initial state.
Information Processing LettersDefining liveness
1,025 Citations1985Bowen Alpern, Fred B. Schneider
A formal definition for liveness properties is proposed, and every property is shown to be the intersection of a safety property and a liveness property.
Journal of the ACM“Sometimes” and “not never” revisited
996 Citations1986E. Allen Emerson, Joseph Y. Halpern
A language, CTL*, in which a universal or existential path quantifier can prefix an arbitrary linear time assertion, is defined and the expressive power of a number of sublanguages is compared.
ACM Transactions on Programming Languages and SystemsProving Liveness Properties of Concurrent Programs
583 Citations1982Susan Owicki, Leslie Lamport
A formal proof method, based on temporal logic, for deriving liveness properties is presented, which allows a rigorous formulation of simple informal arguments and how to reason with temporal logic and use safety (invariance) properties in proving liveness is shown.
Formal Methods in System DesignA stubborn attack on state explosion
572 Citations1992Antti Valmari
The LTL-preserving stubborn set method is presented for reducing the amount of work needed in the automatic verification of concurrent systems with respect to linear-time temporal logic specifications.
Lecture notes in computer scienceStubborn sets for reduced state space generation
542 Citations1991Antti Valmari
The “stubborn set” theory and method for generating reduced state spaces and a more advanced version suited to the analysis of properties of reactive systems is developed.
ACM Transactions on Programming Languages and SystemsA Proof System for Communicating Sequential Processes
324 Citations1980Krzysztof R. Apt, Nissim Francez +1 more
An axiomatic proof system is presented for proving partial correctness and absence of deadlock of communicating sequential processes, the key (meta) rule introduces cooperation between proofs, and CSP's new convention for distributed termination of loops is dealt with.
Verification of Concurrent Programs. Part I. The Temporal Framework,
323 Citations1981Zohar Manna, Amir Pnueli
The temporal formalism is introduced as a tool for reasoning about sequences of states and the set of interesting properties is classified into invariance (safety), eventuality (liveness, and precedence) properties.
Lecture notes in computer scienceImpartiality, justice and fairness: The ethics of concurrent termination
283 Citations1981Daniel Lehmann, Amir Pnueli +1 more
The method of well founded structures for proving termination of programs is extended to concurrent programs and different versions of fairness are introduced: Impartiality, Fairness and Justice.
How to cook a temporal proof system for your pet language
219 Citations1983Zohar Manna, Amir Pnueli
An abstract temporal proof system is presented whose program-dependent part has a high-level interface with the programming language actually studied, and is shown to be relatively complete with respect to pure first-order temporal logic.
Theoretical Computer ScienceCompleting the temporal picture
218 Citations1991Zohar Manna, Amir Pnueli
Science of Computer ProgrammingDecomposition of distributed programs into communication-closed layers
206 Citations1982Tzilla Elrad, Nissim Francez
The safe decomposition of a distributed program into communication closed layers is suggested as a superstructure of its decomposition into a collection of communicating processes.
Distributed ComputingAppraising fairness in languages for distributed programming
153 Citations1988Krzysztof R. Apt, Nissim Francez +1 more
The relations among various languages and models for distributed computation and various possible definitions of fairness are considered, and natural semantic criteria are presented which an acceptable notion of fairness should satisfy.
Theoretical Computer ScienceDefining conditional independence using collapses
119 Citations1992Shmuel Katz, Doron Peled
Abstract Trace semantics is extended to allow conditional commutativity among operations to define a family of possible semantic definitions for each language, where each is an extension of previous standard definitions.
Lecture notes in computer scienceVerification of concurrent programs: Temporal proof principles
90 Citations2005Zohar Manna, Amir Pnueli
This paper presents proof methods for establishing invariance (safety) and eventuality (liveness) properties of temporal logic in concurrent programs.
Theoretical Computer ScienceAlternative semantics for temporal logics
78 Citations1983E. Allen Emerson
This paper shows that each of the first three constraints on the allowable sets of computation paths can be independent of the others, and their conjunction is precisely equivalent to the fourth constraint.
Information and ControlA proof rule for fair termination of guarded commands
78 Citations1985Orna Grümberg, Nissim Francez +2 more
A proof rule for fairly terminating guarded commands based on a well-foundedness argument that is applied to several examples, and proved to be sound and (semantically) complete w.r.t. an operational semantics of computation trees.
Munich Personal RePEc Archive (Ludwig Maximilian University of Munich)Decidability and expressiveness of logics of processes
62 Citations1980Karl Abrahamson
It is shown that PDL is decidable only when processes are tree-like, in Parikh's sense, and that extending PDL by a concurrency operator, a global invariance operator and flowgraph programs, among others, adds no expressive power to PDL.
Understanding and verifying distributed algorithms using stratified decomposition
50 Citations1988Ching Tsun Chou, Eli Gafni
This paper provides firm theoretical ground for temporal ordering in describing the behavior of algorithms-statements like “after A, task B is performed” in the absence of an explicit termination detection for A built into the algorithm.
Lecture notes in computer scienceAn efficient verification method for parallel and distributed programs
47 Citations1989Shmuel Katz, Doron Peled
A formal proof method based on a partial order semantics for parallel or distributed programs which allows concluding the correctness of certain classes of properties for all execution sequences, even though the property is only demonstrated directly for a subset of the execution sequences.
Formal Aspects of ComputingEvent fairness and non-interleaving concurrency
42 Citations1989Marta Kwiatkowska
A class of generalised notions of (weak, strong and unconditional) event fairness relative to progress requirements is derived and the weakest fairness notion in this class is shown to coincide with maximality with respect to the partial order over traces.
Lecture notes in computer scienceTemporal logic and causality in concurrent systems
34 Citations1988Wolfgang Reisig
A logic for detached runs is introduced, tailored for causality based partial order semantics of non-sequential systems, which resembles the purposes of Linear Time Temporal Logic for Interleavings.
OPAL (Open@LaTrobe) (La Trobe University)Fairness for non-interleaving concurrency
33 Citations1989Marta Kwiatkowska
A topological characterization of behavioural properties which includes safety, progress and fairness properties has been provided in a non-interleaving semantic model for concurrency.
A Temporal Logic for Event Structures
31 Citations1990Wojciech Penczek
In this formalism, operators representing the relations of causality and conflict are incorporated, which deals only with local states of a distributed system (program).
Lecture notes in computer scienceDesigning distributed algorithms by means of formal sequentially phased reasoning
28 Citations1989Frank Stomp, Willem P. de Roever
The design principle, formulated using Manna and Pnueli's linear time temporal logic, is applicable to large classes of algorithms, such as those for minimum-path, connectivity, network flow, and minimum-weight spanning trees.
Lecture notes in computer scienceProving partial order liveness properties
27 Citations2005Doron Peled, Amir Pnueli
A temporal verification method which is based upon partial order semantics of traces [31] is presented and can express the distributed nature of a program.
Lecture notes in computer sciencePartial ordering derivations for CCS
27 Citations1985Pierpaolo Degano, Rocco De Nicola +1 more
This paper extends CCS transitions, labelled by strings, to concurrent histories, i.e. to transitions labelled by partial orderings, by a theorem which shows that the strings can be obtained by taking all interleavings compatible with the partial ordering.
Specifying and proving serializability in temporal logic
18 Citations2002Doron Peled, Shmuel Katz +1 more
A formal verification system for serializability that uses classical logic reasoning is provided and Serializability for the multiversion-timestamp algorithm is verified.
Lecture notes in computer scienceCompleting the temporal picture
18 Citations1989Zohar Manna, Amir Pnueli
The presented proof system is based on the classification of temporal properties according to the Borel hierarchy, providing an appropriate proof rule for each of the main classes, such as safety, response, and progress properties.
Workshops in computingDefining Conditional Independence Using Collapses
12 Citations1990Shmuel Katz, Doron Peled
Lecture notes in computer scienceTowards a theory of simulation for verification of concurrent systems
11 Citations1989Ryszard Janicki, Maciej Koutny
It is shown that under some conditions the simulation provides a sufficient information to reason about a number of interesting properties of the system, and there always exists a simulation which provides the required behavioural information and involves a minimal computational effort.