Compte rendu: Kick off meeting ARC Concert, le 3 février 2003

Liste des participants

Exposés

  1. Yves Bertot : Un mini compilateur certifié, Les sources Coq de la preuve décrite sont également joints au serveur CVS de l'action dans le répertoire nommé littlecomp.
  2. Xavier Leroy : formation accélérée en compilation
  3. Catherine Dubois : présentation des résultats connus sur la Compilation de Confiance

Discussions

Choisir un langage intermédiaire à certifier

C complet (?) uhm... maybe too much!

C moins quelque chose? qu'est ce que on pourrait enlever et rester un C *réaliste*? C'est quoi la notion de réaliste? Est-il réaliste un ``C-bof'' tel quel je pourrait l'utiliser comme back-end pour un compilateur d'un langage à haut niveau à la Bigloo, Caml?

Le C-prime de Chez Dassault Aviation : pas d'allocation dynamique, pointeurs sans algèbre et pas sur de fonctions, pas de variables locales: il à été conçu comme langage intermédiaire pour la conception de compilateurs pour des langages ad-hoc.

La volonté de travailler sur un angage proche de la machine est-elle une obsession ou correspond-elle à une réalité industrielle?

Allocation dynamique de mémoire: à première vue on n'a pas forcement en besoin, car elle complique la formalisation et la certification, on pourra en revanche l'ajouter/certifier après.

Le cas CAML: dans la génération de code intermédiaire XL&co passent pour un dialecte de C qu'on pourrait appeler C-- avec des mécanisme de gestion d'exceptions et qui interface un GC

ATTENTION Un autre sous ensemble de C avec le même nom existe déjà: il s 'agit de C-- de Peyton Jones, voir www.cminusminus.org le papier que l'on conseille de lire est l'article d'introduction de S. Peyton-Jones, Norman ramsey et Fermin Reig

A propos, le nom d'action "concert" n'est pas peut-être pas si bien chosi, car il existe un projet de recherche à CMU avec un nom et un objectif apparentés: Certified code for grid computing, voir l'article introductif.

Le cas BIGLOO: le code intermédiaire généré (juste avant la génération du C qui sera après compile par gcc), reste du scheme-like dopé avec des types et copieusement optimisée et manipulée. Le code C généré semble être C ``in toto'', c.à.d. avec setjmp et longjmp.

Formalisations existantes

Formalisations de C en HOL par Norrish. Dans le document il y a beaucoup des complications inutiles. Norrish a tenté de formaliser ANSI-C, c.à.d. le C qui notamment a un comportement non-spécifié dans l'ordre d'évaluation des expressions: cela à été fait essentiellement pour être ``compliant'' w.r.t. toutes les possibles implémentations réelles de C.

- About Norrish: juste pour vous donner un goût de la démarche à la Norrish w.r.t. ce qu'on peut trouver dans la définition ANSI-C: (c'est bien ps2ascii :-)

1.5.1 C terminology The C community tends to use a language of its own to describe notions relating to its language's semantics. Here we introduce some of the more important terms (c.f. the glossary in [ANS89,1.6]). Firstly there are three distinct ways in which the standard under-specifies execution of C programs. We explaine a ch and describe in general how they are modelled in the formal semantics.

Remarque de Luigi Liquori: Est-ce que le système de types de C buggé? Bonne question: j'ai toujours pensé que oui, mais enfin Norrish + le premières pages de Type Systems de L. Cardelli me font plutôt penncher vers le fait que le système de types de C ne respecte tout simplement pas le slogan de Milner ``well typed programs dont go wrong'', et que la choix des erreurs ``trapped'' et ``untrapped'' est diffèrent w.r.t celle qu'on pourrait avoir dans système de type plus exigeants.

Quelques questions ouvertes