Distributed cooperation with action systems

ABSTRACT

Action systems provide a method to program distributed systems that emphasizes the overall behavior of the system. System behavior is described in terms of the possible interactions (actions) that the processes can engage in, rather than in terms of the sequential code that the processes execute. The actions provide a symmetric communication mechanism that permits an arbitrary number of processes to be synchronized by a common handshake. This is a generalization of the usual approach, employed in languages like CSP and Ada, in which communication is asymmetric and restricted to involve only two processes. Two different execution models are given for action systems: a sequential one and a concurrent one. The sequential model is easier to use for reasoning, and is essentially equivalent to the guarded iteration statement by Dijkstra. It is well suited for reasoning about system properties in temporal logic, but requires a stronger fairness notion than it is reasonable to assume a distributed implementation will support. The concurrent execution model reflects the true concurrency that is present in a distributed execution, and corresponds to the way in which the system is actually implemented. An efficient distributed implementation of action systems on a local area network is described. The fairness assumptions of the concurrent model can be guaranteed in this implementation. The relationship between the two execution models is studied in detail in the paper. For systems that will be called fairly serializable, the two models are shown to be equivalent. Proof methods are given for verifying this property of action systems. It is shown that for fairly serializable systems, properties that hold for any concurrent execution of the system can be established by temporal proofs that are conducted entirely within the simpler sequential execution model.

REFERENCES

