Séminaire du LIP 2003-2004

A propos du séminaire du LIP. Comme l'année précédente, les séminaires du LIP ont 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). Un pôt clôture le séminaire.

Abonnement et désabonnement à la liste de diffusion : seminaire.lip "à" ens-lyon.fr

Comment se rendre à l'ENS Lyon ?

Les séminaires des années passées : 2002-2003, 2001-2002, 2000-2001, 1999-2000

Reprise du séminaire le mardi 7 octobre 2003 en alternance avec le séminaire du MIM

Contacts et renseignements : Claude-Pierre Jeannerod (bureau 314)

Programme du séminaire...

Mardi 7 octobre 2003 à 13h30, Amphi B (au 3ème étage)
Gilles Schaeffer - Chargé de recherche au CNRS - LIX, équipe Modèles Combinatoires
Codage optimal et tirage aléatoire de triangulations

Mardi 21 octobre 2003 à 13h30, Amphi B (au 3ème étage)
Patricia Bouyer - Chargée de recherche au CNRS - LSV, ÉNS Cachan
Untameable Timed Automata!

Mardi 4 novembre 2003 à 13h30, Amphi B (au 3ème étage)
Nadia Creignou - Professeur au LIF - Équipe Logique et Complexité
Un théorème de classification croisée, complexité versus transition de phase, pour les problèmes de satisfaction de contraintes booléennes

Mardi 25 novembre 2003 à 13h30, Amphi B (au 3ème étage)
Jean-Luc Beuchat - Chercheur au LIP - Équipe Arenaire
Conception de processeurs spécifiques pour des applications de cryptographie

Mardi 9 décembre 2003 à 13h30, Amphi B (au 3ème étage)
Philippe de Groote - Directeur de recherche à l'INRIA - LORIA, équipe Calligramme
Grammaires Catégorielles Abstraites

Mardi 13 janvier 2004 à 13h30, Amphi B (au 3ème étage)
Claire Kenyon - Professeur au LIX - Équipe Algorithmique
Metric Clustering

Mardi 27 janvier 2004 à 13h30, Amphi B (au 3ème étage)
Franck Petit - Maître de conférences à l'Université de Picardie Jules Verne - LaRIA
Compilateurs distribués stabilisants

Mardi 10 février 2004 à 13h30, Amphi B (au 3ème étage)
Jérôme Durand-Lose - Maître de conférences en délégation CNRS - MC2 (LIP) et laboratoire I3S (Université de Nice-Sophia Antipolis)
Calculer géométriquement sur le plan - Machines à signaux -

Mardi 2 mars 2004 à 13h30, Amphi B (au 3ème étage)
Laurence Nigay - Maître de conférences à l'Université Joseph Fourier - CLIPS-IMAG, équipe IIHM
Modalité d'interaction et multimodalité

Jeudi 11 mars 2004 à 14h00, Amphi B (au 3ème étage)
Jacques Stern - Professeur, directeur du département d'informatique, École normale supérieure
Conception et analyse d'algorithmes cryptographiques

Mardi 16 mars 2004 à 13h30, Amphi B (au 3ème étage)
Arie Hordijk - Mathematical Institute, Leiden University - Professeur invité au LIP
Taylor series expansions for stationary Markov Chains

Mardi 30 mars 2004 à 13h30, Amphi B (au 3ème étage)
Nicolas Brisebarre - Maître de conférences en délégation INRIA - Arenaire (LIP) et LArAl (Université de St-Etienne)
Une méthode pour produire des approximants polynomiaux efficaces en machine

SÉMINAIRE ANNULÉ ! REPORTÉ À LA RENTRÉE PROCHAINE
Gilles Parmentier - Post-Doc au LBMC (ENS Lyon) - Équipe Structure et Évolution des Récepteurs Nucléaires d'Hormones
Une base de données inter-espèces de patrons d'expression

