Exploring Weak Memory Models with Alloy


John Wickerson
Imperial College London


Daniel Jackson
This talk is about the author's adventures over the last few years with using Alloy to analyse "weak memory". In the context of concurrent programming, "weak memory" refers to any behaviour of a processor or compiler that breaks the illusion of all threads executing their instructions in order, and operating on a single monolithic memory that always returns the most recently-stored value. In processors, weak memory effects can be caused by caches and store buffers; in compilers, weak memory effects can be caused by optimisations that reorder instructions.

Precise models of exactly which weak memory behaviours are allowed by any given processor or compiler have been developed in recent years. These models are often written in a relational style, which makes them ideal for analysis with Alloy!

I will describe a tool called Memalloy for analysing weak memory models. Memalloy can discover example programs that: (1) distinguish any two given models; (2) show that certain compiler optimisations are unsound w.r.t. a given model; and (3) show that a certain compilation scheme from one model to another is broken. Memalloy has been applied to weak memory models for CPUs, GPUs, high-level languages, and even FPGAs!

This talk is based on joint work with Mark Batty, Nathan Chong, George Constantinides, Shane Fleming, Nadesh Ramanathan, and Tyler Sorensen. For further reading, please see papers that appeared in [POPL'17](https://johnwickerson.github.io/papers/memalloy.pdf), [PLDI'18](https://johnwickerson.github.io/papers/transactions.pdf), and [ACM TC'18](https://johnwickerson.github.io/papers/feetup_TC.pdf).

Bio: John Wickerson is a Lecturer in the Department of Electrical and Electronic Engineering at Imperial College London, a position he has held since 2018. He holds a PhD in Computer Science from the University of Cambridge. His research interests include weak memory models, high-level synthesis (aka C-to-Verilog), automated compiler testing, transactional memory, software verification (particularly with separation logic), GPU programming (particularly with OpenCL), and mechanised proof (particularly using Isabelle).