Journal Xavier Leroy est le lauréat 2016 du Prix Milner.

Posté par . Licence CC by-sa
52
25
nov.
2016

Hier, jeudi 24 novembre 2016, Xavier Leroy a reçu le prix Milner à Londres à la Royal Society. Le prix Milner est le plus grand prix européen en informatique; il est décerné conjointement par la Royal Society, l'Académie des Sciences et l'académie allemande Leopoldina. Il est décerné en l'honneur de l'informaticien britannique Robin Milner qui fut lauréat du Prix Turing en 1992.

Le prix revient cette année à Xavier Leroy pour ses travaux tant théoriques que pratiques sur la fiabilité des systèmes informatiques. Xavier Leroy est directeur de recherche à l'INRIA et il y dirige l'équipe Gallium. Il est à l'origine du langage OCaml ainsi que du compilateur C certifié CompCert. Ce dernier est un compilateur C écrit en Coq et « garanti sans bugs ». Pour reprendre la présentation qu'en donne Gérard Berry dans le bulletin de la Société Informatique de France :

Un tel développement est une course de haies : il faut d’abord choisir un sous-ensemble approprié de C, qui est loin d’être un langage bien défini. Le sous-ensemble C-light que compile CompCert correspond bien aux besoins du logiciel industriel embarqué dans les systèmes physiques. Il faut ensuite choisir des sous-ensembles des langages machine des processeurs (Intel, Motorola, Mips, etc.) qui soient également formellement définissables. Une fois ces sous-ensembles choisis, il faut définir leur sémantique mathématique de façon appropriée et directement implémentable dans un assistant de vérification. Enfin, il faut démontrer un théorème du type « pour tout programme P écrit en C et toute machine cible M, si CompCert produit un code machine PM pour M à partir de P, alors exécuter PM sur M donne pour toute entrée le même résultat qu’exécuter P dans la sémantique de C ».

(NdM. : la dernière phrase de cette citation comprend une coquille à la source au moment de la rédaction du journal, corrigée ici, la dernière occurrence de P étant par erreur un M à la source)

Autrement dit, le compilateur n'introduit pas de bugs en traduisant le code C en langage machine. S'il y a un bug dans le programme compilé, alors il se trouve dans le code C et non dans le compilateur.

La remise du prix a eu lieu hier et la vidéo de la cérémonie est disponible sur le site de la Royal Society.