Mardi 4 mai 2004 à 13h30, Amphi B (au 3ème étage)
Sylvie Boldo - Doctorante au LIP - Équipe Arenaire
Approximation certifiée de fonctions élémentaires

Mardi 18 mai 2004 à 13h30, Amphi B (au 3ème étage)
Franck Cappello - Directeur de recherche - INRIA Futurs, Projet Grand Large (LRI)
Le projet MPICH-V: vers un MPI tolérant aux pannes automatique pour clusters et grilles

Mardi 1er juin 2004 à 13h30, Amphi B (au 3ème étage)
Mireille Bousquet-Mélou - CNRS, LaBRI, Bordeaux
Pavages par des dominos et suites de Gale-Robinson

Mardi 8 juin 2004 à 13h30, Amphi B (au 3ème étage)
Jean-Christophe Filliâtre - Chargé de recherche au CNRS - LRI (Paris 11) / projet INRIA Logical
Why : un outil de vérification générique

Mardi 22 juin 2004 à 13h30, Amphi B (au 3ème étage)
Augustin Chaintreau - Doctorant - Groupe TREC, département d'informatique, École normale supérieure
Passage à l'Echelle et Fiabilité pour Diffusion Multipoint Pair-à-Pair

Mardi 29 juin 2004 à 13h30, Amphi B (au 3ème étage)
Daniela Genius - Maître de conférences - LIP6, équipe ASIM
Architecture et Programmation des Processeurs Réseaux

Résumés des exposés...

Mardi 7 octobre 2003 à 13h30, Amphi B (au 3ème étage)
Gilles Schaeffer - Chargé de recherche au CNRS - LIX, équipe Modèles Combinatoires
Codage optimal et tirage aléatoire de triangulations

D'un point de vue combinatoire une triangulation est décrite par les relations de voisinage entre ses triangles. Mais cette représentation est relativement coûteuse en espace... Peut on faire mieux et en trouver une plus compacte ?

La question de savoir jusqu'où on peut aller dans ce sens admet une réponse simple en termes de l'entropie de la famille des triangulations, ou plus prosaiquement, en termes du nombre de triangulations à n faces. Or ce nombre est remarquablement simple, il s'agit essentiellement d'un coefficient binomial (4n,n).

L'objet de mon exposé sera de montrer qu'en comprenant de manière constructive ce résultat d'énumération, on arrive à un algorithme de codage garanti optimal dans le cas le pire. Dans le même temps, on obtient un algorithme pour engendrer des triangulations aléatoires exactement selon la distribution uniforme en temps linéaire. Un intérèt de ce dernier résultat est que ce modèle de triangulations aléatoires est utilisé en physique mathématique et que les méthodes de simulation habituelles reposent sur des chaînes de Markov dont les temps de mélange ne sont pas connus.

Pour en savoir plus: D. Poulalhon, G. Schaeffer, Optimal Coding and Sampling of Triangulations, ICALP'03

retour en haut de page

Mardi 21 octobre 2003 à 13h30, Amphi B (au 3ème étage)
Patricia Bouyer - Chargée de recherche au CNRS - LSV, ÉNS Cachan
Untameable Timed Automata!

Le modèle des automates temporisés est un modèle très répandu et étudié. Depuis maintenant 8 ans, des outils implantant ce modèle sont disponibles et ont été utilisés avec succès pour vérifier de vrais systèmes. Cependant, j'ai récemment montré qu'une des techniques utilisées pour vérifier les automates temporisés, l'analyse en avant, n'est pas correcte d'un point de vue algorithmique : en effet, il existe des automates temporisés pour lesquels le résultat de l'algorithme appliqué à ces automates est erroné. Je vais donc présenter ce résultat et expliquer quels sont précisément les problèmes.

Voici un lien vers le bug en question: http://www.lsv.ens-cachan.fr/~bouyer/bug.php

retour en haut de page

