> when stores complete they become visible to all other cores and all cores agree on the exact same list of completed stores.

Not that they agree on what completed but on the order they completed in. That is the "o" in TSO. You inadvertently proved my point.

.

> so I'd say those get to be unspecified.

* CRASH *

You left something unspecified that mattered. Ordering of accesses to mappings with differing permissions matters, and whether they are seen in-program-order or not by other cores will break x86 emulators (main use cases for TSO).

.

That's the point here :) This is the usual "i am sure we can all agree what X means" argument - it does not work when it comes to precise things like memory models.

> Not that they agree on what completed but on the order they completed in. That is the "o" in TSO. You inadvertently proved my point.

A list is ordered. You're trying too hard to nitpick. (Also I gave a disclaimer that my wording wasn't perfect, and it only took a couple words for you to "fix" it. If it can be fixed that easily then that doesn't actually counteract my point.)

> You left something unspecified that mattered. Ordering of accesses to mappings with differing permissions matters, and whether they are seen in-program-order or not by other cores will break x86 emulators (main use cases for TSO).

How many x86 emulators have the emulated code talking directly to hardware, to the same piece of hardware, from multiple cores at the same time?

I don't think this is a "main use case".

Plus there's going to be a baseline for how talking to the hardware works. Only TSO-mode-specific details of the hardware access are left unsaid in this basic model, and many access patterns fitting the above description still won't notice anything one way or the other.