Re: [isabelle] Advertise your work on the mailing list
On Mon, 2010-10-25 at 17:55 +0200, Jasmin Christian Blanchette wrote:
> This is just a reminder that we are all encouraged to let the mailing
> list know about your Isabelle-based work on the mailing list.
Mathematizing C++ Concurrency (POPL 2011, joint work with Mark Batty,
Scott Owens, Susmit Sarkar, and Peter Sewell, Cambridge University)
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 high-performance concurrent code.
However, the current draft standards, while the result of careful
deliberation, are still rather far from clear and rigorous definitions.
In this paper we establish a mathematical (yet readable) semantics for
C++ concurrency. We aim to capture the intent of the current draft as
closely as possible, but discuss a number of points where this is not
straightforward. 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 semantics of examples, using
code generated from our Isabelle/HOL definitions.
This will aid discussion of any further changes to the draft standard,
provide a correctness condition for compilers, and give a much-needed
basis for analysis and verification of concurrent C and C++ programs.
Special thanks to Jasmin Blanchette for his extensive help in getting
Nitpick to work for us!
This archive was generated by a fusion of
Pipermail (Mailman edition) and