Lectures given at the Master Parisien de Recherche en Informatique, 2009.
Part of the Concurrency course, in collaboration with Frank Valencia, Roberto Amadio, Emmanuel Haucourt.
Up-to date slides available from the 2010 course web-page.
- Shared memory, Hoare logic, and separation logic.
- Concurrent separation logic.
- Owicki-Gries and Rely/Guarantee.
- Relaxed memory models.
Some exercises.
The exam questions, and the solution.
References:If you want more:
- 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;
- Stephen Brookes: A semantics for concurrent separation logic.
- 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);
- Cliff Jones: Annotated bibliography on rely/guarantee conditions.
Francesco Zappa Nardelli proposes two stages for 2009/2010:
- compilation of C++ low-level atomics to x86, Power or ARM multiprocessors;
- proofs from tests for ML.
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