[Club2] Wed. Jun 1, 14:00: Jasmin Blanchette: "Nitpicking C++ Concurrency"

[Alexander Krauss]

Dear all,

next week, Jasmin will give a rehearsal of his PPDP 2011 talk on a major 
case study with Nitpick:


Nitpicking C++ Concurrency
====================================================
Wed. Jun 1, 14:00, MI 01.11.018 ("Konrad Zuse")

(joint work with Tjark Weber, Mark Batty, Scott Owens, and Susmit Sarkar)
PPDP 2011
http://www4.in.tum.de/~blanchet/ppdp2011-cpp-mem.pdf

Previous work formalized the C++ memory model in Isabelle/HOL in an 
effort to
clarify the proposed standard's semantics. Here we employ the model finder
Nitpick to check litmus test programs that exercise the memory model, 
including
a simple locking algorithm. We only need to give it a few hints, and 
thanks to
the underlying SAT solver it scales much better than the Cppmem 
explicit-state
model checker. This case study inspired optimizations in Nitpick from which
other formalizations can now benefit.