Détermination de propriétés de flot de données pour améliorer les estimations de temps d’exécution pire-cas

Détermination de propriétés de flot de données pour
améliorer les estimations de temps d’exécution pire-cas

Analyse statique pour le WCET

L’analyse statique consiste à obtenir des propriétés d’un programme sans l’exécuter. Elle nécessite de modéliser sa structure ainsi que le système sur lequel il est exécuté.

Représentation structurelle d’un programme

En analyse statique, un programme est communément représenté sous la forme d’un graphe, appelé le Graphe de Flot de Contrôle ou Control Flow Graph (CFG) [5], illustré sur la Figure 2.3. Le CFG est une abstraction, et une surapproximation dans le sens où il représente un surensemble des chemins d’exécution réellement possibles dans le programme. Les conséquences de cette propriété des CFG sur l’évaluation du WCET sont développées dans la section 2.4 et seront un point central de cette thèse. Nous définissons d’abord la notion de bloc de base. Définition 2.1. Un bloc de base (parfois abrégé BB) est une séquence maximale d’instructions issue du programme respectant les deux conditions suivantes : (i) Un branchement (saut d’instruction) ne peut se faire qu’à partir de la dernière instruction (pas de branchement sortant de l’intérieur d’un bloc) ; (ii) Le programme ne peut entrer dans un bloc de base que par la première instruction (pas de branchement entrant à intérieur d’un bloc). Les blocs de base sont ainsi des parties de code composées d’instructions s’exécutant toujours séquentiellement. Le programme est découpé en blocs de base de manière à avoir aussi peu de blocs que possible. Nous pouvons maintenant définir un CFG. Définition 2.2. Le CFG d’un programme est un graphe orienté G = (V, E, , ω), où • L’ensemble des sommets V correspond à l’ensemble des blocs de base du programme ; • L’ensemble des arêtes E ⊆ V 2 correspond à l’ensemble des transitions possibles : ∀v1, v2 ∈ V, (v1 → v2) ∈ E si et seulement s’il existe un chemin d’exécution qui passe dans v2 immédiatement après v1. • et ω sont des blocs de base (virtuels, vides d’instructions) correspondant respectivement à l’entrée et à la sortie du programme. Dans le cas où le programme a plusieurs points d’entrée ou de sortie possibles, ces sommets sont reliés à chacun de ces points. Il est généralement admis qu’un CFG ne comporte qu’une seule composante connexe (c’est-à-dire que tous ses nœuds sont atteignables). Remarque. Lorsqu’un bloc se termine par un branchement conditionnel, et est donc relié à plusieurs arcs sortants, l’arc qui correspond à une exécution séquentielle du programme est dit non pris (la condition du branchement est fausse). Les autres arcs, représentant le cas où le branchement a eu lieu, sont dits pris. Dans les CFG de code source, il n’y a pas d’instruction de branchement explicite. Par notation, l’arc où la condition est fausse est donc annoté par un inverseur : . Nous définissons enfin les notions de chemins et de chemins d’exécution : Définition 2.3. Un chemin dans un CFG G = (V, E, , ω) (ou plus généralement dans un graphe (V, E)) est une séquence d’arêtes e1.e2 . . . en ∈ E ? consécutives, c’est-à-dire telles que ∀i ∈ [1, n − 1], ∃v, v0 , v00 ∈ V, ei = v → v 0 ei+1 = v 0 → v 00 Un chemin d’exécution dans un CFG G = (V, E, , ω) est un chemin e1.e2 . . . en ∈ E ? tel qui commence par l’entrée de G et finit par sa sortie, c’est-à-dire tel que ∃v, v0 ∈ V, e1 = → v en = v 0 → ω Le temps d’exécution pire-cas d’un programme correspond nécessairement à un chemin d’exécution : c’est le Chemin d’Exécution Pire-Cas ou Worst-Case Execution Path (WCEP). La construction de CFG peut poser quelques difficultés, ou résulter en des formes difficiles à analyser, nous poussant à effectuer des transformations conservatives des chemins d’exécution. Ce sujet sera traité plus loin en section 3.1.2, en particulier à propos du problème des boucles irrégulières, des branchements dynamiques ou des schémas d’appels récursifs

