The Semantics of X86-CC Multiprocessor Machine Code

Free registration required

Executive Summary

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. They develop a rigorous and accurate semantics for x86 multiprocessor programs, from instruction decoding to relaxed memory model, mechanized in HOL. They test the semantic against actual processors and the vendor litmus-test examples, and give an equivalent paper-machine characterization of the axiomatic memory model. For programs that are (in some precise sense) data-race free, they prove in HOL that their behavior is sequentially consistent. They also contrast the x86 model with some aspects of Power and ARM behavior.

  • Format: PDF
  • Size: 285.4 KB