Skip to main content
Kent Academic Repository

A Better x86 Memory Model: x86-TSO

Owens, Scott and Sarkar, Susmit and Sewell, Peter (2009) A Better x86 Memory Model: x86-TSO. In: Berghofer, Stefan and Nipkow, Tobias and Urban, Christian and Wenzel, Makarius, eds. Theorem Proving in Higher Order Logics 22nd International Conference. Lecture Notes in Computer Science . Springer, Berlin, Germany, pp. 391-407. ISBN 978-3-642-03358-2. E-ISBN 978-3-642-03359-9. (doi:10.1007/978-3-642-03359-9_27) (The full text of this publication is not currently available from this repository. You may be able to access a copy if URLs are provided) (KAR id:31903)

The full text of this publication is not currently available from this repository. You may be able to access a copy if URLs are provided.
Official URL:
http://dx.doi.org/10.1007/978-3-642-03359-9_27

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.

Item Type: Book section
DOI/Identification number: 10.1007/978-3-642-03359-9_27
Uncontrolled keywords: event structure; memory model; abstract machine; memory order; actual processor
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Scott Owens
Date Deposited: 24 Oct 2012 10:20 UTC
Last Modified: 16 Nov 2021 10:09 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/31903 (The current URI for this page, for reference purposes)

University of Kent Author Information

  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.