Reasoning about the ARM weakly consistent memory model

ABSTRACT

This paper describes a formalization of the ARM weakly consistent memory model: the architectural contract between parallel programs and shared memory multiprocessor implementations. We claim that a clean, unambiguous, and mechanically verifiable specification is a valuable resource for architects, micro-architects and programmers; it allows implementors to forge aggressive static (compiler) and dynamic (JIT, micro-architecture) machines to run code. We discuss the key construct of the ARM memory model, observability -- the order in which memory accesses become visible to processors in a shared memory multiprocessor system -- and examine its use in litmus tests.

REFERENCES

• 1: ARM. ARM v7A+R Architectural Reference Manual. Available from ARM Ltd.
• 2: Hans-J. Boehm, Threads cannot be implemented as a library, Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation, June 12-15, 2005, Chicago, IL, USA
• 3: William W. Collier, Reasoning about parallel architectures, Prentice-Hall, Inc., Upper Saddle River, NJ, 1992
• 4: Compaq. Alpha Architecture Handbook. Compaq, 1998.
• 5: The Coq Development Team. The Coq proof assistant reference manual. LogiCal Project, 2006. Version 8.1.
• 6: Kevin Elphinstone , Gerwin Klein , Philip Derrin , Timothy Roscoe , Gernot Heiser, Towards a practical, verified kernel, Proceedings of the 11th USENIX workshop on Hot topics in operating systems, p.1-6, May 07-09, 2007, San Diego, CA
• 7: Mike Gordon. A formalization of a simplified subset of the Alpha shared memory model, 1994. Manuscript.
• 8: Sudheendra Hangal , Durgam Vahia , Chaiyasit Manovit , Juin-Yeu Joseph Lu, TSOtool: A Program for Verifying Memory Systems Using the Memory Consistency Model, ACM SIGARCH Computer Architecture News, v.32 n.2, p.114, March 2004
• 9: Intel. Intel 64 Architecture Memory Ordering White Paper. SKU 318147-001, August 2007.
• 10: Gerwin Klein , Tobias Nipkow, A machine-checked model for a Java-like language, virtual machine, and compiler, ACM Transactions on Programming Languages and Systems (TOPLAS), v.28 n.4, p.619-695, July 2006 [doi>10.1145/1146809.1146811]
• 11: Leslie Lamport, How to Make a Correct Multiprocess Program Execute Correctly on a Multiprocessor, IEEE Transactions on Computers, v.46 n.7, p.779-782, July 1997 [doi>10.1109/12.599898]
• 12: Xavier Leroy, Formal certification of a compiler back-end or: programming a compiler with a proof assistant, Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.42-54, January 11-13, 2006, Charleston, South Carolina, USA
• 13: Jeremy Manson , William Pugh , Sarita V. Adve, The Java memory model, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.378-391, January 12-14, 2005, Long Beach, California, USA
• 14: JS Moore. A Grand Challenge Proposal for Formal Methods: A Verified Stack. In Formal Methods at the Crossroads, 2003.
• 15: H Sutter. Prism: A Principle-Based Sequential Memory Model for Microsoft Native Code Platforms. March 2007. Working draft v0.9.4.
• 16: Y Yang, G Gopalakrishnan, G Lindstrom, and K Slind. Analyzing the Intel Itanium Memory Ordering Rules Using Logic Programming and SAT. In Proc of CHARME, 2003.

INDEX TERMS

Primary Classification:
  B. Hardware
  B.3 MEMORY STRUCTURES
      B.3.2 Design Styles
          Subjects: Shared memory

Additional Classification:
  C. Computer Systems Organization
  C.1 PROCESSOR ARCHITECTURES
      C.1.4 Parallel Architectures

General Terms:
Theory, Verification

Keywords:
ARM, weakly consistent memory model