Séminaire  d'informatique DALI 2009-2010

Pour l'année 2009/2010, le séminaire de l'équipe DALI a lieu de préférence le mardi ou le jeudi à 14h, tous les quinze jours. La durée de l'exposé est d'une heure suivi de questions.

Séminaires de l'équipe des années précédentes (2008, 2007, 2006, 2005, 2004).

 
Responsable : Matthieu Martel


29 juin 2010 : Pierre-Loïc Garoche (ONERA, Toulouse), Combinaison d'analyses: un interprète abstraite comme oracle dans une procédure de k-induction

28 juin 2010 : Mourad Bouache (Université de Perpignan - DALI et Université de Boumerdès, Algérie), Outils d'analyse de performances

 11 mai 2010 : Azzam Haidar (University of Tennessee), Linear algebra algorithms for multicore and/or massively parallel architectures

4 mai 2010 : Pierre-Nicolas Clauss (LORIA - Algorille), Algorithmes à  front d'onde et accès transparent aux données

27 avril 2010 : Jean-Claude Charr (INRIA - Lille), Calcul itératif asynchrone à grande échelle sur des architectures hétérogènes et volatiles

6 avril 2010 : Alexandru-Adrian TANTAR (INRIA - Bordeaux), Algorithmes repartis à haute performance sur grilles de calcul

1er avril 2010 : Christophe Joubert (Technical University of Valencia, Spain), Using Boolean Equations and Rewriting Systems to solve Datalog-based Program Analyses

18 mars 2010 :  Sophie Dupuis (Université Paris VI - LIP6), Optimisation automatique des chemins de données arithmétiques par l'utilisation des systèmes de numération redondants

11 mars 2010 :  Corentin Barbu (Université de Perpignan - CBETM), Caractérisation des déplacements de vecteurs de la maladie de Chagas et traitement informatique associé

 9 février 2010 : Florence Plateau (Université Paris Sud - LRI), Modèle n-synchrone pour la programmation de réseaux de Kahn à mémoire bornée

4 février 2010 : Julien Bertrane (Ecole Normale Supérieure - LIENS), Développement de domaines abstraits temporels pour vérifier les spécifications de systèmes embarqués

26 novembre 2009 :  Nadia MRabet (Université de Montpellier 2 - LIRMM), Multiplication dans les corps finis utilisés dans les couplages sur les courbes elliptiques

19 novembre 2009 : Eric Petit (Université de Perpignan - DALI), Partitionnement automatique d’applications en codelets spéculatifs pour les systèmes hétérogènes à mémoires distribuées
 
 22 octobre 2009 :  Sylvain Collange (Université de Perpignan - DALI), LNS sur architectures exotiques




 29 juin 2010 : Pierre-Loïc Garoche (ONERA, Toulouse), Combinaison d'analyses: un interprète abstraite comme oracle dans une procédure de k-induction

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.

28 juin 2010 : Mourad Bouache (Université de Perpignan - DALI et Université de Boumerdès, Algérie), Outils d'analyse de performances

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.

11 mai 2010 :  Azzam Haidar (University of Tennessee), Linear algebra algorithms for multicore and/or massively parallel architectures

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 sys- tems 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.

4 mai 2010 : Pierre-Nicolas Clauss (LORIA - Algorille), Algorithmes à  front d'onde et accès transparent aux données

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.

29 avril 2010 : Alexandre Chapoutot (Université Paris VI - LIP6), Validation des spécifications de systèmes de contrôle-commande

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.

27 avril 2010 : Jean-Claude Charr (INRIA - Lille), Calcul itératif asynchrone à grande échelle sur des architectures hétérogènes et volatiles

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.

