Defining Conditional Independence Using Collapses
Workshops in computingPublished 1 January 1990
Shmuel Katz, Doron Peled
Citations12
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.
Abstract
Trace semantics is extended to allow conditional commutativity among operations. Conditional commutativity is obtained by identifying the context (the set of global states) in which operations are commutative using special predicates. These will allow collapsing execution histories into equivalence classes of conditional traces. Using this approach, it is possible that the execution of two operations will be dependent in one context and independent in another. The predicates allow defining a family of possible semantic definitions for each language, where each is an extension of previous standard definitions. Examples are shown when such a semantics is desired. As an example of an application, a proof method for total correctness is introduced.
Keywords
Computer Science
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.
Acta InformaticaAn axiomatic proof technique for parallel programs I
1,022 Citations1976Susan Owicki, David Gries
Hoare's deductive system for proving partial correctness of sequential programs is extended to include the parallelism described by the language, and the proof method lends insight into how one should understand and present parallel programs.
IEEE Transactions on Electronic ComputersAnalysis of Programs for Parallel Processing
424 Citations1966A. J. Bernstein
A set of conditions are described which determine whether or not two successive portions of a given program can be performed in parallel and still produce the same results.
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.
Science of Computer ProgrammingAdequate proof principles for invariance and liveness properties of concurrent programs
148 Citations1984Zohar Manna, Amir Pnueli
This paper presents proof principles for establishing invariance and liveness properties of concurrent programs based on ''well-founded asserations'' and are applicable to both "just" and "fair" computations.
Journal of Computer and System SciencesProving assertions about parallel programs
143 Citations1975E. A. Ashcroft
A simple but general parallel programming language is considered, and a program simulating an elementary airline reservation system is given, and several properties of the program are demonstrated using the technique.
Interleaving set temporal logic
50 Citations1987Shmuel Katz, Doron Peled
A new temporal logic and interpretation are suggested which have features from linear temporal Logic, branching time temporal logic, and partial order temporal logic which can describe properties essential to the specification and correctness proofs of distributed algorithms such as those for global snapshots.
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.
Lecture notes in computer scienceModeling concurrency by partial orders and nonlinear transition systems
23 Citations1989Haim Gaifman
The avoidance of deadlock by an implementation can be defined and proved, and formally what it means for an implementation to involve loss of parallelism shows in the form of extra order constraints that have to be added to core members of the original process.
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.