Sciweavers

TPHOL
2009
IEEE

A Better x86 Memory Model: x86-TSO

14 years 7 months ago
A Better x86 Memory Model: x86-TSO
Abstract. Real multiprocessors do not provide the sequentially consistent memory that is assumed by most work on semantics and verification. Instead, they have relaxed memory models, typically described in ambiguous prose, which lead to widespread confusion. These are prime targets for mechanized formalization. In previous work we produced a rigorous x86-CC model, formalizing the Intel and AMD architecture specifications of the time, but those turned out to be unsound with respect to actual hardware, as well as arguably too weak to program above. We discuss these issues and present a new x86-TSO model that suffers from neither problem, formalized in HOL4. We believe it is sound with respect to real processors, reflects better the vendor’s intentions, and is also better suited for programming. We give two equivalent definitions of x86-TSO: an intuitive operational model based on local write buffers, and an axiomatic total store ordering model, similar to that of the SPARCv8. Bot...
Scott Owens, Susmit Sarkar, Peter Sewell
Added 24 May 2010
Updated 24 May 2010
Type Conference
Year 2009
Where TPHOL
Authors Scott Owens, Susmit Sarkar, Peter Sewell
Comments (0)