Un phénomène de transition de phase brusque a été mis en évidence il y a quelques années pour le problème NP-complet bien connu 3-SAT. De nature probabiliste ce phénomène se traduit par le fait que la probabilité qu'une formule 3-CNF aléatoire soit satisfaisable présente un brusque changement quand le ratio du nombre de clauses sur L sur le nombre de variables n varie. Plus précisément il existe une valeur critique c telle que si L/n<c alors la formule aléatoire est presque surement satisfaisable, alors que si L/n>c elle est presque surement insatisfaisable. Ce comportement probabiliste a suscité beaucoup d'intérêt ces dernières années car il a été observé d'un point de vue pratique que les instances difficiles des problèmes NP-complets coincidaient avec la fenêtre de transition.

Nous établissons un théorème de classification croisée, complexité (P ou NP-complet) versus nature de la transition de phase (brusque ou progressive), pour les problèmes de satisfaction de contraintes booléennes. Nous proposons un critère concis et local qui, étant donné un ensemble de types de contraintes autorisées en entrée, permet de décider facilement si le problème de satisfaisabilité associé a une transition de phase brusque ou progressive. De plus notre étude fournit une première preuve uniforme, et donc instructive, du fait que de nombreux problèmes de satisfaisabilité bien connus tels k-SAT, k-XOR-SAT, Non-Tous-Egaux-k-SAT, 1-parmi-k-SAT, ont une phase de transition brusque.

retour en haut de page

Mardi 25 novembre 2003 à 13h30, Amphi B (au 3ème étage)
Jean-Luc Beuchat - Chercheur au LIP - Équipe Arenaire
Conception de processeurs spécifiques pour des applications de cryptographie

L'implantation matérielle d'algorithmes de cryptage poursuit essentiellement deux objectifs:
- Amélioration de la sécurité d'un système sensible.
- Obtention des débits de chiffrement requis par exemple par un VPN (Virtual Private Network) et inatteignables à l'aide d'un processeur commercial. La recherche de performances motive également les pirates tentant de casser des cryptosystèmes.

Cet exposé est consacré à ce deuxième aspect et décrit quelques approches adoptées par les chercheurs ces dernières années. Pour les algorithmes symétriques (DES, IDEA, AES, ...), nous verrons qu'il est par exemple possible :
- D'étendre le jeu d'instructions des processeurs commerciaux afin d'implanter efficacement des opérations intervenant dans plusieurs algorithmes, comme les permutations de bits.
- De concevoir des processeurs spécialisés dont les unités arithmétiques et logiques offrent les fonctionnalités requises pour un large ensemble d'algorithmes de cryptage.
- De développer un circuit spécifique à un algorithme.

Dans le cas des algorithmes asymétriques (ou à clef publique), nous nous intéresserons au problème d'exponentiation modulaire intervenant par exemple dans RSA ou Massey-Omura.

retour en haut de page

Mardi 9 décembre 2003 à 13h30, Amphi B (au 3ème étage)
Philippe de Groote - Directeur de recherche à l'INRIA - LORIA, équipe Calligramme
Grammaires Catégorielles Abstraites

Nous présentons une nouvelle famille de grammaires formelles, appelées Grammaires Catégorielles Abstraites. Ces grammaires, basées sur la logique linéaire intuitionniste, permettent un traitement intégré de la syntaxe et de la sémantique des langues naturelles.

L'exposé motivera la définition de ce nouveau formalisme, étudiera ses propriétés mathématiques et se terminera par la présentation de quelques problèmes ouverts.

retour en haut de page

Mardi 13 janvier 2004 à 13h30, Amphi B (au 3ème étage)
Claire Kenyon - Professeur au LIX - Équipe Algorithmique
Metric Clustering

Given n data items in a general metric space, how can we efficiently partition them into k clusters of "similar" items? There are many models for this ubiquitous problem, which arises in application areas such as data mining, image recognition, medical imaging, web analysis, etc. One measure of the quality of a k-clustering is the sum of all pairwise distances inside the clusters, which must be minimized. We discuss techniques and algorithms, first for the complementary problem, which can be seen as a metric analog of Max-Cut in graphs, then for 2-clustering, and finally sketch extensions to variants with other objective functions or with cardinality constraints. The algorithms are based on random sampling.

