More Web Proxy on the site http://driver.im/

research-article

Understanding POWER multiprocessors

Authors:

Derek WilliamsAuthors Info & Claims

ACM SIGPLAN Notices, Volume 46, Issue 6

Pages 175 - 186

https://doi.org/10.1145/1993316.1993520

Published: 04 June 2011 Publication History

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.

References

[1]

A. Adir, H. Attiya, and G. Shurek. Information-flow models for shared memory with an application to the PowerPC architecture. IEEE Trans. Parallel Distrib. Syst., 14(5):502--515, 2003.

Digital Library

[2]

J. Alglave, A. Fox, S. Ishtiaq, M. O. Myreen, S. Sarkar, P. Sewell, and F. Zappa Nardelli. The semantics of Power and ARM multiprocessor machine code. In Proc. DAMP 2009, January 2009.

Digital Library

[3]

S. V. Adve and K. Gharachorloo. Shared memory consistency models: A tutorial. IEEE Computer, 29(12):66--76, 1996.

Digital Library

[4]

Jade Alglave. A Shared Memory Poetics. PhD thesis, Université Paris 7 Denis Diderot, November 2010.

[5]

J. Alglave, L. Maranget, S. Sarkar, and P. Sewell. Fences in weak memory models. In Proc. CAV, 2010.

Digital Library

[6]

J. Alglave, L. Maranget, S. Sarkar, and P. Sewell. Litmus: Running tests against hardware. In Proc. TACAS, 2011.

Digital Library

[7]

ARM. ARM Barrier Litmus Tests and Cookbook, October 2008. PRD03-GENC-007826 2.0.

[8]

H.-J. Boehm and S. Adve. Foundations of the C concurrency memory model. In Proc. PLDI, 2008.

Digital Library

[9]

M. Batty, S. Owens, S. Sarkar, P. Sewell, and T. Weber. Mathematizing C concurrency. In Proc. POPL, 2011.

Digital Library

[10]

N. Chong and S. Ishtiaq. Reasoning about the ARM weakly consistent memory model. In MSPC, 2008.

Digital Library

[11]

W.W. Collier. Reasoning about parallel architectures. Prentice-Hall, Inc., 1992.

Digital Library

[12]

F. Corella, J. M. Stone, and C. M. Barton. A formal specification of the PowerPC shared memory architecture. Technical Report RC18638, IBM, 1993.

[13]

M. Dubois, C. Scheurich, and F. Briggs. Memory access buffering in multiprocessors. In ISCA, 1986.

Digital Library

[14]

K. Gharachorloo. Memory consistency models for shared-memory multiprocessors. WRL Research Report, 95(9), 1995.

Digital Library

[15]

Intel. A formal specification of Intel Itanium processor family memory ordering, 2002. developer.intel.com/design/itanium/downloads/251429.htm.

[16]

R. Joshi, L. Lamport, J. Matthews, S. Tasiran, M. Tuttle, and Y. Yu. Checking cache-coherence protocols with TLA. Form. Methods Syst. Des., 22:125--131, March 2003.

Digital Library

[17]

R. Kalla, B. Sinharoy, W. J. Starke, and M. Floyd. Power7: IBM's next-generation server processor. IEEE Micro, 30:7--15, March 2010.

Digital Library

[18]

D. Lea. The JSR-133 cookbook for compiler writers. http://gee.cs.oswego.edu/dl/jmm/cookbook.html.

[19]

H. Q. Le, W. J. Starke, J. S. Fields, F. P. O'Connell, D. Q. Nguyen, B. J. Ronchetti, W. Sauer, E. M. Schwarz, and M. T. Vaden. IBM POWER6 microarchitecture. IBM Journal of Research and Development, 51(6):639--662, 2007.

Digital Library

[20]

C. May, E. Silha, R. Simpson, and H. Warren, editors. The PowerPC architecture: a specification for a new family of RISC processors. Morgan Kaufmann Publishers Inc., San Francisco, CA, USA, 1994.

Digital Library

[21]

S. Owens, P. Böhm, F. Zappa Nardelli, and P. Sewell. Lightweight tools for heavyweight semantics. Submitted for publication http://www.cl.cam.ac.uk/ so294/lem/.

[22]

S. Owens, S. Sarkar, and P. Sewell. A better x86 memory model: x86-TSO. In Proc. TPHOLs, pages 391--407, 2009.

Digital Library

[23]

Power ISA™ Version 2.06. IBM, 2009.

[24]

J. M. Stone and R. P. Fitzgerald. Storage in the PowerPC. IEEE Micro, 15:50--58, April 1995.

Digital Library

[25]

P. S. Sindhu, J.-M. Frailong, and M. Cekleov. Formal specification of memory models. In Scalable Shared Memory Multiprocessors, pages 25--42. Kluwer, 1991.

[26]

B. Sinharoy, R. N. Kalla, J. M. Tendler, R. J. Eickemeyer, and J. B. Joyner. POWER5 system microarchitecture. IBM Journal of Research and Development, 49(4-5):505--522, 2005.

Digital Library

[27]

The SPARC Architecture Manual, V. 8. SPARC International, Inc., 1992. Revision SAV080SI9308. http://www.sparc.org/standards/V8.pdf.

Digital Library

[28]

S. Sarkar, P. Sewell, J. Alglave, L. Maranget, and D. Williams. Understanding POWER multiprocessors. www.cl.cam.ac.uk/users/pes20/ppc-supplemental, 2011.

Digital Library

[29]

P. Sewell, S. Sarkar, S. Owens, F. Zappa Nardelli, and M. O. Myreen. x86-TSO: A rigorous and usable programmer's model for x86 multiprocessors. Communications of the ACM, 53(7):89--97, July 2010.

