Algorithmes, machines et langages - Gérard Berry Collège de France

Gérard Berry
Algorithmes, machines et langages
Collège de France
LEÇON DE CLÔTURE
Où va l'informatique ? - Plaidoyer pour les trajectoires non linéaires
26 février 2019

Gérard Berry
Algorithmes, machines et langages
Année 2014-2015
Prouver les programmes : pourquoi, quand, comment ?
Sixième leçon : Vérification et optimisation booléennes d'automates et circuits

Ce dernier cours de 2014-2015 introduit les méthodes implicites de manipulation de systèmes de transitions, à travers les méthodes de calcul booléen utilisées à la fois pour la vérification formelles et pour l'optimisation de circuits électroniques et de programmes qui peuvent se réduire au calcul booléen.

Ces méthodes ont révolutionné le domaine en permettant des vérifications formelles de systèmes dont le calcul explicite des états et transitions est impossible, car la taille des formules manipulées par les méthodes implicites est largement indépendante de celle des systèmes qu'ils décrivent. Nous expliquons d'abord les codages booléens d'ensembles, de relations et de fonctions, et montrons comment calculer l'image directe et l'image inverse de sous-ensembles par des fonctions. Nous étudions ensuite les codages booléens d'automates déterministes et non-déterministes, ainsi que leurs implémentations en circuits électroniques. Nous rappelons le fait que le circuit canoniquement associé à un automate non-déterministe est lui déterministe comme tous les circuits combinatoirement acycliques, ce qui montre clairement que le qualificatif « non-déterminisme » est particulièrement mal choisi : en vérification booléenne comme en optimisation de circuits, il est inutile de déterminiser les automates, et c'est souvent nuisible à cause de l'explosion exponentielle que la déterminisation peut produire. Nous montrons comment la vérification formelle de propriétés de sûreté définies par des observateurs se réduit au calcul des états accessibles, et comment effectuer ce calcul de manière implicite. Nous introduisons la première structure fondamentale du calcul booléen, les Binary Decision Diagrams, développés par R. Bryant au milieu des années 1980 (et indépendamment par J-P. Billion chez Bull en France), et expliquons pourquoi ils permettent de faire les calculs nécessaires au passage à la grande échelle; nous mentionnons leurs limitations, qui sont inévitables car le calcul booléen est NP-complet. Les BDDs seront étudiés beaucoup plus en profondeur dans le cours 2015-2015.

Pour terminer, nous montrons que le codage booléen permet de réaliser des optimisations très efficaces des circuits engendrés par les programmes Esterel. Nous insistons sur le fait que la structure du langage source et la façon d'y programmer les applications sont essentiels pour la qualité de l'optimisation finale : c'est grâce à l'interaction de la séquence, du parallélisme et de la préemption hiérarchique des comportements que les circuits engendrés par Esterel sont systématiquement meilleurs que ceux programmés et optimisés par les méthodes classiques, au moins en ce qui concerne leurs parties contrôle.

Gérard Berry
Algorithmes, machines et langages
Année 2014-2015
Prouver les programmes : pourquoi, quand, comment ?
Cinquième leçon : La vérification de modèles (model-checking)

Ce cours termine la présentation générale des méthodes de vérification formelle par la vérification de modèles, plus connue sous son nom anglais original de model-checking. Cette méthode est bien différente des précédentes car elle s'intéresse essentiellement aux programmes d'états finis, ceux dont on peut au moins conceptuellement dérouler complètement toutes les exécutions possibles en temps et espace fini. De plus, contrairement aux méthodes précédemment décrites, le model-checking s'intéresse principalement aux programmes parallèles. Le parallélisme peut y être synchrone comme dans les circuits ou les langages synchrones présentés les années précédentes, ou asynchrones comme dans les protocoles de communication, les réseaux et les algorithmes distribués. Le model-checking est né au début des années 1980, quasi-simultanément en deux endroits : Grenoble avec J-P. Queille et J. Sifakis, qui ont développé le système CESAR et sa logique temporelle, et les USA avec E. Clarke et E. Emerson qui ont développé la logique temporelle CTL et le système EMV. Ces travaux ont donné le prix Turing 2007 à Clarke, Emerson et Sifakis. Ils s'appuyaient eux-mêmes sur les travaux d'Amir Pnueli (prix Turing en 1996) sur la logique temporelle. Le model-checking s'est considérablement développé ensuite, et constitue certainement la méthode formelle la plus utilisée dans l'industrie, en particulier dans la CAO de circuits.

