Parallélisme synchrone
Année 2017–2018

Cours 2-23-1 du MPRI

Début des cours: Mardi 12 septembre 2016, 12h45 - 15h45, Univ. Paris Diderot, Bat. Sophie Germain.

Responsable du cours: Marc Pouzet

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

Pour toute question sur le cours, ne pas hésiter à nous contacter par mail (Marc.Pouzet@ens.fr, Timothy.Bourke@ens.fr, Jean.Vuillemin@ens.fr). Nous sommes situés dans les locaux de l’équipe INRIA/DI PARKAS, au 1er sous-sol du batiment 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 deux séances 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).

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 3 décembre 2017. Le sujet de compilation et le sujet de model-checker avec le code associé. Nous organiserons une soutenance de 15 minutes par projet dans la semaine du 4 décembre.

Ces projet sont sans limite:

Années précédentes


This document was translated from LATEX by HEVEA.