Slides and Resources:
- Slides on hardware models.
- The ppcmem tool
to explore the Power/ARM memory model (and some
tests).
- Slides on programming language models.
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.
- 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.
-
R. Morisset, P. Pawan, F. Zappa Nardelli: Compiler testing via a theory of sound optimisations in the C11/C++11 memory model, in PLDI'13.
-
V. Vafeiadis, T. Balabonsky, S. Chakraborty, R. Morisset, F. Zappa Nardelli: Common compiler optimisations are invalid in the C11 memory model and what we can do about it, in POPL'15.
If you want more:
Email: Francesco.Zappa_Nardelli (at) inria.fr
|