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 2014-2015


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. Last year we covered methods to reason about probabilities and expressiveness in concurrent systems. In 2014-2015, we plan to cover applications of directed algebraic topology to concurrency. Further in 2014-2015, the first part of the course focuses on shared memory models of concurrent systems which are considered both from a semantical and an algorithmic perspective.

This 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.

Plan of the course for 2014-2015

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.

Algorithms for shared memory (Kuznetsov, 12h)

  • Introduction: blocking and nonblocking synchronization
  • Correctness of concurrent algorithms: safety and liveness
  • Read-write memory: definitions and transformations
  • Transactional memory: definitions, lower bounds, and algorithms

Directed Algebraic Topology and Concurrency (Haucourt, 24h)

  • What kind of concurrency in this course?
  • Extended Dijkstra PV language
  • Precubical sets as a generalization of graphs
  • Control-flow graph, conservative programs, and precubical control flow
  • Locally ordered spaces
  • Directed realization of graphs and precubical sets
  • Isothetic regions
  • The fundamental category
  • Seifert and van Kampen theorem for the fundamental category [optional]
  • The category of components
  • Factorisation
  • Some other topological models

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.


Shared memory models of concurrent systems

  • Lecture Notes – ONLY THE FIRST 6 SECTIONS (up to Concurrent objects) ARE COVERED IN 2014-2015.
  • Some Slides – A few slides presented in the course, not immediately subsumed by the lecture notes, and somehow related to the home assignment.

Algorithms for shared memory

Directed Algebraic Topology and Concurrency

Related courses

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


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


A Home Assignment on Amadio's part, a written examination at the mid term on Kuznetzov's part and a written examination at the end of the semester on Haucourt's part.

Possible teachers

R. AmadioUniv. Paris DiderotPPS
K. ChatzikokolakisINRIALIX
E. GoubaultÉcole PolytechniqueLIX
E. HaucourtÉcole PolytechniqueLIX
J. LeiferINRIARocquencourt
C. PalamidessiINRIALIX
F. ValenciaCNRSLIX

Calendar 2014-2015

Date Speaker
22/09, 29/09, 06/10, 13/10 (3 hours lectures, course starts at 8:45) Amadio
27/10, 03/11, 10/11, 17/11 (3 hours lectures, course starts at 8:45) Kuznetsov
Return home assignment and Mid-term written exam : dates available on the pedagogical server
8/12, 15/12, 05/01, 12/01, 19/01, 26/01, 02/02, 09/02, 16/02, 23/02 (course starts at 9:15 and ends at 12:00). Haucourt
Final written exam : 9/03 (WARNING: the exam starts at 8:45 and ends at 11:45)

Previous years 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
Établissements associés Université Pierre-et-Marie-Curie CNRS INRIA CEA