2 ms·

The hardware designers were involved on the standardization process. I don't have citations at hand, I think most of the mailing lists were the discussion re th

The hardware designers were involved on the standardization process. I don't have citations at hand, I think most of the mailing lists were the discussion re the c++ MO happened have been lost, but (as a lurker trying to learn this stuff) I was following the process closely. The question was, given PO, whether it was at all possible to recover sequential consistently on intel either with mfence or a lock xchg, given the possibility of IRIW. Intel then updated their MO to exclude IRIW, de facto standardizing on TSO. This was early 2000s. I think both ARM and IBM published revisions to their architecture clarifying details around the same time. This spawned a set of academic papers that proved the correctness of the agreed mapping of the C++ memory model to those architecture s.

ajross 3y ago
> The hardware designers were involved on the standardization process. That sounds cyclic then. You're saying that Intel's SDM was ambiguous[1] (which it was) and that it was sorted out as part of a standardization process. I'm saying that it doesn't really matter what the SDM said, it mattered whether or not you could reliably write lockless code on x86 using the hardware and docs available at the time, and you could. And further, I'm saying that the standard ended up making things worse by perpetuating arguments like this about what some buggy English text in an SDM said and not about actual hardware behavior. [1] In ways that AFAICT didn't actually impact hardware. I found this, which is probably one of the papers you're citing. It's excellent work in standards-writing, but it's also careful to note that the IRIW cases were never observed on hardware. https://www.cl.cam.ac.uk/~pes20/weakmemory/x86tso-paper.tphols.pdf https://www.cl.cam.ac.uk/~pes20/weakmemory/x86tso-paper.tpho...
- gpderetta 3y ago
  It didn't impact hardware because intel hadn't taken advantage yet of the additional latitude offered by their original model. Then they closed the hole and they guaranteed no IRIW[1]. But in the meantime if your algorithm was susceptible to this reordering, there was no written guarantee that an mfence would fix it. But most importantly as the model was informal and not self consistent, there was no possibility to write formal proofs of correctness of an algorithm or run it against a model checker. [1] in practice this means no store-forwarding from sibling hyper thread store buffers, something that for example POWER allows and is observed in real hardware.

ajross 3y ago

> The hardware designers were involved on the standardization process. That sounds cyclic then. You're saying that Intel's SDM was ambiguous[1] (which it was) and that it was sorted out as part of a standardization process. I'm saying that it doesn't really matter what the SDM said, it mattered whether or not you could reliably write lockless code on x86 using the hardware and docs available at the time, and you could. And further, I'm saying that the standard ended up making things worse by perpetuating arguments like this about what some buggy English text in an SDM said and not about actual hardware behavior. [1] In ways that AFAICT didn't actually impact hardware. I found this, which is probably one of the papers you're citing. It's excellent work in standards-writing, but it's also careful to note that the IRIW cases were never observed on hardware. https://www.cl.cam.ac.uk/~pes20/weakmemory/x86tso-paper.tphols.pdf https://www.cl.cam.ac.uk/~pes20/weakmemory/x86tso-paper.tpho...

gpderetta 3y ago
It didn't impact hardware because intel hadn't taken advantage yet of the additional latitude offered by their original model. Then they closed the hole and they guaranteed no IRIW[1]. But in the meantime if your algorithm was susceptible to this reordering, there was no written guarantee that an mfence would fix it. But most importantly as the model was informal and not self consistent, there was no possibility to write formal proofs of correctness of an algorithm or run it against a model checker. [1] in practice this means no store-forwarding from sibling hyper thread store buffers, something that for example POWER allows and is observed in real hardware.