Parallélisme synchrone
Année 2018–2019

Cours 2-23-1 du MPRI

Début des cours: Lundi 17 septembre 2018, 8h45 - 11h45, Univ. Paris Diderot, Bat. Sophie Germain, salle 1004.

Responsable du cours: Marc Pouzet

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

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

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.

Il y aura une séance de TD/TP sur machine et un projet de programmation.

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).

17 septembreCours 1BourkeIntroduction à la programmation synchrone pour les systèmes embarqués: slides, fulladder.lus, heat.lus, heat.zls.
24 septembreCours 2BourkeVélus: un compilateur Lustre vérifié dans Coq: slides.
1 octobreTP 1PouzetLe compilateur «mini-lustre»: mini-lustre.pdf, mini-lustre.tgz et slides.pdf. Le corrigé.
   Un microprocesseur dans Lustre: hack-en.pdf et hack.tar.gz. A partir de ce livre. Le corrigé.
8 octobreCours 3PouzetOrdonnancement statique modulaire. Structures de contrôle (switch, blocs, reset, automates hiérarchiques) et leur traduction dans le langage noyau. Notes supplémentaires: compilation dirigée par les horloges d’un langage noyau.
15 octobreCours 4PouzetSuites synchrones; calcul d’horloges par typage.
22 octobreCours 5 Cours invité: Adrien Guatto. Horloges entières et types gardés.
29 octobreCours 6BourkeVerification de programmes synchrones par model-checking: slides, ocaml-bdd library, examples.tar.gz et exercises en ligne sur les BDDs.
 Sur la vérification formelle:
  • L’article de Bryant sur les bdds (indispensable !);
  • celui de Sheeran et al. sur la k-induction;
  • L’outil KIND de Hagen et Tinelli utilisant un solveur SMT. L’outil Kind2 qui combine k-induction, BMC et PDR.
  • Les notes sur la vérification formelle sont issues du chapitre rédigé par Pascal Raymond et qui va bien plus loin.

Dans le cours, j’ai mentionné la reconnaissance d’expressions régulières par un circuit synchrone. Lire le magnifique article de Pascal Raymond. Le langage Lutin montre comment un programme synchrone non déterministe permet de spécifier et de simuler un environnement.

5 novembreCours 7PouzetModèles hybrides et temps discret/temps continu.
12 novembreCours 8PouzetModèles hybrides et temps discret/temps continu. Quelques notes sur une expression des dépendances par des types.
19 novembreCours 9BourkeLa modélisation et l’analyse de contrôleurs temps réels: quasi-synchronie et LTTA.
26 novembreExamenBourke et PouzetNotes de cours autorisées. Examens anciens:

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 16 décembre 2017. 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 17 décembre.

Ces projet sont sans limite:


Ce document a été traduit de LATEX par HEVEA