- Slides on hardware models.
- The ppcmem tool to explore the Power/ARM memory model (and some tests).
- Slides on programming language models.
- Slides on the C++11 memory model and on verifying fence elimination optimisations.
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.
- Hans Boehm: Threads Cannot be Implemented as a Library, in PLDI 2005.
- Jaroslav Sevcik: Safe Optimisations for Shared-Memory Concurrent Programs, in PLDI 2011.
- David Howells, Paul McKenney: Linux Kernel Memory Barriers.
- Hans Boehm, Sarita Adve: Foundations of the C++ Concurrency Memory Model, in PLDI 2008.
- Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, Tjark Weber: Mathematizing C++ Concurrency, in POPL 2011.
- Viktor Vafeiadis, Francesco Zappa Nardelli: Verifying Fence Elimination Optimisations, in SAS 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 proposes one internship for 2011/2012:
Email: Francesco.Zappa_Nardelli (at) inria.fr