Abstract
This research started with an algebra for reasoning about rely/guarantee concurrency for a shared memory model. The approach taken led to a more abstract algebra of atomic steps, in which atomic steps synchronise (rather than interleave) when composed in parallel. The algebra of rely/guarantee concurrency then becomes an interpretation of the more abstract algebra. Many of the core properties needed for rely/guarantee reasoning can be shown to hold in the abstract algebra where their proofs are simpler and hence allow a higher degree of automation. Moreover, the realisation that the synchronisation mechanisms of standard process algebras, such as CSP and CCS/SCCS, can be interpreted in our abstract algebra gives evidence of its unifying power. The algebra has been encoded in Isabelle/HOL to provide a basis for tool support.
This work is supported by Australian Research Council (ARC) Discovery Project DP130102901 and the UK EPSRC Taming Concurrency research grant.
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
Notes
- 1.
We use the terms command, program and process synonymously.
- 2.
Here our approach based on DRA differs from approaches based on Kleene algebra, like CKA and SKA, in which \(\top \) is also a right annihilator.
- 3.
A semantic model for this interpretation may be found in [CHM16].
- 4.
References
Aczel, P.H.G.: On an inference rule for parallel composition, Private communication to Cliff Jones (1983). http://homepages.cs.ncl.ac.uk/cliff.jones/publications/MSs/PHGA-traces.pdf
Berry, G., Cosserat, L.: The ESTEREL synchronous programming language and its mathematical semantics. In: Brookes, S.D., Roscoe, A.W., Winskel, G. (eds.) CONCURRENCY 1984. LNCS, vol. 197, pp. 389–448. Springer, Heidelberg (1985). doi:10.1007/3-540-15670-4_19
Bergstra, J.A., Klop, J.W.: Process algebra for synchronous communication. Inf. Control 60(1–3), 109–137 (1984)
Bergstra, J.A., Klop, J.W.: Algebra of communicating processes with abstraction. Theor. Comput. Sci. 37, 77–121 (1985)
Blikle, A.: Specified programming. In: Blum, E.K., Paul, M., Takasu, S. (eds.) Mathematical Studies of Information Processing. LNCS, vol. 75, pp. 228–251. Springer, Heidelberg (1979). doi:10.1007/3-540-09541-1_29
Brookes, S.D.: On the relationship of CCS and CSP. In: Diaz, J. (ed.) ICALP 1983. LNCS, vol. 154, pp. 83–96. Springer, Heidelberg (1983). doi:10.1007/BFb0036899
Colvin, R.J., Hayes, I.J., Meinicke, L.A.: Designing a semantic model for a wide-spectrum language with concurrency (2016). http://arxiv.org/abs/1609.00195
Coleman, J.W., Jones, C.B.: A structural proof of the soundness of rely/guarantee rules. Journal of Logic and Computation 17(4), 807–841 (2007)
Conway, J.H.: Regular Algebra and Finite Machines. Chapman & Hall, Boca Raton (1971)
de Roever, W.-P., Verification, C.: Introduction to Compositional and Noncompositional Methods. Cambridge University Press, Cambridge (2001)
Gardiner, P.H.B., Morgan, C.: A single complete rule for data refinement. Formal Aspects Comput. 5, 367–382 (1993)
Hayes, I.J.: Generalised rely-guarantee concurrency: an algebraic foundation. Form. Asp. Comput. 28(6), 1057–1078 (2016)
Hayes, I.J., Colvin, R.J., Meinicke, L.A., Winter, K., Velykis, A.: An algebra of synchronous atomic steps (2016). http://arxiv.org/pdf/1609.00118v1.pdf
He, J., Hoare, C.A.R.: CSP is a retract of CCS. Theor. Comput. Sci. 411(11–13), 1311–1337 (2010)
Hayes, I.J., Jones, C.B., Colvin, R.J.: Laws and semantics for rely-guarantee refinement. Technical report CS-TR-1425, Newcastle University, July 2014
Hoare, C.A.R., Möller, B., Struth, G., Wehrman, I.: Concurrent Kleene algebra and its foundations. J. Log. Algebr. Program. 80(6), 266–296 (2011)
Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Upper Saddle River (1985)
Jones, C.B., Hayes, I.J., Colvin, R.J.: Balancing expressiveness in formal approaches to concurrency. Formal Aspects Comput. 27(3), 475–497 (2015)
Development methods for computer programs including a notion of interference. Ph.D. thesis, Oxford University, June 1981: Oxford University Computing Laboratory (now Computer Science) Technical Monograph PRG-25
Jones, C.B.: Specification and design of (parallel) programs. In: Proceedings of IFIP 1983, pp. 321–332. North-Holland (1983)
Kozen, D.: Kleene algebra with tests. ACM Trans. Prog. Lang. Sys. 19(3), 427–443 (1997)
Milner, R.: Calculi for synchrony and asynchrony. Theor. Comput. Sci. 25(3), 267–310 (1983)
Milner, A.J.R.G.: Communication and Concurrency. Prentice-Hall, Upper Saddle River (1989)
Morgan, C.C.: The specification statement. ACM Trans. Prog. Lang. Sys. 10(3), 403–419 (1988)
Prisacariu, C.: Synchronous Kleene algebra. J. Logic Algebraic Program. 79(7), 608–635 (2010)
Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice Hall, Upper Saddle River (1998)
Solin, K.: Abstract algebra of program refinement. Ph.D. thesis, Turku Centre for Computer Science (2007)
van Glabbeek, R.J.: Notes on the methodology of CCS and CSP. Theor. Comput. Sci. 177(2), 329–349 (1997)
von Wright, J.: Towards a refinement algebra. Sci. Comput. Program. 51, 23–45 (2004)
Acknowledgements
This work has benefited from input from Cliff Jones and Kim Solin.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing AG
About this paper
Cite this paper
Hayes, I.J., Colvin, R.J., Meinicke, L.A., Winter, K., Velykis, A. (2016). An Algebra of Synchronous Atomic Steps. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds) FM 2016: Formal Methods. FM 2016. Lecture Notes in Computer Science(), vol 9995. Springer, Cham. https://doi.org/10.1007/978-3-319-48989-6_22
Download citation
DOI: https://doi.org/10.1007/978-3-319-48989-6_22
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-48988-9
Online ISBN: 978-3-319-48989-6
eBook Packages: Computer ScienceComputer Science (R0)