More Web Proxy on the site http://driver.im/

Article

Free access

Denotational semantics of concurrency

Authors:

J. W. de Bakker,

J. I. ZuckerAuthors Info & Claims

STOC '82: Proceedings of the fourteenth annual ACM symposium on Theory of computing

Pages 153 - 158

https://doi.org/10.1145/800070.802188

Published: 05 May 1982 Publication History

Abstract

A general framework for the denotational treatment of concurrency is introduced. The key idea is the notion of process which is element of a domain obtained as solution of a domain equation in the style as considered previously by Plotkin. We use tools from metric topology as advocated by Nivat to solve this equation, show how operations upon processes can be defined conveniently, and illustrate the approach with the definition of a variety of concepts as encountered in the study of concurrency. Only few proofs of the supporting mathematical theory are given; full proofs will appear in the final version of the paper.

References

[1]

K.R. Apt -&-amp; G.D. Plotkin, A Cook's tour of countable nondeterminism, Proc. 8th ICALP (Even -&-amp; Kariv, eds), 479-494, Lecture Notes in Comp. Sci., 115, Springer, 1981.

Digital Library

[2]

A. Arnold -&-amp; M. Nivat, The metric space of infinite trees. Algebraic and topological properties, Fund. Inf. III, 4 (1980), 445-476.

[3]

R.J. Back, Semantics of unbounded nondeterminism, Proc. 7th ICALP (De Bakker -&-amp; van Leeuwen, eds), 52-63, Lecture Notes in Comp. Sci., 85, Springer, 1980.

Digital Library

[4]

J.W. de Bakker, Semantics of infinite processes using generalized trees, Proc. 6th MFCS (Gruska, ed.), 240-252, Lecture Notes in Comp. Sci., 53, Springer, 1977).

[5]

J.W. de Bakker, Mathematical Theory of Program Correctness, Prentice Hall International, 1980.

Digital Library

[6]

H. Beki-&-cacute;, Towards a mathematical theory of processes, Tech. Rep. TR 25.125, IBM Lab. Vienna, 1971.

[7]

L. Boasson -&-amp; M. Nivat, Adherences of languages, J. Comp. Syst. Sciences, 20 (3), 281-309 (1980).

[8]

A. de Bruin, On the existence of Cook semantics, Mathematisch Centrum Report IW 163/81. 1981.

[9]

S.A. Cook, Soundness and completeness of an axiom system for program verification, SIAM J. on Comp., 7, 70-90 (1978).

Digital Library

[10]

Dugundji, Topology, Allen -&-amp; Bacon, 1966.

[11]

E.W. Dijkstra, A Discipline of Programming, Prentice-Hall, 1976.

Digital Library

[12]

R. Engelking, General Topology, Polish Scientific Publishers, 1977.

[13]

H. Hahn, Reelle Funktionen, Chelsea, 1948.

[14]

C.A.R. Hoare, Communicating sequential processes, C. ACM 21(8), 666-677 (1978).

Digital Library

[15]

R. Kuiper., An operational semantics for bounded determinism equivalent to an denotational one, IFIP TC. 2-MC Symp. on Algorithmic Languages (De Bakker -&-amp; Van Vliet, eds). 373-398, North-Holland, 1981.

[16]

D. Lehmann, Categories for fixed point semantics, Proc. 17th IEEE Symp. on Found. of Comp. Sci., 122-126, 1976.

[17]

G. Milne -&-amp; R. Milner, Concurrent processes and their syntax, J, ACM 26, 302-321 (1979).

Digital Library

[18]

R. Milner, A Calculus of Communicating Systems, Lect. Notes in Comp. Sci., 92, Springer, 1980.

Digital Library

[19]

Nivat, M., Infinite words, infinite trees, infinite computations, Foundations of Comp. Sci., III, 2 (De Bakker -&-amp; Van Leeuwen, eds) 3-52, Mathematical Centre Tracts 109, 1979.

[20]

M. Nivat, Synchronization of concurrent processes,in: Formal Language Theory (Book, ed.) 429-454, Academic Press, 1980.

[21]

S. Owicki -&-amp; D. Gries, Verifying properties of parallel programs, an axiomatic approach, C. ACM 19, 279-285 (1976).

Digital Library

[22]

D. Park, On the semantics of fair parallelism,in: Abstract Software Specification (Bj-&-oslash;rner, ed.), 504-526, Lect. Notes in Comp. Sci., 86, Springer, 1980.

Digital Library

[23]

G.D. Plotkin, A power domain construction, SIAM J. on Comp. 5, 452-487 (1976).

Digital Library

[24]

G.D. Plotkin, An operational semantics for CSP, Univ. of Edinburgh, 1981.

[25]

A. Pnueli, The temporal logic of programs, Proc. 19th Ann. Symp. on Foundations of Comp. Sci., 46-57, 1977.

Digital Library

[26]

D. Scott, Data type as lattices, SIAM J. on Comp., 5, 522-587 (1976).

Digital Library

[27]

D. Scott, Domain equations,in: Proc. 6th IBM Symp. on Math. Found. of Comp. Sci., 103-256, Corporate -&-amp; Scientific Program, IBM Japan, 1981.

[28]

