An ACL2 Mechanization of an Axiomatic Framework for Weak Memory

ABSTRACT. Proving the correctness of programs written for multiple processors is a challenging proglem, due in no small part to the weaker memory guarantees afforded by most modern architectures. In particular, the existence of store 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