Abstract
Real multiprocessors do not provide the sequentially consistent memory that is assumed by most work on semantics and veriÞcation. Instead, they have relaxed memory models, typically described in ambiguous prose, which leads to widespread confusion. In this talk, I will discuss a formal specification of the x86 processor architecture, concentrating on an assembly- programming-level view of its memory model for multiprocessor or multicore systems. This specification, called x86-TSO, improves upon our previous effort, x86- CC, which closely followed the Intel and AMD documentation, but turned out to be unsound with respect to actual hardware, as well as arguably too weak to program above. We believe that x86-TSO is sound with respect to real processors, reflects better the vendorÕs intentions, and is also better suited for programming.