The semantics of x86-CC multiprocessor machine code

ABSTRACT

Multiprocessors are now dominant, but real multiprocessors do not provide the sequentially consistent memory that is assumed by most work on semantics and verification. Instead, they have subtle relaxed (or weak) memory models, usually described only in ambiguous prose, leading to widespread confusion.

We develop a rigorous and accurate semantics for x86 multiprocessor programs, from instruction decoding to relaxed memory model, mechanised in HOL. We test the semantics against actual processors and the vendor litmus-test examples, and give an equivalent abstract-machine characterisation of our axiomatic memory model. For programs that are (in some precise sense) data-race free, we prove in HOL that their behaviour is sequentially consistent. We also contrast the x86 model with some aspects of Power and ARM behaviour.

This provides a solid intuition for low-level programming, and a sound foundation for future work on verification, static analysis, and compilation of low-level concurrent code.

REFERENCES

• 1: A formal specification of Intel Itanium processor family memory ordering. http://developer.intel.com/design/itanium/downloads/251429.htm.
• 2: CORPORATE SPARC International, Inc., The SPARC architecture manual (version 9), Prentice-Hall, Inc., Upper Saddle River, NJ, 1994
• 3: Linux kernel traffic, 1999. http://www.kernel-traffic.org/kernel-traffic/kt19991220_47.txt.
• 4: AMD64 Architecture Programmer's Manual. Advanced Micro Devices, Sept. 2007. (3 vols).
• 5: Intel 64 and IA-32 Architectures Software Developer's Manual. Intel Corporation, April (vol 1,2A,2B; rev.27), Feb. (vol.3A,3B; rev.26) 2008.
• 6: The semantics of multiprocessor machine code, 2008. www.cl.cam.ac.uk/users/pes20/weakmemory.
• 7: Allon Adir , Hagit Attiya , Gil Shurek, Information-Flow Models for Shared Memory with an Application to the PowerPC Architecture, IEEE Transactions on Parallel and Distributed Systems, v.14 n.5, p.502-515, May 2003 [doi>10.1109/TPDS.2003.1199067]
• 8: Sarita V. Adve , Kourosh Gharachorloo, Shared Memory Consistency Models: A Tutorial, Computer, v.29 n.12, p.66-76, December 1996 [doi>10.1109/2.546611]
• 9: Mustaque Ahamad , Rida A. Bazzi , Ranjit John , Prince Kohli , Gil Neiger, The power of processor consistency, Proceedings of the fifth annual ACM symposium on Parallel algorithms and architectures, p.251-260, June 30-July 02, 1993, Velen, Germany [doi>10.1145/165231.165264]
• 10: M. Ahamad, G. Neiger, J. Burns, P. Kohli, and P. Hutto. Causal memory: Definitions, implementation, and programming. Distributed Computing, 9(1):37--49, 1995.
• 11: ARM. ARM Architecture Reference Manual (ARMv7-A and ARMv7-R edition). 2008. Available from ARM.
• 12: D. Aspinall and J. Sevcik. Formalising Java's data race free guarantee. In Proc. TPHOLs, LNCS, 2007.
• 13: Hans-J. Boehm , Sarita V. Adve, Foundations of the C++ concurrency memory model, ACM SIGPLAN Notices, v.43 n.6, June 2008
• 14: Sebastian Burckhardt , Rajeev Alur , Milo M. K. Martin, CheckFence: checking consistency of concurrent data types on relaxed memory models, Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation, June 10-13, 2007, San Diego, California, USA
• 15: Sebastian Burckhardt , Madanlal Musuvathi, Effective Program Verification for Relaxed Memory Models, Proceedings of the 20th international conference on Computer Aided Verification, July 07-14, 2008, Princeton, NJ, USA [doi>10.1007/978-3-540-70545-1_12]
• 16: Nathan Chong , Samin Ishtiaq, Reasoning about the ARM weakly consistent memory model, Proceedings of the 2008 ACM SIGPLAN workshop on Memory systems performance and correctness: held in conjunction with the Thirteenth International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS '08), March 02-02, 2008, Seattle, Washington [doi>10.1145/1353522.1353528]
• 17: William W. Collier, Reasoning about parallel architectures, Prentice-Hall, Inc., Upper Saddle River, NJ, 1992
• 18: M. Dubois , C. Scheurich , F. Briggs, Memory access buffering in multiprocessors, Proceedings of the 13th annual international symposium on Computer architecture, p.434-442, June 02-05, 1986, Tokyo, Japan
• 19: M. Gordon. Memory access semantics for a multiprocessor instruction set. Unpublished note (c.1993) www.cl.cam.ac.buffering in multiprocessors. In ISCA, 1986.
• 20: L. Higham, L. A. Jackson, and J. Kawash. Programmer-centric conditions for itanium memory consistency. In Proc. ICDCN, 2006.
• 21: The HOL 4 system. http://hol.sourceforge.net/.
• 22: Intel. Intel 64 architecture memory ordering white paper, 2007. SKU 318147-001.
• 23: L. Lamport, How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Progranm, IEEE Transactions on Computers, v.28 n.9, p.690-691, September 1979 [doi>10.1109/TC.1979.1675439]
• 24: D. Lea. The JSR-133 cookbook for compiler writers. gee.cs.oswego.edu/dl/jmm/cookbook.html.
• 25: L.Higham, J.Kawash, and N. Verwaal. Defining and comparing memory consistency models. In PDCS, 1997.
• 26: Victor M. Luchangco , Nancy A. Lynch, Memory consistency models for high-performance distributed computing, Massachusetts Institute of Technology, 2001
• 27: 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
• 28: Seungjoon Park , David L. Dill, An executable specification, analyzer and verifier for RMO (relaxed memory order), Proceedings of the seventh annual ACM symposium on Parallel algorithms and architectures, p.34-41, June 24-26, 1995, Santa Barbara, California, United States [doi>10.1145/215399.215413]
• 29: Vijay A. Saraswat , Radha Jagadeesan , Maged Michael , Christoph von Praun, A theory of memory models, Proceedings of the 12th ACM SIGPLAN symposium on Principles and practice of parallel programming, March 14-17, 2007, San Jose, California, USA [doi>10.1145/1229428.1229469]
• 30: G Winskel, Event structures, Advances in Petri nets 1986, part II on Petri nets: applications and relationships to other models of concurrency, p.325-392, February 1987, Bad Honnef
• 31: Y. Yang, G. Gopalakrishnan, G. Lindstrom, and K. Slind. Nemos: A framework for axiomatic and executable specifications of memory consistency models. In IPDPS, 2004.

INDEX TERMS

Primary Classification:
  C. Computer Systems Organization
  C.1 PROCESSOR ARCHITECTURES
      C.1.2 Multiple Data Stream Architectures (Multiprocessors)

Additional Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.3 Concurrent Programming

General Terms:
Documentation, Reliability, Standardization, Theory, Verification

Keywords:
relaxed memory models, semantics