Evaluation symbolique de pire temps d'exécution avec contextes globaux – Sywext

Les systèmes temps-réel critiques sont des systèmes dont la correction ne dépend pas seulement de la correction des résultats produits, mais aussi du moment où ils sont produits. Ces systèmes sont représentés par un ensemble de tâches, soumises à des contraintes temporelles. Pour garantir le respect de ces contraintes, une analyse de WCET (Worst-Case Execution Time) doit être faite. Le calcul de WCET par analyse statique produit une borne supérieure sur-approximée du pire temps d'exécution de la tâche. Le WCET est normalement calculé sous forme d'une valeur constante, mais nous pensons qu'il serait utile de calculer un WCET symbolique, exprimé sous forme d'une formule dépendant de paramètres.

La plupart des analyses de WCET existantes utilisent soit la méthode IPET, qui est difficile à calculer paramétriquement, soit (plus rarement) des approches à base d'arbres, qui sont peu précises et nécessitent le code source. Malgré les limitations des approches existantes à base d'arbres, nous croyons qu'elles sont plus adaptées pour le calcul paramétrique. L'objectif du projet est de lever ces limitations, et de concevoir une approche à base d'arbre, fonctionnant avec le binaire uniquement, permettant la prise en compte précise d'un vaste éventail d'effets temporels liés au matériel et au logiciel, avec un temps de calcul raisonnable.

Nous avons atténué les limitations des approches à base d'arbre dans des travaux précédents, où nous avons proposé un modèle à base d'arbre et son évaluation pour le WCET symbolique. Ce modèle à base d'arbre représente deux types de propriétés : 1) des propriétés structurelles, représentées par la structure de l'arbre, qui expriment l'ensemble des chemins d'exécution structurellement faisables; 2) propriétés non-structurelles, représentées par des annotations contextuelles, qui enlèvent les chemins d'exécutions structurellement faisables, mais sémantiquement infaisables.

Ces travaux sont prometteurs, mais ne sont que des résultats préliminaires : les annotations contextuelles sont limitées à des contextes locaux, ce qui est suffisant pour représenter certaines propriétés limitée. Des propriétés importantes ne peuvent pas être représentées, car qu'elles nécessitent de modéliser des relations entre des éléments éloignés du programme analysé (contextes globaux). Le but du projet est de généraliser notre approche pour gérer des contextes globaux. C'est un objectif ambitieux car cela nécessite de concevoir un modèle avec une expressivité suffisante pour représenter les informations fournies par un vaste ensemble d'analyses, tout en fournissant une analyse précise de ce modèle qui garde une complexité de calcul faible.

Les analyses de WCET traditionnelles sont précédées par ce que nous appelons des "analyses auxiliaires", qui déterminent des informations temporelles liées au matériel (cache, pipeline, etc.) et logicielles (bornes de boucles, chemins infaisables, etc.) Les résultats de ces analyses doivent être représentées dans notre modèle d'arbre. Le projet débutera par une étude des analyses auxiliaires, la conception d'un modèle d'annotations contextuelles globales, et l'expression des résultats de ces analyses dans notre formalisme d'annotations.

Puis nous concevrons un moyen d'évaluer notre modèle. Cela inclut des transformations d'arbres (préservant le WCET) qui simplifieront le calcul, et des heuristiques permettant d'éliminer les informations moins importantes pour alléger la complexité d'analyse.

Nous évaluerons nos résultats en les comparant à des analyses de WCET traditionnelles, sur un ensemble réaliste de benchmarks, sur des critères pertinents tels que le temps d'analyse et la précision du WCET.

Ce projet permettra le développement d'un outil opensource d'analyse, et les résultats seront publiés dans des journaux et conférences dans les domaines du temps-réel.