Jeudi 18 décembre 2014 à 10h Vladimir Paun soutient sa thèse intitulée "Détermination des pire-temps d’exécution (WCET) pour des plateformes embarquées par analyse statique".
Résumé de la thèse :
La détermination précise de pires temps d’exécution (WCET) est un sujet de grand intérêt pour les systèmes embarqués critiques. Le sujet de la Thèse adresse des problèmes qui ne sont pas résolus dans la littérature notamment l’inertie notable dans le changement de plateformes cibles des analyseurs existant et la perte de précision l’hors du passage à l’échelle.
Nos travaux se concentrent justement sur une souplesse au changement du processeur à analyser et la maitrise de la perte de précision à l’aide d’un nouvel langage de modélisation du matériel qui se trouve en étroit lien avec l’analyseur même.
Une estimation sûre du WCET nécessite la prise en compte du matériel sur lequel le programme est exécuté. Les processeurs embarqués dans les systèmes critiques présentent des composants qui ont été conçu non pas pour faciliter leur analyse mais pour maximiser les performances moyennes, introduisent une variabilité temporelle significative. Le temps d'exécution est donc dépendent, entre autre des valeurs effectives de données mais aussi de l'historique d'exécution. Le but étant d'estimer le pire temps d'exécution, l'option de supposer que à chaque fois l'optimisation ne se produit pas et que le pire temps possible est nécessaire conduit à une surestimation trop importante.
A ce problème se rajoute aussi le fait que nous ne pouvons pas supposer que un pire temps local (par exemple le nombre de cycles pendant une micro-opération du pipeline) contribuera au vrai pire temps global au cause des anomalies temporelles auxquelles des processeurs. Tous les chemins d'exécution, engendrés par la totalité des entrées possibles doivent donc être analysés. Le fait de devoir gérer cette explosion combinatoire, nous a guidé dans les choix de conception du modèle utilisé pour simuler le processeur. Nous avons conçu une méthode de spécification et d'analyse de systèmes, basée sur la méthode des abstract state machines (ASM). L'extension HiTAsm consiste en l'incorporation des notions de hiérarchie et de temporalité, pour pouvoir gérer l'explosion combinatoire en choisissant une définition d'un composant parmi plusieurs niveaux d'abstraction possibles et pour pouvoir estimer le temps écoulé entre chaque transition des états du système. Cela permet l'estimation de la consommation temporelle et la variation dynamique du niveau d'abstraction du système analysé, afin d'analyser un grand nombre d'états, tout en minimisant la perte de précision. Le modèle du processeur et l'analyseur sont complètement séparés, ce qui est nécessaire pour rendre l'outil adaptable aux changements de plateforme. L'analyseur est basé sur une exécution symbolique conjointe du binaire et du modèle de processeur spécifié avec HiTAsm.
En partant des valeurs symboliques, toutes les entrées possibles du binaire sont analysées, en utilisant des sur-approximations uniquement quand c'est nécessaire de manière à minimiser la perte de précision et fournir le pire-temps d’exécution du programme le plus proche de la valeur théorique.
Infos pratiques :
Lieu : ENSTA ParisTech - salle 1.3.24
Heure : 10h