Advertisement

Processes and a fair semantics for the ADA rendez-vous

  • J. W. de Bakker
  • J. I. Zucker
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 154)

Abstract

Processes are mathematical objects which are elements of domains in the sense of Scott and Plotkin. Process domains are obtained as solutions of equations solved by techniques from metric topology as advocated by Nivat. We discuss how such processes can be used to assign meanings to languages with concurrency, culminating in a definition of the ADA rendez-vous. An important intermediate step is a version of Hoare's CSP for which we describe a process semantics and which is used, following Gerth, as target for the translation of the ADA fragment. Furthermore, some ideas will be presented on a mathematically tractable treatment of fairness in the general framework of processes.

Keywords

Elementary Action Cauchy Sequence Mathematical Object Random Choice Denotational Semantic 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [1]
    ADA, The Programming Language ADA, Reference Manual, LNCS 106, Springer, 1981.Google Scholar
  2. [2]
    APT, R.R. & E.R. OLDEROG, Proof rules dealing with fairness, Proc. Logic of Programs 1981 (D. Kozen, ed.), 1–9, LNCS 131, Springer, 1982.Google Scholar
  3. [3]
    DE BARKER, J.W. & J.I. ZUCKER, Denotational semantics of concurrency, Proc 14th ACM Symp. on Theory of Computing, pp. 153–158, 1982.Google Scholar
  4. [4]
    DE BARKER, J.W. & J.I. ZUCKER, Processes and the denotational semantics of concurrency, Report IW 209/82, Mathematisch Centrum, 1982, to appear in Information & Control.Google Scholar
  5. [5]
    BERGSTRA, J.A. & J.W. KLOP, Fixed point semantics in process algebras, Report IW 206/82, Mathematisch Centrum, 1982.Google Scholar
  6. [6]
    BRINCH HANSEN, P., Distributed processes: a concurrent programming concept, C. ACM 21 (1978), 934–941.Google Scholar
  7. [7]
    DUGUNDJI, J., Topology, Allen & Bacon, 1966.Google Scholar
  8. [8]
    GERTH, R., A sound and complete Hoare-like axiomatization of the ADA rendezvous, Proc. 9th ICALP (M. Nielsen & E.M. Schmidt, eds), 252–264, LNCS 140, Springer, 1982.Google Scholar
  9. [9]
    HENNESSY, M. & W. LI, Translating a subset of Ada into CCS, Proc. IFIP Working Conference on Formal Description of Programming Concepts II (D. BjØrner, ed.), North-Holland, to appear.Google Scholar
  10. [10]
    HOARE, C.A.R., Communicating sequential processes, C. ACM 21 (1978), 666–677.Google Scholar
  11. [11]
    KUIPER, R. & W.P. DE ROEVER, Fairness assumptions for CSP in a temporal logic framework, Proc. IFIP Working Conference on Formal Description of Programming Concepts, II (D. BjØrner, ed.), North-Holland, to appear.Google Scholar
  12. [12]
    LEHMANN, D.A. PNUELI & J. STAVI, Impartiality, justice and fairness: the ethics of concurrent computation, Proc. 8th ICALP (S. Even & O. Kariv, eds.), 264–277, LNCS 115, Springer, 1981.Google Scholar
  13. [13]
    LI, W., An operational semantics of tasking and exception handling in ADA, proc. ACM ADA Tec and Tutorial Conference, to appear.Google Scholar
  14. [14]
    MILNE, G. & R. MILNER, Concurrent processes and their syntax, J. ACM 26 (1979), 302–321.Google Scholar
  15. [15]
    MILNER, R., A Calculus for Communicating Systems, LNCS 92, Springer, 1980.Google Scholar
  16. [16]
    NIVAT, M., Infinite words, infinite trees, infinite computations, Foundations of Computer Science III.2 (J.W. de Bakker & J. van Leeuwen, eds.) 3–52, Mathematical Centre Tracts 109, 1979.Google Scholar
  17. [17]
    PARK, D., On the semantics of fair parallelism, in Abstract Software Specifications (D. BjØrner, ed.) pp. 504–526, LNCS 86, Springer, 1980.Google Scholar
  18. [18]
    PLOTKIN, G.D., A power domain construction, SIAM J. on Comp. 5 (1976), 452–487.Google Scholar
  19. [19]
    PLOTKIN, G.D., A power domain for countable nondeterminism, Proc. 9th ICALP (M. Nielsen & E.M. Schmidt, eds.), 418–428, LNCS 140, Springer, 1982.Google Scholar
  20. [20]
    PNUELI, A. & W.P. De Roever, Rendez-vous with ADA, a proof theoretical view, Proc. ACM ADA Tec and Tutorial Conference, to appear.Google Scholar
  21. [21]
    SCOTT, D.S., Data types as lattices, SIAM J. on Comp., 5 (1976), 522–587.Google Scholar
  22. [22]
    SCOTT, D.S., Domains for denotational semantics, Proc. 9th ICALP (M. Nielsen & E.M. Schmidt, eds.), 577–613, LNCS 140, Springer, 1982.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1983

Authors and Affiliations

  • J. W. de Bakker
    • 1
  • J. I. Zucker
    • 2
  1. 1.Department of Computer ScienceMathematisch CentrumAmsterdam
  2. 2.Department of Computer ScienceSUNY at BuffaloAmtierstUSA

Personalised recommendations