Note aux orateurs
Contact et renseignements : Eddy Caron .
Tous les séminaires ont lieu le mardi à 13h30 dans l'amphi
B de l'ENS Lyon
| Date : mardi | Orateur | Titre |
| 8 octobre 2002 | Emmanuel Cecchet | Serveurs Web à contenu dynamique |
| 22 octobre 2002 | Vincent Simonet | Analyse de flots d'information pour Caml, de la théorie à la pratique |
| 5 novembre 2002 | Caroline Fontaine | Le tatouage des documents numeriques, principes et applications |
| 19 novembre 2002 | Francis Wlazinski | Ensembles de test et morphismes sans répétition |
| 3 décembre 2002 | Luis Garces | Système Distribué P2P pour le Stockage des Objets |
| 17 décembre 2002 | Pierre Lescanne | Un calcul pour interpréter les séquents classiques |
| 28 janvier 2003 | Raymond Namyst | Communications sur les grappes de PC : comment concilier efficacité et portabilité ? |
| 4 février 2003 | Christian Pérez | Padico: Une infrastructure à base de composant pour le Grid Computing. |
| 18 février 2003 | Frédéric Mazoit | Pavages de Penrose |
| 25 mars 2003 | Nicolas Magaud | Preuve formelle du programme de calcul de la racine carrée de GMP |
| 6 mai 2003 | Claude Marché |
| Date | 8 octobre 2002 |
| Orateur | Emmanuel Cecchet (INRIA, Projet Sardes) |
| Résumé |
Les serveurs utilisés pour l'Internet comme, par exemple, les serveurs Web, peuvent potentiellement être accédés par un nombre illimité de clients. Ils sont amenés à fournir un volume croissant de données et doivent supporter un ensemble de services Internet devenant de plus en plus nombreux et de plus en plus complexes. La performance de tels serveurs est donc un point critique pour la réussite et l'évolution des infrastructures d'échange d'informations. Dans cette présentation, nous présentons différentes technologies qui permettent à des serveurs Web de générer des pages dynamiquement. Ensuite, nous nous intéressons à l'effet combiné des méthodes d'implantation d'applications (design patterns), des choix de conception des serveurs d'EJB (proxies dynamiques vs précompilation) et de l'efficacité des couches de communication sur la performance et le passage à l'échelle des serveurs d'application J2EE. |
| Présentation | 
|
| Biblio |
 http://www.cs.rice.edu/CS/Systems/DynaServer/ http://sardes.inrialpes.fr/research/ http://sardes.inrialpes.fr/~cecchet/perso.html
