Ben Selfridge
An ACL2 Mechanization of an Axiomatic Weak Memory Model
ACL2 Seminar, Feb. 28, 2014
Abstract:
Proving the correctness of programs written for multiple
processors is a challenging problem, in no small part due to the
weaker memory guarantees afforded by most modern architectures. In
particular, the use of write buffers means that the programmer can no
longer assume that writes to different locations become visible to all
processors in the same order. However, all practical architectures do
provide a collection of weaker guarantees about memory consistency
across processors, which enable the programmer to write provably
correct programs in spite of a lack of full sequential consistency. In
this work, we present a new mechanization in the ACL2 theorem prover
of an axiomatic weak memory model [1]. In the process, we provide a new
proof of the equivalence of one of these axioms, SC-per-location, to
the rejection of five simple patterns.
[1] Jade Alglave, Luc Maranget, and Michael Tautschnig. Herding Cats -
Modelling, simulation, testing, and data-mining for weak memory. To
appear in TOPLAS. URL: http://arxiv.org/abs/1308.6810