Skip to content

Research at St Andrews

Understanding POWER Multiprocessors

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

Standard

Understanding POWER Multiprocessors. / Sarkar, Susmit; Sewell, Peter; Alglave, Jade; Maranget, Luc; Williams, Derek.

PLDI 11: PROCEEDINGS OF THE 2011 ACM CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION. NEW YORK : ASSOC COMPUTING MACHINERY, 2011. p. 175-186.

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

Harvard

Sarkar, S, Sewell, P, Alglave, J, Maranget, L & Williams, D 2011, Understanding POWER Multiprocessors. in PLDI 11: PROCEEDINGS OF THE 2011 ACM CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION. ASSOC COMPUTING MACHINERY, NEW YORK, pp. 175-186, 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 11), San Jose, Canada, 4/06/11.

APA

Sarkar, S., Sewell, P., Alglave, J., Maranget, L., & Williams, D. (2011). Understanding POWER Multiprocessors. In PLDI 11: PROCEEDINGS OF THE 2011 ACM CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION (pp. 175-186). NEW YORK: ASSOC COMPUTING MACHINERY.

Vancouver

Sarkar S, Sewell P, Alglave J, Maranget L, Williams D. Understanding POWER Multiprocessors. In PLDI 11: PROCEEDINGS OF THE 2011 ACM CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION. NEW YORK: ASSOC COMPUTING MACHINERY. 2011. p. 175-186

Author

Sarkar, Susmit ; Sewell, Peter ; Alglave, Jade ; Maranget, Luc ; Williams, Derek. / Understanding POWER Multiprocessors. PLDI 11: PROCEEDINGS OF THE 2011 ACM CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION. NEW YORK : ASSOC COMPUTING MACHINERY, 2011. pp. 175-186

Bibtex - Download

@inproceedings{10039e75002e41d1b78b986b1da02d74,
title = "Understanding POWER Multiprocessors",
abstract = "Exploiting today's multiprocessors requires high-performance and correct concurrent systems code (optimising compilers, language runtimes, OS kernels, etc.), which in turn requires a good understanding of the observable processor behaviour that can be relied on. Unfortunately this critical hardware/software interface is not at all clear for several current multiprocessors.In this paper we characterise the behaviour of IBM POWER multiprocessors, which have a subtle and highly relaxed memory model (ARM multiprocessors have a very similar architecture in this respect). We have conducted extensive experiments on several generations of processors: POWER G5, 5, 6, and 7. Based on these, on published details of the microarchitectures, and on discussions with IBM staff, we give an abstract-machine semantics that abstracts from most of the implementation detail but explains the behaviour of a range of subtle examples. Our semantics is explained in prose but defined in rigorous machine-processed mathematics; we also confirm that it captures the observable processor behaviour, or the architectural intent, for our examples with an executable checker. While not officially sanctioned by the vendor, we believe that this model gives a reasonable basis for reasoning about current POWER multiprocessors.Our work should bring new clarity to concurrent systems programming for these architectures, and is a necessary precondition for any analysis or verification. It should also inform the design of languages such as C and C++, where the language memory model is constrained by what can be efficiently compiled to such multiprocessors.",
keywords = "MICROARCHITECTURE, Relaxed Memory Models, MODELS, SHARED-MEMORY, Semantics",
author = "Susmit Sarkar and Peter Sewell and Jade Alglave and Luc Maranget and Derek Williams",
year = "2011",
language = "English",
isbn = "978-1-4503-0663-8",
pages = "175--186",
booktitle = "PLDI 11: PROCEEDINGS OF THE 2011 ACM CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION",
publisher = "ASSOC COMPUTING MACHINERY",

}

RIS (suitable for import to EndNote) - Download

TY - GEN

T1 - Understanding POWER Multiprocessors

AU - Sarkar, Susmit

AU - Sewell, Peter

AU - Alglave, Jade

AU - Maranget, Luc

AU - Williams, Derek

PY - 2011

Y1 - 2011

N2 - Exploiting today's multiprocessors requires high-performance and correct concurrent systems code (optimising compilers, language runtimes, OS kernels, etc.), which in turn requires a good understanding of the observable processor behaviour that can be relied on. Unfortunately this critical hardware/software interface is not at all clear for several current multiprocessors.In this paper we characterise the behaviour of IBM POWER multiprocessors, which have a subtle and highly relaxed memory model (ARM multiprocessors have a very similar architecture in this respect). We have conducted extensive experiments on several generations of processors: POWER G5, 5, 6, and 7. Based on these, on published details of the microarchitectures, and on discussions with IBM staff, we give an abstract-machine semantics that abstracts from most of the implementation detail but explains the behaviour of a range of subtle examples. Our semantics is explained in prose but defined in rigorous machine-processed mathematics; we also confirm that it captures the observable processor behaviour, or the architectural intent, for our examples with an executable checker. While not officially sanctioned by the vendor, we believe that this model gives a reasonable basis for reasoning about current POWER multiprocessors.Our work should bring new clarity to concurrent systems programming for these architectures, and is a necessary precondition for any analysis or verification. It should also inform the design of languages such as C and C++, where the language memory model is constrained by what can be efficiently compiled to such multiprocessors.

AB - Exploiting today's multiprocessors requires high-performance and correct concurrent systems code (optimising compilers, language runtimes, OS kernels, etc.), which in turn requires a good understanding of the observable processor behaviour that can be relied on. Unfortunately this critical hardware/software interface is not at all clear for several current multiprocessors.In this paper we characterise the behaviour of IBM POWER multiprocessors, which have a subtle and highly relaxed memory model (ARM multiprocessors have a very similar architecture in this respect). We have conducted extensive experiments on several generations of processors: POWER G5, 5, 6, and 7. Based on these, on published details of the microarchitectures, and on discussions with IBM staff, we give an abstract-machine semantics that abstracts from most of the implementation detail but explains the behaviour of a range of subtle examples. Our semantics is explained in prose but defined in rigorous machine-processed mathematics; we also confirm that it captures the observable processor behaviour, or the architectural intent, for our examples with an executable checker. While not officially sanctioned by the vendor, we believe that this model gives a reasonable basis for reasoning about current POWER multiprocessors.Our work should bring new clarity to concurrent systems programming for these architectures, and is a necessary precondition for any analysis or verification. It should also inform the design of languages such as C and C++, where the language memory model is constrained by what can be efficiently compiled to such multiprocessors.

KW - MICROARCHITECTURE

KW - Relaxed Memory Models

KW - MODELS

KW - SHARED-MEMORY

KW - Semantics

M3 - Conference contribution

SN - 978-1-4503-0663-8

SP - 175

EP - 186

BT - PLDI 11: PROCEEDINGS OF THE 2011 ACM CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION

PB - ASSOC COMPUTING MACHINERY

CY - NEW YORK

ER -

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