2010

Sous-typage coercitif en présence de réductions non-standards dans un système aux types dépendants

Par Marie-Magdeleine Lionel (DALI, Univ. de Perpignan Via Domitia) le 2010-12-10

• La théorie des types est une discipline au croisement de la logique, des mathématiques et de l'informatique. Elle peut servir de support au développement de programme "zéro faute". L'objet de cette thèse est d'étudier l'extension d'un système aux types dépendants UTT (comprenant notamment des types inductifs) par une relation de récriture concernant un fragment du calcul, à savoir les types finis.

• Nous nous assurons d'abord que les propriétés de normalisation forte, de confluence et de préservation du type sont toujours préservées malgré l'ajout de la réduction.

• Ensuite nous enrichissons ce système par la notion de sous-typage coercitif vue comme un mécanisme d'abréviation et effectuons la preuve de conservativité pour le système enrichi du sous-typage par rapport au système de base.

• L'intérêt d'un tel système est qu'il améliora l'efficacité des assistants à la preuve et offrira un bon cadre pour l'étude des problèmes faisant intervenir des ensembles finis (combinatoire, manipulation de graphe etc).

An Abstract Interpretation Based Tool for Optimization of Numerical Expressions in LUSTRE Programs

Par Ioualalen Arnault (DALI, Univ. de Perpignan Via Domitia) le 2010-11-18

• L'implémentation de compilateurs dit "sûrs" représente un intérêt crucial pour les fabricants de systèmes critiques (avions, centrales...). Toutefois ce type de propriétés sont souvent indécidables et donc, ne peuvent être obtenues directement. Le projet SARDANES a pour but de produire un compilateur défini pour le langage LUSTRE, et qui permette à la fois de certifier l'erreur numérique que commet le programme par rapport à sa spécification mathématique, mais aussi de réduire cette erreur en ré-écrivant ses expressions numériques. Pour atteindre ces deux objectifs notre outil utilise le cadre de l'interprétation abstraite définit par Cousot et Cousot, et celui des Program Expansion Graph introduit par Tate, Stepp, Tatock et Lerner. Cet exposé a pour but de présenter : les premiers résultats intéressants qui ont été obtenus sur des parties de programme (les expressions), de même que l'état d'actuel de l'outil, mais aussi ses futurs améliorations qui sont en cours.

Vérification de contraintes temporelles strictes sur des programmes par composition d'analyses partielles

Par Ballabriga Clément (IRIT, Université Paul Sabatier, Toulouse) le 2010-10-21

• Les systèmes temps-réel critiques, de plus en plus utilisés dans l'industrie, doivent obéir à des contraintes temporelles strictes, sans quoi les conséquences peuvent être désastreuses. Le respect de ces contraintes temporelles doit être prouvé, et le calcul de pire temps d'exécution (WCET ou Worst Case Execution Time) joue un rôle important dans le processus de validation.

• Le calcul de WCET par analyse statique est traditionnellement réalisé sur un programme entier. Cette approche présente deux inconvénients principaux. Premièrement la plupart de ces méthodes de calcul voient leur temps d'exécution augmenter de manière non linéaire par rapport à la taille de la tâche à analyser, deuxièmement cette approche est problématique lorsque la tâche à analyser est constituée de plusieurs composants, dont certains ne sont pas disponibles au moment de l'analyse.

• Pour ces raisons, il est nécessaire d'introduire une approche d'analyse partielle, permettant d'analyser séparément plusieurs composants d'un programme, produisant un résultat de WCET partiel associé à chaque composant. Ces résultats partiels peuvent ensuite être composés pour obtenir le WCET du programme.

• Le calcul de WCET par analyse statique fait intervenir plusieurs analyses pour modéliser le flot de contrôle du programme ainsi que les effets temporels liés au matériel utilisé, puis ces résultats sont exprimés sous forme d'un système ILP qui est ensuite résolu pour obtenir le WCET. Chaque analyse impliquée dans le WCET doit être adaptée pour faire de l'analyse partielle, ceci sera illustré à l'aide de diverses analyses existantes (cache d'instructions, bornes de boucles, prédiction de branchement), et une formulation plus générale pour l'analyse partielle sera ensuite donnée. Il sera également montré qu'il est possible de tirer parti de l'analyse partielle afin de réduire le temps de résolution ILP. Les résultats expérimentaux, exposés à la fin de la présentation, montrent que l'analyse partielle permet de réduire de manière significative le temps de calcul du WCET et de traiter de manière satisfaisante les programmes comportant plusieurs composants, tout en gardant l'accroissement du pessimisme très faible.

