Parallélisme synchrone
Année 2019–2020

Cours 2-23-1 du MPRI

Début des cours: Lundi 16 septembre 2019, 12h45 - 15h45, Univ. Paris Diderot, Bat. Sophie Germain, salle 1014.

Responsable du cours: Marc Pouzet

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

Pour toute question sur le cours, ne pas hésiter à nous contacter par mail (Marc.Pouzet@ens.fr, Timothy.Bourke@ens.fr, adrien@guatto.org). 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 2020 (mi-mars/fin août). Il y a quelques idées dans le sujet officiel, mais sinon passons 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).

16 septembreCours 1BourkeIntroduction à la programmation synchrone pour les systèmes embarqués: slides et exercices.
23 septembreCours 2BourkeVélus: un compilateur Lustre vérifié dans Coq: slides.
30 septemberCours 3PouzetOrdonnancement statique modulaire; suites, fonctions de suites et horloges (transparents et notes de cours.
7 octobreCours 4PouzetCoiteration.
14 octobreCours 5GuattoGeneralized Clocks and their Modal Aspect.
21 octobreCours 6PouzetAnalyse de causalité par typage.
28 octobreCours 7BourkeVerification de programmes synchrones par model-checking (BDD/SMT): slides, ocaml-bdd library, examples.tar.gz et exercises en ligne sur les BDDs.
4 novembreCours 8PouzetModèles hybrides temps discret/temps continu.
11 novembreJour fériépas de coursFaire le TP1 et/ou TP2.
18 novembreCours 9BourkeLa modélisation et l’analyse de contrôleurs temps réels: quasi-synchrone et LTTA: slides.
25 novembreExamenBourke et PouzetNotes de cours autorisées. Examens anciens:
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 deux projets différents; 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.

A rendre au plus tard 15 décembre 2019. 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 projet sont sans limite:


Ce document a été traduit de LATEX par HEVEA