Comme l'année précédente, les séminaires du LIP auront lieu le mardi après-midi à 13h30 deux fois par mois avec (en principe) en alternance un exposé d'un intervenant local / un exposé d'un intervenant extérieur. La durée est de 45 minutes plus 10 à 15 minutes de questions (des modifications peuvent être envisagées si elles sont demandées à l'avance).
Renseignements et propositions d'exposés à : Nicolas Schabanel
Abonnement et désabonnement à la liste de diffusion :
seminaire.lip "at" ens-lyon.fr
On considère le problème suivant: soient deux lignes de
communication offrant respectivement un débit de A
et B paquets par secondes. On cherche à utiliser les
deux lignes pour écouler au plus vite des paquets qui arrivent
toutes les C unités de temps. Quelle est alors la politique
optimale d'allocation des paquets sur les deux lignes?
On montre dans un premier temps un résultat qualitatif: une
politique optimale est donnée par un mot de Sturm (défini
dans la présentation). Ensuite, on montre comment fixer le paramètre
p du mot de Sturm optimal en fonction de A, B
et C. Cette fonction présente un caractère
fractal et repose essentiellement sur la décomposition en fraction
continue supérieure de A et de B .
Auteurs: B. Gaujal et E. Hyons (LORIA)
Soit le problème consistant à calculer l'intersection de
k ensembles triés de taille donnée. Dans le modèle
de calcul limité aux comparaisons, nous prouvons une nouvelle
borne inférieure, relative à la complexité non-déterministe
de l'instance, c'est à dire à la taille de la preuve
du résultat. Cette borne inférieure implique que l'algorithme
donné par Demaine, López-Ortiz et Munro est optimal
dans le sens "adaptatif". Nous étendons ces résultats
au problème d'ensemble de tseuil, qui ne contient que
les éléments présents dans au moins t ensembles.
Les résultats sur ces deux problèmes seront présentés
à la Conférence SODA.
Ces problèmes sont appliqués aux moteurs de recherche indéxés, dans le cadre du projet FFSS, sous la forme de deux variantes, l'intersection bidimensionelle et l'interunion, sur lesquels sont définis également des bornes inférieures et des algorithmes. Le projet FFSS, qui consiste en un nouveau protocole de partage de fichier (d'utilisation similaire à Samba, mais avec des options intégrées de NetEject) doublé d'un moteur d'index et de recherche sur les partages, est en ce moment testé en version béta sur le réseau universitaire étudiant de la Fédération AURORE, à l'université Paris-Sud.
Il est encore d'intéressants problèmes ouverts et applications, et le concept de l'analyse de la complexité dans le pire des cas sur des familles d'instances autres que celles définies par la taille des instances, formalisé à l'occasion de ces travaux, semble prometteur.
Dans cet exposé, on présente une nouvelle approche sur le problème de contrôle superviseur des réseaux de Petri qui utilise des fonctions de routage au lieu de la méthode traditionnelle qui utilise des places de contrôle. Ensuite, nous allons montrer la relation entre les deux notions. Il y aura aussi un bref résumé sur les réseaux de Petri et le problème de contrôle superviseur: de quoi il s'agit, les applications et les méthodes classiques de résolution.
Dans la deuxième partie de l'exposé, nous abordons la question de la résolution d'un problème spécifique en utilisant notre méthode. Il s'agit de l'évitement de la famine dans des réseaux de Petri généraux. Le contrôle proposé utilise la version continue du réseau et une description de l'évolution du réseau sous forme d' équations ``linéaires'' dans l'algèbre (max,plus). On montre que le problème se ramène à la résolution d'un système d'équations polynômiales pour le cas continu et des équations diophantines sont utilisés pour le cas discret.
Les strategies pour repartir les donnees et les calculs d'une application determinent les parallelisations possibles et finalement les performances qui peuvent etre atteintes. La repartition des donnees par blocs, supportee par les langages High Performance Fortran (HPF) et OpenMP, conduit souvent a des performances acceptables pour de nombreuses applications regulieres. En revanche, pour les applications effectuant des phases de calculs iteratifs le long de chacune des dimensions de donnees multi-dimensionnelles, les performances des versions par blocs compilees sont relativement mauvaises par rapport aux versions optimisees a la main. Ce type de schema de calcul se retrouve frequemment par exemple dans les methodes ADI (Alternating Direction Implicit) permettant de resoudre des equations aux derivees partielles. Pour ce type d'applications, la repartition par bloc sequentialise completement les calculs le long de l'une des dimensions.
Le "multi-partitionnement" est la technique utilisee pour ce type d'applications dans les versions codees a la main, et non la repartition par bloc. La propriete principale du multi-partitioning est que, pour chaque phase de calculs mono-dimensionnelle, tous les processeurs en parallele ont un bloc a calculer, sans sequentialisation. Le deuxieme avantage est la granularite importante des communications necessaires. Le principe sous-jacent est de repartir les blocs sous-forme de "carre latin": en dimension 2, tout numero de processeur apparait exactement une fois dans chaque ligne et chaque colonne de la matrice des donnees. Ce principe a neanmoins une restriction puisqu'on ne manipule que des "carres" multi-dimensionnels: en dimension d, le nombre de processeurs doit etre un entier a la puissance d-1 (un carre en dimension 3).
Le but de notre travail etait de generaliser ce principe a n'importe quel nombre de processeurs (on s'interessera donc a des rectangles et non plus des carres magiques) et d'essayer, par la compilation, d'approcher les performances des versions codees a la main. D'un point de vue theorique, deux problemes doivent etre resolus: premierement, determiner le nombre de tranches dans chaque dimension (ce qui determine les blocs et la taille du "rectangle magique") de sorte que les communications entre processeurs soient minimisees, tout en conservant l'equilibrage de charge; deuxiemement, definir l'allocation des blocs aux processeurs, c'est-a-dire definir les valeurs du "rectangle magique". D'un point de vue mathematique, le probleme est le suivant. Etant donne un nombre de processeurs p, on veut definir un tableau de blocs tel que, pour chaque "tranche" (une dimension de moins) du tableau, le nombre de blocs est un multiple de p (condition necessaire evidente pour garantir l'equilibrage de charge). De plus, on veut choisir les tailles de ce tableau pour minimiser une certaine fonction objective (en pratique, la somme des tailles ou une fonction lineaire). Nous proposons de resoudre ce probleme comme une variation d'un autre probleme connu, trouver le nombre de partitions d'un entier (etudie par Euler et Ramanujam entre autres). Puis, etant donne un tel tableau de blocs, on veut attribuer a chaque bloc un numero (entre 1 et p) de sorte que, dans chaque tranche, chaque nombre apparait exactement le meme nombre de fois (equilibrage de charge a nouveau). Il se trouve que la condition necessaire enoncee plus haut est (heureusement) egalement suffisante. Si, pour chaque tranche, le nombre de blocs est un multiple de p, on peut construire un "rectangle latin magique". Pour cela, on utilise une allocation cyclique multi-dimensionnelle, a l'aide de proprietes sur les groupes abeliens (formes d'Hermite, theoreme d'Hajos), proprietes qui ont egalement des liens avec des problemes de pavages.
Travail en collaboration avec Daniel Chavarria-Miranda, Robert Fowler et John Mellor-Crummey (Rice University).
Cette présentation est centrée sur la conception d'architectures matérielles spécialisées à partir de spécifications fonctionnelles de haut niveau. La complexité des systèmes intégrés augmentant rapidement grâce aux progrès de la technologie, la demande pour une conception sûre et rapide est de plus en plus forte. Aujourd'hui, pour réaliser un circuit, on voudrait pouvoir "compiler" une spécification fonctionnelle (un programme) plutôt que de décrire directement la structure de l'architecture. Nous avons étudié cette compilation dans le cadre restreint des architectures spécialisées parallèles de type systolique, architectures pour lesquelles une méthodologie de conception automatique a pu être mise en place petit à petit. Nous avons implémenté cette méthodologie dans le logiciel MMAlpha et l'on peut aujourd'hui obtenir très rapidement une description d'un circuit en VHDL à partir d'une description fonctionnelle en langage Alpha. La compilation dont il s'agit ici est spécifiquement dédiée au traitement efficace des calculs simples et répétitifs (boucles imbriquées à contrôle statique). Les recherches présentées ici sont très proches de celles qui sont faites dans le domaine de la parallélisation automatique pour machine SIMD. Le modèle utilisé dans ces deux domaines est le modèle polyédrique (on utilise de polyèdres pour modéliser les espaces d'itération des boucles). Le système MMAlpha est un des tout premiers systèmes au monde intégrant la puissance du modèle polyédrique et la compilation/parallélisation d'architecture jusqu'au VLSI. Après une présentation générale du système MMAlpha et des résultats obtenus avec, je détaillerai une des problématiques en cours à savoir l'ordonnancement structuré d'équations récurrentes.
Cet exposé traite du calcul numérique parallèle et les résultats de recherche présentés portent sur la factorisation LU, telle qu'elle est utilisée pour résoudre des systèmes linéaires creux non-symétriques.
Si la matrice à factoriser est symétrique et positive définie, la factorisation de Cholesky peut être utilisée, et pour elle des algorithmes performants parallèles ont été développés. Cependant, dans beaucoup d'applications comme la dynamique des fluides, l'analyse des circuits, le système d'équations associé implique une matrice non-symétrique. Pour ces applications, les besoins en mémoire et en puissance de calcul deviennent importants, car les applications d'aujourd'hui font apparaître des systèmes de plus en plus larges.
L'importance et la variété des domaines d'applications constituent la motivation principale dans la recherche des méthodes de calcul performantes (algorithmes et structures de données) pour la résolution des systèmes linéaires non-symétriques. L'approche principale pour l'obtention de hautes performances dans le calcul scientifique est l'utilisation des noyaux de calculs dense, ainsi que l'identification et l'exploitation du parallélisme entre les tâches.
En général, les calculs sur des matrices creuses ont une phase initiale de prédiction structurelle de la sortie, suivie par une phase de calcul numérique effectif. La connaissance de cette structure permet l'allocation de la mémoire, l'initialisation des structures de données et l'ordonnancement des tâches en parallèle. Dans ce but, nous étudions la prédiction structurelle pour la factorisation LU avec pivotage partiel. Nous nous intéressons principalement à identifier des limites supérieures aussi proches que possible de ces structures. Nos travaux dans le cadre du calcul numérique des facteurs utilisent principalement la notion de forêt d'élimination de fusion par lignes. Encore dans le même but (efficacité et performances supérieures de l'algorithme parallèle), nous développons des techniques pour l'utilisation des noyaux de calculs dense, et pour exploiter la concurrence dans les calculs.
Dans le cadre de la factorisation LU sans pivotage, nous abordons plusieurs problèmes ouverts dans la recherche d'aujourd'hui. En premier nous traitons de l'algorithmique parallèle pour les matrices de taille très grande pour lesquelles la factorisation symbolique constitue un goulet d'étranglement dans le cas séquentiel. Ensuite, nous analysons le problème d'identification et d'ordonnancement de tâches dans la factorisation numérique. Cette analyse nous permet de développer un algorithme scalable, qui utilise d'une manière efficace la mémoire et les ressources de calcul disponibles.
Recently compilation technology has been facing new challenges due to the increased interest of software engineers in higher levels of programming, like object-oriented programming (Java) and functional programming (Haskell, ML). Increasingly sophisticated methods of static program analysis have been and are being developed to meet these challenges. In particular, it has been recognized that the compile-time exploitation of \emph{domain-specific knowledge} is a key ingredient to significant improvements in program performance. Also, hiding domain-specific issues from the application programmer can simplify his/her task considerably.
Domain-specific knowledge is being captured either in a specialized programming language or in modules which are specified in a general-purpose language but given a domain-specific implementation. Several research communities have been developing their own domain-specific approaches -- notably the object-oriented programming community and the high-performance programming community. The talk is about an approach of the second kind in the high-performance programming community.
HDC is a derivative of the functional language Haskell, in which certain functions can be designated as "skeletons". Typically a skeleton is higher-order, since some parameters are program parts instantiating the schema. Skeletons are not compiled like the rest of the program but have custom-made implementations, which are subject to compile-time and, possibly, run-time parameters. During compilation of an application program, the appropriate skeleton implementations are selected and instantiated. The power of functional programming lies in the exploitation of compile-time information in this instantiation process.
The talk will sketch the challenges and promises of this approach.
Nous traiterons des tactiques d'automatisation spécialement conçues et adaptées pour la bibliothèque des nombres réels de Coq. Afin de présenter la problématique concernant ce genre d'automatisation, qui est particulière aux nombres réels, nous commencerons par rappeler brièvement comment sont définis les nombres réels en Coq. Nous parlerons également du nouveau langage de tactique de Coq qui est un atout majeur dans le développement des tactiques, en particulier, dans celles que nous présenterons. Nous donnerons alors quelques exemples de tactiques simples, avant de détailler la tactique réflexive Field.
A robot with k-bit memory has to explore a tree whose nodes are unlabeled and edge ports are locally labeled at each node. The robot has no a priori knowledge of the topology of the tree or of its size, and its aim is to traverse all the edges. While O( log D) bits of memory suffice to explore any tree of maximum degree D if stopping is not required, we show that bounded memory is not sufficient to explore with stop all trees of bounded degree (indeed \Omega(log log log n) bits of memory are needed for some such trees of size n ). For the more demanding task requiring to stop at the starting node after completing exploration, we show a sharper lower bound \Omega (log n) on required memory size, and present an algorithm to accomplish this task with O(log^2 n) -bit memory, for all n-node trees.
Several methods have been developed for identifying more or less complex RNA structures in a genome. Whatever the method is, it is always based on the search of conserved primary and secondary structures. While various efficient methods have been developed for searching motifs of the primary structure, usually represented as regular expressions, few effort has been expended in the efficient search of secondary structure signals. By a helix, we mean a structure defined by a combination of sequence and folding constraints. We present a flexible algorithm that searches for all approximate matches of a helix in a genome. Helices are represented by special regular expressions, that we call secondary expressions. The method is based on an alignment graph constructed from several copies of a pushdown automaton, arranged one on top of another. The worst time complexity is O(R*P*N) , where N is the size of the genome, P the size of the secondary expression, and R its number of union symbols. We present our results of searching for specific signals of the tRNA and RNase P RNA in two genomes. This work has been done with Nadia El-Mabrouk (University of Montreal) and will appear shortly in RECOMB'2002. A complete version of the paper is available at http://www-igm.univ-mlv.fr/~raffinot/ .
Nous introduirons la notion de groupe de pavage et nous verrons comment, un pavage peut etre code par une fonction de la figure qu'il pave vers son groupe. Nous verrons ensuite que ce codage permet de structurer l 'espace des pavages, comment ces notions peuvent etre utilisees pour:
Cet expose est principalement inspire d'un travail commun avec Cris Moore (Santa Fe) et Ivan Rapaport (U. Chile) presente à SODA 2002.
Dans cet exposé, je présenterais les bases des techniques du model checking symbolique et quelques uns des problèmes qui y sont liés. Dans un premier temps, j'expliquerais le model checking dans le cadre de la vérification de systèmes déterministes à l'aide de diagrammes de décision binaires (OBDD), puis j'introduirais le cadre de vérification de systèmes probabilistes.
La validité des calculs utilisant des nombres flottants fait souvent l'objet de doutes à cause des erreurs d'arrondi pouvant fausser les résultats. De plus, il est difficile pour un programmeur de déterminer la précision d'un résultat ainsi que les opérations qui introduisent les principales erreurs.
Dans cet exposé, nous présentons une sémantique non-standard des opérations en virgule flottante pour modéliser la propagation des erreurs d'arrondi pendant un calcul. Chaque opération élémentaire introduit un nouveau terme d'erreur du premier ordre et la combinaison de ces termes au cours des opérations suivantes crée des termes d'erreur d'ordre supérieur. Cela permet de déterminer quelles opérations ont introduit les principales erreurs faussant le résultat. Notre première sémantique modélise la propagation des erreurs de tout ordre et nous nous intéressons par la suite à des approximations sûres de celle-ci. D'une part nous montrons comment étudier seulement les termes d'erreur d'un ordre maximal tout en s'assurant que les termes d'ordre supérieur restent négligeables. D'autre part nous montrons qu'il est possible de paramétrer la granularité des opérations et de traiter de manière atomique les erreurs introduites lors de calculs intermédiaires. Nous montrons que ces sémantiques approchées sont des abstractions correctes de la sémantique la plus générale. Enfin, nous nous intéressons à une interprétation abstraite fondée sur les sémantiques décrites ci-dessus et nous présentons les premiers résultats produits par un analyseur en cours d'implémentation.
Les procédés de fabrication permettent aujourd'hui d'intégrer plusieurs dizaines de millions de transistors, et donc plusieurs dizaines de processeurs sur une même puce. Dans ce contexte, les communications entre les processeurs et la mémoire ou les périphériques deviennent le facteur limitant les performances des applications intégrés.: Le traditionnel "bus système" permettant aux processeurs d'accéder à la mémoire partagée ne fournit pas la bande passante nécessaire. La technologie de micro-réseau à commutation de paquet SPIN développée au LIP6 fournit un bande passante pratiquement illimitée tout en minimisant la consommation. On analyse les problèmes posés aux architectes système par l'utilisation de ce type de micro-réseau intégré.
Connaissant le modèle du comportement d'un système (biologique,
physique...) et un ensemble de données expérimentales,
on cherche à déterminer les valeurs des paramètres
du modèle pour vérifier les données. En présence
de données bruitées et d'un modèle donné
par une fonction réelle, on montre la contribution possible
des techniques de
consistance de contraintes numériques et d'analyse par intervalles.
Pour chaque paramètre, on peut déterminer un sous-ensemble
et un sur-ensemble de l'ensemble des valeurs consistantes avec les
données et le bruit.
This talk investigates the use of advanced communication services in grid environments.
Such services can include augmented communication semantics (e.g., filtering), collective operations, content-based and policy-based routing, and managing communication scope to manage feasibility. These services could be implemented and deployed in a variety of ways, such as a traditional network of servers, or as a middleware forwarding and routing layer, or even in an active network. We demonstrate here a communication service to support time management in distributed simulations that is managed using a grid computing toolkit.
Since the design space for communication services offers so many possibilities and alternatives, we argue for the definition of proper high-level models and APIs such that the underlying implementations and scope of deployment can be developed and improved with minimal impact on applications.
| Dernière mise à jour le 27 juin, 2002 17:10 |