Techniques for the automatic debugging of scientific floating-point programs

Par Revy Guillaume (DALI, Université de Perpignan Via Domitia) le 2010-09-23

• On assiste depuis plusieurs années au développement considérable du domaine des applications scientifiques à grande échelle : au niveau de la complexité des applications, mais également au niveau de la performance des architectures sur lesquelles on souhaite utiliser ses applications (architectures de plus en plus performantes). Ceci rend la phase de déboguage de ce type d'applications de plus en plus compliquée.

• Également, les erreurs d'arrondi dues à l'utilisation de l'arithmétique flottante restent difficiles à déboguer, particulièrement pour les développeurs non experts en analyse numérique.

• L'objectif du projet est donc de proposer un ensemble de techniques et d'outils pour réduire la difficulté du déboguage des applications scientifiques utilisant l'arithmétique flottante, en aidant les développeurs, qui soupçonnent une erreur dans leur programme, à localiser automatiquement cette erreur et à la corriger.

• Après une description des motivations et objectifs du projet, je présenterai les travaux que nous avons effectués sur l'isolation d'erreurs numériques dans les applications utilisant l'arithmétique flottante. La technique utilisée se base essentiellement sur des transformations de code et la détermination de changements à appliquer sur ce code pour améliorer sa précision et se rapprocher d'un résultat attendu. J'illustrerai ensuite l'utilisation de ces techniques sur la correction de bogues dans la bibliothèque LAPACK, avant de terminer par un ensemble de perspectives.

Combinaison d'analyses: un interprète abstraite comme oracle dans une procédure de k-induction

Par Garoche Pierre-Loïc (ONERA, Toulouse) le 2010-06-29

• Bien qu'assez anciennes, les problématiques autour de la satisifiabilité de formules booléenes (SAT) et/ou arithmétiques (SMT) continuent d'intéresser de nombreuses équipes de recherches, et les outils ne cessent de s'améliorer, permettant de traiter de plus en plus rapidement des systèmes de taille considérable. L'utilisation de ces analyses, via le principe de k-induction, proposé par de Moura lorsqu'il était au SRI, a également montré ses preuves et en aujourd'hui au cœur d'outils de vérification commerciaux. Cette méthode qui peut être vue comme une généralisation outillée du principe d'induction, permet de reposer sur de la vérification bornée de modèles (BMC) pour garantir des propriétés de sûreté (invariant) sur des systèmes. Dans cette présentation, nous introduirons les principes de la k-induction et présenterons notre approche d'analyse dans laquelle la k-induction est renforcée par l'appel à un interprète abstrait.

Outils d'analyse de performances

Par Bouache Mourad (Université de Perpignan - DALI et Université de Boumerdès, Algérie) le 2010-06-28

• La simulation est largement utilisée dans de nombreux domaines de la science et de l'ingénierie. Elle est particulièrement utile dans l'expérimentation afin d'évaluer la performance d'un nouveau système. Un bon simulateur offre un mécanisme souple et pratique dans le système a simuler. Un domaine de l'ingénierie informatique principalement touché par les simulations est l'architecture des ordinateurs. La quête de processeurs performants implique de nombreuses décisions d'ingénierie, ces décisions sont souvent basées sur les résultats de la simulation. L'évaluation quantitative des futurs processeurs est souvent difficile, voire impossible, sans simulation. Dans l'industrie, le processeur consacre plusieurs mois de cycles de conception, de simulation et d'analyse des différents aspects comme la consommation d'énergie et de la performance avant toute réalisation dans le silicium. Afin d'aider l'exploration rapide de l'espace de conception, des simulations sont réalisées pour la vérification fonctionnelle de la conception et à la réalisation. La plupart des simulateurs sont sensiblement lents en terme de temps de simulation. La vitesse de simulation est un facteur critique en particulier parce qu'elle limite l'étendue des solutions qui peuvent être évaluées par les architectes de processeurs. L'objectif de cette thèse est de présenter deux outils d'analyse de performances afin d'explorer mieux l'espace de conception. Le premier outil a été développé avec une méthodologie simple et systématique de développement basée sur un nouveau protocole de communication au niveau cycle : la vectorisation de module. Cette méthodologie améliore considérablement la vitesse de simulation et permet aux simulateurs de passer à l'échelle dans le cas d'architectures dont la complexité est basée sur la duplication des ressources. Le deuxième outil d'analyse de performance développé dans le cadre de cette thèse mesure l'ILP(Instruction Level Parallelism). Le calcul d'ILP est une caractéristique totalement indépendante de la micro-architecture sur lequel le programme s'exécute. Nous avons développé deux outils de deux architectures différentes (Intel x86 et PowerPC) qui permettent d'effectuer l'analyse d'un programme.

