There is a joke where a physicist and a mathematician are asked to herd cats. The physicist starts with an infinitely large pen which he reduces until it is of reasonable diameter yet contains all the cats. The mathematician builds a fence around himself and declares the outside to be the inside. Defining memory models is akin to herding cats: both the physicist’s or mathematician’s attitudes are tempting, but we cannot rely on one more than on the other. I have studied weak memory trying to understand precisely what our machines guarantee. This is crucial for writing correct programs, especially since weak memory forces us to revise the programming model that we have been taught at school, namely Lamport’s Sequential Consistency. In this talk, I will show ways of defining formal models for weak memory, within a generic framework in which one can represent for example Sequential Consistency, Intel x86, IBM Power, ARM, C++ and GPUs. I will then present some work on how to exploit these models for devising tools to verify concurrent programs.

Track: ECOOP Summer School

Jade Algave is a lecturer at University College London. Her area of expertise is weak memory models and the interface between hardware and programming languages. She actually understands what C++ programs do when run on a PPC processor!