Skip to main content
SpringerLink
Log in

Contrasting themes in the semantics of imperative concurrency

  • Chapter
  • First Online:
Current Trends in Concurrency

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 224))

Abstract

A survey is given of work performed by the authors in recent years concerning the semantics of imperative concurrency. Four sample languages are presented for which a number of operational and denotational semantic models are developed. All languages have parallel execution through interleaving, and the last three have as well a form of synchronization. Three languages are uniform, i.e., they have uninterpreted elementary actions; the fourth is nonuniform and has assignment, tests and value-passing communication. The operational models build on Hennessy-Plotkin transition systems; as denotational structures both metric spaces and cpo domains are employed. Two forms of nondeterminacy are distinguished, viz. the local and global variety. As associated model-theoretic distinction that of linear time versus branching time is investigated. In the former we use streams, i.e. finite or infinite sequences of actions; in the latter the (metrically based) notion of process is introduced. We furthermore study a model with only finite observations. Ready sets also appear, used as technical tool to compare various semantics. Altogether, ten models for the four languages are described, and precise statements on (the majority of) their interrelationships are made. The paper supplies no proofs; for these references to technical papers by the authors are provided.

The research of J.W. de Bakker was partially supported by ESPRIT Project 415: Parallel Architectures and Languages.

The research of J.N. Kok was supported by the Netherlands Organization for the Advancement of Pure Research (Z.W.O.), grant 125-20-04.