Niveau de représentation du code

L’analyse d’un programme pose la question du choix du niveau de code analysé. Plus le code est de haut niveau, plus il est facile d’en extraire la sémantique du programme. Par exemple, il est plus aisé d’obtenir les bornes de boucle sur du code source que sur de l’assembleur ; la structure du programme y est plus évidente. Certaines opérations simples dans du code source (C, par exemple) comme la division par une constante ou des additions flottantes peuvent être traduites à la compilation en code assembleur très difficile à interpréter. Ces obscures transformations peuvent être motivées par un souci d’optimisation (calcul d’une division par une constante sans boucle, par exemple) ou une nécessité due à la pauvreté du jeu d’instructions (absence de calcul flottant natif sur ARM9, par exemple). Propager des informations de flot issues du code source vers le binaire peut se révéler complexe, en particulier en présence d’optimisations [62, 63]. Les effets de ces optimisations ne peuvent pas être ignorés car, si elles améliorent le cas moyen, elles peuvent parfois aussi dégrader le WCET. D’un autre côté, l’analyse sur le code binaire est potentiellement plus précise : elle travaille directement sur la forme du programme qui sera exécutée par le processeur, est capable d’exploiter toute optimisation du compilateur et peut tracer précisément l’exécution du programme dans le matériel. Certaines parties du code n’apparaissent même qu’à la compilation : c’est le cas, par exemple, des fonctions d’émulation. Le code binaire fait également apparaître les chemins issus de l’évaluation en circuit court des expressions logiques [2], comme sur la Figure 2.4 qui représente le CFG d’un programme compilé à partir du code C if(x && y) z = 1; else z = -1;. Cette figure illustre la décomposition de l’évaluation de l’expression logique x && y en deux tests et deux branchements conditionnels, faisant apparaître un chemin d’exécution invisible dans le code source. Les avantages de cette approche motivent le choix de développer l’intégralité des travaux de cette thèse sous la forme d’analyse sur le code binaire. Un inconvénient de ce choix est que l’analyse devient propre à un jeu d’instructions assembleur en particulier. Il est toutefois possible de contourner ce problème en raisonnant par l’intermédiaire une abstraction des jeux d’instructions, comme celle qui sera proposée dans la section 3.1.1.

Table des matières

