Ben Selfridge

An ACL2 Mechanization of an Axiomatic Weak Memory Model

ACL2 Seminar, Feb. 28, 2014


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: