Why Languages Should Preserve Load-Store Order
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.
Mon 15 JanDisplayed time zone: London change
11:00 - 12:30 | Session 2The Future of Weak Memory at Turing Lecture Chair(s): John Wickerson Imperial College London | ||
11:00 22mTalk | Weak Memory Demands Model-based Compiler Testing The Future of Weak Memory Luke Geeson University College London (UCL) File Attached | ||
11:22 22mTalk | On the need for available, functional, and reusable memory models The Future of Weak Memory Hernán Ponce de León Huawei Dresden Research Center | ||
11:45 22mTalk | What we learned from C++ atomics and memory model standardization The Future of Weak Memory Hans-J. Boehm Google File Attached | ||
12:07 22mTalk | Why Languages Should Preserve Load-Store Order The Future of Weak Memory Stephen Dolan Jane Street |