The semantics of x86-CC multiprocessor machine code

摘要: 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) models, usually described only in ambiguous prose, leading to widespread confusion.We develop a rigorous accurate for x86 multiprocessor programs, from instruction decoding model, mechanised HOL. We test against actual processors vendor litmus-test examples, give an equivalent abstract-machine characterisation of our axiomatic model. For programs (in some precise sense) data-race free, we prove HOL their behaviour consistent. also contrast model with aspects Power ARM behaviour.This provides solid intuition low-level programming, sound foundation future verification, static analysis, compilation concurrent code.