R. J. R. Back
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.
- 1 Ada Programming Language. ANSI/MIL-STD-1815A-1983.Google Scholar
- 2 ANDREWS, G. R., AND SCHNEIDER, F.B. Concepts and notations for concurrent programming. ACM Comput. Surv. 15, 1 (March 1983), 3-43. Google Scholar
- 3 APT, K., FRANCEZ, N., AND KATZ, S. Appraising fairness in languages for distributed programming. In 14th ACM Conference on Principles of Programming Languages (Munich, Jan. 1987), ACM, New York, 1987, 189-198. Google Scholar
- 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.Google Scholar
- 5 BACK, R. J. R., AND KURKI-SUONIO, R. Decentralization of process nets with a centralized control. In Second ACM SIGACT-SIGOPS Symposium on Principles of Distributed Computing (Montreal, Aug. 1983). ACM, New York, 1983, 131-142. Google Scholar
- 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.Google Scholar
- 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.Google Scholar
- 8 BACK, R. J. R., AND KURKI-SUONIO, R. Serializability in distributed systems with handshaking. In Automata, Languages and Programming. Lecture Notes in Computer Science 317. T. Lepist6 amd A. Salomaa, Eds. Springer Verlag, Berlin, 1988, 52-66. Google Scholar
- 9 BAORODIA, R. On the design of high performance distributed systems. Ph.D. dissertation, Univ. of Texas, Austin, 1987.Google Scholar
- 10 BUCKLEY, G. N., AND SlLBERSCHATZ, A. An effective implementation for the generalized inputoutput construct of CSP. ACM Trans. Program. Lang. Syst. 5, 2 (April 1983), 223-235. Google Scholar
- 11 CHANDY, M., AND MISRA, J. An example of stepwise refinement of distributed programs: Quiscence detection. ACM Trans. Program. Lang. Syst. 8, 3 (July 1986), 326-343. Google Scholar
- 12 CHARLESWORTH, A. The multiway rendezvous. ACM Trans. Program. Lang. Syst. 9, 2 (July 1987), 350-366. Google Scholar
- 13 CSMA/CD Access Method and Physical Layer Specifications. IEEE Standard 802.3, IEEE, New York, July 1983.Google Scholar
- 14 DE CINDIO, F., DE MICHELIS, G., POMELLO, L., AND SIMONE, C. Superposed automata nets. In Application and Theory of Petri Nets. In{ormatik-Fachberichte 52, C. Girault and W. Reisig, Eds., Springer-Verlag, Berlin, 1982. Google Scholar
- 15 DIJKSTRA, E.W. A Discipline of Programming. Prentice-Hall, Englewood Cliffs, N.J., 1976. Google Scholar
- 16 DIJKSTRA, E.W. Invariance and nondeterminacy. In Mathematical Logic and Programming Languages. C. A. R. Hoare and J. C. Shepherdson, Eds. Prentice-Hall, Englewood Cliffs, N.J., 1985, 157-165. Google Scholar
- 17 DIJKSTRA, E. W., LAMPORT, L., MARTIN, A. J., AND SCHOLTEN, C. S. On-the-fly garbage collection: An exercise in cooperation. Commun. ACM 21, 11 (Nov. 1978), 966-975. Google Scholar
- 18 EKLUND, P. Synchronizing multiple processes in common handshakes. In Reports in Computer Science 39, Abo Akademi, Abo, Finland, 1985.Google Scholar
- 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.Google Scholar
- 20 FORMAN, I.R. Raddle, an informal introduction. Tech. Rep. STP-182-85, Microelectronics and Computer Technology Corp., Austin, Tex., 1986.Google Scholar
- 21 FRANCEZ, N. Fairness. Springer-Verlag, Berlin, 1986. Google Scholar
- 22 FRANCEZ, N., AND HAILPERN, B. Script: A communication abstraction mechanism. In Second ACM-SIGACT-SIGOPS Symposium on Principles of Distributed Computing (Montreal, Aug. 1983). ACM, New York, 1983, 213-227. Google Scholar
- 23 GRUMBERG, O., FRANCEZ, N., AND KATZ, S. Fair termination of communicating processes. In Third ACM SIGACT-SIGOPS Symposium on Principles of Distributed Computing (Vancouver, Aug. 1984). ACM, New York, 1984, 254-265. Google Scholar
- 24 HOARE, C. A.R. An axiomatic basis for computer programming. Commun. ACM 12, 10 (Oct. 1969), 576-580. Google Scholar
- 25 HOARE, C. A. R. Communicating sequential processes. Commun. ACM 21, 8 (Aug. 1978), 666-677. Reprinted in Commun. ACM 26, 1 (Jan. 1983), 100-106. Google Scholar
- 26 HOARE, C. A.R. Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs, N.J., 1985. Google Scholar
- 27 INMOS LTD. Occam Programming Manual. Prentice-Hall, Englewood Cliffs, N.J., 1985.Google Scholar
- 28 KROEGER, F. Temporal Logic of Programs. EATCS Monographs on Theoretical Computer Science, vol. 8. Springer-Verlag, Berlin, 1986. Google Scholar
- 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.Google Scholar
- 30 LAMPORT, L. Time, clocks, and ordering of events in a distributed system. Commun. ACM 21, 7 (July 1978), 558-565. Google Scholar
- 31 MANNA, Z., AND PNUELI, A. How to cook a temporal proof system for your pet language. In Tenth A C M Conference on Principles of Programming Languages (Austin, Tex., Jan. 1983). ACM, New York, 1983, 141-154. Google Scholar
- 32 PNUELI, A. Applications of temporal logic to the specification and verification of reactive systems: A survey of current trends. In Current Trends in Concurrency. Lecture Notes in Computer Science 224, J. W. de Bakker, W. P. de Roever, and G. Rozenberg, Eds., Springer-Verlag, Berlin, 1986, 510-584. Google Scholar
- 33 RAMESH, S. A new and efficient implementation of multiprocess synchronization. In PARLE Parallel Architectures and Languages Europe. Lecture Notes in Computer Science 259, Springer- Verlag, Berlin, 1987, 387-401. Google Scholar
- 34 RAMESH, S., AND MEHNDIRATTA, S. L. A new class of high-level programs for distributed computing systems. In Proceedings of Fifth Conference on FST- TCS. Lecture Notes in Computer Science 206, Springer-Verlag, Berlin, 1985, 42-72. Google Scholar
- 35 SCHNEIDER, F.R. Synchronization in distributed programs. ACM Trans. Program. Lang. Syst. 4, 2 (April 1982), 125-148. Google Scholar
- 36 SERE, K. Stepwise removal of virtual channels in distributed algorithms. In Second International Workshop on Distributed Algorithms (Amsterdam, 1987). Google Scholar
- 37 TANENBAUM, A, S. Computer Networks. Prentice-Hall, Englewood Cliffs, N.J., 1981. Google Scholar
Index Terms
- Distributed cooperation with action systems
Recommendations
Modelling knowledge and action in distributed systems
We present a formal model that captures the subtle interaction between knowledge and action in distributed systems. We view a distributed system as a set ofruns, where a run is a function from time toglobal states and a global state is a tuple ...
Reducing Aborts in Distributed Transactional Systems through Dependency Detection
ICDCN '15: Proceedings of the 16th International Conference on Distributed Computing and NetworkingExisting distributed transactional system execution model based on globally-consistent contention management policies may abort many transactions that could potentially commit without violating correctness. To reduce unnecessary aborts and increase ...
Reviews
Steven K. Andrianoff
In this paper the authors develop a model for the design of a distributed system called an action system. This model describes the system in terms of process interactions (“actions”) rather than the sequential code of the cooperating processes. An action system is a collection of actions executed in a manner similar to Dijkstra's guarded iteration statement. Each action consists of a guard, a statement body, and an indication of the processes that must participate in the action. An action is enabled when the guard is satisfied and all the participating processes are available (i.e., not currently engaged in other actions). Enabled actions are nondeterministically selected for execution. The action construct provides process synchronization and a symmetric, multiprocess communication mechanism. The authors first introduce a restricted model of an action system in which the actions are executed sequentially. After making a fairness assumption about the selection of enabled actions in this model, they proceed to show that safety and liveness properties can be verified using standard techniques of Hoare logic and temporal logic. A concurrent execution model is defined that corresponds to the way an action system would be implemented. The verification techniques cannot be immediately transferred to this model, however, because weaker notions of fairness apply to it. The authors give a distributed implementation of the concurrent model on a local area network with a reliable broadcast channel and they carefully prove that this implementation guarantees the fairness assumptions of the concurrent model. A large portion of the paper is devoted to a study of the notions of fairness used in the two models and the relationships among them. In particular, the authors describe a class of action systems in which the fairness assumptions of the concurrent model imply the fairness assumption of the sequential model so that system properties can be verified in the (simpler) sequential model. The paper is very well written and gives proper motivation for the various concepts introduced. The two execution models, as well as other terms that are used, are carefully defined. A progression of solutions to the dining philosophers problem is presented to illustrate the semantics of the action construct and to provide examples of safety and liveness properties that are verified. To encounter a paper that presents a language construct for the purpose of easily reasoning about program behavior, and yet carefully shows the limitations of an efficient implementation, is especially satisfying. The proposed model is appealing because it focuses attention on the source of most difficulties in the design of a correct distributed system, namely, the process interactions.
Access critical reviews of Computing literature here
Become a reviewer for Computing Reviews.
Comments