Article

An axiomatic memory model for POWER multiprocessors

Authors:

Derek WilliamsAuthors Info & Claims

CAV'12: Proceedings of the 24th international conference on Computer Aided Verification

Pages 495 - 512

https://doi.org/10.1007/978-3-642-31424-7_36

Published: 07 July 2012 Publication History

Publisher Site

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.

References

[1]

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

Digital Library

Google Scholar

[2]

Alglave, J., Fox, A., Ishtiaq, S., Myreen, M.O., Sarkar, S., Sewell, P., Zappa Nardelli, F.: The semantics of Power and ARM multiprocessor machine code. In: Workshop on Declarative Aspects of Multicore Programming (January 2009).

Digital Library

Google Scholar

[3]

Alglave, J., Maranget, L., Sarkar, S., Sewell, P.: Fences in Weak Memory Models. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 258-272. Springer, Heidelberg (2010).

Digital Library

Google Scholar

[4]

Alglave, J., Maranget, L., Sarkar, S., Sewell, P.: Litmus: Running Tests against Hardware. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 41-44. Springer, Heidelberg (2011).

Digital Library

Google Scholar

[5]

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

Google Scholar

[6]

Een, N., Sorensson, N.: Minisat - a SAT solver with conflict-clause minimization. In: International Conference on Theory and Applications of Satisfiability Testing (2005).

Google Scholar

[7]

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

Google Scholar

[8]

Intel. A formal specification of Intel Itanium processor family memory ordering (2002), http://developer.intel.com/design/itanium/downloads/251429.html

Google Scholar

[9]

Owens, S., Böhm, P., Zappa Nardelli, F., Sewell, P.: Lem: A Lightweight Tool for Heavyweight Semantics. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol. 6898, pp. 363-369. Springer, Heidelberg (2011).

Digital Library

Google Scholar

[10]

Stone, J.M., Fitzgerald, R.P.: Storage in the PowerPC. IEEE Micro 15 (April 1995).

Digital Library

Google Scholar

[11]

Sarkar, S., Memarian, K., Owens, S., Batty, M., Sewell, P., Maranget, L., Alglave, J., Williams, D.: Synchronising C/C++ and POWER. In: Programming Language Design and Implementation (2012).

Digital Library

Google Scholar

[12]

Sarkar, S., Sewell, P., Alglave, J., Maranget, L., Williams, D.: Understanding POWER multiprocessors. In: Programming Language Design and Implementation (2011).

Digital Library

Google Scholar

[13]

An axiomatic memory model for Power multiprocessors -- supplementary material, http://www.seas.upenn.edu/˜selama/axiompower.html

Google Scholar

[14]

Yang, Y., Gopalakrishnan, G.C., Lindstrom, G., Slind, K.: Analyzing the Intel Itanium Memory Ordering Rules Using Logic Programming and SAT. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol. 2860, pp. 81-95. Springer, Heidelberg (2003).

Google Scholar

Cited By

View all

Ambal GDongol BEran HKlimis VLahav ORaad A(2024)Semantics of Remote Direct Memory Access: Operational and Declarative Models of RDMA on TSO ArchitecturesProceedings of the ACM on Programming Languages10.1145/36897818:OOPSLA2(1982-2009)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689781
Haas TMaseli RMeyer RPonce de León H(2023)Static Analysis of Memory Models for SMT EncodingsProceedings of the ACM on Programming Languages10.1145/36228557:OOPSLA2(1618-1647)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622855
Norman CGodbole AManerkar YAamodt TJerger NSwift M(2023)PipeSynth: Automated Synthesis of Microarchitectural Axioms for Memory ConsistencyProceedings of the 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 310.1145/3582016.3582056(513-527)Online publication date: 25-Mar-2023
https://dl.acm.org/doi/10.1145/3582016.3582056
Show More Cited By

Recommendations

The java memory model: operationally, denotationally, axiomatically
ESOP'07: Proceedings of the 16th European Symposium on Programming

