Sémantique du parallélisme

Résumé

• De quoi parle-t-on?
  
  On souhaite analyser et modéliser des systèmes constitués d'entités qui interagissent entre elles. Il s'agit de comprendre en quoi il faut changer de point de vue pour parler de tels systèmes, et ne plus se contenter des modèles “traditionnels” du calcul séquentiel (machine de Turing, λ-calcul)?
  
  Par exemple, le non-déterminisme est volontiers absent de modèles comme le λ-calcul (qui est confluent); au contraire, il joue un rôle important dans les modèles parallèles.
  
  De même, un programme séquentiel est sensé fournir une réponse lorsqu'on lui soumet une entrée, et un programme qui diverge est considéré comme erroné. On attend au contraire d'un serveur qu'il interagisse avec ses clients indéfiniment: la convergence n'est pas toujours souhaitable dans un contexte parallèle.
  
  
• Comment s'exprime l'essence du parallélisme?
  
  De quels ingrédients a-t-on besoin pour définir un modèle formel du parallélisme?
  
  Si le λ-calcul se fonde sur la notion de fonction, avec quelles constructions faut-il `programmer l'interaction' au sein d'un système parallèle? Y a-t-il des modèles dénotationnels rendant compte de ces constructions?
  
  
• Comment raisonne-t-on sur des systèmes qui interagissent?
  
  A partir de la définition d'une algèbre de processus, on montrera comment définir des équivalences comportementales entre processus, ainsi que des approches pour garantir certaines propriétés d'un processus donné (systèmes de types, logiques modales).
  
  
• A quoi ça sert?
  
  Les principales applications des algèbres de processus sont dans la spécification et l'analyse de systèmes. Des outils pour la vérification automatique ont ainsi été développés.
  
  Des formalismes apparentés au π-calcul ont également servi de fondement pour la définition de langages pour la programmation concurrente et distribuée.
  
  Nous évoquerons ces divers domaines d'application.
  
  
• A quoi ça peut servir?
  
  Des liens sont apparus récemment entre le π-calcul et d'autres domaines. Une direction particulièrement intéressante est la connection avec la logique et la théorie de la preuve, via la correspondance de Curry-Howard. Mentionnons également l'utilisation d'algèbres de processus pour raisonner sur des systèmes biologiques.

Plan indicatif de la première partie du cours (avant les exposés)

1. un modèle de la concurrence: CCS
   • le calcul: syntaxe, sémantique opérationnelle, exemples
   • équivalences comportementales; logiques modales, axiomatisations
2. mobilité: le π-calcul
   • éléments du langage, questions d'expressivité
   • systèmes de types, équivalences typées
   • “programmation”: λ-calcul en π-calcul, langages dérivés du π-calcul
   • calculs avec localités: Dπ, les Ambients; logiques spatiales

Bibliographie

• des liens vers des textes introductifs et des références pertinentes seront disponibles à partir de http://perso.ens-lyon.fr/daniel.hirschkoff
  
  http://perso.ens-lyon.fr/daniel.hirschkoff
  
  
  
  
  Les trois livres ci-dessous sont disponibles à la bibliothèque.
  
  
• R. Milner, Communication and Concurrency, Prentice Hall, 1989.
  
  
• M. Hennessy, A Distributed π-calculus, Cambridge University Press, 2007.
  
  
• D. Sangiorgi and D. Walker, The pi-calculus: A Theory of Mobile Processes, Cambridge University Press, 2001.