An ACL2 Mechanization of an Axiomatic Framework for Weak Memory
The work
| Authors | Benjamin Selfridge |
|---|---|
| Editors | |
| Type | inproceedings |
| Year | 2014 |
| Citekey | selfridge2014acl2 |
Where it appeared
| Published in | Proceedings of the 12th International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 2014) |
|---|---|
| Series | Electronic Proceedings in Theoretical Computer Science |
| Volume | 152 |
Identifiers
| arXiv | 1406.1563 from its landing_page_url |
|---|---|
| DOI | 10.4204/eptcs.152.11 |
Access
| Landing page | https://arxiv.org/abs/1406.1563 |
|---|
Related
| Distinct from | lee2026formal |
|---|---|
| Distinct from | poncedeleon2022cats |
| Distinct from | ravi2024qed |
From bibtex.
Abstract
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.
A copy is held
pdf, 123.0 kB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via bibtex |
|---|---|
| Added | 2026-09-17 21:34 UTC |
| Approved by | a person 2026-10-05 21:25 UTC |
Filed under
Cite it as
@inproceedings{selfridge2014acl2,
title = {An ACL2 Mechanization of an Axiomatic Framework for Weak Memory},
author = {Benjamin Selfridge},
year = {2014},
booktitle = {Proceedings of the 12th International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 2014)},
series = {Electronic Proceedings in Theoretical Computer Science},
volume = {152},
doi = {10.4204/eptcs.152.11},
}
This record lives at https://refs.drheap.org/selfridge2014acl2/ and will keep doing so.