Anmerkungen:
Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
Beschreibung:
On utilise des logiciels pour différents rôles, parfois critiques. La présence d’un bogue dans un logiciel peut avoir un coût dévastateur, pouvant aller jusqu’à la perte de vies humaines dans les cas les plus extrêmes. Les bogues viennent en général du code source (ceux-là peuvent être détectés par des méthodes de vérification formelle sur le langage source), mais ils peuvent être également générés par le compilateur. CompCert est le premier compilateur comportant une preuve formelle de correction : il est formellement prouvé que les programmes compilés avec cet outil ont le même comportement que leurs programmes sources originels. Cependant, comme prouver les optimisations d’un compilateur relève d’un défi considérable, CompCert n’en a qu’un nombre limité. Ainsi, en général CompCert génère du code moins performant comparé à d’autres compilateurs classiques tels que GCC. Bien que cela n’impacte peu les architectures à exécution dans le désordre telles que x86, sur des architectures à exécution dans l’ordre, et en particulier sur des processeurs VLIW, le ralentissement est important (le code résultant est deux fois plus lent que GCC -O2). Sur un processeur VLIW , le parallélisme d’instructions est explicite et spécifié dans le code assembleur par des bundles (paquets) d’instructions : le compilateur doit paquétiser les instructions pour obtenir une bonne performance. Le but de cette thèse est d’identifier, d’enquêter, d’implémenter et de vérifier formellementplusieurs optimisations classiques manquantes dans CompCert. Tout d’abord, j’introduis un model formel d’exécution de bundles VLIW sur processeur à bitoduc imbriqué. Nous génèronsces bundles à partir d’un réordonnancement en postpass (après allocation de registres). Ensuite, j’introduis un réordonnancement de superblocks en prepass (avant allocation de registres). Cetravail implique aussi l’introduction d’une prédiction statique de branchements, et une duplica-tion de queue. Enfin, pour continuer d’augmenter la performance du code généré, j’introduis du ...