Ambuj K. Singh
Abstract
Concurrency in distributed systems is usually modeled by a nondeterministic interleaving of atomic events. The consequences of this interleaving (or global time) assumption on the specifications and proofs of distributed programs are examined in this paper. A construction for atomic registers is presented; this construction has the surprising property that it is correct with respect to a specification based on partial orders but is incorrect with respect to a naively derived specification based on global time.
- 1 AHAMAD, M., BURNS, J. E., HUTTO, P. W., AND NEIGER, G. Causal memory. In Proceedings of the Fifth International Workshop on Distributed Algorithms. Lecture Notes in Computer Science, P. Spirakis and S. Toueg, Eds., (1991), in press. Google Scholar
Digital Library
- 2 ANGER, F.D. On Lamport's interprocessor communication model. ACM Trans. Program. Lang. Syst. 11, 3 (July 1989), 404-417. Google ScholarDigital Library
- 3 BEN-DAVID, S. The global time assumption and semantics for concurrent systems. In Proceedings of the Seventh Annual Symposium on Principles of Distributed Computing (Toronto, Aug. 5-7, 1988). pp. 223-230. Google ScholarDigital Library
- 4 BLOOM, B. Constructing two-writer atomic registers. IEEE Trans. Comput. 37, 12 (1988), 1506-1514. Also in Proceedings of the Sixth Annual Symposium on Principles of Distributed Computing (Vancouver, Aug. 10-12, 1987), pp. 249-259. Google ScholarDigital Library
- 5 BURNS, J E., AND PETERSON, G. Constructing multi-reader atomic values from non-atomic values. In Proceedings of the Sixth Annual Symposium on Principle of Distributed Computing (Vancouver, Aug. 10-12, 1987), pp. 222-231. Google ScholarDigital Library
- 6 HERLIHY, M., AND WING, J Linearizability: a correctness condition for concurrent objects. ACM Trans. Program. Lang Syst. 12.3 (July 1990), ~63-~92. Google ScholarDigital Library
- 7 KATZ, S., AND PELED, D. Interleaving set temporal logic In Proceedings of the Seventh Annual Symposium on Principles of Distributed Computing (Toronto, Aug. 15-17, 1988), pp. 178-190. Google ScholarDigital Library
- 8 LAMPORT, L. How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Comput. 28, 9 (Sept. 1979), 690-691Google Scholar
- 9 LAMPORT, L. On interprocess communication, parts I and II. Distr~b. Comput. 1, 2 (Apr. 1986), 77-101.Google ScholarCross Ref
- 10 MIS~A, J. Axioms for memory access in asynchronous hardware systems. A CM Trans. Program. Lang. Syst. 8, 1 (Jan. 1986), 142-153. Google ScholarDigital Library
- 11 NEWMAN-WOLFE, R. A protocol for wait-free, atomic, multi-reader shared variables. In Proceedings of the Sixth Annual Symposium on Principles of Distributed Computing (Vancouver, Aug. 10-12, 1987), pp. 232-248. Google ScholarDigital Library
- 12 PRATT, V. Modeling concurrency by partial orders. Int. J. Parallel Program. 15, 1 (Feb. 1986), 33-71. Google ScholarDigital Library
- 13 SINGH, A., ANDERSON, J., AND GOUDA, M. The elusive atomic register revisited. In Proceedings of the Sixth Annual Symposium on Principles of Distributed Computing (Vancouver, Aug. 10-12, 1987), pp. 206-221. Google ScholarDigital Library
- 14 VITANYI, P., AND AWERBUCH, B. Atomic shared register access by asynchronous hardware. In Proceedings of the 27 th Annual Symposium on Foundations of Computer Science (Toronto, Oct. 27-29, 1986), pp. 233-243.Google ScholarDigital Library
Index Terms
- On reasoning with the global time assumption
Recommendations
Bounded Concurrent Time-Stamping
We introduce concurrent time-stamping, a paradigm that allows processes to temporally order concurrent events in an asynchronous shared-memory system. Concurrent time-stamp systems are powerful tools for concurrency control, serving as the basis for ...
A criterion for atomicity
AbstractMost proof methods for reasoning about concurrent programs are based upon theinterleaving semantics of concurrent computation: a concurrent program is executed in a stepwise fashion, with only one enabled action being executed at each step. ...
A multiversion transaction scheduler for centralized multilevel secure database systems
HASE '96: Proceedings of the 1996 High-Assurance Systems Engineering WorkshopTransactions are vital for multilevel secure database management systems (MLS/DBMSs) because they provide transparency to concurrency and failure. Concurrent execution of transactions may lead to contention among subjects for access to data. In MLS/...
Reviews
Jorgen Staunstrup
An important aspect of defining the semantics of concurrent computations is discussed. Two definitions are contrasted: one is based on a partial ordering of the concurrent operations, the other on interleaving (effectively yielding a total order). Singh shows that the two types of definitions are inherently different, by providing an example of a specification and an implementation that are correct by the partial order semantics, but not by the interleaving semantics. The example is an atomic register along the lines introduced by L. Lamport. The example is supported by a detailed proof occupying six pages of the paper. Some theoretical background is needed to follow this proof, but the paper is self-contained, and detailed knowledge of the papers on atomic register constructions is not required.
Access critical reviews of Computing literature here
Become a reviewer for Computing Reviews.
Comments