Modélisation du comportement temporel du pipeline pour le calcul de WCET

The computation of the Worst Case Execution Time (WCET) is an essential step for the verification and certification of critical real-time embedded systems. The execution time at the precision of processor cycle is determined by the micro-architecture of the processor executing the programs. However, modern processors tend to be more and more complex: they are pipelined and equipped with several acceleration mechanisms, like caches, branch predictors, etc. These mechanisms introduce timing variations that must be taken into account when computing the execution time. For example, the latency of a cache access depends on rather the data that is being loaded is present (Hit) or not (Miss) in the cache. By combining the pipeline and the acceleration mechanisms, execution time becomes a complex function of instructions, pipeline structure, and timing variations. In this thesis, we present a new data structure named XDD (eXecution Decision Diagram) which allows to efficiently and accurately represent the relationship between execution time and timing variations. As its name suggests, it is inspired by BDDs (Binary Decision Diagrams). Using XDDs, we present a model for computing the execution time in the processor pipeline, which represents efficiently this complex function of execution time by a set of matrices associated with the blocks of machine instructions composing the program. It is then possible to compute efficiently the set of timing states along the execution paths of the program and to deduce the WCET therefrom. We experimented this model on classical benchmarks (TACLe), for in-order processors, as well as for processors containing out-of-order resources (memory bus). The experimental results showed a significant improvement in the accuracy of the computed WCET compared to the original method used in the OTAWA tool as well as a significant improvement in terms of analysis time.Le calcul du pire temps d'exécution (WCET, Worst Case Execution Time) est une phase indispensable pour la vérification et la certification des systèmes embarqués strictement temps-réel. Le temps d'exécution des programmes, dont l'évaluation nécessitant une précision au niveau du cycle machine, est le produit du fonctionnement de la micro-architecture du processeur qui exécute le programme. Cependant, les processeurs modernes tendent à être de plus en plus complexes : ils sont équipés de pipelines et de mécanismes d'accélération comme les mémoires caches, la prédiction de branchement, etc. Ces mécanismes introduisent des variations temporelles qu'il est nécessaire de prendre en compte lors du calcul du temps d'exécution. Par exemple, la latence d'accès à une mémoire cache est différente qu'elle contient la donnée (Hit) ou non (Miss). En combinant le pipeline et les mécanismes d'accélération, le temps d'exécution devient une fonction complexe des instructions, de la structure du pipeline et des variations temporelles. Dans cette thèse, nous proposons une nouvelle structure de données nommée XDD (eXecution Decision Diagram) qui permet de représenter efficacement et précisément la relation entre le temps d'exécution et les variations temporelles. Comme son nom l'indique, cette représentation est inspirée des BDD (Binary Decision Diagrams). À l'aide des XDD, nous proposons un modèle de calcul du temps dans le pipeline qui représente de manière compacte cette fonction temporelle complexe sous forme d'un ensemble de matrices associées aux blocs d'instructions machine composant le programme. Il est alors possible de calculer l'ensemble des états temporels tout au long des chemins d'exécution du programme de manière efficace et d'en déduire le WCET. Nous avons expérimenté ce modèle sur des benchmarks classiques (TACLe) pour des processeurs avec exécution dans l'ordre du programme, ainsi que pour des processeurs contenant des ressources allouées dans le désordre (bus mémoire). Les résultats expérimentaux montrent une amélioration significative de la précision du WCET calculé par rapport à la méthode originale utilisée dans l'outil OTAWA, ainsi qu'une amélioration importante des performances de calcul