aiT, comment ça marche ?

Phases du calcul de WCET

aiT, l’outil WCET d’AbsInt, détermine la WCET d’une tâche de programme en différentes phases :

  1. Reconstruction du graphe de flot de contrôle à partir d’un programme binaire.
  2. L’analyse de valeur calcule les plages (ranges) de valeurs des registres et les plages d’adresses pour les instructions accédant à la mémoire.
  3. L’analyse de cache classifie les références mémoire comme misses ou hits de cache.
  4. L’analyse de pipeline prédit le comportement du programme sur le pipeline du processeur.
  5. L’analyse de chemin détermine le chemin d’exécution au pire cas du programme.
  6. L’analyse de bornes de boucles détermine les limites supérieures pour le nombre d’itérations de boucles simples.

L’analyse de cache utilise les résultats de l’analyse de valeur pour prédire le comportement du cache. Les résultats de l’analyse de cache sont utilisés au sein de l’analyse pipeline autorisant la prédiction de pipeline stalls dûs à des misses de cache. Les résultats combinés des analyses cache et pipeline constituent la base pour le calcul des temps d’exécution de chemins de programme.

Diviser la détermination WCET en différentes phases permet d’utiliser différentes méthodes adaptées aux sous-tâches. L’analyse de valeur, l’analyse de cache, ainsi que l’analyse de pipeline sont effectuées selon le principe d’interprétation abstraite, une méthode basée sur la sémantique pour l’analyse statique de programmes. La programmation linéaire en nombres entiers est utilisée pour l’analyse de chemin.

Reconstruction du graphe de flot de contrôle

Le point de départ de notre framework d’analyse est un programme binaire et un fichier .ais contenant des informations supplémentaires fournies à l’utilisateur comprenant le nombre d’itérations de boucles, les bornes supérieures pour la récursion, etc.

Dans une première étape, un parseur lit l’exécutable et reconstruit le flot de contrôle. Ceci néces­site des informations sur le processeur, par exemple quelles instruc­tions représentent les branches ou les appels. Le flot de contrôle reconstruit est annoté avec les informations demandées par les analyses suivantes, et ensuite traduit en CRL (Control Flow Representation Language), un format intermédiaire conçu pour simplifier l’analyse et l’optimisation au niveau exécutable / assemblage. Ce graphe de flot de contrôle annoté constitue l’input pour l’analyse de la micro-architecture.

Analyse de valeur

L’analyse de valeur tente de déterminer les valeurs dans les registres de processeur pour chaque point de programme, et chaque contexte d’exécution. Elle ne peut souvent pas déterminer ces valeurs de façon exacte, et ne trouve que les bornes inférieures et supérieures sûres, càd les intervalles qui contiennent de façon sûre les valeurs exactes. Les résultats de l’analyse de valeur sont utilisés pour déterminer les adresses possibles des accès indirects à la mémoire, importants pour l’analyse de cache, et dans l’analyse de bornes de boucles.

Analyse de cache

L’analyse de cache classifie les accès à la mémoire principale.

Analyse de pipeline

Visualization of pipeline analysis results for one instructionL’analyse de pipeline modélise le comportement pipeline afin de déterminer les temps d’exécution pour les flots séquentiels (blocs de base) d’instructions. Elle prend en compte l’état (ou les états) actuel(s) de pipeline, plus particulièrement l’occu­pation des ressources, les contenus des prefetch queues, le groupage d’instructions, ainsi que la classification de références mémoire par l’analyse cache. Le résultat est un temps d’exécution pour chaque bloc de base, dans chaque contexte distinct d’exécution.


Evaluation gratuite

Commandez votre version d’évaluation gratuite aujourd’hui ou bien contactez nos distributeurs officiels :