|
| Date | 22 octobre 2002 |
| Orateur | Vincent Simonet (INRIA, Projet Cristal) |
| Résumé |
Comment protéger les données stockées dans un système informatique contre toute modification ou divulgation indésirable tout en permettant l'accès à ces données à tout programme qui en fera une utilisation légitime ? Une solution prometteuse consiste à analyser préalablement chaque programme. Si l'analyse garantit que son comportement sera acceptable, on peut lui accorder un accès sans restriction. Cette technique, appelée analyse de flots d'information, présente l'intérêt de ne reposer sur aucune notion de confiance -- seule la correction de l'analyse importe et peut être prouvée formellement. Lors de l'exposé, nous présenterons une telle analyse pour le langage Caml. Elle consiste à enrichir le langage de type existant avec des "niveaux" permettant de tracer les flots d'information grâce à une forme de sous-typage. Nous nous intéresserons à la fois à des aspects théoriques, liés en particulier à la formalisation du système et à la preuve de sa correction, ainsi qu'à des aspects pratiques liés à son implémentation. Nous présenterons également quelques exemples de code analysés automatiquement par notre prototype, Flow Caml. |
| Présentation | 
|
| Biblio | [PS02] François Pottier and Vincent Simonet. Information flow inference for ML. In Proceedings of the 29th ACM Symposium on Principles of Programming Languages (POPL'02), pages 319-330, Portland, Oregon, January 2002. [Sim02] Vincent Simonet. Type inference with structural subtyping: A faithful formalization of an efficient constraint solver. October 2002. http://cristal.inria.fr/~simonet/soft/flowcaml/
|
| Date | 5 novembre 2002 |
| Orateur | Caroline Fontaine (LIFL, Équipe RD2P) |
| Résumé |
Le développement des réseaux de communication et des supports numériques entraîne une diffusion massive de documents numériques (textes, images, sons). Mais si l'utilisation de formats numériques permet de stocker une grande quantité d'information en peu de place, elle facilite aussi l'utilisation illégale des documents : il est en effet extrêmement facile de récupérer un document sur internet ou sur un CD-ROM, et de le copie un grand nombre de fois avant de diffuser ces duplications. Non seulement la copie est facile, mais elle est parfaite ! Ces manipulations, si elles débouchent sur la commercialisation des copies, ou sur toute autre utilisation autre que privée, sont illégales tant que les droits d'auteur n'ont pas été versés à l'ayant droit concerné. Notre problématique est ici d'associer à un document le nom du ou des ayant(s) droit associé(s). Nous passerons en revue les techniques de "tatouage" mises en oeuvre depuis 1995 et discuterons de leur "avenir". |
| Présentation | 
|
| Date | 19 novembre 2002 |
| Orateur | Francis Wlazinski (LaRIA) |
| Résumé |
Les répétitions que nous considérons sont le chevauchement, le cube et la puissance k > 3 avec k entier. Étant donné deux alphabets A et B, un morphisme de A* vers B* est dit sans une répétition donnée s'il préserve l'absence de cette répétition. Par exemple, un morphisme sans chevauchement vérifie : l'image de tout mot sans chevauchement est sans chevauchement. Un ensemble de test pour les morphismes sans une répétition R est un ensemble de mots T tel que, pour tout morphisme f, nous avons l'équivalence entre f sans R et f(T) sans R. L'ensemble de test sera dit fini s'il ne dépend pas du morphisme choisi. Nous donnons une caracterisation complète, lorsqu'ils existent, les ensembles de test finis pour morphismes uniformes sans chevauchement, pour morphismes sans chevauchement et pour morphismes sans cube. Nous donnons aussi des ensembles de test finis pour morphismes sans puissance k dans le cas binaire qui est le seul cas d'existence. Comme résultat adjacent à la caractérisation des ensembles de test finis, nous donnons une nouvelle méthode de détermination des endomorphismes binaires qui engendrent des mots infinis sans cube. |
| Présentation |
|
| Date | 3 décembre 2002 |
| Orateur | Luis Garces (eurecom) |
| Résumé |
Le stockage massive des objets (fichiers, pages Web, contenus en general) et sa distribution represente un vrais probleme d'infraestructure quand la quantite des donnees surpasse la capacite des serveurs (soit des machines ters puissantes ou des clusters des machines), les utilisateurs sont plusieurs millions, et la bande passante necessaire pour tout ce trafic est bien au-dela de possibilites des liens actuelles. Pour tout ca, dernierement il y a eu des conceptions des systemes P2P (peer-to-peer, pair-a-pair), ou la infrastructure est completement distribuee parmi les machines participantes. De cet facon la, l'effort coordonne de plusieurs hosts avec des caracteristiques de puissance de calcul et connections reseau differentes, fait possible des espace de stockage de Teraoctects, des milliers des utilisateurs, et des systemes que sont tres robustes face aux pannes presentes chaque jour sur l'Internet. Ici on presente une solution de stockage que utilise CHORD, un systeme P2P de routage de donnes, pour implementer un systeme de stockage distribue, robuste et fiable, capable de passer a l'echelle pour des millions des utilisateurs. Cet implementation a eu lieu en parallele aux idees presentees par les createurs du CHORD, au MIT. On fera aussi une introduction "historique" aux systemes P2P, et une presentation de nos dernieres lignes de recherche a l'Institut Eurecom dans le cadre du projet de reseau a haut debit VTHD++. |
| Date | 17 décembre 2002 |
| Orateur | Pierre Lescanne (LIP) |
| Résumé |
Je présenterai un calcul dû à Hugo Herbelin qui interprète la logique classique, plus précisément le calcul des séquents classique. Ceci sera fait dans l'esprit de la correspondance de Curry-Howard, qui considère les propositions comme des types, les preuves comme des programmes et les réductions de preuves comme des calculs. Du point de vue de la conception de langages de programmation, le calcul de Herbelin est simple et naturel. Il est basé sur des capsules appelant-appelé et le résultat d'un calcul a un type qui dépend de l'exécution du «programme» à la manière d'un programme qui lève des exceptions. Ceci est donc une autre présentation (peut-être plus simple!) de la connexion entre la logique classique et la levée d'exceptions. Je ne ferai pas l'hypothèse que le public connaît le calcul des séquents et même quoi que ce soit sur la la logique, puisque que je reprendrai tout à partir de zéro. |
| Présentation |
|
| Biblio |
http://coq.inria.fr/~herbelin/DUALITY.ps.gzhttp://www.ens-lyon.fr/~plescann/PUBLICATIONS/lmm.pdf |
| Date | 28 janvier 2003 |
| Orateur | Raymond Namyst (LaBRI) |
| Résumé |
Les grappes de PC occupent une place de plus en plus grande sur le terrain des machines parallèles à mémoire distribuée grâce à leur rapport performance/prix très compétitif. Cet exposé présentera quelques travaux récents (effectués au sein du projet ReMaP à l'ENSL, puis au sein de l'équipe Calcul Parallèle et Distribué du LaBRI) visant à fournir un environnement de communication à la fois performant et portable sur ce type d'architecture. L'exposé commencera par introduire (rapidement) d'une part les méthodes de transfert disponibles avec les principales cartes réseaux actuelles et d'autre part les différents problèmes posés par des schémas de communication s'écartant de l'envoi de message synchrone point-à-point traditionnel (messages construits dynamiquement, RPC, envois asynchrones). La seconde partie de l'exposé présentera l'interface de communication Madeleine conçue pour répondre aux problèmes précédents. Madeleine est une bibliothèque multi-protocoles capable d'exploiter simultanément plusieurs réseaux physiques au sein de la même application. Elle fournit une interface orientée "envoi de messages" permettant la construction incrémentale des messages et l'expression de contraintes de transmission pour chacun des segments d'un message. Ce "contrat" passé entre l'application et Madeleine permet à cette dernière d'optimiser les transferts réseaux tout en respectant la sémantique du programme. Les résultats obtenus sur des réseaux tels que Myrinet et SCI seront présentés. La troisième partie de l'exposé présentera un aspect des performances un peu plus méconnu : le problème de la réactivité aux évènements du réseau. Bien sûr, il sera question de multithreading, mais nous évoquerons aussi et surtout les problèmes liés à la scrutation du réseau ainsi qu'à la prise en compte des interruptions. En particulier, nous présenterons une extension du noyau Linux permettant une gestion très fine des appels systèmes bloquants au sein d'une bibliothèque de threads de niveau utilisateur. L'exposé se terminera par une ouverture sur les architectures hétérogènes de type "grappes de grappes". |
| Présentation |
|
| Date | 4 février 2003 |
| Orateur | Christian Pérez (IRISA) |
| Résumé |
L'émergence et le déploiement de réseaux d'interconnexion longue distance à très haut débit permet la construction de nouvelles infrastructures de calcul connues sous le nom de «grille de calcul». Ces grilles sont constituées de plusieurs calculateurs parallèles (supercalculateurs, grappes de PC, ...) ayant un fort degré d'hétérogénéité (système d'exploitation, processeurs, réseaux, ...). La programmation des grilles de calculs restent encore grandement à découvrir. Cet exposé explore des concepts et des mécanismes visant à programmer simplement et efficacement des grilles de calcul. L'application cible typique est une application de simulation multi-physique où chaque physique est simulée par un code parallèle. Le problème est donc d'offrir un environnement pour coupler simplement et efficacement des codes parallèles en milieu distribué. La première partie de l'exposé introduit la notion de composants logiciels et plus particulièrement la notion de composants logiciels parallèles. Un composant parallèle doit se comporter le plus possible comme un composant séquentiel. Il faut en outre qu'il propose une gestion la plus transparente possible du parallélisme, et, enfin, il faut que les communications entre composants parallèles puissent passer à l'échelle. Nous verrons quelques points importants du modèle GridCCM qui étend le modèle de composant de CORBA. La seconde partie de l'exposé concerne la mise en oeuvre efficace des composants logiciels parallèles, plus particulièrement du point de vue des communications. Les noeuds des grilles de calcul disposent souvent de réseaux locaux haute performance. Il faut alors s'assurer que les communications entre composants logiciels se trouvant sur le même noeud exploitent au mieux les réseaux disponibles. Comme la localisation des composants n'est pas connue à la compilation, il faut donc assurer un accès transparent et efficace aux réseaux. Le problème est en fait plus complexe car les technologies mises en oeuvre dans les communications inter-composants et dans les communications intra-composants sont différentes. Par exemple, un composant parallèle peut encapsuler un code parallèle qui gère son parallélisme via MPI alors que les communications inter-composant utilisent CORBA. Différents intergiciels communiquant sont donc simultanément actifs dans un même processus. Il faut supporter cette situation tout en offrant la transparence et l'efficacité des communications. Les travaux réalisés autour de la plate-forme PadicoTM apportent des réponses à ce problème. |
| Présentation |
|
| Date | 18 février 2003 |
| Orateur | Frédéric Mazoit (ENS Lyon) |
| Résumé |
Après avoir présenté la problématique dans laquelle s'inscrivent les pavage de Penrose, je les présenterai plus précisement. Je montrerai d'une par qu'il est possible de paver le plan avec les tuilles de Penrose, ensuite, je montrerai que les pavages sont toujours apériodiques mais qu'ils sont quasi-périodiques. |
| Date | 25 mars 2003 |
| Orateur | Nicolas Magaud (INRIA - Projet Lemme) |
| Résumé |
L'évolution des systèmes d'aide à la preuve permet de prouver formellement la correction de programmes de plus en plus conséquents. Dans cet exposé, nous présenterons une preuve formelle de correction d'un programme de calcul de la racine carrée pour les grands entiers. Ce programme, distribué dans la bibliothèque GMP, a été proposé par Paul Zimmermann et est connu comme un des plus efficaces à l'heure actuelle. Dans la première partie de l'exposé, nous tenterons de définir ce que signifie "prouver formellement un programme". Nous verrons les moyens nécessaires à mettre en oeuvre pour réaliser de telles preuves ainsi que les bénéfices que l'on peut tirer de la formalisation d'un algorithme. Dans une deuxième partie, nous présenterons l'algorithme de calcul de racine carrée ainsi que son implantation. Nous nous intéresserons à quelques unes de ses propriétés, en particulier sa faible consommation mémoire. Nous verrons que le calcul s'effectue en place et réutilise de façon optimale l'espace mémoire où se trouvaient ses entrées. Dans une troisième partie, nous décrirons la spécification formelle de ce programme dans l'assistant de preuves Coq. Nous montrerons comment passer d'une documentation (informelle) à une spécification mathématique formelle. Nous donnerons ensuite un aperçu de la spécification et de la preuve de ce programme dans l'environnement de preuves Coq/Correctness. |