Skip to main content
Kent Academic Repository

An Axiomatic Memory Model for POWER Multiprocessors

Mador-Haim, Sela and Maranget, Luc and Sarkar, Susmit and Memarian, Kayvan and Alglave, Jade and Owens, Scott and Alur, Rajeev and Martin, Milo M.K. and Sewell, Peter and Williams, Derek (2012) An Axiomatic Memory Model for POWER Multiprocessors. In: Computer Aided Verification 24th International Conference. Lecture Notes in Computer Science . Springer, Berlin, Germany, pp. 495-512. ISBN 978-3-642-31423-0. E-ISBN 978-3-642-31424-7. (doi:10.1007/978-3-642-31424-7_36) (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:31891)

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-31424-7_36

Abstract

The growing complexity of hardware optimizations employed by multiprocessors leads to subtle distinctions among allowed and disallowed 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.

Item Type: Book section
DOI/Identification number: 10.1007/978-3-642-31424-7_36
Uncontrolled keywords: memory model; control dependency; conditional branch; program order; storage subsystem
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:02 UTC
Last Modified: 16 Nov 2021 10:09 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/31891 (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.