Much of the most difficult parts of recent work on memory models has focused on a particular optimisation that some hardware and the occasional compiler perform, where a load is reordered past a subsequent store, if the two operations are independent. Specifying this behaviour in a way that distinguishes the reorderings that can occur from those that cannot has proved remarkably complicated, particularly around defining “independent”, and eliminating out-of-thin-air behaviours. After much research, several systems emerged that solved this problem to varying degrees, but all are more complex than a programmer might expect.

In this talk, I’ll argue that this problem is better left unsolved: difficulties in reasoning occur even when the only load-store reorderings are the seemingly “independent” ones, and I’ll claim language models would be improved and simplified if they specified that load-store reordering never occurs in a programmer-visible way. In particular, I’ll give examples of reasonable program transformations / compiler optimisations that are permissible only if load-store reordering is banned, showing that allowing this behaviour may actually have a negative effect on single-threaded code.