Abstract
A trace of the execution of a concurrent object-oriented program can be displayed in two-dimensions as a diagram of a non-metric finite geometry. The actions of a programs are represented by points, its objects and threads by vertical lines, its transactions by horizontal lines, its communications and resource sharing by sloping arrows, and its partial traces by rectangular figures.
We prove informally that the geometry satisfies the laws of Concurrent Kleene Algebra (CKA); these describe and justify the interleaved implementation of multithreaded programs on computer systems with a lesser number of concurrent processors. More familiar forms of semantics (e.g., verification-oriented and operational) can be derived from CKA.
Programs are represented as sets of all their possible traces of execution, and non-determinism is introduced as union of these sets. The geometry is extended to multiple levels of abstraction and granularity; a method call at a higher level can be modelled by a specification of the method body, which is implemented at a lower level.
The final section describes how the axioms and definitions of the geometry have been encoded in the interactive proof tool Isabelle, and reports on progress towards automatic checking of the proofs in the paper.
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
References
Alglave, J.: A formal hierarchy of weak memory models. Formal Methods Syst. Des. 41(2), 178–210 (2012)
Armstrong, A., Gomes, V.B.F., Struth, G.: Algebraic principles for rely-guarantee style concurrency verification tools. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 78–93. Springer, Cham (2014)
Armstrong, A., Gomes, V.B.F., Struth, G.: Building program construction and verification tools from algebraic principles. Formal Aspects Comput. 28(2), 265–293 (2016)
Brink, C.: Power structures. Algebra Univ. 30(2), 177–216 (1993)
Brink, C., Rewitzky, I.: A Paradigm for Program Semantics: Power Structures and Duality. CSLI Publications, Stanford (2001)
Brookes, S.: A semantics for concurrent separation logic. Theoret. Comput. Sci. 375, 227–270 (2007)
Conway, J.H.: Regular Algebra and Finite Machines. Chapman and Hall, London (1971)
Damm, W., Harel, D.: LSCs - breathing life into message sequence charts. Formal Methods Syst. Des. 19(1), 45–80 (2001)
Dongol, B., Gomes, V.B.F., Struth, G.: A program construction and verification tool for separation logic. In: Hinze, R., Voigtländer, J. (eds.) MPC 2015. LNCS, vol. 9129, pp. 137–158. Springer, Cham (2015)
Gautam, N.: The validity of equations of complex algebras. Arch. Math. Logik Grundl. Mat. 443, 117–124 (1957)
Goldblatt, R.: Varieties of complex algebras. Ann. Pure Appl. Logic 44, 173–242 (1989)
Gomes, V.B.F., Struth, G.: Program construction and verification components based on Kleene algebra. Archive of Formal Proofs (2016)
Gomes, V.B.F., Struth, G.: Modal Kleene algebra applied to program correctness. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 310–325. Springer, Heidelberg (2016)
Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice Hall, Upper Saddle River (1998)
Hoare, C.A.R., Hussain, A., Möller, B., O’Hearn, P.W., Petersen, R.L., Struth, G.: On locality and the exchange law for concurrent processes. In: Katoen, J.-P., König, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 250–264. Springer, Heidelberg (2011)
Hoare, T., Möller, B., Müller, M.: Tracelets and Specifications. Dept of Informatics, University of Augsburg (2016). No. 2017-01
Hoare, T., Möller, B., Struth, G., Wehrman, I.: Concurrent Kleene algebra and its foundations. J. Log. Algebr. Program. 80(6), 266–296 (2011)
Hoare, T., van Staden, S., Möller, B., Struth, G., Zhu, H.: Developments in concurrent Kleene algebra. J. Log. Algebr. Meth. Program. 85(4), 617–636 (2016)
Horn, A., Alglave, J.: Concurrent Kleene Algebra of partial strings. arXiv.org, July 2014
Main, M.: A powerdomain primer – a tutorial for the bulletin of the EATCS 33. Technical report CU-CS-375-87 (1987). Paper 360, Univ. Colorado at Boulder, Dept of Computer Science (1987). http://scholar.colorado.edu/csci_techreports/360
Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle/HOL – A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)
O’Hearn, P.W., Petersen, R.L., Villard, J., Hussain, A.: On the relation between concurrent separation logic and concurrent Kleene algebra. J. Log. Algebr. Meth. Program. 84(3), 285–302 (2015)
Petri, C.A.: Communication with automata. Technical report RADC TR 65-377, RADC, Research and Technology Division, New York (1966)
Winskel, G.: On power domains and modality. Theoret. Comput. Sci. 36, 127–137 (1985)
Acknowledgements
We are grateful for valuable input from discussions with Jade Alglave, Peter OHearn, Peter Höfner, Matthew Parkinson, Stephan van Staden, Ian Wehrman, John Wickerson and Huibiao Zhu.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Möller, B., Hoare, T., Müller, M.E., Struth, G. (2017). A Discrete Geometric Model of Concurrent Program Execution. In: Bowen, J., Zhu, H. (eds) Unifying Theories of Programming. UTP 2016. Lecture Notes in Computer Science(), vol 10134. Springer, Cham. https://doi.org/10.1007/978-3-319-52228-9_1
Download citation
DOI: https://doi.org/10.1007/978-3-319-52228-9_1
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-52227-2
Online ISBN: 978-3-319-52228-9
eBook Packages: Computer ScienceComputer Science (R0)