TY - GEN

T1 - A Better x86 Memory Model: x86-TSO

AU - Owens, Scott

AU - Sarkar, Susmit

AU - Sewell, Peter

PY - 2009

Y1 - 2009

N2 - Real multiprocessors do not provide the sequentially consistent memory that is assumed by most work oil semantics and verification. Instead, they have relaxed memory models, typically described in ambiguous prose, which lead to widespread confusion. These are prune 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, a:3 well as arguably too weak to program above. We discuss these issue's 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. Both are adapted to handle x86-specific features. We have implemented the axiomatic model in our memevents tool; which calculates the set of all valid executions of test programs, and, for greater confidence, verify the witnesses of such executions directly, with code extracted from a third, more algorithmic, equivalent version of the definition.

AB - Real multiprocessors do not provide the sequentially consistent memory that is assumed by most work oil semantics and verification. Instead, they have relaxed memory models, typically described in ambiguous prose, which lead to widespread confusion. These are prune 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, a:3 well as arguably too weak to program above. We discuss these issue's 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. Both are adapted to handle x86-specific features. We have implemented the axiomatic model in our memevents tool; which calculates the set of all valid executions of test programs, and, for greater confidence, verify the witnesses of such executions directly, with code extracted from a third, more algorithmic, equivalent version of the definition.

KW - VERIFICATION

M3 - Conference contribution

SN - 978-3-642-03358-2

T3 - Lecture Notes in Computer Science

SP - 391

EP - 407

BT - THEOREM PROVING IN HIGHER ORDER LOGICS, PROCEEDINGS

A2 - Berghofer, S

A2 - Nipkow, T

A2 - Urban, C

A2 - Wenzel, M

PB - Springer-Verlag

CY - BERLIN

T2 - 22nd International Conference on Theorem Proving in Higher Order Logics

Y2 - 17 August 2009 through 20 August 2009

ER -