Linear algebra algorithms for multicore and/or massively parallel architectures

Par Haidar Azzam (University of Tennessee, TN, USA) le 2010-05-11

• This talk will consider two main topics. First is the study of a numerical technique that has attractive features for an efficient solution of large scale sparse linear systems on large parallel platforms. The robustness and the weak scalability of the method will be illustrated through extensive parallel experiments on up to two thousand processors and for solving up to a 75 millions unknown problem. I will also consider an approach based on two levels of parallelism, that offers the flexibility to combine the numerical and the parallel implementation scalabilities. Consequently such a numerical technique appears as a promising candidate for inten- sive simulations on large massively parallel platforms. The robustness and parallel numerical performance of this approach is reported on large challenging linear systems arising from electromagnetism and structural mechanics. The second direction of this talk will be devoted to the description of the 3rd generation of dense linear algebra algorithms on the future shared-memory, multicore architectures. Current numerical libraries, e.g., LAPACK, show clear limitations on such emerging systems mainly due to their coarse granularity tasks. Thus, many numerical algorithms need to be redesigned to better fit the architectural design of the multicore platform.

Algorithmes à front d'onde et accès transparent aux données

Par Clauss Pierre-Nicolas (LORIA - Algorille) le 2010-05-04

• Beaucoup d'applications scientifiques courantes sont basées sur des algorithmes à front d'onde. La comparaison de séquences génétiques en biologie, l'algèbre linéaire en analyse numérique et la propagation de flux en physique sont autant d'exemples de telles applications. Ces algorithmes ont la caractéristique d'effectuer un calcul sur un espace de données discret en prenant en compte les éléments proches à une distance finie données. Originellement écrites de manière séquentielle, les applications basées sur ces algorithmes peuvent être parallélisées par des techniques de macro-pipelining. Par un découpage préalable des données, les calculs peuvent être réalisés en parallèle sur des sous-ensembles de données qui ne s'impactent pas directement entre eux. La mise en évidence de ces sous-ensembles fait apparaître une onde qui semble traverser l'espace de données et qui donne leur nom à ces algorithmes. Mes travaux de thèse ont consisté à analyser le fonctionnement et maximiser les performances des algorithmes à front d'onde dans un contexte d'exécution dit out-of-core, c'est-à-dire la quantité de données à traiter dépasse la capacité de la mémoire locale. Pour répondre à cette problématique, mes contributions sont orientées selon deux axes : l'accès performant aux données sur disque et la synchronisation simple et transparente des accès. Ces deux apports ont été validés formellement et expérimentalement sur un benchmark classique d'un algorithme à front d'onde opérant sur un espace de données bi-dimensionnel : l'algorithme du Livermore Kernel 23, qui fait partie de la collection LINPACK.

Validation des spécifications de systèmes de contrôle-commande

Par Chapoutot Alexandre (Université Paris 6 - LIP6) le 2010-04-29

• La conception de systèmes embarqués nécessite de plus en plus l'utilisation d'outils logiciels afin de contenir la complexité croissante de ceux-ci. Le principal outil industriel dans ce domaine est Simulink. Pour la conception des systèmes embarqués, Simulink permet de modéliser l'environnement physique et le logiciel embarqué dans un même formalisme. L'application des méthodes formelles sur de telles spécifications permet de valider les logiciels embarqués en étant au plus près de leurs modes de fonctionnement. Nous présentons une analyse statique par interprétation abstraite de modèles Simulink. L'objectif de cette analyse est de calculer automatiquement et conjointement une sur-approximation des comportements mathématiques et des comportements issus de la simulation numérique pour une plage d'entrées possibles. Nous sommes ainsi capable d'estimer l'ensemble des imprécisions introduit par la simulation numérique, c'est-à-dire les erreurs d'arrondi ou les erreurs de troncature liées, par exemple, aux capteurs.

