Amphi H, Ensimag
1er décembre 2017 - 10h00
Analyse temporelle des systèmes temps-réels sur architectures pluri-cœurs avec application à un processeur industriel (Phd Defense)
par Hamza RIHANI de Univ. Grenoble Alpes / Verimag
Résumé : La prédictibilité est un aspect important des systèmes temps-réel critiques. Garantir la fonctionnalité de ces systèmes
passe par la prise en compte des contraintes temporelles. Les architectures mono-cœurs traditionnelles ne sont plus
suffisantes pour répondre aux besoins croissants en performance de ces systèmes. De nouvelles architectures multi-cœurs
sont conçues pour offrir plus de performance mais introduisent d'autres défis. Dans cette thèse, nous nous intéressons
au problème d’accès aux ressources partagées dans un environnement multi-cœur.
La première partie de ce travail propose une approche qui considère la modélisation de programme avec des formules de
satisfiabilité modulo des théories (SMT). On utilise un solveur SMT pour trouver
un chemin d’exécution qui maximise le temps d’exécution. On considère comme ressource partagée un bus utilisant une
politique d’accès multiple à répartition dans le temps (TDMA). On explique comment la sémantique du programme analysé
et le bus partagé peuvent être modélisés en SMT. Les résultats expérimentaux montrent une meilleure précision en
comparaison à des approches simples et pessimistes.
Dans la deuxième partie, nous proposons une analyse de temps de réponse de programmes à flot de données synchrones
s'exécutant sur un processeur pluri-cœur. Notre approche calcule l'ensemble des dates de début d'exécution et des temps
de réponse en respectant la contrainte de dépendance entre les tâches. Ce travail est appliqué au processeur pluri-cœur
industriel Kalray MPPA-256. Nous proposons un modèle mathématique de l'arbitre de bus implémenté sur le processeur. De
plus, l'analyse de l'interférence sur le bus est raffinée en prenant en compte : (i) les temps de réponse
et les dates de début des tâches concurrentes, (ii) le modèle d'exécution, (iii) les bancs
mémoires, (iv) le pipeline des accès à la mémoire. L'évaluation expérimentale est réalisé sur des
exemples générés aléatoirement et sur un cas d'étude d'un contrôleur de vol
