Parisian Master of Research in Computer Science

Master Parisien de Recherche en Informatique (MPRI)

Concurrence (48h, 6 ECTS)

Responsibles : Roberto Amadio, Jean-Jacques Lévy et Catuscia Palamidessi

Teachers for 2010-2011

1. Frank Valencia (CCS, 12h)
2. James Leifer (pi-calculus, 12h)
3. Francesco Zappa Nardelli (Shared Memory, Separation Logic and Rely-Guarantee, 12h)
4. Emmanuel Haucourt (Directed Algebraic Topology and Concurrency, 12h)

Goals

This course introduces several formal methods for reasoning about properties of concurrent and distributed systems.

The first part of the course uses process algebras and other formalisms which abstract the creation and execution of processes and their elementary synchronization: shared memory, communication by channels, etc. These elementary calculi are, for concurrent processes, the correspondent of lambda calculus for sequential programs.

The second part of the course will study some proof methods, based on logics or mathematics, to reason about concurrent programs and shared memory.

Plan of the course

• Introduction and motivations (1h)

• Calculus of Communicating Systems (CCS) (11h)
  • Syntax
  • Operational Semantics (SOS)
  • Synchronization Trees
  • Traces
  • Strong Bisimulation
  • Weak Bisimulation
  • Equality Theory
  • Hennessy-Milner Logic
  • Model checking
  • Examples of Specification and Verification in CCS

• The pi-calculus (12h)
  • Syntax
  • Early and Late Semantics
  • The Asynchonous pi-calculus
  • Types
  • Equality Theory
  • Specifications with the pi-calculus
  • Other approaches to mobility

• Separation Logic, Rely-Guarantee, and Weak Memory models (12h)
  • Shared memory
  • Hoare logics
  • Separation logics
  • Separation logics and Concurrency
  • Rely-Guarantee reasoning
  • Weak Memory models (the x86 processor)

• Directed Algebraic Topology and Concurrency (12h)
  • Dijkstra PV language
  • Control-flow graph
  • Category of paths on a graph
  • Partially ordered spaces
  • Fundamental category in a partially ordered space
  • Seifert and van Kampen theorem for the fundamental category
  • Category of components
  • Factorisation of small, finite, connected, loopless categories
  • Some other topological models

English

Lectures will be in English.

Material

The slides of the classes will be available on line.

Related courses

2-7-1, 2-8, 2-23-1. These course treat related topics and the student may find in them interesting connections and useful background knowledge. However they are not required: the course in Concurrency is self-contained.

Prerequisites

None.

Bibliographie

• Milner, R. (1989). Communication and Concurrency. International Series in Computer Science. Prentice Hall.
• Milner, R. (2001). The pi-calculus. Cambridge University Press.
• Sangiorgi, D. and Walker, D. (2001). The π-calculus: a Theory of Mobile Processes. Cambridge University Press.
• Nachbin, L. (1965) . Topology and Order. Van Nostrand Reinhold.
• Higgins, P.J. (1971). Categories and Groupoids. Van Nostrand Reinhold. TAC reprints version
• Topologie Algébrique Dirigée et Concurrence. Notes de cours (pdf) / Lecture notes (pdf)

Les années précédentes

• Année 2009-2010
• Année 2008-2009
• Année 2007-2008
• Année 2006-2007

Équipe pédagogique

Calendar