retour en haut de page

Mardi 27 janvier 2004 à 13h30, Amphi B (au 3ème étage)
Franck Petit - Maître de conférences à l'Université de Picardie Jules Verne - LaRIA
Compilateurs distribués stabilisants

Un algorithme distribué est auto-stabilisant si, quelles que soient ses conditions de départ, il finit par avoir un comportement correct vis-à-vis du problème qu'il est censé résoudre. Les algorithmes auto-stabilisants sont donc très adaptés aux systèmes distribués admettant des pannes transitoires ou dans lesquels peuvent intervenir des ajouts et retraits imprévus de composants.

Récemment, nous avons introduit le concept de stabilisation instantanée. Un algorithme distribué est instantanément stabilisant si, quelles que soient ses conditions de départ, il se comporte toujours correctement vis-à-vis du problème qu'il est censé résoudre. Autrement dit, un algorithme stabilisant instantanément est un algorithme auto-stabilisant qui a un temps de stabilisation nul. L'intérêt d'un algorithme stabilisant instantanément est que, malgré les erreurs présentes dans le système, tout processeur faisant appel à cet algorithme pour délivrer ou bénéficier d'un service verra se réaliser ce service conformément à ses spécifications dès la première exécution de l'algorithme initiée par ce processeur alors qu'un algorithme délivrant le même service mais qui ne serait qu'auto-stabilisant ne peut assurer la bonne réalisation du service qu'après un certain nombre de répétitions de ce même service.

Après avoir exposé les concepts énoncés ci-dessus, nous présenterons des compilateurs distribués capables de transformer une grande classe d'algorithmes n'étant pas stabilisants (auto- ou instantanément) en leur équivalent stabilisant. Nous poursuivrons avec des compilateurs distribués ayant pour but de permettre à des algorithmes stabilisants distribués écrits dans des modèles à gros grain de s'exécuter dans les modèles à grain plus fin, plus proches de la réalité. Nous terminerons en montrant quelles sont les limites de ces compilateurs et les perspectives qu'ils permettent d'entrevoir.

retour en haut de page

(ceci correspond à mon HDR passée à Nice le 13 décembre 2003).

Cet exposé se place dans l'étude des modèles du calcul continus. Nous y montrons que la géométrie plane permet de calculer. Nous définissons un calcul géométrique et utilisons la continuité de l'espace et du temps pour stocker de l'information au point de provoquer des accumulations.

Dans le monde des automates cellulaires, on parle souvent de particules ou de signaux (qui forment des lignes discrètes sur les diagrammes espace-temps) tant, pour analyser une dynamique que, pour concevoir des automates cellulaires particuliers. Le point de départ de nos travaux est d'envisager des versions continues de ces signaux. Nous définissons un modèle de calcul continu, les machines à signaux, qui engendre des figures géométriques suivant des règles strictes. Ce modèle peut se comprendre comme une extension continue des automates cellulaires.

L'exposé commence par une présentation des automates cellulaires et la mise en avant d'exemples de particules/signaux tirés de la littérature. De là, nous abstrayons le modèle, les machines à signaux.

Dans un premier temps, nous montrons comment tout calcul au sens de Turing (par la simulation de tout automate à deux compteurs) peut y être mené. Nous montrons également comment modifier une machine de manière à réaliser des transformations géométriques (translations, homothéties) sur les diagrammes engendrés. Nous construisons également les itérations automatiques de ces constructions de manière à contracter le calcul à une bande (espace borné) puis, à un triangle (temps également borné).

