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.
✨ Summary
Summary
The paper develops x86-CC, a formal semantics for x86 multiprocessor machine code that combines instruction decoding, instruction-level event semantics, and a relaxed memory model. The model represents executions using per-processor view orders, reads-from relations, per-location write serialization, lock serialization, preserved program order, and a causality relation. This framework captures behaviors that cannot be represented by a single sequentially consistent interleaving, including executions in which processors observe writes to different locations in different orders.
The instruction semantics covers a substantial core of 32-bit x86 instructions and addressing modes. It is parameterized over sequential and event-based combinators, allowing the same instruction definitions to support both sequential execution and weak-memory reasoning. The decoding function is formalized in HOL directly from vendor opcode documentation.
The authors validate the model using three forms of testing: an executable checker for enumerating valid executions, litmus tests run on several Intel and AMD multiprocessors, and randomized testing of sequential instruction semantics against an Intel Pentium 4. The paper also proves that, under the paper’s x86-specific notion of data-race freedom, valid executions can be represented by sequentially consistent executions. An equivalent abstract-machine characterization uses per-processor FIFO write queues and per-location write serializations.
The paper’s later addendum is important: the authors report that x86-CC was too restrictive with respect to at least some observed hardware behaviors and that the underlying vendor specifications were problematic as programming models. This work directly motivated the subsequent x86-TSO model, which replaced x86-CC with a simpler model based on write buffers and was intended to better match hardware and programmer expectations. The Cambridge project page now advises focusing on x86-TSO for most purposes because x86-CC is unsound with respect to observed processor behavior. (citeseerx.ist.psu.edu)
The principal lasting contribution of x86-CC was therefore methodological as well as technical: it demonstrated how vendor memory-ordering prose, machine-code semantics, mechanized proofs, litmus testing, and hardware experiments could be integrated into a rigorous architecture model. Its limitations also exposed the need to validate formal architecture specifications empirically, leading to the more widely used x86-TSO line of work. The paper is subsequently documented as a foundational predecessor to x86-TSO in later formal-memory-model literature. (citeseerx.ist.psu.edu)