potterman28wxcv

Etudiant en thèse : "Compilation optimisée et certifiée pour processeur VLIW" à VERIMAG

À propos de Cyril

Cyril Six

Date de naissance : 28 septembre

Envoyer un message

Biographie

Tout a commencé sur le site du zéro il y a 10 ans de ça - une envie de savoir "comment ça fonctionne", de faire des programmes par moi même. J'ai buché sur un tutoriel qui était à l'époque le tutoriel phare du Site du Zéro quand ça existait encore (une belle époque !) : http://sdz.tdct.org/sdz/apprenez-a-programmer-en-c.html

Suite à ce tuto j'ai pu faire mes premiers programmes. Dont un jeu de Snake et un jeu de "tir aux canards", dont j'ai malheureusement perdu les code sources. Mais si vous cherchez bien vous pouvez trouver les sujets sur lesquels je demandais de l'aide à l'époque, quand j'étais "à votre place" ;)

Je me suis ensuite dirigé vers une prépa PCSI-SI puis PSI, pour ensuite intégrer l'ENSIMAG. Là j'y ai fait un master PDES (Parallel, Distributed and Embedded Systems). Dans ces 3 années d'étude d'école d'ingé, je me suis intéressé et rapproché du domaine de la performance, la compilation, ce qui touche au "bas niveau".

Après un stage à l'équipe CORSE (Compilation, Optimisation and Runtime Systems), j'y ai continué pendant 1 an en tant qu'ingénieur de recherche, où je me suis confronté à des problématiques d'ordonnancement statique et de localité des données, en travaillant sur un générateur de code C pour des réseaux de neurones (Caffé vers C), sur l'architecture manycore MPPA que produit l'entreprise française Kalray.

Je suis maintenant depuis 1 an et demi doctorant, en thèse sur le sujet "Compilation optimisée et certifiée pour processeur VLIW". Je peux expliquer ça brièvement..

Tout d'abord, "compilation certifiée" ? On parle ici de la compilation du langage C, vers du code machine. Vous connaissez bien sûr les compilateurs usuels tels que mingw, gcc, clang. Mais quelle garantie avez-vous que ces compilateurs n'ont pas de bug ? En fait, en tant que programmeur lambda, on fait la supposition que le compilateur n'a pas de bug. Et on a bien raison de faire cette hypothèse là en travaillant sur des programmes non critiques, parce que, heureusement pour nous, une quantité énorme de travail continue à être mise au point ce afin que les compilos qu'on utilise (gcc, clang..) ne soient pas buggés.

Par contre, qu'en est-il des domaines critiques tels que l'aviation, où on n'a pas envie que l'avion se crashe à cause d'un bug logiciel, et a fortiori on ne veut pas que le compilateur introduise de bug ? Dans la pratique, ils vont en fait compiler sans aucune optimisation (en -O0) de façon à ce que le code assembleur puisse par la suite être lisible et vérifié.. Ce qui n'est pas idéal. Pour répondre à ça, Xavier Leroy (inventeur d'OCaml) a mis en place CompCert, un compilateur certifié sans bug. Plus précisément, CompCert va prouver qu'une propriété de préservation de sémantique au passage du C vers l'assembleur : le code assembleur généré doit avoir les "mêmes propriétés" que le code C. CompCert est d'ailleurs écrit en Coq, un langage de preuves formelles qui a notamment permis à prouver formellement le théorème des quatres couleurs.. Mais je m'égare.

Les compilateurs peuvent inclure plusieurs optimisations sur le code C. C'est pour cela qu'on répète souvent aux débutants de ne pas se préoccuper de "l'efficacité" dans un premier temps, et que la lisibilité et la maintenabilité sont plus importants - le compilo fait déjà une grande partie du boulot. En CompCert, certaines optimisations sont aussi inclues - toutes prouvées correctes vis à vis de la propriété de préservation de sémantique. Une difficulté, par contre, est que certaines optimisations (réordonnancement, déroulage de boucles, strength reduction..) sont très complexes à prouver, par conséquent on dit que CompCert est "moyennement optimisant".

 

(rédaction pas finie.. :-) )

Information sur le compte

Date d'inscription : 28 janvier 2009

Dernière connexion : 16 octobre 2019