Skip to content

Research at St Andrews

The Semantics of x86-CC Multiprocessor Machine Code

Research output: Contribution to journalArticle

DOI

Author(s)

Susmit Sarkar, Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Tom Ridge, Thomas Braibant, Magnus O. Myreen, Jade Alglave

School/Research organisations

Abstract

Multiprocessors are now dominant, but real multiprocessors do not provide the sequentially consistent memory that is assumed by most work on semantics and verification. Instead, they have subtle relaxed (or weak) memory models, usually described only in ambiguous prose, leading to widespread confusion.

We develop a rigorous and accurate semantics for x86 multiprocessor programs, from instruction decoding to relaxed memory model, mechanised in HOL. We test the semantics against actual processors and the vendor litmus-test examples, and give an equivalent abstract-machine characterisation of our axiomatic memory model. For programs that are (in some precise sense) data-race free, we prove in HOL that their behaviour is sequentially consistent. We also contrast the x86 model with some aspects of Power and ARM behaviour.

This provides a solid intuition for low-level programming, and a sound foundation for future work on verification, static analysis, and compilation of low-level concurrent code.

Close

Details

Original languageEnglish
Pages (from-to)379-391
Number of pages13
JournalACM SIGPLAN Notices
Volume44
Issue number1
DOIs
StatePublished - Jan 2009

    Research areas

  • Standardization, Documentation, Relaxed Memory Models, Reliability, Verification, MODELS, SHARED-MEMORY, Semantics, Theory

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

Related by journal

  1. Clarifying and Compiling C/C++ Concurrency: from C++11 to POWER

    Batty, M., Memarian, K., Owens, S., Sarkar, S. & Sewell, P. Jan 2012 In : ACM SIGPLAN Notices. 47, 1, p. 509-520 12 p.

    Research output: Contribution to journalArticle

  2. Synchronising C/C plus plus and POWER

    Sarkar, S., Memarian, K., Owens, S., Batty, M., Sewell, P., Maranget, L., Alglave, J. & Williams, D. Jun 2012 In : ACM SIGPLAN Notices. 47, 6, p. 311-321 11 p.

    Research output: Contribution to journalArticle

  3. Mathematizing C++ Concurrency

    Batty, M., Owens, S., Sarkar, S., Sewell, P. & Weber, T. Jan 2011 In : ACM SIGPLAN Notices. 46, 1, p. 55-66 12 p.

    Research output: Contribution to journalArticle

  4. Understanding POWER Multiprocessors

    Sarkar, S., Sewell, P., Alglave, J., Maranget, L. & Williams, D. Jun 2011 In : ACM SIGPLAN Notices. 46, 6, p. 175-186 12 p.

    Research output: Contribution to journalArticle

ID: 44376957