6 avril 2010 : Alexandru-Adrian TANTAR (INRIA - Bordeaux), Algorithmes repartis à haute performance sur grilles de calcul

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 (http://dockinggrid.gforge.inria.fr), 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 (https://www.grid5000.fr), 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.


1er Avril 2010 : Christophe Joubert (Technical University of Valencia), Using Boolean Equations and Rewriting Systems to solve Datalog-based Program Analyses

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.

18 mars 2010 : Sophie Dupuis (Université Paris VI - LIP6), Optimisation automatique des chemins de données arithmétiques par l'utilisation des systèmes de numération redondants

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.

11 mars 2010 :  Corentin Barbu (Université de Perpignan - CBETM), Caractérisation des déplacements de vecteurs de la maladie de Chagas et traitement informatique associé

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.


9 février 2010 : Florence Plateau (Université Paris Sud - LRI), Modèle n-synchrone pour la programmation de réseaux de Kahn à mémoire bornée

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.

4 février 2010 : Julien Bertrane (Ecole Normale Supérieure - LIENS), Développement de domaines abstraits temporels pour vérifier les spécifications de systèmes embarqués

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.

26 novembre 2009 :  Nadia MRabet (Université de Montpellier 2, LIRMM), Multiplication dans les corps finis utilisés dans les couplages sur les courbes elliptiques

Les couplages sur les courbes elliptiques ont de nombreuses applications cryptographiques. On peut citer par exemple le protocole d'échange de clef à trois partie ou encore des protocoles de chiffrement basé sur l'identité. L'implémentation de ces couplages nécessitent, pour un certaines classes de courbes, une longue série de multiplications et d'additions dans les corps F_p^k ou  6 <= k <= 30.  Dans cet exposé nous présenterons un algorithme de multiplication dans ces corps utilisés dans les couplages qui permet d'améliorer l'implémentation des couplages. Cet algorithme s'appuie sur la représentation de F_p dans le système AMNS (SAC04, Bajard, Imbert et Plantard) combiné à l'utilisation de la DFT pour la multiplication de polynôme de degré < k de F_p[X].

19 Novembre 2009 : Eric Petit (Université de Perpignan - DALI), Partitionnement automatique d’applications en codelets spéculatifs pour les systèmes hétérogènes à mémoires distribuées

Devant les difficultés croissantes liées au coût en développement, en consommation, en surface de silicium, nécessaires aux nouvelles optimisations des architectures monocœur, on assiste au retour en force du parallélisme et des coprocesseurs spécialisés dans les architectures. Cette technique apporte le meilleur compromis entre puissance de calcul élevée et utilisations des ressources.
 
Afin d’exploiter efficacement toutes ces architectures, il faut partitionner le code en tâches, appelées codelet, avant de les distribuer aux différentes unités de calcul. Ce partionnement est complexe et l’espace des solutions est vaste. Il est donc nécessaire de développer des outils d’automatisation efficaces pour le partitionnement du code séquentiel. Les travaux présentés dans cette thèse portent sur l’élaboration d’un tel processus de partitionnement. L’approche d’Astex est basée sur la spéculation, en effet les codelets sont construits à partir des profils d’exécution de l’application.

La spéculation permet un grand nombre d’optimisations inexistantes ou impossibles statiquement. L’élaboration, la gestion dynamique et l’usage que l’on peut faire de la spéculation sont un vaste sujet d’étude. La deuxième contribution de cette thèse porte sur l’usage de la spéculation dans l’optimisation des communications entre  processeur et coprocesseur et traite en particulier du cas du GPGPU, i.e. l’utilisation d’un processeur graphique comme coprocesseur de calcul intensif.

Mots clés : compilation, optimisation, spéculation, parallélisme, architecture multicoeur, coprocesseur, communication, GPU, manycore, HMPP, Astex


22 Octobre 2009 :  Sylvain Collange (Université de Perpignan - DALI), LNS sur architectures exotiques

Bien que les GPU se transforment de plus en plus en coprocesseurs généralistes, ils offrent toujours des unités matérielles spécialisées pour le rendu graphique, notamment de filtrage de texture. Nous présenterons une manière de détourner cette unité de filtrage de son usage habituel pour lui faire évaluer des approximations polynomiales par morceaux. En particulier, nous appliquerons cette méthode pour effectuer des calculs dans le système logarithmique (LNS).