On interprocess communication
Distributed ComputingPublished 1 June 1986
Leslie Lamport
Citations841
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
In Part II, the formalism is used to specify several classes of interprocess communication mechanisms and to prove the correctness of algorithms for implementing them.
Abstract
A formalism for specifying and reasoning about concurrent systems is described. Unlike more conventional formalisms, it is not based upon atomic actions. A definition of what it means for one system to implement a higher-level system is given and justified. In Part II, the formalism is used to specify several classes of interprocess communication mechanisms and to prove the correctness of algorithms for implementing them.
Keywords
Computer Science
Communications of the ACMTime, clocks, and the ordering of events in a distributed system
8,437 Citations1978Leslie Lamport
A distributed algorithm is given for synchronizing a system of logical clocks which can be used to totally order the events, and a bound is derived on how far out of synchrony the clocks can become.
The temporal logic of programs
5,586 Citations1977Amir Pnueli
A unified approach to program verification is suggested, which applies to both sequential and parallel programs, and the main proof method is that of temporal reasoning in which the time dependence of events is the basic concept.
ACM Computing SurveysConcurrency Control in Distributed Database Systems
1,165 Citations1981Philip A. Bernstein, Nathan Goodman
This paper describes a decomposition of the concurrency control problem into two major subproblems: read-write and write-write synchronization, and describes a series of synchromzation techniques for solving each subproblem and how to combine these techniques into algorithms for solving the entire conccurrency control problem.
Communications of the ACMConcurrent control with “readers” and “writers”
527 Citations1971Pierre Courtois, F. Heymans +1 more
Distributed ComputingOn interprocess communication
307 Citations1986Leslie Lamport
The formalism developed in Part I is used in proving the correctness of several constructions given for implementing one class of register with a weaker class in Interprocess communication.
Communications of the ACMConcurrent reading and writing
280 Citations1977Leslie Lamport
Two general theorems are proved, and some algorithms are presented to illustrate their use, including a solution to the general problem in which a read is repeated if it might have obtained an incorrect result, and two techniques for transmitting messages between processes.
Journal of the ACMThe mutual exclusion problem
231 Citations1986Leslie Lamport
The theory developed in Part I is used to state the mutual exclusion problem and several additional fairness and failure-tolerance requirements, and four “distributed” N-process solutions are given.
ACM Transactions on Programming Languages and SystemsConcurrent Reading While Writing
171 Citations1983Gary L. Peterson
The problem of asynchronous processes reading shared data while the data are being modified by another process is considered and the number of copies used by all algorithms is shown to be the best possible.
ACM Transactions on Programming Languages and SystemsAxioms for memory access in asynchronous hardware systems
134 Citations1986Jayadev Misra
ACM Transactions on Programming Languages and SystemsA New Approach to Proving the Correctness of Multiprocess Programs
84 Citations1979Leslie Lamport
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, an improved version of the bakery algorithm, specified and proved correct without being decomposed into indivisible, atomic operations.
Lecture notes in computer scienceSemantics of concurrent systems: A modular fixed-point trace approach
54 Citations1985Antoni Mazurkiewicz
A method for finding the set of processes generated by a concurrent system (the behaviour of a system) in modular way is presented and the fixed point method of describing sets of processes is extensively applied, with processes regarded as traces rather than strings of actions.
What it means for a concurrent program to satisfy a specification
39 Citations1985Leslie Lamport
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.