M.B. Smyth, Power domains, Journ. of Comp. Syst. Sci., 16, 23-36 (1978).

[29]

J. Stoy, Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory, MIT Press, 1977.

Digital Library

Cited By

Gavazzo FDi Florio C(2023)Elements of Quantitative RewritingProceedings of the ACM on Programming Languages10.1145/35712567:POPL(1832-1863)Online publication date: 11-Jan-2023
https://doi.org/10.1145/3571256
Abdallah AHoffmann R(2020)The Local Approach to Programming Language TheoryContinuous Lattices and Their Applications10.1201/9781003072621-13(219-236)Online publication date: 11-Dec-2020
https://doi.org/10.1201/9781003072621-13
Tang Qvan Breugel F(2020)Deciding Probabilistic Bisimilarity Distance One for Probabilistic AutomataJournal of Computer and System Sciences10.1016/j.jcss.2020.02.003Online publication date: Mar-2020
https://doi.org/10.1016/j.jcss.2020.02.003
Show More Cited By

Denotational semantics of concurrency
1. Theory of computation
  1. Semantics and reasoning

Recommendations

Semantics-based concurrency control: beyond commutativity

The concurrency of transactions executing on atomic data types can be enhanced through the use of semantic information about operations defined on these types. Hitherto, commutativity of operations has been exploited to provide enchanced concurrency ...
An Experiment with Denotational Semantics
Abstract
The paper is devoted to showing how to systematically design a programming language in “reverse order”, i.e., from denotations to syntax. This construction is developed in an algebraic framework consisting of three many-sorted algebras: of ...
Semantics-based Concurrency Contro: Beyond Commutativity

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

STOC '82: Proceedings of the fourteenth annual ACM symposium on Theory of computing

May 1982

408 pages

ISBN:0897910702

DOI:10.1145/800070

Copyright © 1982 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGACT: ACM Special Interest Group on Algorithms and Computation Theory

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 05 May 1982

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Acceptance Rates

Overall Acceptance Rate 1,469 of 4,586 submissions, 32%

Upcoming Conference

STOC '25

Sponsor:
sigact

57th Annual ACM Symposium on Theory of Computing (STOC 2025)

June 23 - 27, 2025

Prague , Czech Republic

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

38
Total Citations
View Citations
212
Total Downloads

Downloads (Last 12 months)73
Downloads (Last 6 weeks)7

Reflects downloads up to 03 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Gavazzo FDi Florio C(2023)Elements of Quantitative RewritingProceedings of the ACM on Programming Languages10.1145/35712567:POPL(1832-1863)Online publication date: 11-Jan-2023
https://doi.org/10.1145/3571256
Abdallah AHoffmann R(2020)The Local Approach to Programming Language TheoryContinuous Lattices and Their Applications10.1201/9781003072621-13(219-236)Online publication date: 11-Dec-2020
https://doi.org/10.1201/9781003072621-13
Tang Qvan Breugel F(2020)Deciding Probabilistic Bisimilarity Distance One for Probabilistic AutomataJournal of Computer and System Sciences10.1016/j.jcss.2020.02.003Online publication date: Mar-2020
https://doi.org/10.1016/j.jcss.2020.02.003
Audrito GViroli MDamiani FPianini DBeal J(2019)A Higher-Order Calculus of Computational FieldsACM Transactions on Computational Logic10.1145/328595620:1(1-55)Online publication date: 4-Jan-2019
https://dl.acm.org/doi/10.1145/3285956
Gavazzo F(2018)Quantitative Behavioural Reasoning for Higher-order Effectful ProgramsProceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3209108.3209149(452-461)Online publication date: 9-Jul-2018
https://dl.acm.org/doi/10.1145/3209108.3209149
Goens ACastrillon J(2018)Analysis of Process Traces for Mapping Dynamic KPN Applications to MPSoCsSystem Level Design from HW/SW to Memory for Embedded Systems10.1007/978-3-319-90023-0_10(116-127)Online publication date: 17-Apr-2018
https://doi.org/10.1007/978-3-319-90023-0_10
Azevedo de Amorim AGaboardi MHsu JKatsumata SCherigui I(2017)A semantic account of metric preservationACM SIGPLAN Notices10.1145/3093333.300989052:1(545-556)Online publication date: 1-Jan-2017
https://dl.acm.org/doi/10.1145/3093333.3009890
Azevedo de Amorim AGaboardi MHsu JKatsumata SCherigui ICastagna GGordon A(2017)A semantic account of metric preservationProceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages10.1145/3009837.3009890(545-556)Online publication date: 1-Jan-2017
https://dl.acm.org/doi/10.1145/3009837.3009890
McCorkle EHosking AEugster PHirschfeld R(2013)Building connections between theories of computing and physical systemsProceedings of the 2013 ACM international symposium on New ideas, new paradigms, and reflections on programming & software10.1145/2509578.2509587(153-172)Online publication date: 29-Oct-2013
https://dl.acm.org/doi/10.1145/2509578.2509587
Liu BWu J(2012)Polynomial process algebraProceedings of the 10th World Congress on Intelligent Control and Automation10.1109/WCICA.2012.6358386(3004-3007)Online publication date: Jul-2012
https://doi.org/10.1109/WCICA.2012.6358386
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents