Parallélisme synchrone
Année 2024–2025

Cours 2-23-1 du MPRI

Début des cours: Mardi 17 septembre 2024, 8h45 - 11h45, Univ. Paris Diderot, Bat. Sophie Germain, salle 1002.

Responsable du cours: Marc Pouzet

Plan du cours pour 2024–2025:

• Langages synchrones, sémantique et implémentation:
  • 4 cours - 12h, Marc Pouzet
  • 4 cours - 12h, Timothy Bourke

Pour toute question sur le cours, ne pas hésiter à nous contacter par mail (Marc.Pouzet@ens.fr, Timothy.Bourke@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 2025 (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).

Sujets de stages

Exercises

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

Documents à lire

Ci-dessous une liste d’articles a lire.

• Gérard Berry. Real time Programming: special purpose or general purpose languages. RR INRIA no. 1065. Disponible ici.
• A. Benveniste and P. Caspi and S.A. Edwards and N. Halbwachs and P. Le Guernic and R. de Simone. The synchronous languages 12 years later. Proceedings of the IEEE, Volume 91, Number 1, January, 2003. (Une présentation d’ensemble de la programmation synchrone et une bibliographie récente). Disponible ici.
• Edward A. Lee and Alberto Sangiovanni-Vincentelli, A FRAMEWORK FOR COMPARING MODELS OF COMPUTATION, IEEE Transactions on CAD, 1998, Vol. 17, no. 12, December 1998. (Proposition d’un modèle unifié de systèmes). Lire ceci, cela et ce dernier.
• Deux articles intéressants (et de culture générale) donnant le point de vue d’Edward Lee sur les threads (The Problem with Threads) et la modélisation du temps physique (Computation Needs Time).
• Randal E. Bryant. Graph-Based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers, C-35-8, pp. 677-691, August, 1986. (article “historique” sur les BDD). Version disponible ici.
• Mary Sheeran and Satman Singh and Gunnar Stalmark. Checking safety properties using induction and a SAT-solver. FMCAD 2000. (Comment obtenir un model-checker de propriétés de sûreté à partir d’un solveur SAT). Version disponible ici. Le cours sur la vérification donne beaucoup d’autres références. Celui-ci est le premier expliquant l’usage d’un solveur SAT pour une preuve exhaustive.
• Edward A. Lee and Pravin Varaiya. Structure and Interpretation of Signals and Systems. Addison-Wesley, 2003. (Un cours d’introduction aux systèmes réactifs). Voir également la nouvelle version de 2011.
• Un article (un peu ancien) en français sur Lucid Synchrone.

Logiciel

• Fichier donnant une liste (non exhaustive) de références bibliographiques: bibliographie
• mode Emacs pour Lustre
• Distribution de Lustre. Manuel de référence de Lustre. (version Linux à utiliser en cas de problème de liaison avec les librairies tcl/tk).
• Lustre V6
• Distribution de Lucid Synchrone
• Distribution d’Esterel (alternative avec binaire pour Linux ici).
• Distribution de ReactiveML
• Distribution de Zélus
• Distribution de Heptagon

Travail personnel:

Cette année, nous vous proposons plusieurs projets de programmation. L’un consiste à écrire un compilateur vers du code séquentiel (C ou Rust) de Lustre, le second, à développer un model-checker par la technique de k-induction. Une troisième idée est l’écriture, en Coq (ou en Lean) d’un interprète du noyau du langage Zelus à partir de ce qui a été présenté en cours et mis en oeuvre en OCaml (https://github.com/marcpouzet/zrun). Pour ceux qui suivent le cours d’interprétation abstraite, une variante de ce projet est l’écriture d’un interprète abstrait. Nous vous conseillons de le faire alors à deux pour pouvoir tester plusieurs domaines abstraits.

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 ce que vous avez utilisé.

A rendre au plus tard 5 janvier 2025. 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 16 décembre.

Ces projets sont sans limite:

• Pour le compilateur, vous pouvez implémenter des optimisations, en particulier la minimisation des copies, à partir de cet article.
• Vous pouvez également implémenter l’algorithme d’ordonnancement statique modulaire vu en cours. Cela peut être fait au moment de la traduction de Lustre vers Obc, en produisant non pas une seule méthode “step” par fonction synchrone mais plusieurs.
• Pour la vérification formelle, vous pouvez également écrire un traducteur de Lustre vers le model checker Z3-PDR et comparez vos résultats.

Ce document a été traduit de L^AT_EX par H^EV^EA