Abstract
Computations in distributed systems can be described in terms of actions in which one or more processes synchronize by common handshakes. A general formulation for such action systems is given, together with two interleaved execution models: a serial model that allows simple temporal reasoning, and a concurrent model that reflects a distributed execution environment more faithfully. The equivalence of the two models is shown, up to fairness properties. The relationships between the natural fairness and justice notions in the two models are analyzed. This leads to sufficient conditions under which reasoning in terms of the serial model is valid even when the execution environment guarantees the weaker properties of the concurrent model only. Proving that these conditions hold for a particular system can be carried out totally within the simpler serial model. Finally, the results are discussed from the point of view of partial order computations.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
Ada Programming Language. American National Standards Institute, Inc., ANSI/MIL-STD-1815-A-1983, 1983.
Apt, K. R., Correctness proofs of distributed termination algorithms. In Advanced NATO Seminar on Logics and Models for Verification and Specification of Concurrent Systems. INRIA, 1984.
Apt, K. R., N. Francez, and S. Katz, Appraising fairness in languages for distributed programming. In 14th ACM Conference on Principles of Programming Languages, 1987, 189–198.
Attie, P., and N. Francez, Fairness and hyperfairness in multi-party interactions. Manuscript 1988.
Back, R. J. R., Refining atomicity in parallel algorithms. Manuscript 1988.
Back, R. J. R., E. Hartikainen, and R. Kurki-Suonio, Multi-process handshaking on local area networks. Åbo Akademi, Department of Information Processing, Report 42, 1985.
Back, R. J. R., and R. Kurki-Suonio, Decentralization of process nets with a centralized control. In 2nd ACM SIGACT-SIGOPS Symp. on Principles of Distributed Computing, 1983, 131–142.
Back, R. J. R., and R. Kurki-Suonio, A case study in constructing distributed algorithms: distributed exchange sort. In Proc. Winter School on Theoretical Computer Science, Finnish Society of Information Processing Science 1984, 1–33.
Back, R. J. R., and R. Kurki-Suonio, Co-operation in distributed systems using symmetric multiprocess handshaking. Åbo Akademi, Department of Information Processing, Report A 34, 1984.
Back, R. J. R., and R. Kurki-Suonio, Serializability in distributed systems with handshaking. Carnegie-Mellon University, Report CMU-CS-85-109, 1985.
Back, R. J. R., and R. Kurki-Suonio, A new paradigm for the design of concurrent systems. Ada Letters VII, 6, 1987, 110–112.
Back, R. J. R., and R. Kurki-Suonio, Distributed Co-operation with Action Systems. Åbo Akademi, Department of Information Processing, Report A 56, 1987. A revised version of [BK84b], submitted for publication.
Chandy, K. M., and J. Misra, An example of stepwise refinement of distributed programs: quiescence detection. ACM Trans. Programming Languages and Systems 8, 3, 1986, 326–343.
Chandy, K. M., and J. Misra, A Foundation of Parallel Program Design. Addison-Wesley 1988.
Dijkstra, E. W., Hierarchical ordering of sequential processes. In Operating Systems Techniques, eds. C. A. R. Hoare and R. H. Perrott, Academic Press 1972.
Francez, N., Fairness. Springer-Verlag 1986.
Grumberg, O., N. Francez, and S. Katz, Fair termination of communicating processes. In 3rd ACM SIGACT-SIGOPS Symp. on Principles of Distributed Computing, 1984, 254–265.
Hoare, C. A. R., Communicating sequential processes. Communications of the ACM 21, 8, August 1978, 666–677. Reprinted in Communications of the ACM 26, 1, January 1983, 100–106.
Kuiper, R., and W. P. de Roever, Fairness assumptions for CSP in a temporal logic framework. In Formal Description of Programming Concepts-II, ed. Dines Bjørner, North-Holland 1983, 159–167.
Kurki-Suonio, R., and T. Kankaanpää, On the design of reactive systems. Manuscript submitted for publication, 1987.
Lamport, L., Time, clocks, and ordering of events in a distributed system. Communications of the ACM 21, July 1978, 558–565.
Manna, Z., and A. Pnueli, How to cook a temporal proof system for your pet language. In Tenth ACM Conference on Principles of Programming Languages, 1983, 141–154.
Reisig, W., Partial order semantics versus interleaving semantics for CSP-like languages and its impact on fairness. In Automata, Languages and Programming, ed. J. Paredaens, Lecture Notes in Computer Science 172, Springer-Verlag 1984, 403–413.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1988 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Back, R.J.R., Kurki-Suonio, R. (1988). Serializability in distributed systems with handshaking. In: Lepistö, T., Salomaa, A. (eds) Automata, Languages and Programming. ICALP 1988. Lecture Notes in Computer Science, vol 317. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-19488-6_106
Download citation
DOI: https://doi.org/10.1007/3-540-19488-6_106
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-19488-0
Online ISBN: 978-3-540-39291-0
eBook Packages: Springer Book Archive