Calcul efficace du pire temps d'exécution symbolique à base d'arbres
Efficient tree-based symbolic WCET computation
- Analyse statique de programmes
- Analyse Pire Cas
- Temps réel (informatique)
- Calcul symbolique
- Arbres (théorie des graphes)
- Worst-Case execution time
- Static analysis
- Symbolic computation
- Langue : Anglais
- Discipline : Informatique et applications
- Identifiant : 2023ULILB028
- Type de thèse : Doctorat
- Date de soutenance : 07/11/2023
Résumé en langue originale
Un système temps réel est un système informatique soumis à descontraintes de temps, et en particulier à des échéances. Les systèmestemps réels critiques sont une sous-classe de ces systèmes qui doiventimpérativement respecter leurs échéances. Dans ce genre de systèmes,manquer une échéance peut avoir des conséquences catastrophiquespouvant aller jusqu'à la perte de vies humaines. Pour s'assurer queces systèmes ne manquent jamais leurs échéances, l'analyse de piretemps d'exécution (PTE, ou WCET en anglais) calcule une limitesupérieure au temps d'exécution des programmes qui doivent êtreexécutés.Traditionnellement, l'analyse statique du PTE produit un entier quireprésente une borne supérieure au nombre de cycles du processeurnécessaires à l'exécution de ce programme. Cependant, le tempsd'exécution d'un programme peut dépendre de paramètres matériels,l'état du cache notamment, ou de paramètres logiciels, comme lesparamètres d'entrée du programme. Calculer un seul PTE sous la formed'un entier, peu importe la valeur des paramètres, est donc souventpessimiste. Pour résoudre ce problème, l'analyse paramétrique du PTEproduit une formule arithmétique qui dépend de différents paramètreschoisis. Instancier cette formule avec des valeurs pour chaqueparamètre permet d'obtenir un PTE plus précis qui prend en compte lavaleur de ces paramètres.Parmi les différentes analyses paramétriques, les techniques à based'arbres montrent une complexité faible. En effet, elles utilisent unestructure arborescente qui peut facilement être transformée en uneformule arithmétique, ce qui permet de calculer le PTE en incluant dessymboles, et donc des paramètres, de manière efficace. Néanmoins, cesapproches ont aussi des inconvénients. Tout d'abord, ces méthodes sontconnues pour leurs difficultés à tenir compte des effets descomposants matériels sur le PTE. Ensuite, elles montrent également desdifficultés à prendre en compte certains aspects sémantiques duprogramme, qui peuvent avoir un impact conséquent sur lePTE. Finalement, tout comme les autres analyses paramétriques, lesparamètres proposés doivent être déterminés par l'utilisateur.Dans cette thèse, nous étendons une technique de calcul symbolique duPTE pour aborder trois problèmes liés à des techniques de calcul dePTE paramétrique:- nous avons développé une technique qui élimine les cheminssémantiquement infaisables de la représentation du programmeutilisée pour calculer le PTE;- nous avons adapté une technique existante d'analyse de pipeline,qui fonctionne avec les techniques non paramétriques de calcul duPTE à base de graphes, afin de l'utiliser dans une techniqued'analyse paramétrique du PTE utilisant des arbres;- nous avons développé une technique paramétrique qui prendautomatiquement en compte les effets des paramètres d'entrée duprogramme sur le PTE. Cette technique produit une formule dont lesparamètres sont les paramètres d'entrée du programme et ne requiertaucune connaissance du programme de la part de l'utilisateur.
Résumé traduit
A real-time system is a computer system subject to timing constraints,and in particular to deadlines. Critical real-time systems are asubclass of those systems that absolutely must meet theirdeadlines. In such systems, missing a deadline can have disastrousconsequences and may even cause the loss of human lives. So as toensure that such a system never misses a deadline, the worst-caseexecution time (WCET) analysis computes an upper bound to theexecution time of the programs to be executed.Static WCET analysis traditionally takes a program and produces aninteger upper bound to the number of processor cycles required toexecute this program. However, the execution time of a program mayvary according to various parameters, such as hardware parameters,e.g. the state of the cache, or software parameters, e.g. input valuespassed to the program. Thus computing a single WCET, regardless of theparameter values, is often pessimistic. To overcome this issue,parametric WCET analysis produces an arithmetic formula that dependson various chosen parameters. Instantiating this formula with actualparameter values enables to produce a more precise WCET that takesinto account these parameters.Among the different parametric techniques, tree-based WCET computationtechniques have a low complexity. Indeed, they rely on a treestructure that can easily be transformed into an arithmetic formula,which enables to handle symbols, and thus parameters,efficiently. Nevertheless, these approaches also exhibit somedrawbacks. First, they struggle to take the effect of the hardwarecomponents on the WCET into account. Second, they also struggle totake some aspects of the semantic of the program into account, thatcan have a big impact on the WCET. Third, as other parametric WCETanalysis techniques, the proposed parameters must be determined by theuser.In this thesis, we extend a symbolic WCET computation technique, totackle three issues with parametric tree-based WCET computationtechniques:- We developed a technique that eliminates program paths that areinfeasible, due to the program semantic, from the programrepresentation used to compute the WCET;- We adapted an existing pipeline analysis, that works withgraph-based non-para-met-ric WCET analysis, to use it in a parametrictree-based WCET analysis;- We developed a parametric technique that automatically takesinto account the effect of the program input values on theWCET. This technique produces a formula whose parameters are theargument values passed to the program and it does not require theuser to have any knowledge about this program.
- Directeur(s) de thèse : Lipari, Giuseppe - Forget, Julien
- Président de jury : Grolleau, Emmanuel
- Membre(s) de jury : Ballabriga, Clément
- Rapporteur(s) : Moy, Matthieu - Puaut, Isabelle
- Laboratoire : Centre de Recherche en Informatique, Signal et Automatique de Lille
- École doctorale : École graduée Mathématiques, sciences du numérique et de leurs interactions (Lille ; 2021-....)
AUTEUR
- Grebant, Sandro