L'idée de base est de construire le graphe de toutes les exécutions possibles d'un programme, qu'on appelle son modèle. Ce modèle peut prendre la forme d'une structure de Kripke (logicien et philosophe de la logique modale), c'est-à-dire d'un graphe où les états sont étiquetés par des prédicats élémentaires, ou encore d'une structure de transitions, où les étiquettes sont portées par les transitions entre états. Une fois construit, le modèle devient indépendant du langage qui l'a engendré. Pour raisonner sur un modèle, un moyen très répandu est l'utilisation de logiques temporelles, définissent les propriétés temporelles à l'aide de propriétés élémentaires des états ou transitions et de quantificateurs sur les états ou les chemins de son graphe. On peut ainsi exprimer et vérifier des propriétés de sûreté (absence de bugs), comme « à aucun moment l'ascenseur ne peut voyager la porte ouverte », d'absence de blocages de l'exécution, ou de vivacité, comme « l'ascenseur finira par répondre à toutes les demandes des passagers » ou encore « chaque processus obtiendra infiniment souvent la ressource partagée s'il la demande infiniment souvent ».

Nous présenterons d'abord la logique CTL*, la plus générale, qui permet d'imbriquer arbitrairement les quantifications d'états et de chemin sur les structures de Kripke. Mais cette logique très expressive est difficile à utiliser et les calculs y sont d'un coût prohibitif. Deux sous-logiques différentes sont utilisées : LTL (Linear Temporal Logic), qui ne quantifie pas sur les états et considère donc seulement des traces linéaires, et CTL, logique arborescente qui permet de quantifier sur les chemins mais avec des restrictions par rapport à CTL*. Ces deux logiques sont d'expressivités différentes et ont chacune des avantages et des inconvénients que nous discuterons brièvement. LTL est la logique la mieux adaptées pour la vérification de propriétés de vivacité, comme le montre L. Lamport (prix Turing 2014) avec son système TLA+. Mais, au contraire, elle ne permet pas d'exprimer des prédicats sur l'existence de calculs particuliers.

La modélisation par systèmes de transitions, systématisée par R. Milner (prix Turing 1992) dans l'étude des calculs de processus communicants, permet de bien

Gérard Berry
Algorithmes, machines et langages
Année 2014-2015
Prouver les programmes : pourquoi, quand, comment ?
Quatrième leçon : Des logiques d'ordre supérieur à la programmation vérifiée en Coq

Ce cours complète le précédent en terminant la présentation des méthodes générales de preuve de programmes par celle fondée sur les logiques d'ordre supérieur (celles où l'on peut aussi quantifier sur les prédicats) et sur le lambda-calcul déjà présenté en détail dans le cours 2009-2010. Nous montrons d'abord pourquoi l'ordre supérieur est plus expressif que l'ordre un. Par exemple, pour prouver une propriété par récurrence, il faut avoir en calcul des prédicats un schéma d'axiome de récurrence qui engendre un axiome particulier par prédicat à étudier, et donc une infinité d'axiomes ; en ordre supérieur, un seul axiome standard suffit puisqu'on peut quantifier universellement le prédicat de travail. D'autres avantages apparaîtront dans la suite du cours. Un inconvénient est bien sûr une plus grande complexité de la logique et de certains des algorithmes permettant de la traiter.

