Ce qu’il faut savoir sur les compilateurs et leur vérification (1/2)

Sandrine Blazy, Professeure à l’université de Rennes et directrice adjointe de l’IRISA, est une spécialiste des compilateurs et des logiciels sûrs. Elle a développé avec Xavier Leroy, CompCert, le premier compilateur pour le langage C vérifié à l’aide de Coq. Pour ce véritable tour de force scientifique et technique, elle a obtenu la médaille d’argent du CNRS (une des plus belles récompenses scientifiques en France). Si vous ne comprenez pas en quoi cela consiste, Sandrine va l’expliquer à binaire et ce sera l’occasion d’un peu mieux comprendre ce qui se passe dans un ordinateur. Serge Abiteboul et Pierre Paradinas
© Jean-Claude MOSCHETTI / IRISA / CNRS Images

Les débuts de l’informatique

Les liens entre mathématiques et informatique sont féconds. Dans les années quarante, la nécessité de mécaniser des calculs numériques permettant de résoudre des équations mathématiques a permis le développement des premières machines de calcul à grande échelle, qui ont préfiguré les premiers ordinateurs. Ces calculateurs universels enchaînaient en séquence des opérations mathématiques élémentaires, décomposant des calculs modélisant des phénomènes physiques. Aujourd’hui, ces calculs sont réalisés par une simple calculette de bureau.

Chaque opération était fidèlement décrite par un code constitué de commandes compréhensibles par la machine, c’est-à-dire des suites de chiffres zéros et un (signifiant l’absence et la présence de courant dans les composants d’un circuit électronique). Aussi, faire exécuter une opération par un calculateur était une véritable gageure. Les experts dont c’était le travail devaient encoder l’opération (c’est-à-dire trouver les nombres adéquats pour représenter l’opération, ainsi que les valeurs auxquelles elle s’appliquait qui étaient encodées sur des cartes perforées), en plus d’effectuer des manipulations physiques sur la machine. Ces experts écrivaient ces codes sur papier, avant de les fournir à la machine, dont ils devaient de plus comprendre le fonctionnement électromécanique. Ces premières machines étaient gigantesques et complexes à manipuler. En guise d’écran, des marteaux (tels que ceux utilisés par les machines à écrire) imprimaient sur papier des caractères. Par contre, elles avaient l’avantage de fonctionner sans cesse et d’accélérer grandement les temps de calcul de chaque opération, en enchaînant en des temps records des successions de calculs variés, ce qui a fait leur succès.

Le succès aidant et les calculs devenant de plus en plus complexes, il a été nécessaire de rendre l’écriture des codes moins absconse et d’automatiser davantage l’enchaînement des calculs. Une première réponse a été l’utilisation répandue d’une notation plus expressive et graphique (à l’aide de boîtes reliées par des flèches) pour représenter l’enchaînement des calculs. Les diagrammes résultants, appelés organigrammes permettaient de représenter simplement non seulement des séquences de calculs, mais aussi des décisions à prendre en fonction de résultats intermédiaires, et donc des enchaînements plus sophistiqués de calculs (comme la répétition d’étapes de calculs jusqu’à atteindre un certain seuil). Ces diagrammes permettaient de s’abstraire du matériel, et de décomposer un problème avant d’écrire du code. Plus faciles à comprendre par des humains, ils permettaient de réutiliser une opération lorsque la machine évoluait en fonction des progrès technologiques fréquents.

L’expressivité des organigrammes a favorisé l’émergence d’”algorithmes”, c’est-à-dire d’enchaînements plus efficaces des calculs (c’est-à-dire réduisant le temps de calcul), du fait de la représentation particulière des nombres en machine. Par exemple, en 1949, Alan Turing a proposé une nouvelle façon de calculer la fonction mathématique factorielle, sans utiliser les opérations coûteuses de multiplication mais seulement des additions. Il se demande alors comment être sûr que ce que calcule son organigramme est effectivement le même résultat que celui de la fonction factorielle du mathématicien, en d’autres termes que son organigramme est correct. Pour y répondre, il a effectué ce qu’on appellerait aujourd’hui la première preuve de programme, en annotant son organigramme avec des assertions, dont il a ensuite vérifié la cohérence.