Digital Library

[30]

S. Sarkar, P. Sewell, F. Zappa Nardelli, S. Owens, T. Ridge, T. Braibant, M. Myreen, and J. Alglave. The semantics of x86-CC multiprocessor machine code. In Proc. POPL 2009, January 2009.

Digital Library

[31]

Y. Yang, G. Gopalakrishnan, G. Lindstrom, and K. Slind. Analyzing the Intel Itanium memory ordering rules using logic programming and SAT. In Proc. CHARME, LNCS 2860, 2003.

Cited By

Geeson LSmith L(2024)Compiler Testing with Relaxed Memory Models2024 IEEE/ACM International Symposium on Code Generation and Optimization (CGO)10.1109/CGO57630.2024.10444836(334-348)Online publication date: 2-Mar-2024
https://doi.org/10.1109/CGO57630.2024.10444836
Abdulla PAtig MFurbach FGodbole AHendi YKrishna SSpengler S(2023)Parameterized Verification under TSO with Data TypesTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-031-30823-9_30(588-606)Online publication date: 22-Apr-2023
https://dl.acm.org/doi/10.1007/978-3-031-30823-9_30
Haas TMeyer RPonce de León H(2022)CAAT: consistency as a theoryProceedings of the ACM on Programming Languages10.1145/35632926:OOPSLA2(114-144)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563292
Show More Cited By

Index Terms

Understanding POWER multiprocessors

Recommendations

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

ARM has a relaxed memory model, previously specified in informal prose for ARMv7 and ARMv8. Over time, and partly due to work building formal semantics for ARM concurrency, it has become clear that some of the complexity of the model is not justified by ...
Understanding POWER multiprocessors
PLDI '11: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation

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 ...
Modelling the ARMv8 architecture, operationally: concurrency and ISA
POPL '16

In this paper we develop semantics for key aspects of the ARMv8 multiprocessor architecture: the concurrency model and much of the 64-bit application-level instruction set (ISA). Our goal is to clarify what the range of architecturally allowable ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 46, Issue 6

PLDI '11

June 2011

652 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/1993316

Issue’s Table of Contents

PLDI '11: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation
June 2011
668 pages
ISBN:9781450306638
DOI:10.1145/1993498
General Chair:
Mary Hall
University of Utah
,
Program Chair:
David Padua
University of Illinois at Urbana-Champaign

Copyright © 2011 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 04 June 2011

Published in SIGPLAN Volume 46, Issue 6

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

264
Total Citations
View Citations
778
Total Downloads

Downloads (Last 12 months)47
Downloads (Last 6 weeks)12

Reflects downloads up to 01 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Geeson LSmith L(2024)Compiler Testing with Relaxed Memory Models2024 IEEE/ACM International Symposium on Code Generation and Optimization (CGO)10.1109/CGO57630.2024.10444836(334-348)Online publication date: 2-Mar-2024
https://doi.org/10.1109/CGO57630.2024.10444836
Abdulla PAtig MFurbach FGodbole AHendi YKrishna SSpengler S(2023)Parameterized Verification under TSO with Data TypesTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-031-30823-9_30(588-606)Online publication date: 22-Apr-2023
https://dl.acm.org/doi/10.1007/978-3-031-30823-9_30
Haas TMeyer RPonce de León H(2022)CAAT: consistency as a theoryProceedings of the ACM on Programming Languages10.1145/35632926:OOPSLA2(114-144)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563292
Raad AMaranget LVafeiadis V(2022)Extending Intel-x86 consistency and persistency: formalising the semantics of Intel-x86 memory types and non-temporal storesProceedings of the ACM on Programming Languages10.1145/34986836:POPL(1-31)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498683
Abdulla PAtig MBouajjani AJonsson BKumar KSaivasan P(2022)Consistency and Persistency in Program Verification: Challenges and OpportunitiesPrinciples of Systems Design10.1007/978-3-031-22337-2_24(494-510)Online publication date: 29-Dec-2022
https://doi.org/10.1007/978-3-031-22337-2_24
Colvin R(2022)Separation of Concerning Things: A Simpler Basis for Defining and Programming with the C/C++ Memory ModelFormal Methods and Software Engineering10.1007/978-3-031-17244-1_5(71-89)Online publication date: 24-Oct-2022
https://dl.acm.org/doi/10.1007/978-3-031-17244-1_5
Liu LMillstein TMusuvathi M(2021)Safe-by-default Concurrency for Modern Programming LanguagesACM Transactions on Programming Languages and Systems10.1145/346220643:3(1-50)Online publication date: 3-Sep-2021
https://dl.acm.org/doi/10.1145/3462206
Zhao HZeng XChen TLiu ZWoodcock J(2021)Learning safe neural network controllers with barrier certificatesFormal Aspects of Computing10.1007/s00165-021-00544-533:3(437-455)Online publication date: 1-Jun-2021
https://dl.acm.org/doi/10.1007/s00165-021-00544-5
Hesselink W(2021)UNITY and Büchi automataFormal Aspects of Computing10.1007/s00165-020-00528-x33:2(185-205)Online publication date: 1-Mar-2021
https://dl.acm.org/doi/10.1007/s00165-020-00528-x
Colvin R(2021)Parallelized Sequential Composition and Hardware Weak Memory ModelsSoftware Engineering and Formal Methods10.1007/978-3-030-92124-8_12(201-221)Online publication date: 6-Dec-2021
https://dl.acm.org/doi/10.1007/978-3-030-92124-8_12
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Issue’s Table of Contents