Nous décrirons d'abord brièvement les systèmes HOL de M. Gordon, HOL-Light de J. Harrison, PVS de N. Shankar, S. Owre et J. Rushby, et Isabelle de L. Paulson, ce dernier étant en fait un méta-système logique dans lequel plusieurs logiques peuvent être définies. Ces systèmes ont conduit à des preuves très importantes en pratique : la preuve de correction de l'arithmétique entière et flottante du Pentium d'Intel par J. Harrison après le fameux bug de division du Pentium Pro qui a coûté 470 millions de dollars à Intel en 1994 ; la preuve de correction du micronoyau de système d'exploitation seL4 effectuée par G. Klein et. al. à NICTA Sydney en utilisant Isabelle (cf. le séminaire de D. Bolignano le 11 mars 2015 pour une autre preuve de système d'exploitation).

Nous présentons ensuite avec plus de détails le système Coq, développé en France et titulaire de grandes récompenses récentes. Coq est fondé sur le calcul des constructions CoC de G. Huet et T. Coquand (1984) et sa version inductive CiC développée par C. Paulin, qui parlera en séminaire, à la suite de ce cours. Coq diffère des systèmes classiques par le fait qu'il intègre complètement calcul et preuve dans un formalisme très riche, incorporant et développant considérablement des idées et théorèmes de de Bruijn (Automath, 1967), Girard (SystemF, 1972), etc.

Gallina, le langage de programmation de Coq est un langage typé d'ordre supérieur, c'est-à-dire dont les types peuvent eux-mêmes être des fonctions. Le typage est décidable, et le système de types garantit que tous les calculs de termes bien typés se terminent sur des formes normales uniques. La programmation classique est facilitée par la couche inductive, qui permet des définitions récursives puissantes mais à terminaison garantie. Grâce à la mise en pratique de la correspondance fondamentale de Curry-Howard entre calculs et preuves, il n'y a plus vraiment de différence entre calculer et prouver. Ainsi, un programme a pour type sa spécification alors qu'une preuve a pour type le théorème qu'elle démontre, ce de façon absolument identique. De plus, les preuves sont des fonctions standards du calcul, au même titre que les fonctions sur les types de données classiques. Enfin, une fois un programme développé et prouvé en Coq, on peut en extraire automatiquement un code objet directement exécutable écrit en Caml, correct par construction et normalement efficace. Tout cela donne à Coq une richesse considérable à la fois pour spécifier, programmer, prouver et exporter, quatre activités qui deviennent complètement intégrées.

Le cours se terminera par la présentation de deux succès majeurs de Coq : d'abord le compilateur certifié CompCert de X. Leroy, seul compilateur C ayant passé le filtre des tests aléatoires présenté dans

Gérard Berry
Algorithmes, machines et langages
Année 2014-2015
Prouver les programmes : pourquoi, quand, comment ?
Troisième leçon : Les méthodes générales : assertions, réécriture, interprétation abstraite, logiques et assistants de preuve

Il y a deux principaux types de méthodes formelles pour la preuve de programme : les méthodes générales, qui s'adressent à tous les types de programmes et seront présentées dans ce cours, et celles de la vérification de modèles (model-checking), qui s'intéressent principalement aux programmes à espaces d'états finis et aux circuits électroniques et seront traitées dans le cours no 5 du 25 mars 2015.

La nécessité de traiter les programmes comme des objets mathématiques à part entière a été reconnue par A. Turing dès 1949. Il a alors introduit la notion d'assertion associant un prédicat logique à un point de contrôle du programme, ainsi que l'importance de la notion d'ordre bien fondé pour montrer la terminaison des programmes. Son approche par assertions est la première que nous traiterons dans le cours. Elle a été étendue et perfectionnée par R. Floyd, C.A.R. Hoare, E.W. Dijkstra, et bien d'autres, pour aboutir à une théorie et une pratique complètes de la définition logique des langages de programmation et de la vérification de programmes, applicables initialement aux programmes séquentiels impératifs. La notion d'assertion a été ensuite étendue en celle de contrat (assume/guarantee) à respecter par les fonctions ou modules d'un programme, applicable aussi aux langages objets et aux langages parallèles.

En 1963, dans un article fondateur militant pour le traitement mathématique de la programmation et introduisant une brochette remarquable de nouveaux concepts, J. McCarthy a introduit l'idée bien différente d'utiliser la réécriture de termes comme outil applicable à la fois pour l'optimisation de programmes et leur vérification formelle. Cette approche, la seconde que nous étudierons, a eu une longue descendance dans les systèmes de vérification (Boyer&More, ACL2, PVS, Key, ProVerif, etc.), et continue d'irriguer les autres approches. Elle a eu des succès remarquables en circuits, en avionique, en sécurité, etc.

La troisième approche historique est celle de la sémantique dénotationnelle des langages introduite par Scott et Strachey vers 1970. Ici, un programme est interprété comme une fonction dans un espace topologique ordonné par un ordre d'information, et toutes les fonctions sont rendues totales par l'ajout explicite d'éléments indéfinis. Une théorie générale du point fixe dans les espaces ordonnés permet d'interpréter de façon uniforme les boucles, la récursion et la programmation fonctionnelle d'ordre supérieur. Au début des années 1970, cette théorie a été à l'origine du pionnier des assistants de preuve de programmes, LCF, créé par Milner et al. Mais le traitement explicite de l'indéfini s'est révélé trop compliqué, et les assistants de preuve ont ensuite suivi un autre chemin. La sémantique dénotationnelle a cependant eu un succès considérable dans une autre approche de la vérification, l'interprétation abstraite créé par P. et R. Cousot en 1977. L'idée est ici de travailler avec des assertions portant non plus sur les valeurs exactes calculées, mais sur une abstraction de celles-ci, comme la preuve par 9 le fait pour détecter des erreurs dans la multiplication. De nombreux domaines abstraits ont été développés, ainsi que des méthodes algorithmiques générales de combinaison de ces domaines et d'accélération des calculs de points fixes. L'interprétation abstraite est maintenant développée industriellement. Elle a permis de vérifier des propriétés critiques de très gros programmes, comme l'absence d'erreurs à l'exécution dans le code de pilotage de l'Airbus A380. Elle est également utilisée pour l'évaluation du temps de calcul maximal de logiciels emb

Gérard Berry
Algorithmes, machines et langages
Année 2014-2015
Prouver les programmes : pourquoi, quand, comment ?
Deuxième leçon : De la spécification à la réalisation, au test et à la preuve : les approches formelles

Ce premier cours du cycle « Prouver les programmes : pourquoi, quand, comment » a pour but d'introduire les méthodes formelles de développement et vérification de programmes, en les reliant aux méthodes de programmation, test et validation classiques.

Dès les débuts de l'informatique, la difficulté de faire des programmes justes est apparue comme un problème majeur. Deux approches bien différentes ont été développées : d'une part, le génie logiciel, qui s'est développé lentement mais est maintenant bien en place au moins dans les entreprises sérieuses, et, d'autre part, une approche formelle beaucoup plus scientifique, introduite par Turing dès 1949 et fondée sur l'idée de voir un programme comme une entité mathématique sur laquelle il faut raisonner mathématiquement. C'est cette dernière qui a conduit aux méthodes formelles que nous étudierons cette année et les suivantes. Ces deux approches se sont développées très indépendamment l'une de l'autre et ne commencent à converger que depuis peu de temps : développement et vérification formels apparaissent désormais comme des moyens efficaces voire privilégiés d'éviter les bugs, au moins dans les applications où leur coût humain et matériel peut être catastrophique. Les techniques de vérification formelle ont eu une maturation assez lente, d'une part parce que le sujet est intrinsèquement difficile, d'autre part parce que l'industrie ne s'y est vraiment intéressée que récemment. Mais les choses bougent rapidement, avec des succès de plus en plus fréquents. Et, ce qui ne gâche rien pour un tel enseignement, les chercheurs français jouent un rôle majeur dans ce domaine en plein essor.

Génie logiciel et vérification formelle partagent deux prérequis essentiels : d'abord, la qualité des spécifications initiales, qui doivent être précises, non-contradictoires, et complètes mais sans excès de précision inutile ; ensuite, la qualité des langages de programmation, dont la sémantique doit être précise tout en restant intuitive. Beaucoup de projets industriels échouent encore à cause de leur non-respect de ces contraintes.

Le génie logiciel classique écrit les spécifications en langage habituel et fournit des outils de traçabilité permettant de relier spécifications et réalisation. Pour la validation du résultat, il s'appuie sur des revues de code et surtout sur des tests, ce qui pose deux problèmes majeurs : il est difficile de mesurer ce que les tests testent réellement, et le test n'apporte aucune information sur ce qui n'est pas testé. Mais nous verrons que des systèmes de génération de tests aléatoires dirigés permettent d'obtenir des résultats étonnants.

À l'opposé, les méthodes formelles écrivent les spécifications en langage mathématique, le seul langage rigoureux dont nous disposions réellement, et font aussi progresser ce langage. Les systèmes modernes de typage des programmes permettent de détecter des erreurs dès les premières passes de compilation. Les meilleurs d'entre eux sont directement issus des recherches en sémantique de la programmation, elles-mêmes directement liées à la vérification formelle. Pour aller plus loin, on cherche à remplacer ou compléter les tests dynamiques de validation par des preuves statiques là encore mathématiques, aidées par des systèmes de vérification formelle plus ou moins automatisés. Au contraire des tests, la vérification formelle dit tout sur les propriétés à valider : prouvées vraies, elles le sont en toutes circonstances ; détectées comme fausses, les outils permettent souvent de construire des tests les invalidant et de découvrir ainsi la source de l'erreur. Mais la preuve, techniquement pl