• 1: Ada Programming Language. ANSI/MIL-STD-1815A-1983.
• 2: Gregory R. Andrews , Fred B. Schneider, Concepts and Notations for Concurrent Programming, ACM Computing Surveys (CSUR), v.15 n.1, p.3-43, March 1983 [doi>10.1145/356901.356903]
• 3: K. R. Apt , N. Francez , S. Katz, Appraising fairness in distributed languages, Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.189-198, January 21-23, 1987, Munich, West Germany [doi>10.1145/41625.41642]
• 4: BACK, R. J. R., HARTIKAINEN, E., AND KURKI-SUONIO, R. Multi-process handshaking on broadcasting networks. In Reports in Computer Science 42, Abo Akademi, Abo, Finland, 1985.
• 5: R. J. R. Back , R. Kurki-Suonio, Decentralization of process nets with centralized control, Proceedings of the second annual ACM symposium on Principles of distributed computing, p.131-142, August 17-19, 1983, Montreal, Quebec, Canada [doi>10.1145/800221.806716]
• 6: BACK, R. J. R., AND KURKI-SUONIO, R. A case study in constructing distributed algorithms: Distributed exchange sort. In Proceedings of Winter School on Theoretical Computer Science (Lammi, Finland, Jan. 1984). Finnish Society of Information Processing Science, 1-33.
• 7: BACK, R. J. R., AND KURKI-SUoNIO, R. Co-operation in distributed systems using symmetric multi-process handshaking. In Reports in Computer Science 34, Abo Akademi, Abo, Finland, 1984.
• 8: Ralph-Johan Back , Reino Kurki-Suonio, Serializability in Distributed Systems with Handshaking, Proceedings of the 15th International Colloquium on Automata, Languages and Programming, p.52-66, July 11-15, 1988
• 9: BAORODIA, R. On the design of high performance distributed systems. Ph.D. dissertation, Univ. of Texas, Austin, 1987.
• 10: G. N. Buckley , Abraham Silberschatz, An Effective Implementation for the Generalized Input-Output Construct of CSP, ACM Transactions on Programming Languages and Systems (TOPLAS), v.5 n.2, p.223-235, April 1983 [doi>10.1145/69624.357208]
• 11: Mani Chandy , Jayadev Misra, An example of stepwise refinement of distributed programs: quiescence detection, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.3, p.326-343, July 1986 [doi>10.1145/5956.5958]
• 12: Arthur Charlesworth, The multiway rendezvous, ACM Transactions on Programming Languages and Systems (TOPLAS), v.9 n.3, p.350-366, July 1987 [doi>10.1145/24039.24050]
• 13: CSMA/CD Access Method and Physical Layer Specifications. IEEE Standard 802.3, IEEE, New York, July 1983.
• 14: Fiorella de Cindio , Giorgio De Michelis , Lucia Pomello , Carla Simone, Superposed Automata Nets, Selected Papers from the First and the Second European Workshop on Application and Theory of Petri Nets, p.269-279, September 28-30, 1980
• 15: Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
• 16: E. W. Dijkstra, Invariance and non-determinacy, Proc. of a discussion meeting of the Royal Society of London on Mathematical logic and programming languages, p.157-165, June 1985, London, United Kingdom
• 17: Edsger W. Dijkstra , Leslie Lamport , A. J. Martin , C. S. Scholten , E. F. M. Steffens, On-the-fly garbage collection: an exercise in cooperation, Communications of the ACM, v.21 n.11, p.966-975, Nov. 1978 [doi>10.1145/359642.359655]
• 18: EKLUND, P. Synchronizing multiple processes in common handshakes. In Reports in Computer Science 39, Abo Akademi, Abo, Finland, 1985.
• 19: FORGY, C., AND DERMOT, M.C. OPS, a domain independent production system language. In Proceedings of Fifth International Joint Conference on Artificial Intelligence (Cambridge, Mass., Aug. 1977), Morgan Kaufmann, 1977, 933-939.
• 20: FORMAN, I.R. Raddle, an informal introduction. Tech. Rep. STP-182-85, Microelectronics and Computer Technology Corp., Austin, Tex., 1986.
• 21: Nissim Francez, Fairness, Springer-Verlag New York, Inc., New York, NY, 1986
• 22: Nissim Francez , Brent Hailpern, Script: A communication abstraction mechanism, Proceedings of the second annual ACM symposium on Principles of distributed computing, p.213-227, August 17-19, 1983, Montreal, Quebec, Canada [doi>10.1145/800221.806723]
• 23: Orna Grumberg , Nissim Francez , Shmuel Katz, Fair termination of communicating processes, Proceedings of the third annual ACM symposium on Principles of distributed computing, p.254-265, August 27-29, 1984, Vancouver, British Columbia, Canada [doi>10.1145/800222.806752]
• 24: C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
• 25: C. A. R. Hoare, Communicating sequential processes, Communications of the ACM, v.26 n.1, p.100-106, Jan. 1983 [doi>10.1145/357980.358021]
• 26: C. A. R. Hoare, Communicating sequential processes, Prentice-Hall, Inc., Upper Saddle River, NJ, 1985
• 27: INMOS LTD. Occam Programming Manual. Prentice-Hall, Englewood Cliffs, N.J., 1985.
• 28: Fred Krögr, Temporal logic of programs, Springer-Verlag New York, Inc., New York, NY, 1986
• 29: KUIPER, R., AND DE ROEVER, W. P. Fairness assumptions for CSP in a temporal logic framework. In Formal Description of Programming Concepts--II, D. Bj~rner, Ed. North-Holland, Amsterdam, 1983, 159-167.
• 30: Leslie Lamport, Time, clocks, and the ordering of events in a distributed system, Communications of the ACM, v.21 n.7, p.558-565, July 1978 [doi>10.1145/359545.359563]
• 31: Zohar Manna , Amir Pnueli, How to cook a temporal proof system for your pet language, Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.141-154, January 24-26, 1983, Austin, Texas [doi>10.1145/567067.567082]
• 32: A Pnueli, Applications of temporal logic to the specification and verification of reactive systems: a survey of current trends, Current trends in concurrency. Overviews and tutorials, Springer-Verlag New York, Inc., New York, NY, 1986
• 33: S Ramesh, A new and efficient implementation of multiprocess synchronization, Volume II: Parallel Languages on PARLE: Parallel Architectures and Languages Europe, p.387-401, March 1987, Eindhoven, The Netherlands
• 34: S. Ramesh , S. L. Mehndiratta, A New Class of High Level Programs for Distributed Computing Systems, Proceedings of the Fifth Conference on Foundations of Software Technology and Theoretical Computer Science, p.42-72, December 16-18, 1985
• 35: Fred B. Schneider, Synchronization in Distributed Programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.4 n.2, p.125-148, April 1982 [doi>10.1145/357162.357163]
• 36: Kaisa Sere, Stepwise Removal of Virtual Channels in Distributed Algorithms, Proceedings of the 2nd International Workshop on Distributed Algorithms, p.408-428, July 08-10, 1987
• 37: A. S. Tanenbaum, Computer networks, Prentice-Hall, Inc., Upper Saddle River, NJ, 1988

INDEX TERMS

Primary Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES

Additional Classification:
  C. Computer Systems Organization
  C.2 COMPUTER-COMMUNICATION NETWORKS

  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Concurrent programming structures

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

General Terms:
Languages, Theory, Verification