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 ǝpɐןƃu∀ nǝıɥʇʇɐW-ǝɹɹǝıԀ (site web personnel) . Évalué à 6.
Peut-on en savoir plus rapidement sur le Clight ? Quels sont les éléments du C qui en sont exclus ?
« IRAFURORBREVISESTANIMUMREGEQUINISIPARETIMPERAT » — Odes — Horace
[^] # Re: Clight
Posté par kantien . É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 :
Je pense que cela parlera plus aux développeurs C qu'à moi-même. Et pour l'architecture, on trouve ce schéma :
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 ǝpɐןƃu∀ nǝıɥʇʇɐW-ǝɹɹǝıԀ (site web personnel) . É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.
« IRAFURORBREVISESTANIMUMREGEQUINISIPARETIMPERAT » — Odes — Horace
[^] # Re: Clight
Posté par Ontologia (site web personnel) . Évalué à 2.
Et citons l'argument
-dcmmde 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 Clément David (site web personnel) . É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/setjmpsont peu utilisé aussi sauf pour du très bas-niveau et lesVariable-length arraypeuvent aussi une spécificité du C99 (utile mais contournable facilement).# prix Microsoft
Posté par Jiel (site web personnel) . É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.
[^] # Re: prix Microsoft
Posté par Axioplase ıɥs∀ (site web personnel) . Évalué à 5. Dernière modification le 28 novembre 2016 à 18:09.
Microsoft Research, c'est quand même bien reconnu et estimé….
# Verified toolchain
Posté par Harvesterify (site web personnel) . É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.
[^] # Commentaire supprimé
Posté par Anonyme . Évalué à -3.
Ce commentaire a été supprimé par l’équipe de modération.
[^] # Commentaire supprimé
Posté par Anonyme . Évalué à -6.
Ce commentaire a été supprimé par l’équipe de modération.
# Nuance
Posté par Cioran_Naroic . É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 kantien . Évalué à 5.
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) :
En ce qui concerne les approches formelles :
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 :
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 gasche . É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 anaseto (site web personnel) . É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 Cioran_Naroic . É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):
Concernant le deuxième paragraphe:
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).
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 kantien . Évalué à 3.
Les erreurs semblent bien avoir été corrigées. Au moins pour celle sur la signature du la fonction
maind'après le manuel datant du 30 juin 2016 :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 gasche . Évalué à 6.
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.
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.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.)
[^] # Commentaire supprimé
Posté par Anonyme . Évalué à -7. Dernière modification le 28 novembre 2016 à 17:05.
Ce commentaire a été supprimé par l’équipe de modération.
[^] # Re: Nuance
Posté par gasche . É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 !)
# Commentaire supprimé
Posté par Anonyme . Évalué à 0. Dernière modification le 26 novembre 2016 à 12:06.
Ce commentaire a été supprimé par l’équipe de modération.
[^] # Commentaire supprimé
Posté par Anonyme . Évalué à -2.
Ce commentaire a été supprimé par l’équipe de modération.
[^] # Re: Petite coq... uille
Posté par Benoît Sibaud (site web personnel) . Évalué à 3.
Corrigé, merci.
[^] # Commentaire supprimé
Posté par Anonyme . Évalué à -1.
Ce commentaire a été supprimé par l’équipe de modération.
[^] # Re: Petite coq... uille
Posté par kantien . Évalué à 5. Dernière modification le 26 novembre 2016 à 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 Benoît Sibaud (site web personnel) . Évalué à 3.
Corrigé, merci.
Suivre le flux des commentaires
Note : les commentaires appartiennent à celles et ceux qui les ont postés. Nous n’en sommes pas responsables.