MPRI > WebSite > C-2-3	Page sur le site du MPRI	MPRI webs: Main | TWiki | Sandbox
	WebSite . { Changes | Index | Search | Go }

Parisian Master of Research in Computer Science

Master Parisien de Recherche en Informatique (MPRI)

Concurrence (48h, 6 ECTS)

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

Intervenants prévus pour 2009-2010

1. Frank Valencia (CCS, 12h)
2. Roberto Amadio (Extensions: Mobilité, Temps et Probabilité 12h)
3. Francesco Zappa Nardelli (Logique de séparation et Modèles Faibles de Mémoire, 12h)
4. Emmanuel Haucourt (Topologie Algébrique Dirigée et Concurrence, 12h)

Objectifs

Ce cours est une introduction aux modèles de langages concurrents et possiblement répartis et aux techniques qui permettent de les analyser.

La première partie du cours (Valencia) se focalise sur un calcul de processus (CCS) qui représente à un niveau abstrait la création et l'exécution de processus et la synchronisation basée sur la communication par canaux.

La deuxième partie du cours (Amadio) considère un certain nombre d'extensions du modèle de base qui prennent en compte la notion de mobilité (pi-calcul) de synchronie (ou temporisation) et de probabilité.

La troisième partie du cours (Zappa Nardelli) introduit la logique de séparation qui est une extension de la logique de Hoare aux programmes avec pointeurs. On s'intéresse notamment à l'extension de cette logique aux programmes concurrents avec mémoire partagée ainsi qu'aux modèles ``faibles'' de mémoire.

La quatrième partie du cours (Haucourt) se concentre sur la représentation du parallélisme en termes de modèles topologiques. On compare la sémantique opérationnelle d'un simple langage de processus concurrents avec mémoire partagée à celle donnée par l'homotopie dirigée entre chemins dans les modèles. Le principe est que l'homotopie dirigée entre chemins représente naturellement le parallélisme asynchrone et la dimension "géométrique" du modèle d'un programme reflète le nombre de ses processus concurrents.

Plan du cours

• Introduction et motivations (1h)

• Calcul des Systèmes Communicants (CCS) (11h)
  • Syntaxe
  • Sémantique Opérationnelle (SOS)
  • Bisimulation Forte
  • Bisimulation Faible
  • Traces et Echecs
  • Théorie de l'Egalité
  • Logique de Hennessy-Milner et LTL
  • Expressivité du calcul CCS.

• Extensions: Mobilité, Temps et Probabilité (12h)
  • Un langage fonctionnel-concurrent et sa traduction CPS.
  • Un langage intermédiaire: le pi-calcul.
  • Synchronie et Temps.
  • Probabilité et Non-déterminisme.

• Logique de séparation et et Modèles Faibles de Mémoire (12h)
  • Programmation concurrente par mémoire partagée
  • Logique de Hoare
  • Logique de séparation
  • Extension de la logique de séparation à la concurrence
  • Raisonnement ``Rely-Guarantee''
  • La programmation au dessus des modèles faibles de mémoire (le cas x86)

• Topologie Algébrique Dirigée et Concurrence (12h)
  • Le langage PV de Dijkstra
  • Graphe de flot de contrôle
  • Catégorie des chemins sur un graphe
  • Espaces partiellement ordonnés
  • Catégorie fondamentale d'un espace partiellement ordonné
  • Le théorème de Seifert et van Kampen pour les catégories fondamentales
  • Catégorie des composantes
  • Factorisation des petites catégories finies connexes et sans boucle
  • Quelques autres modèles topologiques

Langue

Supports didactiques

Les transparents des cours seront disponibles en ligne.

Cours liés

2-1, 2-2, 2-4-2, 2-7-1, 2-8, 2-19, 2-23-1. Ces cours couvrent des thématiques voisines. Ceci dit, aucun n'est requis pour la compréhension du cours Concurrence.

Pré-requis

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 2008-2009
• Année 2007-2008
• Année 2006-2007

Équipe pédagogique

Calendrier

• Set ALLOWTOPICCHANGE = WebMastersGroup, JamesLEIFER, CatusciaPalamidessi, RobertoAmadio, FrancescoZappaNardelli, PierreLouisCurien, FrankValencia, EmmanuelHaucourt