1 Introduction
2 Contexte
2.1 Temps d’exécution pire-cas (WCET)
2.1.1 Introduction : systèmes temps-réel critiques
2.1.2 Problème
2.1.3 Approches
2.2 Analyse statique pour le WCET
2.2.1 Représentation structurelle d’un programme
2.2.2 Niveau de représentation du code
2.2.3 La méthode IPET pour le WCET
2.2.3.1 Évaluation du temps d’exécution d’une instruction
2.2.3.2 Système de contraintes numériques de flot
2.2.3.3 Obtention des bornes de boucle
2.2.4 Conclusion
2.3 Interprétation abstraite
2.3.1 Introduction
2.3.2 Correspondance de Galois
2.3.3 Construction par fonctions de représentation
2.3.4 Choix du domaine abstrait
2.3.4.1 Intervalles
2.3.4.2 k-sets
2.3.4.3 CLP
2.3.4.4 Polyèdres
2.3.4.5 Conclusion
2.3.5 Notre philosophie
2.4 Chemins infaisables
2.4.1 Problématique
2.4.2 État de l’art
2.4.2.1 Pour le WCET
2.4.2.2 Pour l’amélioration de la génération de cas de tests
2.4.3 Expression et exploitation
2.5 Conclusion générale
3 Interprétation abstraite
3.1 Introduction : représentation du programme
3.1.1 Instructions sémantiques
3.1.1.1 Fondamentaux
3.1.1.2 Combinaison d’instructions sémantiques
3.1.1.3 Instruction scratch
3.1.1.4 Traduction des branchements
3.1.1.5 Conclusion
3.1.2 Graphes de flot de contrôle
3.1.2.1 Sous-programmes
3.1.2.2 Boucles
3.1.2.3 Récursivité
3.1.2.4 CFG sémantique
3.1.2.5 Branchements dynamiques
3.1.2.6 Slicing
3.2 Représentation de la machine
3.2.1 États concrets
3.2.2 Fonction d’interprétation concrète
3.3 Abstraction de la machine
3.3.1 Le domaine S
3.3.2 Le domaine S
3.4 Abstraction par prédicats
3.4.1 Le domaine eS
3.4.1.1 Définition
3.4.1.2 Concrétisation
3.4.1.3 Interprétation
3.4.2 Interprétation par les prédicats
3.4.3 Conclusion
3.5 Vers une abstraction paramétrée et composable
3.5.1 Le domaine bS0
3.5.1.1 Définition
3.5.1.2 Vue fonctionnelle
3.5.1.3 Concrétisation
3.5.1.4 Notations
3.5.2 Interprétation abstraite sur bS0
3.5.3 Le domaine bS : Introduction de variables abstraites
3.5.4 Interprétation abstraite sur bS
3.5.5 Composition
3.5.6 Concrétisation de bS
3.6 Conclusion générale
4 Flot du programme
4.1 Parcours d’un CFG acyclique
4.1.1 Parcours d’un graphe acyclique
4.1.1.1 Algorithme de base
4.1.1.2 Avec rendez-vous
4.1.1.3 Avec énumération des chemin
4.1.2 Parcours avec interprétation abstraite du programme
4.1.2.1 Interprétation sur un CFG acylique indépendant
4.1.2.2 Appels de fonction
4.2 Interprétation des boucles par point fixe
4.2.1 Introduction
4.2.2 Union abstraite
4.2.3 Notations pour les boucles
4.2.4 Méthode : calcul de point fixe
4.2.5 Formalisation et validation
4.2.6 Algorithme
4.3 Interprétation des boucles par accélération
4.3.1 Le besoin d’une interprétation efficace des boucles
4.3.2 Le domaine Sˇ
4.3.3 Accélération d’état
4.3.3.1 Principe
4.3.3.2 Formalisation
4.3.3.3 Calcul de sˆh
4.3.4 Algorithme
4.4 Discussion et conclusion
4.4.1 Discussion
4.4.2 Conclusion générale
5 Chemins infaisables
5.1 Introduction : un problème SMT
5.1.1 Les chemins infaisables, un problème de décision
5.1.2 Des états abstraits aux prédicats SMT
5.1.3 Solveurs SMT
5.1.3.1 Principe
5.1.3.2 Unsat cores
5.1.3.3 Choix du solveur
5.2 Détection et expression de chemins infaisables
5.2.1 Implémentation de la routine Ξ
5.2.2 Chemins abstraits
5.2.3 Expression de chemins infaisables dans FFX
5.2.3.1 Les conflits dans FFX
5.2.3.2 Écriture mathématique des conflits FFX
5.2.3.3 Sémantique des conflits FFX
5.2.4 Minimisation des chemins infaisables
5.2.4.1 Le fractionnement des chemins infaisables détectés
5.2.4.2 Identification d’ensembles d’arcs en conflit
5.2.4.3 Extraction d’ensembles d’arcs en conflit à partir de
sous-ensembles minimaux insatisfiables
5.2.4.4 Le problème des effets de bords
5.2.4.5 D’un ensemble d’arcs en conflits à un conflit FFX
5.2.5 Modification de la routine Ξ pour la recherche de conflits
5.2.6 Discussion
5.2.6.1 Optimisation
5.2.6.2 Limitation à Z32
5.3 Applications
5.3.1 Exploitation des chemins infaisables pour la réduction du WCET
5.3.2 Résultats expérimentaux
5.3.2.1 Benchmarks utilisés
5.3.2.2 Résultats et impact sur le WCET
5.3.2.3 Nature des chemins infaisables détectés
5.4 Conclusion générale
6 Conclusion
Annexes
A Structures et abstractions définies dans la thèse
B Sémantique abstraite complète sur bS
C Démonstration du Théorème 3.1
D Validation de ˆI par Correspondance de Galois
D.1 Construction de la correspondance de Galoi
D.2 Validation de ˆI
D.2.1 Instruction seti
D.2.2 Instruction scratch
D.2.3 Conclusion
E Concrétisation de bS0
F Démonstration du Lemme 4.1
Bibliographie