2014/06/04 by Benjamin Selfridge
Computer Science · #Distributed systems and fault tolerance #Logic, programming, and type systems #Parallel Computing and Optimization Techniques #cs.LO
paper · pdf · doi:10.4204/eptcs.152.11
published as EPTCS 152, 2014, pp. 129-144 · In Proceedings ACL2 2014, arXiv:1406.1238
openalex publication_date 2014/06/04 · arxiv created 2014/06/06 · arxiv updated 2014/06/09 · openalex created_date 2016/06/24 · openalex updated_date 2026/07/31
Proving the correctness of programs written for multiple processors is a challenging problem, 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 programs in spite of a lack of full sequential consistency. In this work, we present a mechanization in the ACL2 theorem prover of an axiomatic weak memory model (introduced by Alglave et al.). In the process, we provide a new proof of an established theorem involving these axioms.