PhD of Paul Jeanmaire

Paul Jeanmaire developed a functional semantics for the dataflow core of Vélus. This work is described in his PhD dissertation (in French).

The slides of the defense are available.

Références au développement Coq, par section

Les conventions de nommage diffèrent parfois entre la thèse et le code source. Les liens donnés ici se réfèrent aux noms imprimés dans la thèse (les noms du code sont mis entre parenthèses).

Le développement complet est disponible ici.

2.1.4 Le langage d’entrée, syntaxe et typage

• On définit un sous-ensemble de la syntaxe complète de Vélus à l'aide des prédicats suivants:

  • restr_exp: expressions
  • restr_block: équations
  • restr_node: nœuds
  • restr_global: programmes

• Les opérateurs arithmétiques et logiques, hérités de CompCert.

• Le type des horloges

• Les règles de typage

• Les règles de typage des horloges

2.1.5 Sémantique synchrone relationnelle

• value : le type abstrait des valeurs, et son instance dans CompCert
• svalue : le type des valeurs synchrones
• LSemantics : les règles de la sémantique relationnelle
• sem_node : la sémantique d'un nœud, et la fonction base-of (clocks_of)
• sem_equation : la sémantique d'une équation
• Sconst : la sémantique d'une constante, et la fonction const
• Sbinop : la sémantique d'une opération binaire, la fonction lift2 et la fonction sem_binop
• fby/fby1 : les prédicats relationnels du délai initialisé

2.1.7 Correction de la compilation

• behavior_asm : correction de la compilation
• det_global : déterminisme de la sémantique relationnelle

2.2.2 Modèle synchrone à types dépendants

Importé de Boulmé et Hamon, adapté à la nouvelle syntaxe de Coq par Chantal Keller.

• Str (samplStr) : le type des flots cadencés
• sp_when : l'opérateur d'échantillonnage
• rec1 : l'opérateur de point fixe

3.1 La bibliothèque CPO et nos extensions

Importé de C. Paulin-Mohring.

Définitions génériques

• ord : type ordonné
• monotonic : fonctions monotones
• cpo : CPO
• continuous : fonctions continues
• FIXP : opérateur de point fixe, lui-même fonction continue

Définitions de flots

• Steam_ε (DStr) : le type des flots
• DS_bot : le flot vide (Eps pour toujours)
• DS : le CPO des flots finis et infinis
• infinite : la propriété d'infinitude
• REM : la primitive tl
• MAP : la primitive map définie comme un point fixe
• APP : le fby en sémantique de Kahn
• first, filter, zip, take

Principes de preuve

• bi-simulation
• le take-lemma
• le principe de préfixe infini
• le principe d'induction de Scott
• l'expression des propriétés de sûreté

3.2.1 Flots avec erreurs

• sevalue (sampl) : le type des valeurs synchrones possiblement erronées

3.2.2 propriétés et conversions

• val_val (sval_of_sampl) : conversion des valeurs
• S_of_Se : conversion d'un flot de Kahn en flot de Coq
• Se_of_S : conversion inverse
• safe (safe_DS) : un flot sans erreurs
• ⌈·⌉ (S_of_DSv) : conversion des flots
• ⌊·⌋ (ea) : effacement des absences

3.3 Sémantique des opérateurs de flots

Constantes

• const : constantes dans Vélus
• sconst : flot constant dénotationnel
• ok_const : lemme de correspondance

Opérateurs unaires

• lift1 : règle relationnelle
• sunop : opérateur dénotationnel
• lemme 3.1 (ok_unop) : lemme de correspondance
• lemme 3.2 (erase_unop) : effacement des absences

Opérateurs binaires

• lift2 : règle relationnelle
• sbinop : opérateur dénotationnel
• lemme 3.3 (ok_binop) : lemme de correspondance
• lemme 3.4 (erase_sbinop) : effacement des absences

Délai initialisé

• fby : règle relationnelle
• fby : opérateur dénotationnel
• lemme 3.5 (ok_fby) : lemme de correspondance
• lemme 3.6 (erase_fby) : effacement des absences

Échantillonnage

• when : règle relationnelle
• swhen : opérateur dénotationnel
• lemme 3.7 (ok_when) : lemme de correspondance
• merge : règle relationnelle
• smerge : opérateur dénotationnel
• lemme 3.8 (ok_merge) : lemme de correspondance

Conditionnelle

• case : règle relationnelle
• scase : opérateur dénotationnel
• lemme 3.9 (ok_case) : lemme de correspondance

3.4 Réinitialisation modulaire

• mask : l'opérateur relationnel de masquage
• Sapp : la règle de la sémantique relationnelle pour les instances réinitialisées
• reset : caractérisation du reset à la Lucid Synchrone
• merge : un merge adapté à la récursion instantanée
• sreset : caractérisation du reset dénotationnel
• lemme 3.14 (smask_sreset) : correspondance du reset dénotationnel et relationnel
• lemme 3.15 (reset_match) : correspondance des deux caractérisations

3.5 Interprétation et composition

• SEnv (DS_prod SI) : le type des environnements de flots
• FEnv (Dprodi FI) : le type des environnements de fonctions de flots
• denotN (denot_node) : la dénotation d'un nœud
• denotG (denot_global) : la dénotation d'un programme
• denotE (denot_exp_eq) : la dénotation des expressions
• lemme 3.16 : correction de la dénotation des expressions
• théorème 3.17 : correction de la dénotation des nœuds

4.1 Infinitude des flots et causalité

• théorème 4.1 : principe d'induction causale
• théorème 4.2 : condition d'infinitude
• propriétés 4.1 : productivité des opérateurs synchrones
• propriété 4.2 (is_ncons_S_fby) : productivité du délai
• lemme 4.3 (exp_n)
• lemme 4.4 (exp_S)
• lemme 4.5 (denot_S)
• lemme 4.6 (denot_n)
• théorème 4.7 (denot_inf)

4.2 Commutativité du préfixe

• propriété 4.8 : premier point
• propriétés 4.3 : commutativité du préfixe avec les opérateurs synchrones
• lemme 4.11 : expressions
• lemme 4.12 : nœuds
• théorème 4.13 : correction

4.3 Indépendance à l'absence initiale

• théorème 4.14 : correction

4.4 Sûreté du typage

• définition 4.1, clock-of (AC) : horloge abstraite (booléenne) d'un flot
• définition 4.2, base-of (bss) : flot d'horloge de base
• définition 4.3, denotC (denot_clock) : interprétation d'une annotation d'horloge
• wt_value
• figure 4.1 : typage des constantes, opérations unaires, opérations binaires, etc.
• figure 4.2 : typage des horloges des constantes, opérations unaires, opérations binaires, échantillonnages, etc.
• définition 4.4 (wf_env) : environnements bien formés
• lemme 4.15 : sûreté de la réinitialisation
• no-rte-exp, no-rte-node, no-run-time-errors.
• théorème 4.16 : sûreté du typage

5.1 Correction du compilateur

• behavior_asm : correction de la compilation, avant
• behavior_asm_new : correction de la compilation, après

5.2 Détection statique des erreurs à l’exécution

• check_unop : classification des opérateurs unaires de CompCert
• check_binop : classification des opérateurs binaires de CompCert
• check_exp : la procédure check-ops pour les expressions
• théorème 5.1 (check_global_ok) : correction de la procédure
• behavior_asm_new_check : correction de la compilation avec heuristique