Computer Laboratory
University of Cambridge
4pm Monday 15th of December, 2008
Room 4.31/4.33, Informatics Forum
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 x86-CC semantics for x86 multiprocessor programs, as described by the recent Intel and AMD informal specifications, from instruction decoding to relaxed memory model. Our semantics is 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.
Such models are needed to provide 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.
However, it now appears that the informal specifications are not useful descriptions of the real processors - either those recent specifications that were the basis for x86-CC, or the current (Nov. 2008) version. We discuss examples showing that they are too weak and unsound, and speculate about how they should be improved.