- Slides on hardware models.
- The ppcmem tool to explore the Power/ARM memory model (and some tests).
- Slides on programming language models.
- Slides on lr/sc, x86-TSO, fence-elimination optimisations, concurrency compiler bugs...
References:
- P. Sewell, S. Sarkar, S. Owens, F. Zappa Nardelli, M. Myreen: x86-TSO: a rigorous and usable programmer's model for x86 multiprocessors, CACM 53, 2010.
- Susmit Sarkar, Peter Sewell, Jade Alglave, Luc Maranget, Derek Williams: Understanding POWER Multiprocessors, in PLDI 2011.
- Luc Maranget, Susmit Sarkar, Peter Sewell: A tutorial introduction to the ARM and POWER relaxed memory model, draft.
- Jaroslav Sevcik: Safe Optimisations for Shared-Memory Concurrent Programs, in PLDI 2011.
- A web-page describing our research on weak memory concurrency;
- Maurice Herlihy, Nir Shavit: The Art of Multiprocessor Programming, Morgan Kaufmann.
Francesco Zappa Nardelli
has several ideas for internships, including:
- The Linux Memory Model (with Peter Sewell, U. Cambridge);
- Translation validation for a synchronous data-flow equations in a Lustre compiler (with Marc Pouzet, ENS).
Email: Francesco.Zappa_Nardelli (at) inria.fr