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


1er Avril 2010 : Christophe Joubert (Technical University of Valencia), 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



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).