Dans un second temps, nous nous intéressons aux points d'accumulation. Nous montrons que la prévision de l'apparition d'une accumulation est indécidable. Ce problème est même $\Sigma_2^0$-complet (hiérarchie arithmétique), en construisant pour tout automate à deux compteurs une machine à signaux et une configuration initiale simulant l'automate pour toutes les valeurs possibles. Nous prenons ensuite un point de vue statique, et non plus dynamique, sur les diagrammes espace-temps engendrés (de même qu'entre automates cellulaires et pavages). Pour chaque position, la valeur doit correspondre au voisinage sur un ouvert suffisamment petit. Muni de cet outil, nous regardons les plus simples accumulations possibles (les singularités isolées) et proposons un critère pour y "prolonger" le calcul.

L'exposé se conclut par la présentation de perspectives de recherches.

retour en haut de page

Mardi 2 mars 2004 à 13h30, Amphi B (au 3ème étage)
Laurence Nigay - Maître de conférences à l'Université Joseph Fourier - CLIPS-IMAG, équipe IIHM
Modalité d'interaction et multimodalité

My research focuses on the engineering of Human Computer Interaction (HCI). My interests include ergonomic as well as software design (software architecture) aspects of HCI. My primary motivation is to develop ways for making interaction techniques more usable. In the seminar, after presenting my research approach, I will present a design space for multimodality. The considerations involved in this design space are not only based on current technological capabilities but also on the psychological consequences of the design features on users. With the results of this work in hand (modality definition and design space), I then examine two research avenues: (1) In the first one, I focus on output multimodal user interfaces applied to visualization of large information spaces. (2) In the second one, I concentrate on new interaction modalities based on the augmented reality paradigm. For each of these two avenues, new ergonomic properties, design rules and patterns, software architectural solutions and new interaction techniques such as the clickable reality and the augmented stroll have been developed.

retour en haut de page

En 1883, Auguste Kerckhoffs énonça plusieurs principes s'appliquant à la conception de systèmes cryptographiques, notamment:

1) Le système doit être matériellement, sinon mathématiquement, indéchiffrable.

2) Il faut qu'il n'exige pas le secret, et qu'il puisse sans inconvénient tomber entre les mains de l'ennemi.

Dans mon exposé j'essaierai de mettre en perspective ces principes et les recherches sur la conception et l'analyse d'algorithmes cryptographiques asymétriques menées depuis l'invention de la cryptographie à clé publique par Diffie et Hellman en 1976 et celle du RSA par Rivest, Shamir et Adleman en 1978. D'un certain point de vue, ces inventions et le développement ultérieur des méthodes de "sécurité prouvée", poussent à leur terme extrême les principes de Kerckhoffs.

J'illustrerai l'exposé par deux exemples de travaux auxquels j'ai participé:

- celui de l'analyse de la norme OAEP (Optimal Asymmetric Encryption), dont la preuve de sécurité a été reconnue incorrecte puis - heureusement - restaurée,

- celui de l'analyse du sytème de Ajtai et Dwork, dont la preuve de sécurité, correcte au demeurant, n'élimine pas les attaques pour les choix de paramètres ayant un sens "pratique".

retour en haut de page

Mardi 16 mars 2004 à 13h30, Amphi B (au 3ème étage)
Arie Hordijk - Mathematical Institute, Leiden University - Professeur invité au LIP
Taylor series expansions for stationary Markov Chains

In this talk, the Taylor series expansions of stationary characteristics of general-state-space Markov chains is presented. The elements of the series are explicitely calculated and a lower bound for the radius of convergence is established. Applications are made to queueing systems.

retour en haut de page

