#+TITLE: Programmation synchrone 2025/2026 -- Journal du cours #+AUTHOR: Adrien Guatto #+EMAIL: guatto@irif.org #+LANGUAGE: fr #+OPTIONS: ^:nil p:nil #+LATEX_CLASS: article #+LATEX_CLASS_OPTIONS: [a4paper,11pt] #+LATEX_HEADER: \usepackage{a4wide} #+LATEX_HEADER: \usepackage{microtype} #+LATEX_HEADER: \hypersetup{hidelinks} #+LATEX_HEADER: \usepackage[french]{babel} # (org-latex-export-to-pdf) * Cours 01 <2025-09-29> On lit le syllabus ainsi que le début des notes. Le manuel d'Heptagon peut être trouvé sur le dépôt git du projet. On peut cliquer sur le bouton /download/ pour télécharger une copie PDF. https://gitlab.inria.fr/synchrone/heptagon/-/blob/ec26be27b91f3e601b98b8b7e15e8d56d4b9afc7/manual/heptagon-manual.pdf * Cours 02 <2025-10-06> On traite des constructions de base du langage. * Cours 03 <2025-10-13> On traite des horloges et automates. * Cours 04 <2025-10-20> On traite des automates et tableaux. * Cours 05 <2025-10-27> ** Programmation Heptagon On traite des tableaux. ** Exemples On traite la génération d'échantillons audios, disponbile dans son [dossier](audio/). * Cours 06 <2025-11-04> ** Projet On traite du fonctionnement du projet. * Cours 07 <2025-11-10> ** Exemples On traite l'exemple du pendule inversé, disponible dans son [dossier](inverted-pendulum/). ** Implémentation des langages synchrones On commence à expliquer la compilation d'Heptagon, avec l'explication de MiniLS vers Obc jusqu'au traitement des horloges *exclu*. * Cours 08 <2025-11-17> ** Implémentation des langages synchrones On discute de la compilation des horloges en MiniLS, de la traduction des automates et des structures de contrôle plus simples (notamment ~switch~) en Heptagon. On présente l'analyse d'initialisation. * Cours 09 <2025-11-24> ** Implémentation des langages synchrones On termine la partie concernant l'implémentation des langages synchrones. ** Vérification automatique L'outil Kind2 est un vérificateur de modèle (/model checker/) pour un langage proche d'Heptagon développé à l'université de l'Iowa. https://kind.cs.uiowa.edu Un tel outil est une des justifications pour l'emploi d'un langage très limité comme Heptagon, SCADE et leurs variantes. La vérification automatique est beaucoup plus difficile lorsque le langage d'entrée est un langage généraliste comme C, Python ou OCaml. *** Introduction Le langage accepté par Kind2 est une variante d'Heptagon beaucoup plus proche de son ancêtre Lustre. Les différences sont assez mineures mais peuvent rendre l'écriture du code désagréable lorsqu'on est habitué aux constructions d'Heptagon. Par exemple, le langage ne propose pas l'opérateur ~fby~, uniquement ~pre~ et ~->~. Notre classique compteur doit donc être écrit comme suit. #+BEGIN_SRC node counter() returns (o : int) let o = 0 -> (pre o + 1); tel #+END_SRC Kind2 est capable de traduire ce programme vers du code impératif, jouant ainsi le même rôle que le compilateur ~heptc~ pour Heptagon. Plutôt que de générer du code C, Kind2 produit du code Rust. #+BEGIN_SRC $ kind2 --compile true ex0.lus kind2 v1.1.0-16-g9572d9b System counter has no property, skipping verification step. -------------------------------------------------------------------------------- Post-analysis: rust generation Compilation to Rust is still a rather experimental feature: in particular, arrays are not supported. Compiling node "counter" to Rust in `ex0.lus.out/counter/implem`. Done compiling. -------------------------------------------------------------------------------- $ wc -l ex0.lus.out/counter/implem/src/main.rs 366 ex0.lus.out/counter/implem/src/main.rs #+END_SRC L'intérêt principal de Kind2 est ailleurs : il est capable de /vérifier formellement/ des propriétés. Par opposition au test, la vérification formelle permet de vérifier qu'une propriété est vraie pour *toute* entrée, plutôt que pour une entrée particulière. De plus, dans le cas des langages synchrones, les entrées sont des suites infinies, dont on ne peut tester qu'un préfixe fini. La vérification formelle, elle, considère des entrées de longueur infinie. Lorsqu'on découvre un outil de vérification formelle, un des premières questions à se poser est celle du langage dans lequel les propriétés sont écrites. Certains outils de vérification offrent un langage spécialisé pour ce faire, par exemple une logique temporelle pour le model-checker PRISM. Les outils de vérification de langages synchrones comme Kind2 font un choix un peu différent. Le langage des propriétés est le même que celui des programmes, et la propriété à vérifier est exprimée par un flot booléen désigné par l'utilisateur doit toujours être vrai. Avec cette approche, on va avoir tendance à écrire des /observateurs synchrones/, c'est-à-dire des noeuds qui sont utilisés uniquement pour vérifier que le noeud qui va être déployé sur le système embarqué final va respecter certaines propriétés, éventuellement sous certaines hypothèses concernant ses entrées. #+BEGIN_SRC node top() returns (ok : bool) var o : int; let o = counter(); ok = o >= 0; --%PROPERTY ok; tel #+END_SRC En lançant Kind2 sur ce fichier, on lui demande de vérifier que le flot ~ok~ est toujours vrai. Il est capable de vérifier que c'est le cas, même si ~ok~ contient une infinité de valeurs. #+BEGIN_SRC $ kind2 ex0.lus kind2 v1.6.0 ==================================================================================================================== Analyzing top with First top: 'top' subsystems | concrete: counter Property ok is valid by property directed reachability after 0.148s. -------------------------------------------------------------------------------------------------------------------- Summary of properties: -------------------------------------------------------------------------------------------------------------------- ok: valid (at 1) ==================================================================================================================== #+END_SRC (Cet exemple montre que Kind2 suppose que la sémantique du type ~int~ de Lustre est celle des entiers relatifs, sans limite de taille. Pourquoi ? Remarquons que jusqu'ici on avait supposé que les types des langages synchrones étaient tous finis, ce qui assurait la finitude de la mémoire. Comme on le décrira plus bas, ce choix n'est pas sans conséquences théoriques et pratiques.) Cet exemple laisse aussi deviner que la vérification est un processus coûteux, beaucoup plus coûteux que la compilation. Ce fichier étant écrit dans le sous-ensemble commun à Heptagon et Lustre, on peut le compiler avec ~heptc~ et comparer le temps de compilation au temps de vérification. #+BEGIN_SRC $ time heptc -target c ex0.lus real 0m0,026s user 0m0,013s sys 0m0,013s #+END_SRC On peut montrer des propriétés un peu plus intéressantes, par exemple en écrivant une variante du compteur avec une valeur d'initialisation. #+BEGIN_SRC node counterini(ini : int) returns (o : int) let o = ini -> (pre o + 1); tel node top(ini : int) returns (ok : bool) var o : int; let o = counterini(ini); ok = o >= 0; check ok; tel #+END_SRC Cet exemple est plus intéressant que le précédent en ce que le noeud ~top~ dispose désormais d'une entrée. Kind2 va donc essayer de vérifier que toutes les valeurs de la suite ~ok~ sont vraies et ce /pour toutes les suites d'entrée ~ini~/. Va-t-il réussir ? #+BEGIN_SRC shell $ kind2 ex0.lus kind2 v1.6.0 ==================================================================================================================== Analyzing top with First top: 'top' subsystems | concrete: counterini Property ok is invalid by bounded model checking for k=0 after 0.041s. Counterexample: Node top () == Inputs == ini -1 == Outputs == ok false == Locals == o -1 Node counterini (top[l14c7]) == Inputs == ini -1 == Outputs == o -1 -------------------------------------------------------------------------------------------------------------------- Summary of properties: -------------------------------------------------------------------------------------------------------------------- ok: invalid after 0 steps ==================================================================================================================== #+END_SRC La vérification a échoué, mais Kind2 nous a fourni un contre-exemple sous la forme d'une séquence d'entrées qui falsifie la propriété. Il suffit bien sûr de donner un ~ini~ strictement négatif au premier instant ! Notre propriété est donc fausse. Peut-on exprimer que le flot ~o~ est toujours vrai mais *à condition* que la première valeur de ~ini~ soit positive ? Oui, en utilisant l'opérateur booléen d'implication pour exprimer une /précondition/ (hypothèse) sur l'entrée ~ini~. (Remarque : l'implication dont il s'agit ici n'est que l'opérateur combinatoire sur les flots défini par ~x => y = not x or y~, rien de plus. En particulier, Kind2 n'a aucun traitement spécifique de cet opérateur.) Un premier essai pourrait ressembler à ce qui suit. #+BEGIN_SRC node top(ini : int) returns (ok : bool) var o : int; let o = counterini(ini); ok = ((ini >= 0) -> true) => (o >= 0); check ok; tel #+END_SRC La vérification échoue encore, avec le contre-exemple qui suit. #+BEGIN_VERBATIM Counterexample: Node top () == Inputs == ini -2 0 == Outputs == ok true false == Locals == o -2 -1 Node counterini (top[l19c7]) == Inputs == ini -2 0 == Outputs == o -2 -1 #+END_VERBATIM Comment comprendre ce contre-exemple ? Au premier instant, ~i~ vaut ~-2~ et la précondition sur ~ini~ est fausse, donc l'implication est vraie. Au deuxième instant, la précondition sur ini est vraie, donc l'implication prend la valeur de ~o >= 0~, qui se trouve fausse. Quel est le problème ? Ce que nous avions en tête n'est pas ce que nous avons écrit. On aurait voulu dire "si ~ini < 0~ au premier instant, la précondition est fausse pour toujours", mais on a écrit "si ~ini < 0~ au premier instant, la précondition est fausse /au premier instant/". On peut régler le problème en introduisant un noeud ~always~ dont la sortie devient fausse pour toujours dès que son entrée est fausse. #+BEGIN_SRC node always(b : bool) returns (o : bool) let o = (true -> pre o) and b; tel node top(ini : int) returns (ok : bool) var o : int; let o = counterini(ini); ok = always((ini >= 0) -> true) => (o >= 0); check ok; tel #+END_SRC La vérification réussit. En particulier, le contre-exemple précédent n'est plus valide. Si la valeur initiale de ~ini~ est ~-2~, la valeur de ~always((ini >= 0) -> true)~ sera toujours fausse, et donc la vérité de l'implication dépendra de ~o >= 0~, toujours vraie. Le fait d'exprimer une précondition sur les entrées est très fréquent, et Kind2 propose une syntaxe un peu plus agréable pour ce faire. #+BEGIN_SRC node top(ini : int) returns (ok : bool) var o : int; let o = counterini(ini); ok = o >= 0; check ok provided always((ini >= 0) -> true); tel #+END_SRC *** Comparaison de noeuds On peut utiliser le principe des observateurs synchrones pour comparer le comportement de deux noeuds, et éventuellement tester leur équivalence. Par exemple, comment quelle relation voyez vous entre notre premier noeud ~counter~ et le noeud ~counterini~ ? Et comment la feriez-vous vérifier par Kind2 ? Le lien est essentiellement qu'ajouter la première valeur de ~ini~ à la sortie de ~counter~ donne celle de ~counterini~. La tentative donnée ci-dessous est trop naïve puisqu'il ne faut prendre en compte ~ini~ uniquement au premier instant. #+BEGIN_SRC node compare(ini : int) returns (ok : bool) let ok = counter() + ini = counterini(ini); check ok; tel #+END_SRC On peut utiliser un noeud ~constant~ qui maintient la valeur reçue au premier instant. On obtient le noeud suivant, dont la propriété est vérifiée. #+BEGIN_SRC node constant(ini : int) returns (o : bool) let o = ini -> pre o; tel node compare(ini : int) returns (ok : bool) let ok = counter() + constant(ini) = counterini(ini); check ok; tel #+END_SRC *** Les contrats Les propriétés qu'on a vérifié jusqu'ici sont des propriétés globales du système. Il s'agit certainement d'une approche utile, mais elle n'est pas tout à fait convaincante du point de vue du génie logiciel. On aimerait plutôt vérifier chaque noeud indépendamment. Kind2 le permet via l'écriture de /contrats/ qui permettent à chaque noeud de documenter ses attentes vis-à-vis de ses appelants (mot-clef /assume/) et ses garanties (mot-clef /guarantee/). #+BEGIN_SRC node counterini(ini : int) returns (o : int) (*@contract assume (ini >= 0) -> true; guarantee o >= 0; *) let o = ini -> (pre o + 1); tel #+END_SRC Notez que Kind2 assure la bonne sémantique pour l'hypothèse (/assume/), c'est-à-dire qu'elle doit être valide de toute la séquence d'entrées, et ce sans avoir à utiliser une noeud comme ~always~. (Pour ceux et celles d'entre vous qui connaissent la logique temporelle, si $A$ est la formule booléenne des hypothèses et $G$ est la formule booléenne des garanties, la formule que l'outil cherche à démontrer est $\square A \Rightarrow \square G$ plutôt que $\square A \Rightarrow \square G$. Je finis cette partie pratique par une difficulté à laquelle tous les utilisateurs de vérification formelle finissent par se heurter un jour ou l'autre : des hypothèses trop fortes rendent la garantie triviale. Voir ci-dessous pour un exemple caricatural ; /garbage in, garbage out/. #+BEGIN_SRC node counterini(ini : int) returns (o : int) (*@contract assume false; guarantee (o = constant(o)); *) let o = ini -> (pre o + 1); tel #+END_SRC Cependant, Kind2 aide à détecter le problème. L'outil va chercher à vérifier que tout appelant à ce ~counterini~ satisfait aux hypothèses, ce qui ici est impossible... Sauf si l'appelant a lui-même fait des hypothèses contradictoires sur ses entrées, bien entendu ! * Cours 10 <2025-12-01> ** Vérification automatique, suite *** Exemples **** Compteurs On va s'intéresser à la vérification d'équivalence entre compteurs périodiques de 0 à 3, formulé avec des entiers, puis en codage binaire, classique puis de Gray. On commence par écrire le compteur sur deux bits avec un entier #+BEGIN_SRC node intcounter (rst : bool; const max : int) returns (out : bool); var t : int; let t = 0 -> if rst or pre t = max then 0 else pre t + 1; out = t = 3; tel node graycounter (rst : bool) returns (out : bool); var a, b : bool; let a = false -> (not rst and not pre b); b = false -> (not rst and pre a); out = not a and b; tel node bincounter (rst : bool) returns (out : bool); var a, b : bool; let a = false -> (not rst and (pre a <> pre b)); b = false -> (not rst and not pre b); out = a and b; tel node top (rst : bool) returns (); var grayc, binc, intc : bool; let grayc = graycounter(rst); intc = intcounter(rst, 3); binc = bincounter(rst); check binc = intc; check grayc = intc; tel #+END_SRC *** Les bases de l'algorithmique de la vérification Les données du problème sont : 1. un programme synchrone à vérifier, 2. un /observateur/ pour la propriété à démontrer (~check ok~), 3. un /observateur/ pour l'hypothèse supposée (~assert hyp~). L'objectif d'un vérificateur de modèle pour un programme synchrone à flots de données est de démontrer : ~always(so_far(hyp) => ok)~. Notons qu'on ne traite que les propriétés de sûreté (``quelque-chose de mauvais n'arrive toujours'') et pas de vivacité (``quelque-chose de bon finit toujours par arriver''), comme expliqué au cours précédent. On va s'intéresser à ce problème dans le cas *purement booléen*, c'est-à-dire où toutes les variables manipulées sont des suites de booléens. Notre description est basée sur le rapport de recherche de Pascal Raymond disponible à [[https://www.di.ens.fr/~pouzet/cours/mpri/bib/lesar-rapport.pdf][cette adresse]]. Si $X$ est un ensemble, on écrit $\overline{X}$ pour les fonctions de $X$ dans $\mathbb{B}$, qui sont en bijection avec les parties de $X$. On identifiera librement les sous-ensembles et leurs fonctions charactéristiques dans ce qui suit. Les données du problème sont les n-uplets ($V$, $S$, $I \subseteq \overline{S}$, $g : \overline{S} \times \overline{V} \to \overline{S}$, $H \subseteq \overline{S} \times \overline{V}$, $\Phi \overline{S} \times \overline{V}$), où : - $S$ et $V$ sont des ensembles *finis* dont les éléments sont respectivement les variables d'état de d'entrée du programme, - $I$ est l'ensemble des états initiaux, - $H$ est l'hypothèse, - $\Phi$ est la propriété à démontrer. On écrira $q \to^v q'$ pour $q' = g(q, v)$ avec $q,q' \in \overline{S}$ et $v \in \overline{V}$. On définit les états successeur/prédécesseurs d'un état $q$ ou d'un ensemble d'états~$X$ par : \begin{align*} post_H(q) & = \{ q' \mid \exists v \in q \to_v q' \wedge H(q, v) \} \\ pre_H(q) & = \{ q' \mid \exists v \in q' \to_v q \wedge H(q', v) \} \\ POST_H(X) & = \bigcup_{q \in X} post_H(q) \\ PRE_H(X) & = \bigcup_{q \in X} pre_H(q) \end{align*} L'ensemble des états d'erreurs immédiate sont ceux qui satisfont l'hypothèse mais pas la propriété à démontrer. \[ Err = \{ q \mid \exists v, H(q, v) \wedge \neg \Phi(q, v) \} \] On définit maintenant l'ensemble $Acc$ des états accessibles du programme et l'ensemble $Bad$ des mauvais états par un plus petit point fixe ensembliste : $\mu X . F(X)$ désigne le plus petit ensemble $Y$ tel que $F(Y) \subseteq Y$ ; son existence est garantie dès lors que $F$ est croissante pour l'inclusion. \begin{align*} Acc & = \mu X. (I \cup POST_H(X)) \\ Err & = \{ q \mid \exists v, H(q, v) \wedge \neg \Phi(q, v) \} \\ Bad & = \mu X . (Err \cup PRE_H(X)) \end{align*} L'objectif est maintenant de démontrer que le système est *sûr*, c'est-à-dire que $Acc \cap Bad = \emptyset$. Autrement dit, aucun état accessible du système n'est un état d'erreur. Pour ce faire, il existe deux grandes méthodes : - l'exploration en *avant* : on démontre $Acc \cap Err = \emptyset$, - l'exploration en *arrière* : on démontre $Bad \cap I = \emptyset$. L'approche la plus simple pour ce faire est une approche énumérative : on explore explicitement l'automate induit par le programme, en imitant le calcul du plus petit point fixe correspondant à $Acc$ ou $Bad$. #+BEGIN_SRC Known := I; Explored := {} while there is q in Known \ Explored: for all q' in post(q): if q' in Err: return FAILURE move q' to Known move q to Explored } return SUCCESS #+END_SRC Cet algorithme peut être implémenté et termine puisque tous les ensembles manipules sont finis, les prédicats calculables, tout comme la fonction de transition du programme. En particulier, vous pouvez implémenter les ensembles ~Known~ et ~Explored~ par votre structure d'ensemble fini favorite, et énumérer les valeurs possibles pour calculer ~post(q)~. Il s'agit donc en somme d'exécuter le programme sur toutes les entrées possibles ; on voit que c'est très inefficace. On peut aussi implémenter une version en arrière. #+BEGIN_SRC Known := Err; Explored := {} while there is q in Known \ Explored: for all q' in pre(q): if q' in I: return FAILURE move q' to Known move q to Explored } return SUCCESS #+END_SRC Les deux algorithmes sont très inefficaces, tellement qu'ils en deviennent inutilisables en pratique. En effet, les structures de données représentant les ensembles d'état ou d'entrées deviendront très grosses, et les calculs attenants (différence ensembliste, ajout, choix d'un élément...) coûteux à réaliser. Notons que le second algorithme est encore moins efficace que le premier. Voyez-vous pourquoi ? Le calcul de ~pre(q)~ est encore plus coûteux, puisqu'il faut calculer l'image inverse de la fonction de transition $g$, c'est-à-dire trouver l'ensemble des $q'$ tel que $g(q', v) = q$ pour $v$ et $q$ fixés. Depuis les années 1990, on utilise plutôt des méthodes dites *symboliques*. L'idée générale est de représenter les ensembles finis par des formules logiques plutôt que par des énumérations explicites. Par exemple, on pourrait représenter l'ensemble $\{ (x, y, z) \mid x \overline{y} + z = 1 \}$ directement par le *code* de sa fonction caractéristique $f(x, y, z) = x \overline{y} + z$ plutôt qu'explicitement par l'ensemble de triplets $\{ (1, 0, 0), (1, 0, 1), (0, 0, 1), (0, 1, 1), (1, 1, 1) \}$. Les méthodes symboliques sont donc un exemple de compromis temps-espace : on y gagne une représentation nettement plus succincte des données que la représentation explicite, en contrepartie de quoi les opérations (notamment test d'égalité, du vide, d'inclusion, etc.) seront plus coûteuses. Il existe deux grandes méthodes d'implémentation pour exprimer les opérations et les tests : 1. On peut représenter les formules directement par leur code et utiliser un solveur SAT général pour répondre aux questions intéressantes pour la vérification. Par exemple, l'ensemble $\{ \vec{x} \mid \phi(\vec{x}) \}$ est inclus dans l'ensemble $\{ vec{x} \mid \psi(\vec{x}) \}$ si et seulement si $\forall \vec{x}, \phi(\vec{x}) \implies \psi(\vec{x})$, question à laquelle un solveur SAT peut répondre, y compris pour de très grosses formules $\phi$ et $\psi$. D'autres questions, comme par exemple l'énumération des valeurs appartenant à un ensemble, sont d'un traitement moins direct mais peuvent être gérée avec un peu de réflexion et d'effort. 2. On peut utiliser une représentation canonique des formules booléennes, par exemple les /diagrammes de décision binaire/ (ou /binary decision diagrams/ en anglais, BDD). Ici, toutes les formules équivalentes sont représentées par la même structure de données. La construction de cette représentation est donc forcément coûteuse, mais une fois construite on peut l'utiliser pour répondre efficaement à beaucoup de questions. C'est cette approche qui est très bien exposée dans le rapport de P. Raymond cité plus haut. Le principe des diagrammes de décision binaire a été brièvement expliqué en cours mais ne sera pas détaillé dans ces notes.