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

Concurrency (48h, 6 ECTS)

Course directors: Roberto Amadio and Catuscia Palamidessi

Teachers for 2013-2014

  1. Roberto Amadio (12h)
  2. Daniele Varacca (12h)
  3. Kostas Chatzikokolakis (12h)
  4. Frank Valencia (12h)

Goals

This course introduces formal methods for reasoning about properties of concurrent systems. Starting from 2013-2014, the second part of the course changes every year. This year we cover methods to reason about probabilities and expressiveness in concurrent systems. In 2014-2015 we plan to cover applications of directed algebraic topology to concurrency.

Plan of the course

The course is organised in 20 lectures. The course is `breakable'. This means that you get 3 credits if you pass only the first part (up to the mid-term exam) or the second part (after the mid-term) and 6 credits if you pass both. Notice that the grade we consider to give 6 credits is the average of the grades of the first and second part. For instance, if your grade is 12/20 in one part and 8/20 in the other you get 6 credits.

Shared memory models of concurrent systems (Amadio, 12h)

  • A shared variable parallel language.
  • Compositional trace model.
  • Denotational presentation of the trace model.
  • Implementing atomicity.
  • Rely-guarantee reasoning.
  • Concurrent objects.

CCS and the pi-calculus (Varacca, 12h)

  • Labelled transition systems. Bisimulation. Proof techniques.
  • The trace-bisimulation spectrum and the related modal logics
  • CCS a calculus of communicating systems. Characterisation of labelled bisimulation.
  • The pi-calculus.
  • Functions as processes: compiling lambda into pi.

Probabilistic models and applications (Chatzikokolakis, 12h)

  • Probabilistic asyncronous pi calculus
  • Semantics based on simple probabilistic automata
  • Probabilistic bisimulation (maybe also testing equivalence)
  • Introduction to probabilistic model checking and PRISM
  • Verification of anonymity protocols: Dining Cryptographers, Crowds

Expressive power of concurrent models (Valencia, 12h)

  • Expressiveness in Concurrency: Techniques and Criteria.
  • The Expressiveness of Iteration, Recursion and Name Scoping in CCS-based Calculi.
  • Expressiveness in the pi-Calculus: Polyadic vs Monadic Communication.
  • Expressiveness in the pi-Calculus: Asynchronous vs Synchronous Communication.
  • Expressive fragments of the pi-calculus.
  • The Expressiveness of Shared-Memory Communication.

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 and home assignment for the first period are available here

Related courses

Semantics (2.1, 2.2, 2.4), Concurrent algorithms (2.18.2, 2.18.3), Concurrent programming (2.23.1, 2.37.1).

Prerequisites

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

Possible teachers

R. AmadioUniv. Paris DiderotPPS
K. ChatzikokolakisINRIALIX
E. GoubaultCEA LIST Saclay
E. HaucourtCEA LIST Saclay
J.-J. LévyINRIARocquencourt
J. LeiferINRIARocquencourt
C. PalamidessiINRIALIX
F. ValenciaCNRSLIX
D. VaraccaUniv. Paris DiderotPPS

Calendar

Date Speaker
20 Sep Amadio
27 Sep Amadio
4 Oct Amadio
11 Oct Amadio
18 Oct Amadio
25 Oct Varacca: LTS, simulation, bisimulation, Hennessy-Milner Logic (Lecture Notes, sections 7.1,7.2,8.1)
1 Nov Holidays
8 Nov Varacca: mu-calculus, CCS, weak bisimulation (Lecture Notes, sections 8.2, 9.1,9.2, 7.3)
15 Nov Varacca: reduction semantics, value passing, pi and LTS for pi (Lecture Notes, sections 9.3,9.4, 13.1 + SLIDES )
22 Nov Varacca: Up-to techniques, some notion of typing, encoding functions (beginning) (7.4, 13.2,13.3,14 + SLIDES )
29 Nov Varacca: Encoding functions (ending), exercices (14)
6 Dec Deadline home assignment (Amadio) + Mid-term exam (Varacca)
13 Dec Chatzikokolakis slides
20 Dec Chatzikokolakis slides
10 Jan Chatzikokolakis slides
17 Jan Chatzikokolakis slides
24 Jan Chatzikokolakis slides, prism files
31 Jan Valencia handouts relative expressiveness
7 Feb Valencia handouts absolute expressiveness
14 Feb Valencia handouts expressiveness of asynchronous communication
21 Feb Valencia handouts expressiveness of shared-memory and spatial communication (ECCP)
28 Feb Valencia handouts expressiveness of spatial communication (Ambients)
Valencia handouts expressiveness of higher-order communication(HOCORE)
Valencia handouts pre-exam exercises
7 Mar Final exam (Chatzikokolakis+Valencia)

Previous years

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