A compositional approach to superimposition

ABSTRACT

A general definition of the notion of superimposition is presented. We show that previous constructions under the same name can be seen as special cases of our definition. We consider several properties of superimposition definable in our terms, notably the nonfreezing property. We also consider a syntactic representation of our construct in CSP

REFERENCES

• 1: K. R. Apt, Correctness proofs of distributed termination algorithms, Logics and models of concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1989
• 2: K. R. Apt , L. Bougé , Ph. Clermont, Two normal form theorems for CSP programs, Information Processing Letters, v.26 n.4, p.165-171, Dec. 4, 1987 [doi>10.1016/0020-0190(87)90001-9]
• 3: K.R. Apt, Ph. Clermont, ~Two normal forms theorems for CSP programs", Rept. No. RC 10975, IBM Research Center, Yorktown Heights, N.Y., Febr. 1985.
• 4: Krzysztof R. Apt , Nissim Francez, Modeling the distributed termination convention of CSP, ACM Transactions on Programming Languages and Systems (TOPLAS), v.6 n.3, p.370-379, July 1984 [doi>10.1145/579.584]
• 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: R. Back, R. Kurki-Suonio, =Serializability in distributed systems with handshaking~, Rept. No. CMU- CS-85-I09, Dept. Comp. Science, CM'U, Pittsburgh, 1985.
• 7: L. Bougé, Repeated snapshots in distributed systems with synchronous communications and their implementation in CSP, Theoretical Computer Science, v.49 n.2-3, p.145-169, January 1987 [doi>10.1016/0304-3975(87)90005-3]
• 8: L. Bough, "Symmetry and genericity for CSP distributed systems', Rept. No. 85-32, LITP, Univ. Paris 7, May 1985.
• 9: 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]
• 10: 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]
• 11: K. Mani Chandy , Leslie Lamport, Distributed snapshots: determining global states of distributed systems, ACM Transactions on Computer Systems (TOCS), v.3 n.1, p.63-75, Feb. 1985 [doi>10.1145/214451.214456]
• 12: K. M. Chandy , J. Misra, A paradigm for detecting quiescent properties in distributed computations, Logics and models of concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1989
• 13: K. M. Chandy , Jayadev Misra, How processes learn, Distributed Computing, v.1 n.1, p.40-52, Jan. 1986 [doi>10.1007/BF01843569]
• 14: E.W. Dijkstra, W.H.J. Feijen, A.J.M. van Gasteren, "Derivation of a termination detection alKorithm for distributed computations', IPL 16, pp. 217-219, 1983.
• 15: E.W. Di}kstra, C.S. Scholten, "Termination detection for diffusing computations~, IPL 11, 1, pp. I-4) 1980.
• 16: Tz. Elrad, N. Francez, ~Decomposition of distributed programs into communication closed layers", SCP 2, pp. 155-173, December 1982.
• 17: Nissim Francez, Distributed Termination, ACM Transactions on Programming Languages and Systems (TOPLAS), v.2 n.1, p.42-55, Jan. 1980 [doi>10.1145/357084.357087]
• 18: I.R. Forman, ~On the design of large distributed systems', Rept. No. MCC/STP-098-86 (roy. 1), MCC, Austin, Tx., Jan. 1987. Also in Proc. 1~t int. conf. on computer languages, M/~mi, FI., Oct. 1986.
• 19: N. Francez , B. Hailpern , G. Taubenfeld, Script: a communication abstraction mechanism and its verification, Logics and models of concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1989
• 20: N. Francez, M. Rodeh, ~A distributed abstract data type implemented by a probabilistic communication scheme~, Proc. 21~ FOCS, Syracuse, N.Y., October 1980.
• 21: N. Francez, M. Rodeh, "Achieving distributed termination without freezing~, IEEE..TSE 8, 3, pp. 287- 292, May 1982.
• 22: E. Gafni, ~Perspectives on distributed networks protocols: A case for building blocks~, Proc. A41LCOM 86, Monterey, Ca., October 1986.
• 23: R.G. Gallager, R.A. Humblet, P.M. Spira, "A distributed algorithm for minimum-weight spanning trees," IEEE Trans. on CommunicaHons 31, 6, pp. 756- 762, 1983.
• 24: C. A. R. Hoare, Communicating sequential processes, Communications of the ACM, v.21 n.8, p.666-677, Aug. 1978 [doi>10.1145/359576.359585]
• 25: S. Katz, ~A superimposition control construct for distributed systems", Techn. Rept., MCC-STP, MCC, Austin, Tx., August 1987.
• 26: E. Korach , S. Kutten , S. Moran, A modular technique for the design of efficient distributed leader finding algorithms, Proceedings of the fourth annual ACM symposium on Principles of distributed computing, p.163-174, August 1985, Minaki, Ontario, Canada [doi>10.1145/323596.323611]
• 27: J.S. Schwarz, ~rDistributed synchronisation of communicating sequential processes", Techn. Rept., Dept. Artificial Intelligence, Univ. Edinburgh, July 1978.
• 28: L. Shrira, N. Francez, ~A program transformation regarded as a proof transformation~, submitted for publication, 1985.
• 29: F.A. Stomp, W.P. de Roever, ~A correctness proof of a distributed minimum-weight spanning tree algorithm~, Rept. No. 87-4, Dept. Irtformatics, Nimegen Univ., April 1987. Submitted for publication, January 1987.
• 30: N Shavit , N Francez, A new approach to detection of locally indicative stability, International Colloquium on Automata, Languages and Programming on Automata, languages and programming, p.344-358, September 1986, Rennes, France
• 31: G. Tel, R.B. Tan, J. van Leeuwen, "The deriwtion of graph marking algorithms form distributed termination detection algorithms~, Rept. No. RUU-CS-86-11, Univ. Utrecht, August 1986.

INDEX TERMS

Primary Classification:
  D. Software
  D.4 OPERATING SYSTEMS

Additional Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Semantics
      D.3.2 Language Classifications

          Nouns: CSP
      D.3.3 Language Constructs and Features
          Subjects: Concurrent programming structures

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Control primitives

General Terms:
Algorithms, Languages, Theory