Princeton University

School of Engineering & Applied Science

Herding Cats: Modelling, Simulation, Testing and Verification for Weak Memory

Speaker: 
Jade Alglave, University College London
Location: 
Engineering Quadrangle B205
Date/Time: 
Monday, September 29, 2014 - 4:30pm to 5:30pm

<strong>Abstract:</strong>  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 one cannot rely on one more than on the other.
 
In this talk, I will present an overview of my work. I have mostly been involved in studying weak memory (i.e. the execution models of multiprocessors).  Understanding precisely what our machines guarantee 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.
 
I will show how to define formal models for weak memory, within a generic framework in which one can represent Sequential Consistency (SC), Intel x86 (i.e. Sparc Total Store Order, TSO), IBM Power, ARM, C++ and GPUs. I will then show how to exploit these models for devising tools to verify concurrent programs.
 
<strong>Biography:</strong>  Dr. Jade Alglave (http://www.cs.ucl.ac.uk/staff/j.alglave/) is a lecturer at University College London (UCL). She is currently a visiting researcher at Nvidia Redmond. She will start in the fall as a researcher at Microsoft Research Cambridge, keeping her lectureship at UCL.