CTL
10 juillet 2013 - 14h00
Certification d'un simulateur de jeu d'instructions (Phd Defense)
par Xiaomu Shi de VERIMAG UJF
Résumé : Cette thèse expose nos travaux de certification d'une partie d'un
programme C/C++ nommé SimSoC (Simulation of System on Chip), qui
simule le comportement d'architectures basées sur des processeurs tels
que ARM, PowerPC, MIPS ou SH4. Un tel simulateur peut être utilisé
pour developper le logiciel d'un système embarqué spécifique, afin de
raccourcir les phases des développement et de test, en particulier
quand la vitesse de simulation est réaliste (environ 100 millions
d'instructions par seconde par coeur dans le cas de SimSoC).
SimSoC est un logiciel complexe, comprenant environ 60000 de C++,
intégrant des parties écrites en SystemC et des optimisations non
triviales pour atteindre une grande vitesse de simulation. La partie
de SimSoC dédiée au processeur ARM, l'un des plus répandus dans le
domaine des SoC, transcrit les informations contenues dans un manuel
épais de plus de 1000 pages. Les erreurs sont inévitables à ce niveau
de complexité, et certaines sont passées au travers des tests
intensifs effectués sur la version précédente de SimSoC pour l'ARMv5.
Un problème critique se pose alors : le simulateur simule-t-il
effectivement le matériel réel ? Pour apporter des éléments de
réponse positifs à cette question, notre travail vise à prouver la
correction d'une partie significative de SimSoC, de sorte à augmenter
la confiance de l'utilisateur en ce similateur notamment pour des
systèmes critiques.
Nous avons concentré nos efforts sur un composant particulièrement
sensible de SimSoC : le simulateur du jeu d'instructions de l'ARMv6,
faisant partie de la version actuelle de SimSoC.
Les approches basées sur une sémantique axiomatique (logique de Hoare
par exemple) sont les plus répandues en preuve de programmes
impératifs. Cependant, nous avons préféré essayer une approche moins
classique mais plus directe, basée sur la sémantique opérationnelle de
C: cela était rendu possible en théorie depuis la formalisation en Coq
d'une telle sémantique au sein du projet CompCert et mettait à notre
disposition toute la puissance de Coq pour gérer la complexitité de la
spécification. À notre connaissance, au delà de la certification d'un
simulateur, il s'agit de la première expérience de preuve de
correction de programmes C à cette échelle basée sur la sémantique
opérationnelle.
Nous définissons une représentation du jeu d'instruction ARM et de ses
modes d'adressage formalisée en Coq, grâce à un générateur automatique
prenant en entrée le pseudo-code des instructions issu du manuel de
référence ARM. Nous générons également l'arbre syntaxique abstrait
CompCert du code C simulant les mêmes instructions au sein de
Simlight, une version allégée de SimSoC.
À partir de ces deux représentations Coq, nous pouvons énoncer et
démontrer la correction de Simlight, en nous appuyant sur la
sémantique opérationnelle définie dans CompCert. Cette méthodologie a
été appliquée à au moins une instruction de chaque catégorie du jeu
d'instruction de l'ARM.
Au passage, nous avons amélioré la technologie disponible en Coq pour
effectuer des inversions, une forme de raisonnement utilisée
intensivement dans ce type de situation.
Jury :
- Yves Bertot
- Sandrine Blazy, rapporteur
- Vania Joloboff, co-directeur
- Xavier Leroy
- Laurent Maillet-Contoz
- Claude Marché, rapporteur
- Jean-François Monin, directeur
- Frédéric Rousseau
