POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom
Mon 15 Jan 2024 12:07 - 12:30 at Turing Lecture - Session 2 Chair(s): John Wickerson

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 Jan

Displayed 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
22m
Talk
Weak Memory Demands Model-based Compiler Testing
The Future of Weak Memory
Luke Geeson University College London (UCL)
File Attached
11:22
22m
Talk
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
22m
Talk
What we learned from C++ atomics and memory model standardization
The Future of Weak Memory
File Attached
12:07
22m
Talk
Why Languages Should Preserve Load-Store Order
The Future of Weak Memory
Stephen Dolan Jane Street