UCAM-CL-TR-745: A better x86 memory model: x86-TSO (extended version)
tech-r...@cl.cam.ac.uk
A better x86 memory model: x86-TSO
(extended version)
Scott Owens, Susmit Sarkar, Peter Sewell
Technical report UCAM-CL-TR-745, University of Cambridge,
Computer Laboratory, March 2009, 52 pages.
This document is now available at
http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-745.html
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.
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.
--
University of Cambridge, Computer Laboratory,
Technical Reports (ISSN 1476-2986)
http://www.cl.cam.ac.uk/techreports/