Pour conclure sur une note de chauvinisme, chantons le cri du Coq : Cocorico !

  • # Clight

    Posté par (page perso) . Évalué à 6.

    Peut-on en savoir plus rapidement sur le Clight ? Quels sont les éléments du C qui en sont exclus ?

    • [^] # Re: Clight

      Posté par . Évalué à 8.

      Je ne sais pas trop, je ne suis que le messager et je ne connais pas les entrailles du système. Sur le site du projet, à la page consacrée à son fonctionnement, on peut y lire :

      The subset of C supported

      CompCert C supports all of ISO C 99, with the following exceptions:

      • switch statements must be structured as in MISRA-C; unstructured "switch", as in Duff's device, is not supported.
      • longjmp and setjmp are not guaranteed to work.
      • Variable-length array types are not supported.

      Consequently, CompCert supports all of the MISRA-C 2004 subset of C, plus many features excluded by MISRA (such as recursive functions and dynamic heap memory allocation).

      Several extensions to ISO C 99 are supported:

      • The _Alignof operator and the _Alignas attribute from ISO C2011.
      • Pragmas and attributes to control alignment and section placement of global variables.

      Je pense que cela parlera plus aux développeurs C qu'à moi-même. Et pour l'architecture, on trouve ce schéma :

      compcert

      De ce que j'ai compris, la certification commence après la traduction en Clight.

      Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

      • [^] # Re: Clight

        Posté par (page perso) . Évalué à 4.

        Merci. Pour ajouter à cette réponse, ce papier décrit le Clight. On y comprend que toutes les structures de contrôle du C sauf le goto existent en Clight. Pour le reste c'est trop compliqué pour une lecture entre deux copies.

        • [^] # Re: Clight

          Posté par (page perso) . Évalué à 2.

          Et citons l'argument -dcmm de ocamlopt qui génère une sorte de Clight, mais dans une syntaxe Lisp.

          « Il n’y a pas de choix démocratiques contre les Traités européens » - Jean-Claude Junker

      • [^] # Re: Clight

        Posté par (page perso) . Évalué à 4.

        En regardant la liste, visiblement la couverture du langage C est vraiment bonne. Le "unstructured switch" est plus un défaut de spécification C car peu utilisé en pratique et difficile à comprendre. En embarqué micro-contrôleur il existe cependant un cas d'usage.
        longjmp / setjmp sont peu utilisé aussi sauf pour du très bas-niveau et les Variable-length array peuvent aussi une spécificité du C99 (utile mais contournable facilement).

  • # prix Microsoft

    Posté par (page perso) . Évalué à 3.

    Bravo à Xavier Leroy qui est un grand monsieur de l'informatique.

    Rappelons tout de même que ce prix s'appelait auparavant « Microsoft Award » jusque 2009 et qu'il est toujours supporté par Microsoft Research. Cela biaise sans doute le fait que cela puisse être un vrai grand prix académique, puisqu'il est lié à une entreprise en particulier.

  • # Verified toolchain

    Posté par (page perso) . Évalué à 9.

    A noter que CompCert est utilisé comme base de nombreux autres projets de recherche/industriels, notamment le projet Verified Toolchain (qui fait parti du projet plus grand DeepSpec) qui vise à avoir la maîtrise complète de chaîne de compilation : http://vst.cs.princeton.edu/

    DeepSpec vise à atteindre la même maîtrise, mais sur un écosystème entier : http://deepspec.org/

    Ca passe par un noyau et un OS formellement vérifiés (CertikOS), et d'autres choses.

    Mes messages engagent qui je veux.

    • [^] # Re: Verified toolchain

      Posté par . Évalué à -3.

      DeepSpec vise à atteindre la même maîtrise, mais sur un écosystème entier : http://deepspec.org/

      Ca passe par un noyau et un OS formellement vérifiés (CertikOS), et d'autres choses.

      Intéressant ! Je cite les deux premières lignes de la page d'accueil du site deepspec.org :

      DeepSpec is an Expedition in Computing funded by the National Science Foundation.
      We focus on the specification and verification of full functional correctness of software and hardware.

      Ainsi, donc, DeepSpect viserait à produire les spécifications et vérifications formelles d'une architecture matérielle ?

      A ce stade, ce n'est pas leur objectif, si j'en crois la page titrée « Research Overview » (accessible depuis le menu Research puis Overview). D'après mon analyse rapide, il ne s'agit que de spécification formelle du jeu d'instruction x86 pour avoir une preuve formelle du théorème cité dans le présent journal concernant les cibles x86, c'est à dire pour valider la justesse du code binaire produit par le compilateur CompCert sur l'architecture x86. Je cite le passage où l'on retrouve les deux seules occurrences de "hardware" de cette page de présentation :

      The correctness of CompCert's translation is proved in Coq. Finally, the hardware is correct: the instruction set architecture x86-ISA is specified in the Bluespec hardware-description language, which itself has a deep specification defining its precise semantics. The Kami synthesizer translates this to register transfers written in Verilog (which, again, itself has a deep specification).

      En voici une traduction personnelle :

      L'exactitude de la traduction de CompCert est prouvée en Coq. Enfin, le matériel est exact : l'architecture x86-ISA du jeu d'instruction est spécifiée dans le langage de description matérielle Bluespec qui lui-même a une spécification approfondie définissant sa sémantique précise. Le synthétiseur Kami traduit cela en des transferts de registre écrits en Verilog (qui, à nouveau, a lui-même une spécification approfondie).

      • [^] # Re: Verified toolchain

        Posté par . Évalué à -6.

        Je rappelle que la preuve formelle de code pour la conception matérielle est un atout important dans la production de matériel libre :

        Je me cite :

        la libération [des spécifications matérielles] amènera la capacité d'audit communautaire et la capacité de répliquer l'expérience en produisant des versions alternatives et dérivées, or la diversité importe pour des raisons de sécurité.

        Notons que dans ces conditions, des failles de sécurité dans la conception sont plus facilement identifiables par des groupes malveillants qui garderaient pour eux leurs découvertes, de manière à les exploiter dans le secret. Cette question aura vocation a être traitée par de la preuve formelle de programme couvrant la plus grande surface possible du code (l'architecture des portes logiques peut être considérée comme étant du code).

        [source]

        Plus loin, dans le même fil de discussion, j'abordais le problème associé du coût de la preuve formelle :

        si le coût de conception pourrait être réduit du fait de l'activité pour partie bénévole et s'appuyant sur un existant déjà sous licence libre, par contre l'investissement intellectuel devrait être plus important que l'usage courant, pour tendre à produire un cadre de preuves formelles de code. Ensuite, le coût lié à la supervision de la production et pour partie de la distribution (je ne rentre pas dans le détail) est nouveau par rapport aux usages et représente un coût.

        [source]

  • # Nuance

    Posté par . Évalué à 6.

    Bravo à Mr. Leroy pour ce prix amplement mérité.

    Petite nuance cependant concernant CompCert, puisque le journal laisse entendre qu'il serait infaillible. CompCert n'est infaillible que si l'on suppose ses spécifications correctes, mais rien n'indique que les spécifications sont complètes et réalistes. On retombe un peu sur l'idée que les approches formelles supposent souvent un monde qui n'est pas la réalité. Ces dernières années, différents bugs ont été trouvés dans CompCert par test aléatoire (PLDI'11, ISSTA'15, peut-être d'autres, je ne suis pas expert), vraisemblablement causés par des "trous" dans la spécification.

    Loin de moi l'idée de remettre en cause l'outil génial qu'est CompCert cependant, juste une nuance :)

    • [^] # Re: Nuance

      Posté par . Évalué à 5.

      Ces dernières années, différents bugs ont été trouvés dans CompCert par test aléatoire (PLDI'11, ISSTA'15, peut-être d'autres, je ne suis pas expert), vraisemblablement causés par des "trous" dans la spécification.

      Effectivement, mais cela a été corrigé. Je ne suis pas rentré dans les détails dans le journal, mais Gérard Berry en parle dans sa présentation dont le lien est dans le journal (il y parle aussi du projet deepspec) :

      L’importance de CompCert devient claire quand on regarde d’autres projets comme l’outil Csmith développé à l’université d’Utah, qui, à l’aide de techniques de génération aléatoire, a permis d’engendrer automatiquement un million de programmes C destinés à casser les compilateurs. Le résultat a été étonnant : Csmith a permis de détecter des centaines de bugs dans les principaux compilateurs C, mais aucun dans CompCert (en fait deux au début, mais pas dans les parties bien définies de C, et ces bugs ont ensuite été corrigés).

      En ce qui concerne les approches formelles :

      On retombe un peu sur l'idée que les approches formelles supposent souvent un monde qui n'est pas la réalité.

      Cette remarque s'applique inéluctablement à la conception de matériel qui repose sur des théories physiques qui sont une modélisation de la réalité. Comment prouver que le modèle « correspond » au réel ? Et d'ailleurs quel sens pourrait bien avoir une telle question ?

      Pour ce qui est de la formalisation de processus de calcul, ce n'est pas le cas. Mais on peut tomber sur d'autres problématiques ironiquement bien formulées dans cet article :

      1973 - Robin Milner creates ML, a language based on the M&M type theory. ML begets SML which has a formally specified semantics. When asked for a formal semantics of the formal semantics Milner's head explodes.

      Robin Milner est un des pères fondateurs de la discipline dans laquelle travaille Xavier Leroy : la preuve mathématique assistée par ordinateur. Le langage OCaml est un langage de la famille ML, et tous les langages de cette famille (avec SML, OCaml, Haskell, Coq, Idris…) sont tous fondés sur la correspondance de Curry-Howard ou correspondance preuve-programme : un programme est une preuve d'un théorème mathématique et son type est l'énoncé du théorème.

      Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

    • [^] # Re: Nuance

      Posté par . Évalué à 8.

      Tu mélanges un peu deux choses différentes: une spécification peut être différente de la réalité, et aussi il y a des parties d'un programme à qui on ne sait pas forcément donner de spécification. Les erreurs trouvées par Csmith¹ sont dans des parties du logiciel qui n'avaient pas de spécification formelle (par exemple l'affichage de code assembleur, depuis la représentation interne du compilateur à un fichier texte à passer à un outil externe), et pas dans des erreurs d'une spécification qui les couvrirait. (Je chipote; mais on ne peut pas vraiment parler de gap spécification/réalité ici.)

      ¹: Csmith c'est ce que tu appelles "PLDI'11"; je ne suis pas convaincu par cette façon de nommer des articles qui tait l'important (le titre et les auteurs—et l'année) et montre la conférence, peu importante et source de vanité.

      Les "erreurs" citées par l'article "Randomized Stress-Testing of Link-Time Optimizers" de Vu Le, Chengnian Sun et Zhendong Su me semblent extrêmement suspectes, pour ne pas dire foireuses. Il faut réfléchir à ça plus en détail mais je ne crois pas qu'il soit correct de dire que ce sont des bugs de Compcert. Dans un cas, c'est un comportement qui n'est pas défini selon la norme C, mais qui est défini par la spécification "Compcert C" qui est plus fine; ce n'est pas un bug, mais une différence d'interprétation. Le second "bug" concerne un comportement de l'interpréteur, pas du compilateur, et il s'agit d'un message d'erreur oublié pour une façon particulière de rejeter le programme sans l'exécuter—donc il n'y a même pas eu d'interprétation incorrecte. Dans le cas du premier soit-disant bug en tout cas, j'ai l'impression que les auteurs n'ont pas compris les garanties données par Compcert.

      • [^] # Re: Nuance

        Posté par (page perso) . Évalué à 2.

        Il me semble qu'il n'y a pas si longtemps il avait été question d'un petit bug dans la sémantique de C de CompCert, quelque chose qui avait avoir avec les pointeurs. Je sais, c'est pas très précis, mais je n'y avais pas prêté beaucoup d'attention, donc c'est tout ce que j'ai retenu :)

        En tous cas, c'est sûr que la surface où peuvent se trouver des bugs par rapport à un compilateur normal est minime.

      • [^] # Re: Nuance

        Posté par . Évalué à 1.

        Concernant le premier paragraphe, je ne cherche pas à dire que les spécifications de CompCert sont fausses, seulement qu'on ne peut pas savoir si elles sont complètes et réalistes. Pour citer Xavier Leroy (source):

        Csmith has many uses for CompCert, ranging from validating the formal C semantics to finding missing cases and “assertion failed” in the compiler.

        Concernant le deuxième paragraphe:

        Les "erreurs" citées par l'article "Randomized Stress-Testing of Link-Time Optimizers" de Vu Le, Chengnian Sun et Zhendong Su me semblent extrêmement suspectes, pour ne pas dire foireuses.

        Je ne suis pas suffisamment expert pour juger de la validité des bugs ou non. En revanche, ils précisent bien que les auteurs de CompCert eux-mêmes ont reconnu la validité de ces bugs (qui ont j'imagine été corrigés depuis).

        Csmith c'est ce que tu appelles "PLDI'11"; je ne suis pas convaincu par cette façon de nommer des articles qui tait l'important (le titre et les auteurs—et l'année) et montre la conférence, peu importante et source de vanité.

        Juste pour donner mon point de vue: je considère au contraire que la conférence/journal (ainsi que l'année, incluse dans cette notation) est bien l'une, si ce n'est la plus importante, des informations à donner—à l'inverse de la liste des auteurs qui est bien elle l'information la moins importante. J'aurais du citer le titre en revanche.

        • [^] # Re: Nuance

          Posté par . Évalué à 3.

          Les erreurs semblent bien avoir été corrigées. Au moins pour celle sur la signature du la fonction main d'après le manuel datant du 30 juin 2016 :

          The following limitations apply to the C source files that can be interpreted.

          1. […]
          2. […]
          3. The main function must be declared with one of the two types allowed by the C standards, namely:
          int main(void) { ... }
          int main(int argc, char ** argv) { ... }
          

          Par contre, je ne comprends pas ce que tu entends par réaliste lorsque tu dis : « je ne cherche pas à dire que les spécifications de CompCert sont fausses, seulement qu'on ne peut pas savoir si elles sont complètes et réalistes ». Que l'on se demande si les spécifications d'un langage sont correctes et complètes (ou plutôt leur formalisation dans un autre langage), je peux le comprendre (et il n'est pas possible de le prouver formellement non plus, la question ne portant pas sur la forme mais sur la matière ou le contenu). Mais se demander si elles sont réalistes n'a aucun sens.

          Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

        • [^] # Re: Nuance

          Posté par . Évalué à 6.

          je ne cherche pas à dire que les spécifications de CompCert sont fausses, seulement qu'on ne peut pas savoir si elles sont complètes et réalistes

          Comme le souligne kantien, il n'est pas clair de savoir ce que tu veux dire par "complètes et réalistes". J'aimerais expliquer pourquoi je me permets de chipoter ici. On a peu de logiciels vérifiés formellement, Compcert est un des premiers qu'on puisse envisager d'utiliser à grande échelle (parce que bon tout le monde n'a pas de raison de faire tourner SeL4 ou CertiKOS sur sa machine, alors qu'un compilateur C si), donc c'est le bon moment de bien comprendre et bien expliquer les garanties (non absolues, bien sûr) données par la vérification formelle. Au grand public, on peut se permettre des approximations et simplifications—encore que. Mais toi tu sembles assez proche du milieu de la recherche pour avoir un avis (foireux) sur comment citer les articles, alors je pense que ça vaut le coup de pousser la discussion un peu plus loin et de te demander d'être précis dans la critique que tu as en tête.

          Je ne suis pas suffisamment expert pour juger de la validité des bugs ou non. En revanche, ils précisent bien que les auteurs de CompCert eux-mêmes ont reconnu la validité de ces bugs (qui ont j'imagine été corrigés depuis).

          J'aimerais mieux qu'on discute de la question technique sous-jacente (les soi-disant bugs; tu peux essayer de te renseigner mieux, puisque le sujet t'intéresse; moi je me suis renseigné en lisant l'article et j'ai donné mon avis), plutôt que de discuter de on-dit. On n'a pas la réponse précise des auteurs de Compcert, le fait que les auteurs d'un article (qui, même de bonne foi, ont tout intérêt à gonfler l'importance des remarques qu'ils ont fait sur Compcert) disent vaguement "les auteurs sont d'accord" ne veut pas dire grand chose—par exemple si j'étais un auteur poli, ma réponse sur le premier "bug" rapporté serait quelque chose comme "merci beaucoup pour ce retour, je vais effectivement corriger ça, en testant plus strictement les accès aux sous-objets je peux rendre l'interpréteur plus utile", ce qui ne veut pas dire qu'un bug a été trouvé dans Compcert, mais peut être présenté par les auteurs de l'article comme "les auteurs de CompCert sont d'accord et d'ailleurs ont corrigé"—ce qui est faux si on interprète comme tu le fais "sont d'accord" comme "reconnaissent un bug dans Compcert". On est dans l'hypothétique là, et justement j'aimerais en sortir en discutant le fond et pas qui a dit quoi.

          Le fait qu'une remarque aux auteurs conduise à un changement dans CompCert ne veut pas du tout dire qu'il y avait un bug à la base. Par exemple le second problème rapporté dans l'article est lié au type de la fonction main, on peut trouver un correctif associé dans le commit 3eb2b3b7bb464, mais la version avant correction respectait tout autant la spécification de correction et compilait tout aussi correctement les programmes valides.

          Je considère au contraire que la conférence/journal (ainsi que l'année, incluse dans cette notation) est bien l'une, si ce n'est la plus importante, des informations à donner—à l'inverse de la liste des auteurs qui est bien elle l'information la moins importante.

          Question de point de vue peut-être, mais qui n'est pas totalement subjective ou arbitraire. En nommant les auteurs je les récompense pour leur travail (puisque la valeur dans le milieu de la recherche n'est pas récompensée financièrement mais par la reconnaissance)—ça me semble très important et juste, et en particulier je préfère toujours citer tous les auteurs et pas "Machin et al.". En nommant la conférence, tu donnes l'impression que la valeur du travail est liée à la réputation de la conférence : les travaux publiés dans une "bonne" conférence sont mis en valeur et ceux qui viennent d'une conférence moins connue sont moins bien considérés. C'est un système qui me semble dommageable, qui encourage la compétition et les mauvaises pratiques—au contraire je préfère que le travail des gens parle de lui-même, qu'on juge l'article par son contenu et pas son étiquette. Après si tu tiens à citer la conférence aussi, rien ne t'en empêche et c'est plutôt la norme, mais le mettre à la place du nom des auteurs me semble mauvais.

          (Il faut distinguer de la façon dont les gens citent leur propre travail, par exemple dans leur CV ou leurs exposés de présentation de carrière. Dans ce cas il est courant et compréhensible d'utiliser le format CONF'YY, puisque les auteurs sont toujours l'exposant et ses collaborateurs. Et puis ça correspond à la façon dont beaucoup de gens se souviennent de leurs propres travaux: ils ou elles peuvent avoir plusieurs publications sur la même année et se souviennent souvent bien de l'endroit où chaque travail a été présenté. Mais ça ne se généralise pas nécessairement aux travaux des autres.)

          • [^] # Re: Nuance

            Posté par . Évalué à -7. Dernière modification le 28/11/16 à 17:05.

            [remarque sur la typographie - pas sur le fond]

            bluestorm< (alias gasche), j'apprécie grandement les efforts pédagogiques que tu fais pour rendre accessible l'état de la recherche. Merci. Concernant la forme, je te propose quelques conseils de typographe amateur :

            • le tiret long (ou tiret quadratin) que tu utilises à bon escient nécessite un espace avant et après. Pour l'obtenir, une façon de faire sur Linuxfr est de placer deux espaces puis deux tirets puis à nouveau deux espaces — ceci permettant de produire ce que tu vois ici — ce que j'ai découvert par l'expérience.
            • pour les signes de ponctuation point virgule et deux points, il convient de placer un espace avant (idéalement c'est un espace insécable) et après, au moins en français. Il me semble que tu utilises l'usage qui a cours en anglais, sans doute par la mauvaise influence de tes lectures ;) Je précise à toute fin utile que, de même, si en anglais on ne met pas d'espace avant le point d'interrogation ni le point d'exclamation, il convient d'en mettre un en français.

            Bien cordialement,
            SamWang, amateur de typographie à ses heures.

            • [^] # Re: Nuance

              Posté par . Évalué à 4.

              Merci pour les compliments et les remarques. Je passe souvent de l'anglais au français et il m'arrive de rater mes convenients. J'aimerais mieux que le moteur de rendu de linuxfr mette la bonne typographie pour le français (ajoute l'espace nécessaire avant : ou ; et gère les -- correctement). Hélas il n'est toujours pas possible d'éditer ses messages sur LinuxFR donc, comme je remarque ce genre de soucis systématiquement après avoir publié le message, il y a très peu de chances que j'arrive à corriger ici. J'essaierai d'en tenir compte sur les plateformes dont les utilisateurs se font assez confiance les uns aux autres pour s'autoriser à éditer leurs messages.

              (La typographie c'est un sujet maudit à mon avis : on est heureux tant qu'on l'ignore, et le fait de l'apprendre n'attire que des désagréments — et on peut difficilement le désapprendre. Attention à bien mesurer les risques que tu fais subir aux gens en leur faisant des points d'information !)

  • # Petite coq... uille

    Posté par . Évalué à 0. Dernière modification le 26/11/16 à 12:06.

    1) Il me semble qu'il y a une petite coquille dans le journal, dans l'énoncé du théorème à démontrer, et qu'il conviendrait de remplacer la dernière occurrence de M par un P.

    Voici l'énoncé originel du journal :

    Enfin, il faut démontrer un théorème du type « pour tout programme P écrit en C et toute machine cible M, si CompCert produit un code machine PM pour M à partir de P, alors exécuter PM sur M donne pour toute entrée le même résultat qu’exécuter M dans la sémantique de C ».

    Voici la phrase corrigée (la dernière occurrence de M est remplacée par un P) :

    Enfin, il faut démontrer un théorème du type « pour tout programme P écrit en C et toute machine cible M, si CompCert produit un code machine PM pour M à partir de P, alors exécuter PM sur M donne pour toute entrée le même résultat qu’exécuter P dans la sémantique de C ».

    2) Je propose la traduction du précédent paragraphe dans une forme plus littéraire au paragraphe ci-après avec pour but de faciliter la lecture (où l'on découvre que le théorème est très simple à comprendre). Cette traduction ne nécessite pas de définition de P (le programme écrit en C), ni de M (la machine cible), ni de PM (un code machine produit par CompCert à partir du programme P pour une machine cible M). J'en profite pour remplacer l'expression "code machine" par "code binaire", de manière à s'éloigner du mot machine qui est aussi utilisé isolément.

    Enfin, il faut démontrer un théorème du type « pour tout programme écrit en C et toute machine cible, si le compilateur CompCert produit un code binaire pour une de ces machines, alors exécuter ce code binaire sur ladite machine donne, pour toute entrée, le même résultat qu’exécuter ledit programme en C dans la sémantique de C ».

    • [^] # Re: Petite coq... uille

      Posté par . Évalué à -2.

      La petite coquille concerne le journal et, au-delà, le bulletin de la Société Informatique de France qui est cité dans le journal. Je viens de vérifier à la source.

    • [^] # Re: Petite coq... uille

      Posté par (page perso) . Évalué à 3.

      Corrigé, merci.

      • [^] # Re: Petite coq... uille

        Posté par . Évalué à -1.

        Attention, la version corrigée n'est plus une citation de la source. Tel que formulé, le journal n'est plus correct (il ne compile pas avec mon analyseur sémantique approfondi). Je pense qu'une formulation correcte impliquerait une NDM (note du modérateur) à la suite du paragraphe cité pour préciser que la dernière phrase est corrigée par rapport à la source qui a une coquille au moment de la rédaction du journal. Un truc du genre :

        [NDM : la dernière phrase de cette citation comprend une coquille à la source au moment de la rédaction du journal, corrigée ici, la dernière occurrence de P étant par erreur un M à la source]

        • [^] # Re: Petite coq... uille

          Posté par . Évalué à 5. Dernière modification le 26/11/16 à 14:06.

          Effectivement, la coquille se trouve dans l'article d'origine de Gérard Berry, je n'ai pas relu attentivement la phrase (sachant ce qu'elle cherchait à exprimer) en citant. Mais c'est une bonne chose au final, cela illustre une source potentielle de bug dans la démarche : lorsque l'humain traduit formellement la spécification du langage. Ce qui minimise grandement la surface. Il suffit de lire les deux articles cités dans ce commentaire : 4 erreurs minimes trouvées et corrigées pour CompCert face à des centaines, non toutes corrigées, pour GCC et LLVM. :-)

          Pour la note de modérateur à rajouter sur la correction, je ne sais si elle est vraiment nécessaire. Quoi que la source a une clause ND : un correction de coquille est-elle une œuvre dérivée ? :-P

          Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.

        • [^] # Re: Petite coq... uille

          Posté par (page perso) . Évalué à 3.

          Corrigé, merci.

Suivre le flux des commentaires

Note : les commentaires appartiennent à ceux qui les ont postés. Nous n'en sommes pas responsables.