Skip to content

Research at St Andrews

An Axiomatic Memory Model for POWER Multiprocessors

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

Author(s)

Sela Mador-Haim, Luc Maranget, Susmit Sarkar, Kayvan Memarian, Jade Alglave, Scott Owens, Rajeev Alur, Milo Martin, Peter Sewell, Derek Williams

School/Research organisations

Abstract

The growing complexity of hardware optimizations employed
by multiprocessors leads to subtle distinctions among allowed and dis-
allowed behaviors, posing challenges in specifying their memory models
formally and accurately, and in understanding and analyzing the behavior of concurrent software. This complexity is particularly evident in the
IBM Power Architecture , for which a faithful specification was published only in 2011 using an operational style. In this paper we present
an equivalent axiomatic specification, which is more abstract and concise. Although not officially sanctioned by the vendor, our results indicate
that this axiomatic specification provides a reasonable basis for reasoning
about current IBM POWER multiprocessors. We establish the equivalence of the axiomatic and operational specifications using both manual
proof and extensive testing. To demonstrate that the constraint-based
style of axiomatic specification is more amenable to computer-aided verification, we develop a SAT-based tool for evaluating possible outcomes
of multi-threaded test programs, and we show that this tool is significantly more efficient than a tool based on an operational specification.
Close

Details

Original languageEnglish
Title of host publicationProceedings of the 24th International Conference on Computer Aided Verification
EditorsP Madhusudan, Sanjit Seshia
PublisherSpringer-Verlag
Pages495
Number of pages512
ISBN (Print)978-3-642-31423-0
DOIs
StatePublished - Jul 2012

Publication series

NameLecture Notes in Computer Science
Volume7358

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: 45512316