Decentralization of process nets with centralized control
Tóm tắt
The behavior of a net of interconnected, communicating processes is described in terms of the joint actions in which the processes can participate. A distinction is made between centralized and decentralized action systems. In the former, a central agent with complete information about the state of the system controls the execution of the actions; in the latter no such agent is needed. Properties of joint action systems are expressed in temporal logic. Centralized action systems allow for simple description of system behavior. Decentralized (two-process) action systems again can be mechanically compiled into a collection of CSP processes. A method for transforming centralized action systems into decentralized ones is described. The correctness of this method is proved, and its use is illustrated by deriving a process net that distributedly sorts successive lists of integers.
Tài liệu tham khảo
Apt K, Francez N, Katz S (1987) Appraising fairness in languages for distributed programming. Proc 14th ACM POPL Conf, Munich 1987, pp 189–198
Back RJR, Hartikainen E, Kurki-Suonio R (1985) Multi-process handshaking on broadcasting networks. Rep Comput Sci 42, Abo Akademi
Back RJR, Kurki-Suonio R (1983) Decentralization of process nets with centralized control. 2nd Annu ACM Symp on PoDC, Montreal, Canada, 1983, pp 131–142
Back RJR, Kurki-Suonio R (1984) A case study in constructing distributed algorithms: distributed exchange sort. Proc Winter School on Theoretical Computer Science, Lammi 1984, Finnish Society for Information Processing, pp 1–33
Back RJR, Kurki-Suonio R (1984) Co-operation in distributed systems using symmetric multi process handshaking. Rep Comput Sci 34, Abo Akademi
Back RJR, Kurki-Suonio R (1985) Serializability in distributed systems with handshaking. Res Rep CMU-CS-85-109, Carnegie-Mellon University, Pittsburgh
Back RJR, Kurki-Suonio R (1987) Distributed co-operation with action systems. Rep Comput Sci Mathematics 56, Abo Akademi
Bagrodia R (1987) A distributed algorithm to implement n-party rendezvous. University of Texas, Department of Computer Science technical report, June 1987
Bouge L, Francez N (1988) A compositional approach to super-imposition. 15th ACM Conf on Principles of Programming Languages. San Diego, Calif, pp 240–249
Buckley GN, Silberschatz A (1983) An effective implementation for the generalizated input-output construct of CSP. ACM TOPLAS vol 5, 2 (April 1983), pp 223–235.
Chandy M (1985) Concurrent programming for the masses. Proc 4th Annu ACM Symp PODC
Chandy KM, Lamport L (1985) Distributed snapshots: determining global states of distributed systems. ACM Trans Comput Syst 3(1):63–75
Chandy M, Misra J (1982) A distributed algorithm for detecting resource deadlocks in distributed systems. ACM SIGACTSIGOPS Symp on Principles of Distributed Computing 1982, pp 157–164
Chandy M, Misra J (1986) An example of stepwise refinement of distributed programs: quiescence detection. ACM TOPLAS, vol 8, no 3 (July 1866), pp 326–343
Chandy M, Misra J (1988) A foundation of parallel program design. Addison-Wesley (forthcoming)
Chandy KM, Misra J, Haas L (1983) Distributed deadlock detection. ACM Trans Comput Syst 1(2):144–156
de Cindio FG, de Michelis D, Pomello L, Simone C (1982) Superposed automata nets. Second European Workshop on Application and Theory of Petri Nets. In: Girault C, Reisig W (eds), Application and Theory of Petri Nets. Inf Fachber 52, Springer, Berlin Heidelberg New York Tokyo
Dijkstra EW, Scholten CS (1980) Termination detection for diffusing computations. Inf Process Lett, 11(1):1–4
US Department of Defense (1980) Reference manual for the Ada programming language. Proposed Standard Document, US Department of Defense, July 1980
Eklund P (1985) Synchronizing multiple processes in common handshakes. Rep Comput Sci 39, Abo Akademi
Evengelist M, Shen VY, Forman I, Graf M (1987) Using raddle to design distributed systems. MCC Tech Rep STP-285-87, September 1987
Francez N (1980) Distributed termination. ACM Trans Program Lang syst 2(1):42–55
Grancez N (1986) Fairness. Springer, Berlin Heidelberg New York Tokyo
Gergely L, Ury L (1982) Representation and verification of communicating sequential processes. Comp Ling Comput Lang 15:157–174
Grumberg O, Francez N, Katz S (1984) Fair termination of communicating processes. 3rd ACM SIGACT-SIGOPS Symp on Principles of Distributed Computing, Vancouver 1984
Hoare CAR (1978) Communicating sequential processes. Commun ACM 21(8):666–677
Katz S (1987) A superimposition control construct for distributed systems. MCC Tech Rep STP 268-87
Manna Z, Pnueli A (1983) How to cook a temporal proof system for your pet language. 10th ACM Conf on Principles of Programming Languages, Austin, Texas, pp 141–154
Martin AR, Tucker JV (1987) The concurrent assignment representation of synchronous systems. PARLE, Parallel Architectures and Languages Europe, Proc vol II. (Lect Notes Comput Sci 256) Springer, Berlin Heidelberg New York Tokyo, pp 369–386
McCurley R, Schneider FB (1986) Derivation of a distributed algorithm for finding paths in directed networks. Sci Comput Program 6:1–9
Pnueli A (1986) Applications of temporal logic to the specification and verification of reactive systems: a survey of current trends Current trends in concurrency (Lect Notes Comput Sci 224) Springer, Berlin Heidelberg New York Tokyo, pp 510–584
Ramesh S (1987) A new and efficient implementation of multiprocess synchronization. PARLE, Parallel Architectures and Languages Europe, Proc vol II. (Lect Notes Comput Sci 256), Springer, Berlin Heideberg New York Tokyo, pp 387–401
Ramesh S, Mehndiratta SL (1987) A methodology for developing distributed algorithms. IEEE Trans Software Engineering SE-13(8):967–976
Shankar A, Lam S (1987) Time-dependent distributed systems: proving safety, liveness and real-time properties. Distrib Comput 2:61–79