The Semantics of X86 Multiprocessor Machine Code Supplementary Examples

This note contains supplementary details for the paper The Semantics of x86 Multiprocessor Machine Code [SSZN+09], with an informal-mathematics paper of the axiomatic memory model, and illustrating the possible event structures and valid executions of the examples. All the figures were produced with the movements tool, described in the paper.