|
- Slides on hardware models.
- The ppcmem tool
to explore the Power/ARM memory model (and some
tests).
- Slides on programming language models.
- Slides on Linux, C11,
x86-TSO, fence 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.
- Luc Maranget, Susmit Sarkar, Peter Sewell:
A tutorial introduction to the ARM and POWER relaxed memory model, draft.
- 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.
If you want more:
Email: Francesco.Zappa_Nardelli (at) inria.fr
|