zbMATH — the first resource for mathematics

Operational reasoning for concurrent Caml programs and weak memory models. (English) Zbl 1144.68305
Schneider, Klaus (ed.) et al., Theorem proving in higher order logics. 20th international conference, TPHOLs 2007, Kaiserslautern, Germany, September 10–13, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-74590-7/pbk). Lecture Notes in Computer Science 4732, 278-293 (2007).
Summary: 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.
For the entire collection see [Zbl 1142.68010].

68N15 Theory of programming languages
68Q55 Semantics in the theory of computing
68Q60 Specification and verification (program logics, model checking, etc.)
ACL2; SPIN; Ott; Isabelle/HOL
Full Text: DOI