Mathematizing C++ concurrency

10 years 1 months ago
Mathematizing C++ concurrency
Shared-memory concurrency in C and C++ is pervasive in systems programming, but has long been poorly defined. This motivated an ongoing shared effort by the standards committees to specify concurrent behaviour in the next versions of both languages. They aim to provide strong guarantees for race-free programs, together with new (but subtle) relaxed-memory atomic primitives for highperformance concurrent code. However, the current draft standards, while the result of careful deliberation, are not yet clear and rigorous definitions, and harbour substantial problems in their details. In this paper we establish a mathematical (yet readable) semantics for C++ concurrency. We aim to capture the intent of the current (‘Final Committee’) Draft as closely as possible, but discuss changes that fix many of its problems. We prove that a proposed x86 implementation of the concurrency primitives is correct with respect to the x86-TSO model, and describe our CPPMEM tool for exploring the sema...
Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewe
Added 17 Sep 2011
Updated 17 Sep 2011
Type Journal
Year 2011
Where POPL
Authors Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, Tjark Weber
Comments (0)