Proposed by Francesco Zappa Nardelli (francesco.zappa_nardelli (at) inria.fr), Moscova Project-Team, INRIA Paris-Rocquencourt, and Peter Sewell (Peter.Sewell (at) cl.cam.ac.uk), Computer Laboratory, University of Cambridge.
Creation date: 8 December 2010.
Problem
Currently multi-threaded C or C++ programs combine a single-threaded programming language with a separate threads library. This is not entirely sound [1].
The next revision of the C++ standard (currently known as C++0x) will define an explicit semantics for threads [2]. The approach will be similar to (but simpler than) that recently followed by Java, in that it will give sequentially consistent semantics to programs that do not contain data races but will give no semantics to racy programs.
However, enforcing sequential consistency is expensive on some platforms, and there are some frequently used idioms for which sequential consistency is not required. The proposed model supports low-level atomic operations that allow the programmer to explicitly specify memory ordering constraints, allowing close to optimal implementations of these idioms.
Research Proposal
In this project, we study how the semantics of low-level atomics can be implemented on modern architectures such as x86 [3], Power, and ARM. We aim to prove that the proposed implementations of the low-level atomics, above one or more of those architectures, are correct with respect to semantic models of C++0x and of the architecture(s). We will first address the atomic operations in isolation. If this goes well, we will consider the correctness of a simple compiler that makes use of them.
References
[1] Boehm, Threads cannot be implemented as a library, PLDI 2005.
[2] Bohem, Adve, Foundations of the C++ Concurrency Memory Model, PLDI 2008.
[3] Owens, Sarkar, and Sewell, A Better x86 Memory Model: x86-TSO . TPHOLs 2009.
Organisation
This internship will be supervised by Francesco Zappa Nardelli (INRIA Paris-Rocquencourt) and Peter Sewell (Computer Laboratory, University of Cambridge). It should be possible to work on part of the internship in Cambridge, UK. Pursuing this line of research in a PhD is also possible.
Contact Francesco Zappa Nardelli for more information.