Parisian Master of Research in Computer Science
Master Parisien de Recherche en Informatique (MPRI)

Concurrency (24h, 3 ECTS)

Course director: Roberto Amadio

Teachers for 2015-2016

Goals

This course introduces formal methods for reasoning about properties of concurrent systems. Topics covered change every year and include models of shared memory concurrency (Java,...), logics to reason on such systems (rely-guarantee, concurrent separation logic,...), process calculi (CCS, pi-calculus,...), models of timed and stochastic behaviour, and applications of directed algebraic topology to concurrency.

Plan of the course for 2015-2016

Shared memory models and logics of concurrent systems (12h)

  • A shared variable parallel language.
  • Compositional trace model.
  • Denotational presentation of the trace model.
  • Introduction to rely-guarantee reasoning.
  • Separation Logic 1 : frame rule, parallel rule
  • Separation Logic 2 : permissions, RGSep, copyless message-passing,

Process calculi and related type and proof systems (12h)

  • Labelled transition systems.
  • CCS.
  • Determinacy and confluence.
  • pi-calculus.
  • Session types.
  • Separation logic and communication contracts.
  • Proof assistants for separation logic.

French and English

Lectures are given either in French or in English depending on the teacher. The lecture notes and the text of the examinations are in English. The students may answer in French or English.

Material

  • Lecture Notes by R. Amadio This year we will cover (at most) chapters 1,2,3,5,7,9,10,13. A trace of what has actually been covered in the lectures is here. A compact reference for what is needed at the exam is here (just 10 pages in duplex printing...sorry for the dangling pointers but you cannot have it all...)

Bibliography

  1. Local Reasoning about Programs that Alter Data Structures. Peter W. O'Hearn, John C. Reynolds, Hongseok Yang.
  2. Local Action and Abstract Separation Logic. Cristiano Calcagno, Peter W. O'Hearn, Hongseok Yang.
  3. Smallfoot: Modular Automatic Assertion Checking with Separation Logic. Josh Berdine, Cristiano Calcagno, Peter W. O'Hearn.
  4. Separation and Abstraction. Gavin Bierman, Matthew Parkinson.
  5. Local Reasoning for Java. Matthew Parkinson, phD.
  6. Proving Copyless Message Passing J. Villard, E. Lozes, C. Calcagno.

Intership Proposals

Related courses

Semantics (2.1, 2.2, 2.4), Concurrent algorithms (2.18.2), Concurrent programming (2.23.1, 2.37.1), Proofs of programs (2.36.1). Formalisms related to the pi-calculus are used in the modelling of cryptographic protocols (course 2.30) and of biological reactions (course 2.19).

Prerequisites

It is useful, though not strictly necessary, to have attended courses (similar to) 1-15 (Semantics) and 1-16 (Concurrency).

Exams

This year course alternates between lectures on core/introductive material (Amadio's lectures) and lectures on more specialized/research topics (Lozes' lectures). Knowledge of the core material will be checked via a final exam while the more specialized/research topics will be the subject of a home assignment.

Final exam 2015-2016 with correction

Possible teachers

R. AmadioUniv. Paris DiderotPPS
E. GoubaultÉcole PolytechniqueLIX
E. HaucourtÉcole PolytechniqueLIX
J. LeiferINRIARocquencourt
E. LozesENS CachanLSV
F. ValenciaÉcole PolytechniqueLIX

Calendar 2015-2016

Date Speaker
16 Sept., 23 Sept. Amadio
30 Sept., 7 Oct. Lozes
14 Oct. 21 Oct. Amadio
28 Oct. 4 Nov. Lozes
18 Nov. Optional exercise, questions/answers session (contact R. Amadio if interested)
25 Nov. Final written exam (Amadio)

Previous years Year 2015-2016 Year 2014-2015 Year 2013-2014 Year 2012-2013

 
Universités partenaires Université Paris-Diderot
Université Paris-Saclay
ENS Cachan École polytechnique Télécom ParisTech
ENS
Établissements associés Université Pierre-et-Marie-Curie CNRS INRIA CEA