Colloquium Details
Snakes and Ladders
Speaker: Jade Alglave, Microsoft Research Cambridge (UK) & University College London
Location: Warren Weaver Hall 1302
Date: November 6, 2015, 11:30 a.m.
Host: Patrick Cousot
Synopsis:
At school, we are taught that running a concurrent program could lead to any interleaving of the instructions involved by each of the threads of the program. Sadly that model is not quite right: multiprocessors (that is, any kind of chip that we have in our phones or desktops for example) provide only weak consistency guarantees, exhibiting more behaviours than the ones that we can expect from the interleaving intuition. Similar additional behaviours can arise in distributed systems too.
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. In this talk, I will show ways of defining formal consistency models, hoping to convey the message that understanding a handful of idioms should be enough to get anyone started.
Speaker Bio:
Jade Alglave is both a lecturer at University College London and a researcher at Microsoft Research Cambridge (UK). She studies concurrent systems such as hardware CPU chips since her PhD at INRIA where she developed axiomatic consistency models. More recently she has also developed models of Nvidia GPUs, including one for a chip to be deployed in the upcoming years. Since her PhD, she has also examined verification methods for concurrent systems: model-checking as a post-doc in Oxford University, and more recently static analysis. She is the recipient of the Royal Society Brian Mercer Award for Innovation 2015.
Notes:
In-person attendance only available to those with active NYU ID cards.