x86-TSO in ACL2: Current Status and Future Directions
Ben Selfridge
Jan. 20, 2015

Understanding the semantics of concurrent memory operations on the x86
architecture can be a daunting task due to the complexity of its
presentation in the Intel and AMD software manuals. x86-TSO is a
memory model (devised by Sewell et al.) for concurrent x86 programs
that is rigorous and sound with respect to actual hardware. We present
an ACL2 mechanization of this memory model, and discuss possible
future directions, along with potential strategies for incorporating
this memory model into the ACL2 x86 ISA model.