A semantics to a small fragment of Java capturing the new memory model (JMM) described in the Language Specification is given by combining operational, denotational and axiomatic techniques in a novel semantic framework. The operational steps (specified ...
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 ...
Reconciling Axiomatic and Model-Based Specifications Using the B Method
ZB '00: Proceedings of the First International Conference of B and Z Users on Formal Specification and Development in Z and B

The worlds of model-based and axiomatic specification are frequently regarded as separate. The formal specification notations of Z and B (the B Method) are usually employed for mathematical modelling. On the other hand, it could be desirable to base ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

CAV'12: Proceedings of the 24th international conference on Computer Aided Verification

July 2012

789 pages

ISBN:9783642314230

Editors:
P. Madhusudan
Dept. of Computer Science, University of Illinois at Urbana-Champaign, Urbana, IL
,
Sanjit A. Seshia
Dept. of Electrical Engineering and Computer Science, University of California, Berkeley, Berkeley, CA

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 07 July 2012

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

60
Total Citations
View Citations
0
Total Downloads

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

Reflects downloads up to 14 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Ambal GDongol BEran HKlimis VLahav ORaad A(2024)Semantics of Remote Direct Memory Access: Operational and Declarative Models of RDMA on TSO ArchitecturesProceedings of the ACM on Programming Languages10.1145/36897818:OOPSLA2(1982-2009)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689781
Haas TMaseli RMeyer RPonce de León H(2023)Static Analysis of Memory Models for SMT EncodingsProceedings of the ACM on Programming Languages10.1145/36228557:OOPSLA2(1618-1647)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622855
Norman CGodbole AManerkar YAamodt TJerger NSwift M(2023)PipeSynth: Automated Synthesis of Microarchitectural Axioms for Memory ConsistencyProceedings of the 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 310.1145/3582016.3582056(513-527)Online publication date: 25-Mar-2023
https://dl.acm.org/doi/10.1145/3582016.3582056
Abdulla PAtig MGodbole AKrishna SVahanwala M(2023)Overcoming Memory Weakness with Unified FairnessComputer Aided Verification10.1007/978-3-031-37706-8_10(184-205)Online publication date: 17-Jul-2023
https://dl.acm.org/doi/10.1007/978-3-031-37706-8_10
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
Lustig DCooksey SGiroux OSalapura VZahran MChong FTang L(2022)Mixed-proxy extensions for the NVIDIA PTX memory consistency modelProceedings of the 49th Annual International Symposium on Computer Architecture10.1145/3470496.3533045(1058-1070)Online publication date: 18-Jun-2022
https://dl.acm.org/doi/10.1145/3470496.3533045
Xiao LZhu H(2022)UTP semantics for the MCA ARMv8 architectureJournal of Systems Architecture: the EUROMICRO Journal10.1016/j.sysarc.2022.102438125:COnline publication date: 18-May-2022
https://dl.acm.org/doi/10.1016/j.sysarc.2022.102438
Barroso PPereira MRavara A(2022)Leroy and Blazy Were Right: Their Memory Model Soundness Proof is AutomatableVerified Software. Theories, Tools and Experiments.10.1007/978-3-031-25803-9_2(20-32)Online publication date: 17-Oct-2022
https://dl.acm.org/doi/10.1007/978-3-031-25803-9_2
Yan PMurray T(2021)SecRSL: security separation logic for C11 release-acquire concurrencyProceedings of the ACM on Programming Languages10.1145/34854765:OOPSLA(1-26)Online publication date: 15-Oct-2021
https://dl.acm.org/doi/10.1145/3485476
Tao RYao JLi XLi SNieh JGu R(2021)Formal Verification of a Multiprocessor Hypervisor on Arm Relaxed Memory HardwareProceedings of the ACM SIGOPS 28th Symposium on Operating Systems Principles10.1145/3477132.3483560(866-881)Online publication date: 26-Oct-2021
https://dl.acm.org/doi/10.1145/3477132.3483560
Show More Cited By

Abstract

References

Cited By

Recommendations

The java memory model: operationally, denotationally, axiomatically

Understanding POWER multiprocessors

Reconciling Axiomatic and Model-Based Specifications Using the B Method

Comments

Information

Published In

Sponsors

Publisher

Publication History

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations