Sciweavers

TPHOL
2007
IEEE

Operational Reasoning for Concurrent Caml Programs and Weak Memory Models

13 years 12 months ago
Operational Reasoning for Concurrent Caml Programs and Weak Memory Models
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.
Tom Ridge
Added 04 Jun 2010
Updated 04 Jun 2010
Type Conference
Year 2007
Where TPHOL
Authors Tom Ridge
Comments (0)