The research of J.I. Zucker was supported by the National Science Foundation under grant no. MCS-8010728.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. ADA, The Programming Language ADA, Reference Manual, American National Standards Institute, Inc. ANSI/MIL-STD-1815A-1983, LNCS 155 Springer, 1983.

    Google Scholar 

  2. P. America, Definition of the programming language POOL-T, ESPRIT project 415, Doc. Nr. 0091, Philips Research Laboratories, Eindhoven, June 1985.

    Google Scholar 

  3. P. America, J.W. de Bakker, J.N. Kok, J.J.M.M. Rutten, Operational semantics of a parallel object-oriented language, CS-R8515, Centre for Mathematics and Computer Science, 1985.

    Google Scholar 

  4. P. America, J.W. de Bakker, J.N. Kok, J.J.M.M. Rutten, Denotational semantics of a parallel object-oriented language, in preparation.

    Google Scholar 

  5. K.R. Apt, Recursive assertions and parallel programs, Acta Inf. 15 (1981) 219–232.

    Google Scholar 

  6. K.R. Apt, Formal justification of a proof system for communicating sequential processes, J. Assoc. Comput. Mach., 30 1 (1983) 197–216.

    Google Scholar 

  7. K.R. Apt (ed.), Logics and Models of Concurrent systems, Springer, 1985.

    Google Scholar 

  8. A. Arnold, M. Nivat, Metric interpretations of infinite trees and semantics of nondeterministic recursive programs, Theor. Comp. Science 11 (1980) 181–206.

    Google Scholar 

  9. R.J. Back, A continuous semantics for unbounded nondeterminism, Theoret. Comp. Sci. 23 (1983) 187–210.

    Google Scholar 

  10. J.W. de Bakker, Mathematical theory of program correctness, Prentice Hall International, London, 1980.

    Google Scholar 

  11. J.W. de Bakker, J.A. Bergstra, J.W. Klop, J.-J. Ch. Meyer, Linear time and branching time semantics for recursion with merge, TCS 34 (1984) 135–156.

    Google Scholar 

  12. J.W. de Bakker, J.N. Kok, Towards a uniform topological treatment of streams and functions on streams, in: Proc. 12th ICALP (W. Brauer, ed.), LNCS 194, Springer (1985), 140–148.

    Google Scholar 

  13. J.W. de Bakker, J.-J. Ch. Meyer, E.-R. Olderog, Infinte streams and finite observations in the semantics of uniform concurrency, in: Proceedings 12th ICALP (W. Brauer, ed.), LNCS 194, Springer (1985) 149–157.

    Google Scholar 

  14. J.W. de Bakker, J.-J. Ch. Meyer, E.-R. Olderog, Infinite streams and finite observations in the semantics of uniform concurrency, Report CS-R8512, Centre for Mathematics and Computer Science, 1985. (full version of [BMO1]).

    Google Scholar 

  15. J.W. de Bakker, J.-J. Ch. Meyer, E.-R. Olderog, Hiding discriminates between order and metric in the stream semantics of concurrency, Report CS-R85.., Centre for Mathematics and Computer Science, to appear.

    Google Scholar 

  16. J.W. de Bakker, J.-J. Ch. Meyer, E.-R. Olderog, J.I. Zucker, Transition systems, infinitary languages and the semantics of uniform concurrency, in: Proceedings 17th ACM STOC, Providence, R.I. (1985) 252–262.

    Google Scholar 

  17. J.W. de Bakker, J.-J. Ch. Meyer, E.-R. Olderog, J.I. Zucker, Transition systems, metric spaces and ready sets in the semantics of uniform concurrency, preprint SUNY at Buffalo, 1985 (full version of BMOZ1), to appear.

    Google Scholar 

  18. J.W. de Bakker, J.I. Zucker, Denotational semantics of concurrency, in: Proceedings 14th Assoc. Comput. Mach. Symp. on Theory of Computing (1982) 153–158.

    Google Scholar 

  19. J.W. de Bakker, J.I. Zucker, Processes and the denotational semantics of concurrency, Inform. and Control 54 (1982) 70–120.

    Google Scholar 

  20. J.W. de Bakker, J.I. Zucker, Compactness in semantics for merge and fair merge, in: Proceedings Workshop Logics of Programs, (E. Clarke & D. Kozen, eds.) Pittsburgh, LNCS 164 Springer (1983) 18–33.

    Google Scholar 

  21. J.W. de Bakker, J.I. Zucker, Processes and a fair semantics for the ADA rendez-vous, in: Proceedings 10th ICALP (J. Diaz, ed.) LNCS 154, Springer (1983) 52–66.

    Google Scholar 

  22. J.A. Bergstra, J.W. Klop, Process algebra for synchronous communication, Information and Control, 60 (1984) 109–137.

    Google Scholar 

  23. J.A. Bergstra, J.W. Klop, Algebra of communicating processes with abstraction, TCS 37 (1985) 77–121.

    Google Scholar 

  24. J.A. Bergstra, J.W. Klop, Algebra of communicating processes, in: Proceedings CWI Symposium (J.W. de Bakker, M. Hazewinkel, J.K. Lenstra, eds.), CWI Monographs, North-Holland, Amsterdam, to appear.

    Google Scholar 

  25. J.A. Bergstra, J.W. Klop, E.R. Olderog, Readies and failures in the algebra of communicating processes, CWI Report CS-R85.., Amsterdam, 1985.

    Google Scholar 

  26. E. Best, Relational semantics of concurrent programs (with some applications), in: Proceedings IFIP TC2 Working Conference (D. Bjørner, ed.), North-Holland, Amsterdam (1982) 431–452.

    Google Scholar 

  27. S.D. Brookes, On the relationship of CCS and CSP, in: Proceedings 10th ICALP (J. Diaz, ed.), LNCS 154, Springer (1983) 83–96.

    Google Scholar 

  28. S.D. Brookes, C.A.R. Hoare, A.W. Roscow, A theory of communicating sequential processes, J. ACM 31 (1984) 560–599.

    Google Scholar 

  29. S.D. Brookes, A.W. Roscoe, G. Winskel (eds.), Seminar on Concurrency, LNCS 197, Springer, 1985.

    Google Scholar 

  30. M. Broy, Fixed point theory for communication and concurrency, in: Formal Description of Programming Concepts II (D. Bjørner ed.), North-Holland, Amsterdam, (1983) 125–146.

    Google Scholar 

  31. M. Broy, Applicative real time programming, in: IFIP Information Processing 83 (R.E.A. Mason, ed.) North-Holland, Amsterdam, (1983) 259–264.

    Google Scholar 

  32. P. Degano, U. Montanari, Liveness properties as convergence in metric spaces, Proc. 16th ACM STOC (1984) 31–38.

    Google Scholar 

  33. J. Dugundji, Topology, Allen and Bacon, Rockleigh, N.J. 1966.

    Google Scholar 

  34. E.W. Dijkstra, Cooperating Sequential Processes, in Programming Languages (F. Genuys, ed.), Academic Press, 1968.

    Google Scholar 

  35. R. Engelking, General topology, Polish Scientific Publishers 1977.

    Google Scholar 

  36. N. Francez, C.A.R. Hoare, D.J. Lehmann, W.P. de Roever, Semantics of nondeterminism, concurrency and communication, JCSS 19 (1979) 290–308.

    Google Scholar 

  37. N. Francez, D.J. Lehmann, A. Pnueli, A linear history semantics for languages for distributed programming, TCS 32 (1984) 25–46.

    Google Scholar 

  38. W.G. Golson, W.C. Rounds, Connections between two theories of concurrency: metric spaces and synchronization trees, Inform. and Control 57 (1983) 102–124.

    Google Scholar 

  39. H. Hahn, Reelle Funktionen, Chelsea, New York, 1948.

    Google Scholar 

  40. M.C.B. Hennessy, Synchronous and asynchronous experiments on processes, Information and Control 59 (1983) 36–83.

    Google Scholar 

  41. M.C.B. Hennessy, An algebraic theory of fair asynchronous communicating processes, Manuscript, Dept. of Comp. Sci., Univ. of Edinburgh, 1984.

    Google Scholar 

  42. C.A.R. Hoare, Communicating sequential processes, Comm. ACM 21 (1980) 666–677.

    Google Scholar 

  43. M. Hennessy, G.D. Plotkin, Full abstraction for a simple parallel programming language, in: Proceedings 8th MFCS (J. Bečvař ed.), LNCS 74 Springer (1979) 108–120.

    Google Scholar 

  44. J.E. Hopfcroft, J.D. Ullman, Introduction to automata theory, languages and computation, Addison-Wesley, Reading, Mass., 1979.

    Google Scholar 

  45. INMOS Ltd., The Occam Programming Manual, Prentice-Hall International, London, 1984.

    Google Scholar 

  46. R. Keller, Formal verification of parallel programs, Comm. Assoc. Comput. Mach. 19 (1976) 371–384.

    Google Scholar 

  47. R. Kuiper, An operational semantics for bounded nondeterminism equivalent to a denotational one, IFIP TC2-MC Symp. on Algorithmic Languages (J.W. de Bakker & J.C. van Vliet, eds.) North-Holland, Amsterdam (1981) 373–398.

    Google Scholar 

  48. A. Mazurkiewicz, Concurrent program schemes and their interpretations, DAIMI, PB 78, Aarhus University, 1977.

    Google Scholar 

  49. J.-J. Ch. Meyer, Fixed points and the arbitrary and fair merge of a fairly simple class of processes, Tech. Reports IR-89/IR-92, Free University, Amsterdam, 1984.

    Google Scholar 

  50. J.-J. Ch. Meyer, Programming calculi based on fixed point transformations: semantics and applications, dissertation, Free University of Amsterdam, 1985.

    Google Scholar 

  51. E. Michael, Topologies on spaces of subsets, Trans. AMS 71 (1951) 152–182.

    Google Scholar 

  52. G. Milne, R. MilnerConcurrent processes and their syntax, J. ACM 26 (1979) 302–321.

    Google Scholar 

  53. R. Milner, Processes: a mathematical model of computing agents, in: Proceedings Logic Coll. 73 (Rose & Shepherdson, eds.) North-Holland, Amsterdam, 1983.

    Google Scholar 

  54. R. Milner, A calculus of communicating systems, LNCS 92, Springer, 1980.

    Google Scholar 

  55. R. Milner, Calculi for synchrony and asynchrony, TCS 25 (1983) 267–310.

    Google Scholar 

  56. R. de Nicola, M.C.B. Hennessy, Testing equivalences for processes, TCS 34 (1984) 83–134.

    Google Scholar 

  57. M. Nivat, Infinite words, infinite computations, Foundations of Computer Science III. 2, Mathematical Centre Tracts 109 (1979) 3–52.

    Google Scholar 

  58. M. Nivat, Synchronization of concurrent processes, in Formal Language Theory (R.V. Book, ed.), Academic Press, New York (1980) 429–454.

    Google Scholar 

  59. E.-R. Olderog, C.A.R. Hoare, Specification-oriented semantics for communicating processes, in: Proceedings 10th ICALP (J. Diaz, ed.), LNCS 154 Springer (1983) 561–572.

    Google Scholar 

  60. E.-R. Olderog, C.A.R. Hoare, Specification-oriented semantics for communicating processes, Tech. Monograph PRG-37, Prog. Research Group, Oxford Univ., 1984 (to appear in Acta Informatica).

    Google Scholar 

  61. D. Park, Concurrency and automata on infinite sequences, Proceedings, Theor. Comp. Sci. (P. Deussen, ed.), LNCS 104, Springer, 1981.

    Google Scholar 

  62. G.D. Plotkin, A powerdomain construction, SIAM J. Comp. 5 (1976) 452–487.

    Google Scholar 

  63. G.D. Plotkin, Dijkstra's predicate transformers and Smyth's powerdomains, in: Abstract Software Specification (D. Bjørner ed.), LNCS 86, Springer (1980) 527–553.

    Google Scholar 

  64. G.D. Plotkin, A structural approach to operational semantics, Report DAIMI FN-19, Comp. Sci. Dept., Aarhus Univ. 1981.

    Google Scholar 

  65. G.D. Plotkin, An operational semantics for CSP, in: Formal Description of Programming Concepts II (D. Bjørner ed.) North-Holland, Amsterdam (1983) 199–223.

    Google Scholar 

  66. A. Pnueli, Linear and branching structures in the semantics and logics of reactive systems, in: Proceedings 12th ICALP (W. Brauer, ed.), LNCS 194, Springer (1985) 15–32.

    Google Scholar 

  67. W.C. RoundsOn the relationships between Scott domains, synchronization trees and metric spaces, Report Univ. of Michigan CRL-TR-25-83, 1983.

    Google Scholar 

  68. W.C. Rounds, S.D. Brookes, Possible futures, acceptances, refusals, and communicating processes, in: Proceedings 22nd Symp. Found. of Comp. Sc. IEEE (1981), 140–149.

    Google Scholar 

  69. M.O. Rabin, D.S. Scott, Finite automata and their decision problems, IBM J. Res. 3:2, 1959.

    Google Scholar 

  70. D.S. Scott, Domains for denotational semantics, Proceedings 9th ICALP (M.Nielsen & E.M. Schmidt, eds.) LNCS 140, Springer (1982) 577–613.

    Google Scholar 

  71. M.B. Smyth, Power domains, JCSS 16 (1978) 23–26.

    Google Scholar 

  72. J. Stoy, Denotational semantics: The Scott-Strachey approach to programming language theory, MIT Press, Cambridge, Mass, 1977.

    Google Scholar 

  73. G. Winskel, Synchronisation trees, TCS 34 (1984) 33–82.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Centre for Mathematics and Computer Science, Kruislaan 413, 1098 SJ, Amsterdam, The Netherlands

    J. W. de Bakker & J. N. Kok

  2. Subfaculteit Wiskunde en Informatica, Vrije Universiteit, De Boelelaan 1081, 1081 HV, Amsterdam, The Netherlands

    J. -J. Ch. Meyer

  3. Institut für Informatik, Christian-Albrechts-Universität, Olshausenstrasse 40–60, 2300, Kiel 1, Federal Republic of Germany

    E.-R. Olderog

  4. Department of Computer Science, University of Buffalo (SUNY), 226 Bell Hall, 14260, Buffalo, New York, USA

    J. I. Zucker

Authors
  1. J. W. de Bakker
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. J. N. Kok
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. J. -J. Ch. Meyer
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. E.-R. Olderog
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. J. I. Zucker
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

J. W. de Bakker W. -P. de Roever G. Rozenberg

Rights and permissions

Reprints and permissions

Copyright information

© 1986 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

de Bakker, J.W., Kok, J.N., Meyer, J.J.C., Olderog, ER., Zucker, J.I. (1986). Contrasting themes in the semantics of imperative concurrency. In: de Bakker, J.W., de Roever, W.P., Rozenberg, G. (eds) Current Trends in Concurrency. Lecture Notes in Computer Science, vol 224. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0027040

Download citation

  • DOI: https://doi.org/10.1007/BFb0027040

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-16488-3

  • Online ISBN: 978-3-540-39827-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation