Sujets de mémoire de Master Recherche Informatique - année 2014-2015


Stages

Vérification paramétrée de systèmes temps-réel

  • Équipe EMERAUDE
  • Contact Giuseppe Lipari, e-mail
  • Remarques : Co-encadrement avec Étienne André (LIPN, Université de Paris 13, Sorbonne Paris Cité). Le stage peut être effectué au LIPN (Paris 13) ou au LIFL (Lille), en fonction du souhait du candidat. Rémunération standard.

Le contexte

Les systèmes temps réel multi-processeurs sont devenus omniprésents ces dernières années. Certains d'entre eux (pilotage automatique des avions et drones, voitures sans chauffeur) sont critiques en ce sens qu'aucune erreur ne doit survenir. Tester de tels systèmes peut éventuellement détecter la présence de bugs, mais pas en garantir l'absence. Il est alors nécessaire d'utiliser des méthodes telles que le model checking afin de prouver formellement la correction d'un système.

Le problème: ordonnancement paramétrique

Déterminer un ordonnancement (scheduling) correct des tâches effectuées par les processeurs est crucial pour la sûreté du système. Ces systèmes sont caractérisés par un ensemble de constantes temporelles, telles que la période de lecture d'un capteur d'altitude sur un drone, ou la durée minimale ou maximale d'un calcul sur un satellite. Bien que des techniques permettant de vérifier le système pour un ensemble de constantes existent, vérifier formellement le système pour de nombreuses valeurs de ces constantes peut demander un temps extrêmement long, voire infini si l'on cherche à vérifier des ensembles denses de valeurs.

Il est alors intéressant de raisonner paramétriquement, en considérant que ces constantes temporelles sont inconnues, c'est-à-dire des paramètres, et synthétiser une contrainte sur ces paramètres garantissant qu'il existe un ordonnancement des tâches à effectuer par les processeurs tel que le système est correct.

Objective du stage

L'objectif du stage est de mettre au point des techniques de vérification paramétrée de systèmes temps-réel dédiées au cas de l'ordonnancement multi-processeurs. Une implémentation sera également effectuée par l'étudiant afin de valider l'approche proposée. Une option possible est de réutiliser l'outil IMITATOR.

Plus de détails sur le sujet (en anglais).

Mots-clés

Méthodes formelles, model-checking, systèmes multiprocesseurs, ordonnancement, systèmes temps-réel, synthèse de paramètres

Compétences

Une connaissance d’un ou plusieurs des concepts suivants serait un plus, sans être indispensable pour autant : automates temporisés, scheduling, OCaml.

Références

  • [AFKS12] Étienne André, Laurent Fribourg, Ulrich Kühne, and Romain Soulat. IMITATOR 2.5 : A tool for analyzing robustness in scheduling problems. In Dimitra Giannakopoulou and Dominique Méry, editors, Proceedings of the 18th International Symposium on For- mal Methods (FM’12), volume 7436 of Lecture Notes in Computer Science, pages 33–36. Springer, August 2012.
  • [AHV93] Rajeev Alur, Thomas A. Henzinger, and Moshe Y. Vardi. Parametric real-time reasoning. In STOC 93, pages 592–601. ACM, 1993.
  • [AS13] Étienne André and Romain Soulat. The Inverse Method. FOCUS Series in Computer Engineering and Information Technology. ISTE Ltd and John Wiley & Sons Inc., 2013. 176 pages.
  • [BK08] Christel Baier and Joost-Pieter Katoen. Principles of Model Checking. MIT Press, 2008.

[SSL 13] Youcheng Sun, Romain Soulat, Giuseppe Lipari, Étienne André, and Laurent Fribourg. Parametric schedulability analysis of fixed priority real-time distributed systems. In Cy- rille Artho and Peter Ölveczky, editors, Second International Workshop on Formal Tech- niques for Safety-Critical Systems (FTSCS’13), volume 419 of Communications in Com- puter and Information Science, pages 212–228. Springer, October 2013.


Gestion de la Qualité de Service pour les applications temps réel Audio/Vidéo sous Linux

Le contexte

Les applications temps réel multimédia ont des contraintes temporelles souples. Généralement, elles se composent de plusieurs tâches concurrentes qui doivent être executées avant leurs échéances, sous peine de réduction de la qualité perçue du service par les utilisateurs.

Example I

L'application Mplayer permet de visionner sur un ordinateur des fichiers vidéo. Les "frames" vidéo et les "paquets" audio doivent être décodés puis affichés à l'écran ou envoyés à la carte son à un rythme bien précis. Le non-respect de ces échéances temporelles peut provoquer des défauts tels qu'une image qui saute ou se fige momentanément, un déclic ou un parasite dans le son, etc.

Example II

Pour produire de la musique de qualité professionnelle avec un ordinateur (MAO, Musique Assistée par Ordinateur), il est nécessaire d'utiliser des outils logiciels spécifiques. Par exemple, l'outil JACK (http://jackaudio.org/) permet de manipuler des flux (streams) audio en temps réel de manière très simple. Il est ainsi possible de faire de l'enregistrement audio multipiste et du MIDI simultanément.

Le traitement temps réel des flux audio est très sensible à la latence. Pour utiliser JACK de manière optimale, il est donc nécessaire de configurer le noyau pour une utilisation temps réel.

Le problème

Même en utilisant un noyau configuré pour le temps réel et un ordonnancement à priorités fixées, il n'est pas simple d'obtenir de bons résultats.

Un premier problème est que l'ordonnanceur temps réel requiert les droits d'administration du système (root). Par conséquent, si des processus avec des priorités temps réel s'exécutent sans jamais s'interrompre, les autres processus ne s'exécutent jamais : ils souffrent de "famine" (starvation). Un deuxième problème est qu'il n'est pas simple de choisir la priorité à affecter aux différentes tâches concurrentes temps réel.

Pour permettre à un utilisateur sans les droits d'administrateur d'utiliser les fonctionnalités temps réel, il faut empêcher qu'un processus obtienne le contrôle exclusif du processeur. Le nouvel ordonnanceur SCHED_DEADLINE, disponible dans le noyau Linux à partir de la version 3.14, à été conçu pour répondre en partie à ce problème. Avec SCHED_DEADLINE, il est possible de contraindre le temps d'exécution d'une tâche à respecter un "quota" correspondant à une fraction du temps d'exécution total du processeur. De plus, avec SCHED\_DEADLINE l'utilisateur n'a pas besoin de spécifier les priorités des tâches (elles sont calculées par l'ordonnanceur).

Il est donc possible de construire une architecture middleware pour la gestion plus efficace de la qualité de service des tâches temps réel. Cependant, l'ordonnanceur est un outil bas-niveau qui nécessite un temps d'apprentissage conséquent pour un programmeur.

Objectifs

L'objectif de ce projet est de concevoir et de réaliser une architecture logicielle pour gérer la qualité de service des applications multimedia sur Linux, basée sur le nouvel ordonnanceur SCHED_DEADLINE.

Cet objectif final ambitieux dépasse vraissemblablement le cadre de ce projet. On propose donc de concevoir un ensemble de petits outils, chacun simple et extensible. Voici une première liste, qui pourra être revue en fonction de l'évolution du projet :

  • Un outil pour mesurer les temps d'exécution des tâches gérées par SCHED_DEADLINE. On peut utiliser le module sched-deadline-spy comme point de départ.
  • Un outil pour contrôler l'admission de nouvelles tâches temps réel. L'outil est un processus "daemon" qui s'exécute avec des droits "root" et s'interface avec les tâches. Si une tâche demande à être gérée par l'ordonnancer SCHED_DEADLINE, elle envoie une requête au processus daemon qui vérifie qu'il reste suffisament de quota processeur pour accepter la requête. Si la réponse est positive, la tâche est acceptée ; sinon, la tâche est rejetée.
  • Un outil pour adapter le quota des tâches à leurs besoins, en utilisant un "feedback controller" (par exemple, comme ici: AQuOSA).
  • Une application de ces outils à JACK ou MPlayer.

Mots-clés

Linux, systèmes d'exploitation, systèmes temps-réel souples, multimedias, gestion de la Qualité du Service, ordonnancement

Compétences

Une connaissance d’un ou plusieurs des concepts suivants serait un plus: bon niveau de programmation en C/C++, programmation système, programmation concurrent et parallèle, configuration et compilation du noyaux Linux.

Références

  • [Soj11] Michal Sojka, Pavel Píša, Dario Faggioli, Tommaso Cucinotta, Fabio Checconi, Zdeněk Hanzálek and Giuseppe Lipari, "Modular software architecture for flexible reservation mechanisms on heterogeneous resources", Journal of Systems Architecture Volume 57, Issue 4, April 2011, Pages 366-382
  • [Cuc10] Tommaso Cucinotta, Luigi Palopoli, Luca Abeni, Dario Faggioli, Giuseppe Lipari, "On the integration of application level and resource level QoS control for real-time applications," IEEE Transactions on Industrial Informatics, vol 6, issue 4, pp. 479-491, Nov. 2010, DOI: 10.1109/TII.2010.2072962
  • [Aqu09] Luigi Palopoli, Tommaso Cucinotta, Luca Marzario, Giuseppe Lipari, "AQuoSA - adaptive quality of service architecture." Softw., Pract. Exper. 39(1): 1-31 (2009)
  • [Lel11] Juri Lelli, Giuseppe Lipari, Dario Faggioli, and Tommaso Cucinotta. An efficient and scalable implementation of global EDF in Linux. In Proceedings of the International Workshop on Operating Systems Platforms for Embedded Real-Time Applications (OSPERT), 2011

Auteur: Giuseppe Lipari

Created: 2017-05-15 lun. 16:24

Validate