Abstract
This paper concerns the formal semantics of programming languages, and the specification and verification of software. We are interested in the verification of real programs, written in real programming languages, running on machines with real memory models. To this end, we verify a Caml implementation of a concurrent algorithm, Peterson’s mutual exclusion algorithm, down to the operational semantics. The implementation makes use of Caml features such as higher order parameters, state, concurrency and nested general recursion. Our Caml model includes a datatype of expressions, and a small step reduction relation for programs (a Caml expression together with a store). We also develop a new proof of correctness for a modified version of Peterson’s algorithm, designed to run on a machine with a weak memory.
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
Burckhardt, S., Alur, R., Martin, M.M.K.: Bounded model checking of concurrent data types on relaxed memory models: A case study. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 489–502. Springer, Heidelberg (2006)
Compton, M.: Stenning’s protocol implemented in UDP and verified in Isabelle. In: Atkinson, M.D., Dehne, F.K.H.A. (eds.) CATS. CRPIT, vol. 41, pp. 21–30. Australian Computer Society (2005)
Gonthier, G.: A computer-checked proof of the Four Colour Theorem (2005), http://research.microsoft.com/~gonthier/4colproof.pdf
Gopalakrishnan, G., Yang, Y., Sivaraj, H.: An efficient execution verification tool for memory orderings. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 401–413. Springer, Heidelberg (2004)
Holzmann, G.J., Bosnacki, D.: The design of a multi-core extension of the Spin Model Checker. In: FMCAD. Formal Methods in Computer Aided Design (November 2006)
Homeier, P.V., Martin, D.F.: A mechanically verified verification condition generator. Comput. J. 38(2), 131–141 (1995)
Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM, 12 (1969)
Jones, C.B.: Development methods for computer programs including a notion of interference. Technical Report PRG-25, Programming Research Group, Oxford University Computing Laboratory (1981)
Kawash, J.Y.: Limitations and capabilities of weak memory consistency systems. PhD thesis, Computer Science, University of Calgary (2000)
Liu, H., Moore, J.S.: Java program verification via a JVM deep embedding in ACL2. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol. 3223, pp. 184–200. Springer, Heidelberg (2004)
Lynch, N.A.: Distributed Algorithms. Morgan Kaufmann, San Francisco (1996)
Morris, F.L., Jones, C.B.: An early program proof by Alan Turing. Annals of the History of Computing 6(2), 143–193 (1984)
Midkiff, S.P., Lee, J., Padua, D.A.: A compiler for multiple memory models. Concurrency and Computation: Practice and Experience 16(2-3), 197–220 (2004)
Mehta, F., Nipkow, T.: Proving pointer programs in higher-order logic. Information and Computation 199, 200–227 (2005)
Peterson, G.L.: Myths about the mutual exclusion problem. Information Processing Letters 12(3), 115–116 (1981)
Ridge, T.: Simpson’s four slot algorithm in Isabelle/HOL, available online, at http://www.cl.cam.ac.uk/~tjr22
Ridge, T., Margetson, J.: A mechanically verified, sound and complete theorem prover for FOL. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, Springer, Heidelberg (2005)
Sewell, P., Nardelli, F.Z., Owens, S., Peskine, G., Ridge, T., Sarkar, S., Strniša, R.: Ott: Effective tool support for the working semanticist. In: ICFP 2007. The 12th ACM SIGPLAN International Conference on Functional Programming (accepted, 2007)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ridge, T. (2007). Operational Reasoning for Concurrent Caml Programs and Weak Memory Models. In: Schneider, K., Brandt, J. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2007. Lecture Notes in Computer Science, vol 4732. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74591-4_21
Download citation
DOI: https://doi.org/10.1007/978-3-540-74591-4_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-74590-7
Online ISBN: 978-3-540-74591-4
eBook Packages: Computer ScienceComputer Science (R0)