Lorsque l'on conçoit un circuit dédié ou un programme pour évaluer une fonction et que l'on choisit (c'est le cas le plus fréquent) de le faire en approchant cette fonction par un polynôme, on calcule des coefficients idéaux puis on tronque ces coefficients à la taille permise par les opérateurs utilisés. Cette troncature est nécessaire, à cause de la finitude des représentations virgule flottante ou du besoin d'avoir des circuits multiplieurs de petite taille. On doit donc considérer des approximations polynomiales dont le i-ème coefficient a au plus un nombre fixé m_i de bits fractionnaires. Dans un travail commun avec J.-M. Muller et A. Tisserand, nous proposons une méthode efficace permettant d'obtenir le polynôme de meilleure approximation d'une fonction sous cette contrainte. Le gain en précision par rapport à une simple troncature des coefficients est souvent très appréciable : J.-M. Muller a montré que pour des approximations par des polynômes de degré 2, le gain était d'environ 3 bits.

retour en haut de page

Mardi 20 avril 2004 à 13h30, Amphi B (au 3ème étage)
Gilles Parmentier - Post-Doc au LBMC (ENS Lyon) - Équipe Structure et Évolution des Récepteurs Nucléaires d'Hormones
Une base de données inter-espèces de patrons d'expression

Notre travail porte sur la création d'une ontologie des patrons d'expression. En pratique, nous avons commencé par développer une base de données inter-espèces de patrons d'expression. Nous commencerons par un rapide rappel des bases biologiques de notre travail, et nous expliquerons l'importance de ce travail pour les biologistes moléculaires. Nous présenterons l'architecture choisie pour notre application. Nous présenterons rapidement le pipeline de traitement des données et nous discuterons des probèmes posés par ce pipeline. J'introduirai également les recherches futures liées à cette base de données et les questions qui se poseront du point de vue de l'informatique.

retour en haut de page

Mardi 4 mai 2004 à 13h30, Amphi B (au 3ème étage)
Sylvie Boldo - Doctorante au LIP - Équipe Arenaire
Approximation certifiée de fonctions élémentaires

Cet exposé présentera nos derniers résultats concernant les preuves formelles (en Coq) appliquées à l'arithmétique des ordinateurs. Plus précisément, nous nous intéresserons à la façon dont les ordinateurs calculent les fonctions élémentaires (exponentielle, sinus...) et à la validation assistée par ordinateur de chaque étape de calcul.

En effet, les calculs sur ordinateurs sont faits sur des nombres à virgule flottante ayant une précision donnée. Toute opération, même calculée aussi bien que possible, commet donc généralement une erreur petite relativement au résultat, mais qui peut ensuite être amplifiée. Or nous voulons être sûrs de la correction du résultat final malgré toutes les erreurs et tous les cas particuliers qui peuvent arriver lors d'un long calcul. C'est pourquoi nous vérifions nos démonstrations à l'aide d'un assistant de preuve.

retour en haut de page

MPI est un standard de bibliothèque de programmation à passage de messages pour les applications haute performance. La disponibilité de nombreuses implémentations ont favorisé son développement et son acceptation dans la communauté. Aujourd'hui il existe de très nombreuses applications programmées selon cette bibliothèque. Les plates-formes d'exécution des applications haute performance sont de plus en plus grandes (grands clusters et grilles) et leur stabilité est de plus en plus précaire. En effet, il n'est pas rare de considérer un MTBF de quelques heures sur les grandes architectures associant plusieurs milliers de processeurs. Le standard MPI ne prévoit pas la gestion des pannes et suppose, en principe, un arrêt complet du calcul si l'un des processus est en panne. Ces trois éléments sont à l'origine de l'effervescence actuelle autour de l'étude et la réalisation d'environnements MPI tolérant aux pannes.

Un environnement MPI se compose en deux parties : la bibliothèque de fonctions de passage de messages et un support exécutif. Ces deux composants sont utilisés différemment selon les approches de tolérances aux pannes proposées : certains projets proposent de modifier l'API de MPI pour permettre au programmeur de détecter les éventuelles pannes et prévoir des opérations correctives, d'autres projets ne supposent aucune modification des programmes MPI et agissent uniquement au niveau exécutif.

MPICH-V est un projet de recherche étudiant différents protocoles de tolérance aux pannes et leur implémentation au sein d'un exécutif MPI. MPICH-V suit l'approche automatique et transparente du point de vue de l'utilisateur et du programmeur. Les différents protocoles étudiés sont le checkpoint coordonné et le checkpoint non coordonné associé à des techniques d'enregistrement de messages pessimistes et causales.

Dans ce séminaire nous présenterons l'architecture de MPICH-V et les différents protocoles implémentés. Nous discuterons leurs mérites respectifs en termes de performance et de tolérance aux pannes. Nous montrerons comment l'architecture de MPICH-V permet de combiner la tolérance aux pannes avec la faible latence et le haut débit. Ce dernier point est essentiel pour que les applications hautes performances tirent bénéfice des réseaux rapides existant dans les architectures modernes.

Enfin nous montrerons des propriétés a priori étonnantes de MPICH-V comme la possibilité de migrer des exécutions MPI sur des réseaux haute performance hétérogènes et l'ordonnancement en temps partagé d'applications MPI.

retour en haut de page

Mardi 1er juin 2004 à 13h30, Amphi B (au 3ème étage)
Mireille Bousquet-Mélou - CNRS, LaBRI, Bordeaux
Pavages par des dominos et suites de Gale-Robinson

Considérons la suite a(n) définie par les conditions initiales a(0)=a(1)=a(2)=a(3)=1 et par la récurrence suivante, valable pour n>3:

a(n) a(n-4) = a(n-1) a(n-3) + a(n-2) a(n-2).

Bref, un produit de 2 termes est la somme de deux produits du même type. On remarque qu'il faut DIVISER par a(n-4) pour caluler a(n), et on se dit qu'on va trouver des nombres rationnels.

Eh bien non : la suite a(n) est entière. Qui plus est, ce résultat est vrai pour toutes les suites de Gale-Robinson : a(n) a(n-m) = a(n-i) a(n-j) + a(n-k) a(n-l) avec i+j=k+l=m. Ce résultat a été prouvé algébriquement, mais un combinatoriste ne connaîtra pas le repos avant d'avoir répondu à la question suivante :

Que comptent ces nombres ?

Réponse : des pavages par dominos de certaines figures du réseau carré qui ressemblent à des pommes de pin.

Travail en commun avec Jim Propp (Brandeis) et Julian West (Vancouver)

retour en haut de page

Mardi 15 juin 2004 à 13h30, Amphi B (au 3ème étage)
Jean-Christophe Filliâtre - Chargé de recherche au CNRS - LRI (Paris 11) / projet INRIA Logical
Why : un outil de vérification générique

Nous présentons l'outil de vérification Why. À l'instar de nombreux systèmes existants, cet outil produit des obligations de preuve à partir de programmes annotés. Il y a cependant plusieurs différences notables. D'une part, le langage d'entrée se veut générique : c'est un mini-ML avec traits impératifs et exceptions vers lequel on va compiler des langages existants --- dit autrement, c'est un langage intermédiaire spécifique à la génération d'obligations de preuve. D'autre part, les obligations de preuve peuvent être produites pour plusieurs systèmes de preuve existants : quatre assistants de preuve (semi-)interactifs (Coq, PVS, HOL Light et Mizar) et deux procédures de décision (Simplify et haRVey). Enfin, la technologie interne à l'outil Why s'appuie sur une traduction fonctionnelle à base de monades, et non sur les règles de logique de Hoare traditionnelles, même si le résultat est souvent identique.

Nous détaillerons l'application pratique de cet outil à la preuve de programmes Java annotés avec JML (Java Modeling Language) et à la preuve de programmes C.

retour en haut de page

Pour une diffusion fiable et efficace du même contenu, instantanément, à un groupe de destinations, le Multicast Pair-à-pair, ou multicast overlay, utilise un arbre de connections TCP point à point entre destinaires des données. La simplicité de déploiement de ce mécanisme cache d'autres avantages de passage à l'échelle, comme l'attestent l'existence d'un débit positif pour un groupe de taille infini, et les bornes que l'on peut prouver sur les délais à travers des groupes de grandes tailles. C'est ce que nous nous proposons ici d'établir en interprétant avec des temps de dernière percolation à la fois la compétition avec le traffic transverse du réseau, et les événements de contrôle des protocoles utilisés (TCP, et ceux déployés sur l'arbre de connection overlay). Nous étudierons en particulier une condition de moment, assez particulière, sur les perturbations induites par le traffic transverse qui est nécessaire pour justifier ces comportements asymptotiques.

retour en haut de page

Mardi 29 juin 2004 à 13h30, Amphi B (au 3ème étage)
Daniela Genius - Maître de conférences - LIP6, équipe ASIM
Architecture et Programmation des Processeurs Réseaux

Les "processeurs réseaux" (network processor) sont des processeurs spécialisés utilisés dans les équipements télécoms. Ces processeurs sont des systèmes intégrés sur puce (System on Chip) qui possèdent un parallélisme matériel très élevé, puisqu'une seule puce peut contenir plusieurs dizaines de coeurs de micro-processeurs. Ils exécutent des applications logicielles qui possèdent elles-mêmes un fort parallélisme, puisqu'une application peut comporter plusieurs dizaines ou centaines de "threads" qui s'exécutent en parallèle.

Le thême ASIM a développé et modélisé en SystemC dans l'environnement SOCLIB, une plate-forme matérielle multi-processeur "générique" instanciant un nombre quelconque de processeurs MIPSR3000, des coprocesseurs matériels spécialisés, et des bancs mémoire. Ces composants sont interconnectés par un micro-réseau intégré sur puce. Les applications logicielles multithreads sont exécutées sous le contrôle du système d’exploitation embarqué MUTEK, qui est un OS multi-threads, multi- processeurs, respectant la norme POSIX, développé au LIP6 par F.Pétrot. Dans un premier temps, en 2003, nous avons porté avec succès une application de routage Ipv4 sur cette plate-forme. Ce travail a permis de déterminer que les deux causes principales de perte de performance sont les conflits d'accès à la mémoire partagée, et les problèmes de synchronisation entre threads.

Ensuite était défini un "gabarit" précisant la structure générale d'une application multi-threads adaptée au traitement de paquets (cellules ATM ou trames IP). Ce "gabarit" s'appuie sur les mécanismes de synchronisations fournis par le noyau MUTEK, et sur un canal de communication Multi-Ecrivains/Multi-Lecteurs défifni par Alain Greiner et Etienne Faure, permettant une communication aisée entre tâches logicielles et coprocesseurs matériels spécialisés.

La deuxième application actuellement examinée est un classifieur developpé par l'équipe Réseaux et performance du LIP6, actuellement commercialisée par la société QoSMos, startup du LIP6. Un classifieur dissocie un flux de paquets qui seront ensuite traités des manières différentes (Differentiated Services, Traffic Management, Monitoring).

La parallélisation d'une application, ainsi que son intégration sur puce permettent d'espérer un gain d'un ou plusieurs ordres de grandeur sur les performances en termes de débit. Cela ne constitue qu'une première étape : Puisqu'on contrôle à la fois l'architecture matérielle et les couches basses du système d'exploitation, on souhaite explorer différentes variantes architecturales, en particulier pour ce qui concerne le placement des tâches, l'allocation des tampons de communication, ainsi que la gestion des verrous de synchronisation, de façon à exploiter au mieux la bande passante du micro-réseau intégré sur puce. La gestion de la mémoire est à repenser, ouvrant des opportunités de recherche supplémentaires, notamment pour ce qui concerne la cohérence et le stockage des données (sur puce ou à l'extérieur).

On souhaite trouver d'autres applications qui correspondent au gabarit défini. Il semble pour cela très interessant de regarder les ordonnanceurs developpés par l'équipe RESO du LIP.

retour en haut de page

Dernière mise à jour: lundi 24 mai 2004 - Merci à Nicolas Schabanel pour le style de cette page !