- Slides on shared memory, Hoare logic, and separation logic.
- Slides on concurrent separation logic.
- Slides on Owicki-Gries and Rely/Guarantee.
- Introduction to relaxed memory models (no slides, but a reference).
Some exercises.
The exam questions.
References:
- Mike Gordon: Specification and Verification I, chapters 1 and 2;
- John Reynolds: Introduction to Separation Logic, parts 1-4;
- Peter O'Hearn: Resources, Concurrency and Local Reasoning;
- Viktor Vafeiadis: Concurrent separation logic and operational semantics;
- Viktor Vafeiadis, Maurice Herlihy, Tony Hoare, Marc Shapiro: A safety proof of a lazy concurrent list-based set implementation (esp. sec. 1-6);
- Sewell et al.: The semantics of multiprocessor machine code.
- Maurice Herlihy, Nir Shavit: The Art of Multiprocessor Programming, Morgan Kaufmann;
- Leonor Prensa Nieto: Verification of Parallel Programs with the Owicki-Gries and Rely-Guarantee Methods in Isabelle/HOL (esp. sec. 2.1-2.4 and 2.8);
- Stephen Brookes: A semantics for concurrent separation logic;
- Cliff Jones: Annotated bibliography on rely/guarantee conditions.
Francesco Zappa Nardelli proposes two stages for 2010/2011:
- verified compilation of C / C++ low-level atomics to x86, Power or ARM multiprocessors;
- relaxed memory concurrency and compiler optimisations.
Email: Francesco.Zappa_Nardelli (at) inria.fr
Address: Francesco Zappa Nardelli, Projet Moscova, INRIA Paris-Rocquencourt, Domaine de Voluceau, B.P. 105, 78153 Le Chesnay Cedex, France