L’effort pour démocratiser la mécanisation des calculs s’est poursuivi avec l’invention des premiers langages de programmation. Les organigrammes ont fait place au pseudo-code, puis aux algorithmes et programmes écrits dans un langage dont la syntaxe est plus intuitive. Un langage de programmation définit un ensemble de commandes abstraites mais précises pour effectuer toutes les opérations exprimables dans un organigramme, avec des mots-clés en anglais (plus faciles à appréhender que les seuls nombres d’un code). Le premier livre sur la programmation paraît en 1951, alors que très peu de machines sont en service; il est utilisé pour des recherches en physique, astronomie, météorologie et biochimie.

Les langages de programmations et les compilateurs

Le langage de programmation devient un intermédiaire nécessaire entre l’humain et la machine, et il devient indispensable d’automatiser la traduction des programmes en code machine. Le premier compilateur A-0 mis au point par Grace Hopper est disponible en 1952. Ce terme résulte de son premier usage, mettre bout à bout des portions de code, à la manière d’une bibliothécaire qui rassemble des documents sur un sujet précis. Pour expliquer de plus les possibilités prometteuses offertes par un tel programme de traduction (d’un langage source en un code machine), Grace Hopper utilise la métaphore d’une ligne de production dans une usine, qui produirait des nombres (plutôt que des automobiles) et plus généralement des données au moyen d’outils (tables de calcul, formules, calculs numériques).

Le compilateur devient un point de passage obligé pour traduire tout programme écrit par un humain en un code compréhensible par la machine, et la traduction de l’un vers l’autre est un défi scientifique. En effet, un problème se pose du fait de la faible vitesse des calculs, des capacités très limitées de stockage, mais aussi de l’abstraction et la généralité des programmes écrits : plus le programme source est facile à comprendre pour un humain, moins l’exécution du code machine engendré est efficace.

File:Fortran logo.svgEn 1953, le langage Fortran est le premier à être dédié au calcul numérique, et donc à s’abstraire du matériel spécifique à une machine. C’est aussi le premier qui devient un standard: pour la première fois, les programmeurs parlent un même langage, quelle que soit la machine qu’ils utilisent. IBM consacre un effort notable à développer son compilateur, afin qu’il produise un code efficace. C’est le début de l’invention de nouvelles techniques de compilation, les premières optimisations (ex. compiler séparément des portions de code, ou encore détecter des calculs communs pour les factoriser). Le manuel de Fortran est disponible en 1956, et son compilateur en 1957.

Cet effort pour démocratiser la programmation se poursuit avec le langage Cobol dédié au traitement des données. Désormais, l’ordinateur ne calcule pas que des nombres; il permet plus généralement de structurer des données et de les traiter efficacement. COBOL ouvre la voie à de nouvelles applications. Le premier programme COBOL est compilé en 1960; en 1999 la grande majorité des logiciels seront écrits en COBOL, suite à son utilisation massive dans les domaines de la banque et de l’assurance. Ainsi, dans les années 60, la pratique de la programmation se répand et devient une science; les langages de programmation foisonnent. Aujourd’hui encore, les langages de programmation évoluent sans cesse, pour s’adapter aux nouveaux besoins.

Sandrine Blazy

Pour aller plus loin retrouvez  :

      • La vidéo du CNRS à l’occasion de la Médaille d’argent de Sandrine
      • La vidéo pour le Prix ACM décerné au logiciel CompCert
Partager cet article :

Commentaires

Laisser un commentaire

Votre adresse e-mail ne sera pas publiée. Les champs obligatoires sont indiqués avec *