The Future of Weak Memory 2024
2024-01-15
London, United Kingdom
who it's for
programming language researchers, compiler engineers, systems architects, hardware architects, operating system developers, gpu engineers, formal verification and tooling engineers
topics
memory persistency models; compiler testing for weak memory; C++ atomics and standardization; semantic dependency preservation; out-of-thin-air behaviours; reproducible memory-model tooling; heterogeneous weak-memory ISAs; NVM persistency validation; load-store order preservation; write-buffer and instruction-cache flushes; RISC-V memory mapping issues; GPU axiomatic memory models
| title | author | length |
|---|---|---|
| Welcome | John Wickerson, Azalea Raad, Brijesh Dongol, Mark Batty, Peter Sewell | 05m |
Program opens by defining weak versus strong memory and lists concrete agenda items: empirical validation of memory persistency models, tooling for checking… | ||
| Some things I wish I hadn’t seen | Matthew J. Parkinson | 21m |
Finds real code patterns in the .NET runtime and a Microsoft project that use flush_process_write_buffers as an intentionally heavyweight IPI to restore… | ||
| Chasing Unicorns and Not Losing Hope in Validating Weak Memory Persistency Model... | Vasileios Klimis | 21m |
A practical method to validate NVM persistency on real machines: hardware bus interception with a SoCal DDR detective fails on x86 because the persistent… | ||
| How Do We Know That Weak Memory Matters? | Mike Dodds | 23m |
Argues current evidence is weak that weak memory causes widespread system or security failures, citing only a single Rust Belt CVE and few reproducible… | ||
| Weak Memory Demands Model-based Compiler Testing | Luke Geeson | 21m |
Claim: hardware is using RV 8.2a with Large Systems Extension behaviors more aggressively, so compiled C/C++ can exhibit outcomes not allowed by the C++ model… | ||
| On the need for available, functional, and reusable memory models | Hernán Ponce de León | 25m |
Paper data vanishes after a PhD student leaves, so reproducibility fails; experiments and examples claim conformance but links are dead, so demand is permanent… | ||
| What we learned from C++ atomics and memory model standardization | Hans-J. Boehm | 22m |
C++ codebases show atomics as common as mutexes, with many using weakly ordered atomics rather than clever lock‑free structures; measurements on ARM cores show… | ||
| Why Languages Should Preserve Load-Store Order | Stephen Dolan | 22m |
Argues programming-language memory models should ban load-store reordering and preserve load-before-store so induction and pointer-alias reasoning remain… | ||
| Compilers should get over themselves and respect semantic dependencies! | Paul E. McKenney | 22m |
Argues that C/C++ compilers must preserve meaningful runtime dataflow because no real system exhibits OOTA and physics plus hardware practice constrain… | ||
| A case against semantic dependencies | Ori Lahav | 22m |
Argues that the proposed three-step C/C++ fix—derive a global semantic dependency from all candidate executions then apply RC11 consistency—fails on concrete… | ||
| What Compilers desire from Weak Memory Semantics | Akshay Gopalakrishnan | 19m |
Claims a method to derive weaker memory models that preserve SC-safe optimizations so compilers need not be reproved for every model. Demonstrates concrete… | ||
| Programmers love mind-bogglingly complicated weak memory models | Simon Cooksey | 19m |
Nvidia documents a concrete, unusually weak GPU memory model that adds proxies and enforces proxy preserved program order so that cycles in pppo and fr are… | ||
| Evolving Weak Memory Models for Evolving Architectures | Reese Levine | 17m |
Empirical litmus testing shows load buffering visible on most GPUs with observed rates from ~0.001% (Intel) to >1% (AMD); a methodology mutates candidate… | ||
| In-order execution nails every weak memory behavior | Chung-Kil Hur | 22m |
Claims that an in-order, view-based model (an operational V‑IC1 semantics) captures all weak‑memory behaviors typically attributed to out‑of‑order models and… | ||
| System-level weak memory models: The need for formalisation, ISA semantics integ... | Thibaut Pérami | 19m |
Argues for fully formalised system-level weak memory models and presents an executable Coq/ROCK-style library that composes a full instruction-set semantics… | ||
| Relaxed systems semantics and how we (hope to) reason above it | Ben Simner | 20m |
Plan to verify a production Google Pixel hypervisor against a faithful ARM semantics that currently lacks a unified model for instruction fetch, cache… | ||
| Heterogeneous concurrency -- a new frontier for weak memory | Soham Chakraborty | 18m |
Claims a compound memory model that composes x86 and PTX semantics, gives both an axiomatic formulation and a POP‑style operational model, and proves the usual… | ||
| nothing matches | ||