X86-TSO: A Rigorous and Usable Programmer’s Model for x86 Multiprocessors (2010)
cl.cam.ac.uk
cl.cam.ac.uk
The fact that Intel had to relax their spec, to allow for observed behavior of their chips is ridiculous. I guess they need those formal specifications for their internal testing as much as we programmers do.
Parallel programming is hard enough, the manufacturers need to get their act together if they want to continue to sell those multicores...
The point of an architecture specification is not to dictate a specific hardware implementation, but to establish a contract between hardware and software. When both parts comply, then the new implementation of a chip will run the old software without problems. A _formal_ specification is just a better contract. Of course it limits future implementation options, but if you want to stay backward compatible, you are limited anyway.
Trying to read this paper, what's a little annoying is that the authors don't seem to define the important acronyms and/or leave them to forward references: "SB" I assume meant "Sandy Bridge" (i.e. that was observed beginning with that microarchitecture) until a little later when I realised they were talking about store buffers, "IRIW" (is it somehow related to "IWP"?) is never defined. Also odd are the examples named "n6", "n5", and "n4b" in that order; a subtle pun about ordering?
IWP stands for "Intel white paper".
The submitted article (published in CACM) is a less formal and condensed form of https://www.cl.cam.ac.uk/~pes20/weakmemory/x86tso-paper.pdf which does, in fact, define all of its acronyms and include examples numbered n1 through n8.