Calcul itératif asynchrone à grande échelle sur des architectures hétérogènes et volatiles

Par Charr Jean-Claude (NRIA - Lille) le 2010-04-27

• Avec l'émergence de nouvelles architectures distribuées, comme les grappes de calcul distantes et les architectures de calcul volontaire, il apparaît important de définir des algorithmes et des intergiciels bien adaptés à ces architectures. En effet, l'utilisation de ces plate-formes introduit plusieurs nouvelles contraintes par rapport à un contexte de grappes locales homogènes : hétérogénéité des machines, hétérogénéité des réseaux, volatilité des noeuds de calcul, etc. Dans ce contexte, plusieurs travaux montrent que pour les algorithmes itératifs il peut être préférable d'utiliser les algorithmes IACA (Itérations Asynchrones avec Communications Asynchrones) pour lesquels les communications sont recouvertes par du calcul et la perte des messages de données est tolérée. Les travaux qui seront présentés concernent la conception et la mise en oeuvre d'une plate-forme dédiée à l'exécution d'algorithmes IACA sur des architectures distribuées, hétérogènes et volatiles. Cette plate-forme, JACEP2P-V2, est tolérante aux pannes et décentralisée. Elle offre un mécanisme de communications asynchrones et un mécanisme de détection de la convergence globale adapté aux caractéristiques des algorithmes IACA. De plus, nous reportons des expérimentations au cours desquelles nous résolvont des systèmes linéaires et non linéaires avec des méthodes parallèles, itératives et asynchrones (comme la multi-décomposition et la relaxation d'ondes). Ces expérimentations sont menées sur des grappes hétérogènes volatiles et distantes afin d'évaluer l'efficacité et la robustesse de notre plate-forme. Les résultats obtenus, avec plus de 1000 coeurs de calculs, sont très encourageants et montrent que JACEP2P-V2 est extensible et performante.

Algorithmes repartis à haute performance sur grilles de calcul

Par Tantar Alexandru-Adrian (INRIA - Bordeaux) le 2010-04-06

• Les problèmes abordés au cours des dernières années dans le domaine de la bio-informatique se retrouvent à la confluence de l'optimisation et du calcul haute performance à large échelle. Dans ce cadre, le projet ANR d'échantillonnage conformationnel Docking@Grid, finalisé en 2009, s'attaquait aux aspects les plus diverses émanant de la modélisation mathématique, la bio-informatique et les algorithmes repartis à haute performance. Les sujets de cet exposé portent principalement sur la parallélisation et le déploiement des algorithmes sur grilles de calcul, notamment sur Grid'5000, une grille à l'échelle nationale. Ayant comme domaine d'application la prédiction de la structure des protéines et le problème d'amarrage moléculaire (molecular docking), plusieurs méta-heuristiques de haute complexité sont discutées (sur des aspects de parallélisation et modèles (a)synchrones, fonctions adaptatives, approches hiérarchiques, etc.) ainsi que la sélection des algorithmes et le déploiement à grande échelle des expériences sur grilles de calcul.

Using Boolean Equations and Rewriting Systems to solve Datalog-based Program Analyses

Par Joubert Christophe (Technical University of Valencia, Spain) le 2010-04-01

• In this talk, we present two powerful, fully automated methods to evaluate Datalog queries in the context of object-oriented program analyses: the first approach transforms the Datalog program in an implicit Boolean Equation Systems (BESs) solved by existing general purpose verification toolboxes, such as CADP, providing local BES resolutions with linear-time complexity; the second approach transforms Datalog programs into Rewriting Logic and produces an efficient rewrite system exploiting the main features of the high-level programming language Maude. Datalog is used as a specification language for expressing both complex interprocedural program analyses involving dynamically created objects and queries. We confirm our results experimentally by applying it to some real-world Datalog-based analyses.

Optimisation automatique des chemins de données arithmétiques par l'utilisation des systèmes de numération redondants

Par Dupuis Sophie (Université Paris 6 - LIP6) le 2010-03-18

• Depuis l'apparition des circuits intégrés dans les années cinquantes, leurs performances ont évolué de manière exponentielle. La loi de Moore, exprimée en 1975, indiquait que la densité des transistors dans les circuits intégrés doublerait tous les deux ans. Cette loi s'est révélée exacte jusqu'à nos jours. Un tel rythme d'évolution technologique implique une mise sur le marché de plus en plus rapide des composants. C'est dans ce contexte que l'utilisation d'outils optimisant les circuits de façon automatique selon un critère donné (surface, chaîne longue, etc ...) trouve toute sa signification. Ceci se vérifie principalement dans des domaines peu connus des concepteurs de circuits, tel celui de l'optimisation arithmétique. Nous présentons l'optimisation des chemins de données arithmétiques par l'intégration automatique du système des notations redondantes dans le flot de conception VLSI, de façon à le rendre plus accessible. Les travaux effectués se découpent en deux phases. La première a pour objectif d'incorporer les opérateurs redondants et le savoir-faire lié à leur usage dans la synthèse bas niveau. Différents algorithmes d'optimisation sont proposés, basés sur la redéfinition des enchaînements entre opérateurs arithmétiques. La seconde est consacrée à la mise en place de l'environnement de conception dans lequel seront utilisés ces algorithmes. Cet environnement répond aux besoins liés à l'arithmétique et fournit un langage de description de circuits ayant un haut niveau d'abstraction.

Caractérisation des déplacements de vecteurs de la maladie de Chagas et traitement informatique associé

Par Barbu Corentin (Université de Perpignan Via Domitia - CBETM) le 2010-03-11

• La maladie de Chagas est la première maladie parasitaire d'Amérique Latine. La transmission est assurée principalement par des insectes présents dans les maisons et piquant les habitants pendant leur sommeil. L'OMS recommande la lutte contre les insectes entrant dans les maisons, il est donc déterminant pour l'avenir du contrôle de la maladie d'identifier les caractéristiques du déplacement des insectes. Pour cela, j'ai mis en place un programme qui, à partir de relevés d'abondance dans les villages atteints, permet de caractériser ces déplacements par la modélisation des déplacements. Ce programme est basé sur un traitement massivement parallélisé des données qui sera présenté lors de cette présentation.

Modèle n-synchrone pour la programmation de réseaux de Kahn à mémoire bornée

Par Plateau Florence (Université Paris Sud - LRI) le 2010-02-09

• Dans cette exposé, nous nous intéressons aux modèles et aux langages pour la programmation d'applications de traitement de flux ayant des contraintes de temps-réel, comme les applications multimédias. Les langages synchrones flot de données fournissent un cadre simple pour la programmation de réseaux de processus communiquant de manière synchrone, c'est-à-dire sans buffers. Ce mode de communication permet de garantir une exécution en mémoire bornée, mais présente l'inconvénient de manquer de flexibilité. Le modèle n-synchrone est une extension du modèle synchrone qui relâche la contrainte de synchronisme de manière contrôlée. Il fournit ainsi une communication plus souple, tout en conservant les garanties statiques fortes offertes par les langages synchrones. Nous présentons un langage qui met en oeuvre le modèle n-synchrone. En particulier, nous détaillons les analyses permettant de vérifier statiquement qu'un programme est exécutable avec des buffers bornés et de calculer automatiquement leur taille.

Développement de domaines abstraits temporels pour vérifier les spécifications de systèmes embarqués

Par Bertrane Julien (Ecole Normale Supérieure - LIENS) le 2010-02-04

• Nous considérons les comportements complexes des systèmes constitués de plusieurs ordinateurs communicants, programmés dans un langage synchrone. Afin de simuler une exécution réaliste, les horloges sont supposées possiblement défaillantes et les canaux de communication non-instantanés. De tels systèmes sont utilisés pour contrôler des systèmes embarqués. Nous utilisons une sémantique à temps-continu, qui peut être abstraite pour prouver les spécifications temporelles de ces systèmes. Cette abstraction est effectuée automatiquement par un produit-réduit de plusieurs domaines abstraits. Ces domaines ont la particularité d'être temporels, c'est à dire de fournir une représentation abstraite et continue du temps. Pour ces domaines temporels, il est possible de définir des opérateurs et des produits réduits optimisés par rapport à ceux que l'on pourrait définir sans notion de temps. Par ailleurs, on peut définir des transformeurs de domaines, comme la complétion disjonctive, permettant, à partir d'un domaine abstrait, d'en générer d'autres plus précis, et cela de façon automatique.