Summary
Joint actions are introduced as a language basis for operational specification of reactive systems. Joint action systems are closed systems with no communication primitives. Their nondeterministic execution model is based on multi-party actions without an explicit control flow, and they are amenable for stepwise derivation by superposition. The approach is demonstrated by deriving a specification for serializable databases in simple derivation steps. Two different implementation strategies are imposed on this as further derivations. One of the strategies is two-phase locking, for which a separate implementation is given and proved correct. The other is multiversion timestamp ordering, for which the derivation itself is an implementation.
Similar content being viewed by others
References
Abadi M, Lamport L: The existence of refinement mappings. Theor Computer Sci 82(2):253–284 (1991)
Alpern B, Schneider FB: Defining liveness. Inf Process Lett 21(4): 181–185 (1985)
Back RJR: Refining atomicity in parallel algorithms. In: Odijk E, Rem M, Syre J-C (eds) PARLE '89 Parallel architectures and languages europe, LNCS vol 366 Springer, Berlin Heidelberg New York 1989, pp 199–216
Back RJR: Refinement calculus II: parallel and reactive programs. In: de Bakker JW, de Roever W-P, Rozenberg G (eds) Stepwise refinement of distributed systems: models, formalisms, correctness, LNCS vol. 430 Springer, Berlin Heidelberg New York 1990, pp 67–93
Back RJR, Hartikainen E, Kurki-Suonio R: Multi-process handshaking on broadcasting networks. Reports in Computer Science 42, Åbo Akademi 1985
Back RJR, Kurki-Suonio R: Decentralization of process nets with a centralized control. Distrib Comput 3: 73–87 (1989). An earlier version in 2nd ACM SIGACT-SIGOPS Symposium on Principles of Distributed Computing, Montreal, Canada, August 1983, pp 131–142
Back RJR, Kurki-Suonio R: A case study in constructing distributed algorithms: distributed exchange sort. In: Back RJR, Mannila H, Räihä K-J, Ukkonen E (eds) Proceedings Winter School on Theoretical Computer Science. Finnish Society of Information Processing Science 1984, pp 1–33
Back RJR, Kurki-Suonio R: Serializability in distributed systems with handshaking. In: Lepistö T, Salomaa A (eds) Automata, languages and programming LNCS vol 317. Springer, Berlin Heidelberg New York 1988, pp 52–66
Back RJR, Kurki-Suonio R: Distributed cooperation with action systems. ACM Trans Program Lang Syst 10, (4): 513–554 (1988)
Balzer R, Goldman N: Principles of good software specification and their implications for specification languages. Specification of Reliable Software, IEEE Computer Society 1979, pp 58–67
Bernstein P, Hadzilacos V, Goodman N: Concurrency control and recovery in database systems. Addison-Wesley, 1986
Bolognesi T, Brinksma E: Introduction to the ISO specification language LOTOS. Comput Networks and ISDN Syst 14: 25–59 (1987)
Bougé L, Francez N: A compositional approach to superimposition. Proceedings 15th ACM Symposium on Principles of Programming Languages, San Diego, California 1988, pp 240–249
Chandy KM, Misra J: Parallel program design: a foundation. Addison-Wesley, 1988
Dijkstra EW: A discipline of programming. Prentice-Hall, 1976
Dijkstra EW, Scholten CS: Termination detection for diffusing computations. Inf Proces Lett 11(1): 1–4 (1980)
Eswaran KP, Gray JN, Lorie RA, Traiger IL: The notions of consistency and predicate locks in a database system. Commun ACM 19(11): 624–633 (1976)
Feather MS: Language support for the specification and development of composite systems. ACM Trans Program Lang Syst 9(2): 198–234 (1987)
Harel D: Statecharts: a visual formalism for complex systems. Sci Comp Program 8: 231–274 (1987)
Hoare CAR: Communicating sequential processes. Prentice-Hall, 1985
Järvinen H-M, Kurki-Suonio R: The DisCo language. Tampere University of Technology, Software Systems Laboratory, Report 8, 1990
Järvinen H-M, Kurki-Suonio R, Sakkinen M, Systä K: Object-oriented specification of reactive systems. Proceedings 12th International Conference on Software Engineering, Nice, France, IEEE Computer Society Press, 1990 pp 63–71
Katz S: A superimposition control construct for distributed systems. Microelectronics and Computer Technology Corporation, Report STP-268-87, August 1987
Kurki-Suonio R, Järvinen H-M: Action system approach to the specification and design of distributed systems. Proceedings Fifth International Workshop on Software Specification and Design. ACM Software Engineering Notes vol 14(3) 1989, pp 34–40
Kurki-Suonio R, Kankaanpää T: On the design of reactive systems. BIT 28, 3: 581–604 (1988)
Lam SS, Shankar AU: Protocol verification via projections. IEEE Trans Software Eng. SE-10, 4: 325–342 (1984)
Lamport L: Solved problems, unsolved problems, and non-problems in concurrency. Invited address in 2nd Annual ACM Symposium on Principles of Distributed Computing, Montreal, Canada, 1983. Proceedings 3rd Annual ACM Symposium on Principles of Distributed Computing 1984, pp 1–11
Lamport L: A serializable database interface. Problem given in Lake Arrowhead Workshop, 1987
Lamport L: A simple approach to specifying concurrent systems. Commun ACM 32, 1: 32–45 (1989)
London PE, Feather MS: Implementing specification freedoms. Sci Comp Program 2: 91–131 (1982)
Lynch NT, Tuttle MR: Hierarchical correctness proofs for distributed algorithms. Proceedings 6th ACM SIGACT-SIGOPS Symposium on Principles of Distributed Computing, 1987, pp 137–151
Manna Z, Pnueli A: How to cook a temporal proof system for your pet language. Proceedings 10th ACM Symposium on Principles of Programming Languages. Austin, Texas 1983, pp 141–154
Pnueli A: Applications of temporal logic to the specification and verification of reactive systems: a survey of current trends. In: de Bakker W, de Roever W-P, Rozenberg G (eds) Current trends in concurrency, LNCS vol 224 Springer, Berlin Heidelberg New York 1986, pp 510–584
Zave P: An operational approach to requirements specification for embedded systems. IEEE Trans Software Eng SE-8, 3: 250–269 (1982)
Author information
Authors and Affiliations
Additional information
Reino Kurki-Suonio received a Dr. Phil. degree from the University of Helsinki in 1964. At the University of Tampere he headed the first computer science department in Scandinavia since its creation in 1965. Currently he is professor of computer science and engineering at Tampere University of Technology. He has held visiting positions at Carnegie-Mellon and Stanford Universities. During the years his research interests have shifted from formal grammars, parsing methods, and programming languages to formal specification and design of distributed systems.
Rights and permissions
About this article
Cite this article
Kurki-Suonio, R. Operational specification with joint actions: Serializable databases. Distrib Comput 6, 19–37 (1992). https://doi.org/10.1007/BF02276639
Received:
Accepted:
Issue Date:
DOI: https://doi.org/10.1007/BF02276639