Skip to content

Research at St Andrews

A Better x86 Memory Model: x86-TSO

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Author(s)

Scott Owens, Susmit Sarkar, Peter Sewell

School/Research organisations

Abstract

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.

Close

Details

Original languageEnglish
Title of host publicationTHEOREM PROVING IN HIGHER ORDER LOGICS, PROCEEDINGS
EditorsS Berghofer, T Nipkow, C Urban, M Wenzel
Place of PublicationBERLIN
PublisherSpringer-Verlag
Pages391-407
Number of pages17
ISBN (Print)978-3-642-03358-2
StatePublished - 2009
Event22nd International Conference on Theorem Proving in Higher Order Logics - Munich, Germany
Duration: 17 Aug 200920 Aug 2009

Publication series

NameLecture Notes in Computer Science
PublisherSPRINGER-VERLAG BERLIN
Volume5674
ISSN (Print)0302-9743

Conference

Conference22nd International Conference on Theorem Proving in Higher Order Logics
CountryGermany
CityMunich
Period17/08/0920/08/09

    Research areas

  • VERIFICATION

Discover related content
Find related publications, people, projects and more using interactive charts.

View graph of relations

Related by author

  1. Memory consistency models using constraints

    Akgün, Ö., Hoffmann, R. & Sarkar, S. 27 Aug 2018 The Seventeenth Workshop on Constraint Modelling and Reformulation (ModRef 2018), Proceedings. 16 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  2. Automatically deriving cost models for structured parallel processes using hylomorphisms

    Castro, D., Hammond, K., Sarkar, S. & Alguwaifli, Y. Feb 2018 In : Future Generation Computer Systems. 79, Part 2, p. 653-668

    Research output: Contribution to journalArticle

  3. Simplifying ARM concurrency: multicopy-atomic axiomatic and operational models for ARMv8

    Pulte, C., Flur, S., Deacon, W., French, J., Sarkar, S. & Sewell, P. Jan 2018 Proceedings of the ACM on Programming Languages (POPL '18). New York: ACM, Vol. 2 Issue POPL, 29 p. 19

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  4. Verification of a lazy cache coherence protocol against a weak memory model

    Banks, C., Elver, M., Hoffmann, R., Sarkar, S., Jackson, P. & Nagarajan, V. 2 Oct 2017 Proceedings of the 17th Conference on Formal Methods in Computer-Aided Design (FMCAD). ACM, p. 60-67

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  5. Mixed-size Concurrency: ARM, POWER, C/C++11, and SC

    Flur, S., Sarkar, S., Pulte, C., Nienhuis, K., Maranget, L., Gray, K., Sezgin, A., Batty, M. & Sewell, P. 1 Jan 2017 Proceedings of the 44th annual ACM-SIGPLAN Symposium on Principles of programming languages. ACM, p. 429-442

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

ID: 44377146