Abstract
This paper studies algebraic models for concurrency, in light of recent work on Concurrent Kleene Algebra and Separation Logic. It establishes a strong connection between the Concurrency and Frame Rules of Separation Logic and a variant of the exchange law of Category Theory. We investigate two standard models: one uses sets of traces, and the other is state-based, using assertions and weakest preconditions. We relate the latter to standard models of the heap as a partial function. We exploit the power of algebra to unify models and classify their variations.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Bloom, S.L., Ésik, Z.: Free shuffle algebras in language varieties. TCS 163(182), 55–98 (1996)
Brookes, S.D.: A semantics of concurrent separation logic. TCS 375(1-3), 227–270 (2007); Prelim. version appeared in CONCUR 2004
Calcagno, C., O’Hearn, P.W., Yang, H.: Local action and abstract separation logic. In: LICS, pp. 366–378. IEEE Computer Society, Los Alamitos (2007)
Dijkstra, E.W.: A discipline of programming. Prentice-Hall series in automatic computation. Prentice-Hall, Englewood Cliffs (1976)
Gischer, J.L.: The equational theory of pomsets. TCS 61, 199–224 (1988)
Hoare, C.A.R., Jifeng, H.: Unifying Theories of Programming. Prentice-Hall series in computer science. Prentice-Hall, Englewood Cliffs (1998)
Hoare, T., Möller, B., Struth, G., Wehrman, I.: Concurrent Kleene algebra and its foundations. Journal of Logic and Algebraic Programming (2011); Prelim. version in CONCUR 2009
Kozen, D.: A completeness theorem for Kleene algebras and the algebra of regular events. Inf. Comput. 110(2), 366–390 (1994)
O’Hearn, P.W.: Resources, concurrency and local reasoning. TCS 375(1-3), 271–307 (2004); Prelim. version appeared in CONCUR 2004
Yang, H., O’Hearn, P.W.: A semantic basis for local reasoning. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol. 2303, pp. 402–416. Springer, Heidelberg (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hoare, C.A.R., Hussain, A., Möller, B., O’Hearn, P.W., Petersen, R.L., Struth, G. (2011). On Locality and the Exchange Law for Concurrent Processes. In: Katoen, JP., König, B. (eds) CONCUR 2011 – Concurrency Theory. CONCUR 2011. Lecture Notes in Computer Science, vol 6901. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-23217-6_17
Download citation
DOI: https://doi.org/10.1007/978-3-642-23217-6_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-23216-9
Online ISBN: 978-3-642-23217-6
eBook Packages: Computer ScienceComputer Science (R0)