Parallélisme synchrone
Année 2020–2021

Cours 2-23-1 du MPRI

Début des cours: Mardi 15 septembre 2020, 16h15 - 19h15, Univ. Paris Diderot, Bat. Sophie Germain, salle 1014.

Responsable du cours: Marc Pouzet

Plan du cours et intervenants prévus pour 2020–2021:

Pour toute question sur le cours, ne pas hésiter à nous contacter par mail (Marc.Pouzet@ens.fr, Timothy.Bourke@ens.fr, Guillaume.Baudart@inria.fr). Nous sommes situés dans les locaux de l’équipe INRIA/DI PARKAS, au 1er sous-sol du bâtiment Rataud, à l’ENS.

Il est possible de faire un stage dans l’équipe PARKAS en printemps 2021 (mi-mars/fin août). Passez discuter avec nous!

Objectifs

Les langages synchrones permettent de programmer des systèmes réactifs embarqués à la fois très complexes et très sûrs. Ils rencontrent un grand succès dans divers domaines industriels, pour la programmation du logiciel de controle/commande dans les avions, les trains, les centrales nucléaires, etc. Le système de commande de vol des Airbus, par exemple, est développé avec l’outil SCADE issu du langage synchrone Lustre.

Ils sont fondés sur le modèle du parallélisme synchrone qui introduit une notion de temps logique dans les programmes et donne la possibilité d’écrire des programmes parallèles déterministes. Le compilateur d’un langage synchrone garantit des propriété de sûreté importantes pour le logiciel critique: exécution déterministe du code, absence de blocage (deadlock), génération de code séquentiel s’exécutant en temps et mémoire bornés, génération de code parallèle, etc.

Les langages ont évolué pour traiter des applications et domaines nouveaux: calcul vidéo intensif (TVHD, radars); grandes simulations (réseaux électriques, réseaux de capteurs, interlocking); systèmes de criticité mixte (automobile); combinaison du temps discret et du temps continu. Et les principes des langages synchrones ont étés intégrés dans des langages généralistes (e.g., ReactiveC, SugarCubes en Java, ReactiveML, FRP en Haskell).

Le cours présente les concepts fondamentaux des langages synchrones, leurs fondements sémantiques et logiques, les techniques de compilation vers du logiciel et des circuits, leur vérification formelle (par model-checking) et des travaux de recherche récents. Le cours montre les liens avec les langages fonctionnels.

Une partie du cours est consacrée aux travaux récents sur la sémantique et l’implémentation des langages pour modéliser des systèmes hybrides combinant du temps discret et du temps continu (modélisation de l’environnement physique ou encore l’interface analogique/discret dans un circuit électronique). Le cours montre comment étendre de manière conservatrice un langage synchrone avec du temps continu.

Introduction au domaine avec les vidéos de Gérard Berry sur les systèmes embarqués; Jean Vuillemin sur les circuits synchrones; Nicolas Halbwachs sur Lustre; Marc Pouzet sur les langages de programmation des systèmes hybrides à temps discret/continu au Collège de France.

Notes de cours

Toutes les notes sont en anglais (course notes are in English. If not, send me a mail).

15 septembreCours 1BourkeIntroduction à la programmation synchrone pour les systèmes embarqués: slides et exercices.
22 septembreCours 2BourkeVélus: un compilateur Lustre vérifié dans Coq: slides.
29 septembreCours 3BourkeVerification de programmes synchrones par model-checking (BDD/SMT). slides, ocaml-bdd library, examples.tar.gz et exercices en ligne sur les BDDs.
6 octobreCours 4PouzetOrdonnancement statique modulaire.
13 octobreCours 5PouzetSémantique synchrone fondée sur la co-itération.
20 octobreCours 6PouzetSuite du cours du 13/10. Automates hiérarchiques.

Conseil de lecture:

  1. D. Harel. StateCharts: a Visual Approach to Complex Systems. Science of Computer Programming, 8-3:231–275, 1987.
  2. F. Maraninchi and Y. Remond. Mode-automata: a new domain-specific construct for the development of safe critical systems. Science of Computer Programming, (46):219–254, 2003.
  3. Jean-Louis Colaco, Bruno Pagano, and Marc Pouzet. A Conservative Extension of Synchronous Data-flow with State Machines. In ACM International Conference on Embedded Software (EMSOFT’05), Jersey city, New Jersey, USA, September 2005.

Notes supplémentaires:Structures de contrôle et leur traduction dans le langage noyau.

3 novembreCours 7PouzetCausalité.
 
10 novembrecours 8PouzetModèles hybrides temps discret/temps continu. Sémantique et compilation de Zélus.
17 novembreCours 9BaudartProgrammation réactive probabiliste.
24 novembreCours 10 Suite et fin du cours 8 (sémantique et compilation des langages pour les systèmes hybrides).
1 décembre  L’examen est remplacé par le projet.
TP1  Le compilateur «mini-lustre»: mini-lustre.pdf, mini-lustre.tgz et slides.pdf. Le corrigé.
TP2  Un microprocesseur dans Lustre: hack-en.pdf et hack.tar.gz. A partir de ce livre. Le corrigé.

Exercices

Une petite liste d’exercices (anciens) de programmation Lustre/Esterel/Lucid Synchrone.

Documents à lire

Ci-dessous une liste d’articles a lire.

Logiciel

Travail personnel:

Cette année, nous vous proposons trois projets possibles. L’un consiste à écrire un compilateur vers du code séquentiel (C ou Rust) de Lustre, l’autre consiste à développer un model-checker par la technique de k-induction. Une troisième idée de projet est l’écriture, en Coq, d’un interprète du noyau du langage Zelus décrit dans le cours 4 à partir de l’interprète écrit en OCaml (https://github.com/marcpouzet/zrun).

Pour tous ces projets, n’hésitez pas à copier/adapter tout ou partie des code sources OCaml décrivant des sémantiques et/ou interprètes et/ou compilateurs qui vous sont montrés, à condition d’indiquer clairement ce que vous avez utilisé!

A rendre au plus tard 18 décembre 2020. Le sujet de compilation et le sujet de model-checker avec le code associé. Nous organiserons une soutenance de 30 minutes par projet dans la semaine du 14 décembre.

Ces projet sont sans limite:


Ce document a été traduit de LATEX par HEVEA