Talk abstract
From LRDE
This is a property of type Text.
S
Dans cet exposé je présenterai la bibliothèque d'algorithmes
géometriques CGAL. Cette bibliothèque C++ fournit des algorithmes
comme le calcul d'enveloppes convexes, de triangulations, en 2D,
3D... J'illustrerai surtout les problèmes de robustesse numériques que
l'on y rencontre, puis je détaillerai les solutions que l'on utilise
pour les résoudre de manière efficace. Elles sont basées sur plusieurs
types d'arithmétique: arithmétique d'intervalles et
multiprécision. Ces différentes techniques sont combinées dans
l'implementation grâce à la généricité du code (template C++), ce qui
produit à la fois un code efficace, compact, et proche des concepts
mathématiques, donc plus facilement prouvable. +, Dans cet exposé, nous présenterons la bibliothèque d'algorithmes de
morphologie mathématique Morph-M. Cette bibliothèque C++ fournit un
grand nombre de fonctions en traitement d'image (arithmétiques,
colorimétrique...) et en morphologie mathématique (filtrage,
segmentation, graphes etc.). Nous discuterons principalement des
concepts proposés par la bibliothèque, et leurs utilisations dans la
mise en oeuvre de nouveaux algorithmes. Nous illustrerons les
potentialités par quelques algorithmes actuellement implémentés dans
cette bibliothèque. Enfin nous discuterons des inconvénients de
l'approche générique. +
Dans cet exposé nous verrons l'ensemble des outils de la plate-forme
Qgar, avec une attention particulière pour la généricité et les
performances du code de la bibliothèque QgarLib. Nous verrons
également les autres composants du logiciel, quelques standards de
développement Qgar, ainsi que les défis pour l'évolution de la
plate-forme. +
Context-oriented Programming allows one to modularize a software
system using partial class and method definitions organized into
layers. Layers are composed into or out of the system depending on the
context apparent during program execution. The basic concept of layers
as partial program definitions has been suggested before, but with our
approach we extend this idea by the notion of dynamically scoped layer
activation, resulting in a viable approach for expressing
context-dependent behavior. We will discuss the basic language
constructs for Context-oriented Programming, the development of
non-trivial examples, implementation issues, especially with regard to
retaining efficient method dispatch, integration with the CLOS
Metaobject Protocol, and if time permits, advanced topics like
ContextL's reflective facilities for controlling layer activation and
deactivation. +, Separation of concerns is the idea of breaking down a program into
encapsulated pieces that overlap in functionality as little as
possible. Encapsulated entities, such as classes, methods or modules,
are more manageable, easier to test and maintain, and may be reused
more easily than a large, entangled program. A cross-cutting concern
is something that cannot be encapsulated using normal abstraction
mechanisms, thus defeating separation of concerns. A classical example
of this is logging (e.g., logging calls and returns to a file while
the program is running) - the logging code needs to be added to every
applicable method in the program. The logging code for each method may
be almost identical, creating an undesirable overlap in
functionality. Aspects let a programmer implement a cross-cutting
concern as a separate entity, through advice (how a concern should be
implemented) and join points (where it should be implemented). I will
give an introduction to aspect-orientation and aspect languages, and
also talk a bit about domain-specific aspect languages. +
Mouldable programming is about looking at programs as mouldable
fragments of code, not as the static, brittle syntax software often
turns out to be. Some simple examples follow. The notation for calling
a method "push" which adds an element "E" to a stack "S" can be OO or
static method style, it can modify "S" or return the new stack
etc. Can we simplify usage to just one form, and mould it to the
actual call? A function which breaks down for some input can signal
this using return flags, special return values, or exceptions, to name
some common ways. Can we abstract over this, and mould to the relevant
error handling technique? Often we need to do run-time checking of
arguments, e.g., array indexing bounds, forcing us to introduce lots
of code to deal with the unwanted cases. Can we use mouldable ideas to
simplify the code? In the presentation, we will elaborate on such
examples, discussing how we can free us from awkward syntactic
constraints. +, Writing code in an abstract, high-level style can cut development time
and make code more maintainable and easier to reason about - but at
the cost of lower run-time performance. For performance-critical
applications, such as in numerical programming, this can render modern
abstraction techniques infeasible. Fortunately, code that is easy for
humans to reason about is also easier to reason about
automatically. We're studying different abstraction mechanisms and
generative programming techniques, as well as optimization techniques
to produce efficient code for them. As an example, basic element-wise
operations on arrays may be expressed in terms of high-level
operations, which may be automatically combined in order to increase
performance. I will present some of the things we've been working on
so far, and some of the ideas we have for the future. +
L'algorithmique constructive permet, partant d'une spécification écrite
sous forme d'une combinaison non-efficace de fonctions, de dériver, sous
certaines conditions, des algorithmes parallèles efficaces. Cette dérivation
s'appuie sur des théorèmes d'équivalence de programmes et est formellement
correcte. Elle aide le programmeur à concevoir des programmes parallèles.
Toutefois les bibliothèques de squelettes proposées ne sont pas certifiées.
Dans le cadre d'une collaboration avec l'université de Tokyo, nous proposons
de cibler des squelettes algorithmiques développés en BSML et certifiés à
l'aide de l'assistant de preuve Coq. +, Nous présenterons BSML (Bulk Synchronous Parallel ML), un langage de
programmation de haut-niveau pour machines parallèles, ainsi que des
exemples classiques de parallélisme implémentés dans ce langage. Nous
complèterons cette présentation par une étude comparative des coûts
théoriques de ces algorithmes réalisée sur la grappe de PC du LACL. +
Dans cet exposé je présenterai le modèle bulk-synchronous parallelism (BSP)
des algorithmes et architectures parallèles, ainsi qu'un tour d'horizon des
domaines d'application du parallélisme. BSP propose une vue unifiée des
principaux paramètres de la performance des algorithmes parallèles et de
leur adéquation sur les architectures multi-processeur, multi-coeur et leurs
réseaux de communication interne. Il permet une analyse portable et
extensible des performances ce qui permet d'éviter les principaux pièges de
l'informatique parallèle: mauvaise granularité, réseau mal adapté,
déséquilibres. +, Les besoins croissants en puissance de calcul exprimés par de nombreux
domaines scientifiques exercent une pression très forte sur les
architectures émergentes, les rendant toujours plus performantes mais
toujours plus complexes à maîtriser. Dans ce cadre, le développement
d'outils tirant parti des spécificités de ces architectures (quadri-
et bientôt octo-coeurs, processeurs Cell ou GPU par exemple) devient
une gageure car allier expressivité et efficacité est une tâche
ardue. Les travaux exposés ici montrent comment l'utilisation de la
programmation générative, et en particulier de la méta-programmation
template, permet de répondre au problème de performances et
d'abstractions.
Nous montrerons comment ces techniques ont permis de développer Quaff,
un outil de placement automatique d'applications data-flow sur des
cibles variées comme les clusters, les multi-coeurs ou le processeur
Cell. +
Dans un intergiciel schizophrène, une représentation intermédiaire
des interactions entre composants applicatifs est construite et
manipulée. Cette représentation est neutre vis-à-vis du choix d'une
personnalité application (interface entre les composants et
l'intergiciel) et d'une personnalité protocolaire (interface entre
intergiciels distants). Elle rend possible le découplage entre ces
deux aspects.
Cette représentation doit préserver la structure des données associées
aux interactions. Cependant, sa construction in extenso s'avère coûteuse
dans le cas de données composites complexes. Cette conversion peut être
économisée en remplaçant la réplication complète de la structure par la
définition d'un emballage « fantôme » autour de celle-ci (et de chacun
de ses composants) : il suffit que cet emballage fournisse les accesseurs
permettant de parcourir la structure et de construire un message la
représentant.
Après avoir présenté un exemple concret de représentation neutre
des données structurées, nous montrons comment cette optimisation
peut être mise en oeuvre pour réaliser de manière efficace la
fonction de représentation dans un intergiciel schirophrène. Nous
concluons cette discussion par une évaluation du gain de performance
ainsi obtenu. +, Le langage Ada est connu pour sa sûreté intrinsèque : son typage fort,
ses mécanismes de contrôle de valeurs et son système d'exceptions notamment
permettent d'avoir une grande confiance en les programmes. Comme dit
le vieux proverbe, « En Ada, quand ça compile, ça marche ».
Cependant, une des puissances d'Ada provient également de ses systèmes
de vérification lors de l'exécution du programme. Par exemple, si une
valeur se trouve en dehors de l'intervalle qui lui était autorisé, une
exception, rattrapable par le langage, sera automatiquement levée. Ce
système de vérification dynamique a bien évidemment un coût. Nous verrons
comment le système de compilation GNAT mélange analyse statique et
vérification lors de l'exécution pour fournir la totalité des
garanties définies par le langage tout en minimisant les surcoûts et
la perte de performance. +
L'outil BTL++ (Benchmark Template Library in C++) développé à EDF R&D se
fonde sur la programmation générique et permet de mesurer les performances
de noyaux de calcul intensif. Il s'agit d'une bibliothèque générique dont
la conception vise à faciliter l'extensibilité par l'utilisateur.
Récemment, le lien entre les mesures de performance et la génération
automatique de bibliothèques optimales à été étudié pour le domaine de
l'algèbre linéaire dense. Quelques mesures de performance de noyaux de
calcul à base d'"Expression Template" permettront d'illustrer l'usage de
l'outil BTL++. +, La multiplication des architectures HPC (CPU multi-coeurs, GPU, Cell,..)
implique autant de spécialisations des codes de calcul intensif. Dans un
contexte industriel, les codes de calcul multi-cibles posent alors des
problèmes de maintenance et d'évolutivité importants. La génération
automatique des spécialisations est une réponse à ces problématiques. Pour
le domaine de l'algèbre linéaire, nous étudions les possibilités offertes
par la programmation générique. La mise au point d'une bibliothèque
générique multi-cible et performante constitue le sujet de départ d'une
thèse dédiée aux méthodes de développement HPC qui minimisent l'adhérence
aux machines cibles. +
JoCaml est une extension d'Objective Caml pour la programmation
concurrente et distribuée, inspirée par le join-calcul. Nous avons
récemment publié une nouvelle version de JoCaml, dont la compatibilité
avec OCaml est meilleure que celle de la version initiale de F. Le
Fessant. La nouvelle version pourra facilement être mise à jour au
rythme d'OCaml et est binaire-compatible avec OCaml.
L'exposé s'attachera plus au langage JoCaml qu'au système JoCaml. Il
montrera comment, à partir d'un programme potentiellement
parallélisable écrit en OCaml (le ray tracer du concours ICFP 2001),
on peut facilement produire un programme distribué, dans le cas
abordé, très efficace. Ce sera l'occasion d'aborder la programmation
en JoCaml de la coordination de multiples agents coopérants, d'une
manière simple et concise dans l'esprit de la programmation
fonctionnelle.
JoCaml est disponible en http://jocaml.inria.fr/. +, ReactiveML est une extension d'OCaml basée sur le modèle réactif
synchrone introduit par F. Boussinot au début des années 90. Il permet
la programmation de systèmes tels que les jeux vidéo ou les
simulateurs.
Dans cet exposé, je présenterai ReactiveML à travers l'utilisation et
la programmation de rmltop, le pendant ReactiveML du toplevel
d'OCaml. Ce toplevel permet au programmeur d'écrire interactivement
des programmes ReactiveML qui sont typés, compilés et exécutés à la
volée. Toute expression ReactiveML valide peut être chargée dans le
toplevel et a la même sémantique et la même efficacité que sa version
compilée. +
Dans cet exposé je présenterai un outil, appelé Tom, qui permet de
simplifier la programmation d'outils de manipulation et de
transformation de structures arborescentes, telles que les AST
(Abstract Syntax Trees) ou les documents XML par exemple.
Tom est un langage de programmation qui ajoute à Java des
constructions inspirées du calcul de réécriture et des langages à
base de règles. On peut, de manière approximative, voir Tom comme une
intégration d'un sous-ensemble de Caml dans Java.
Le langage repose sur trois notions fondamentales :
(i) les termes, qui sont un modèle universel permettant de
décrire des structures arborescentes, et en particulier les notions de
programmes et de preuves.
(ii) les règles, qui permettent de décrire de manière expressive des
transformations.
(iii) les stratégies, qui permettent de contrôler l'application des
règles.
La séparation transformation-contrôle est un point essentiel
permettant de rendre les règles indépendantes de leur contexte
d'utilisation, facilitant ainsi leur écriture, leur réutilisation et
l'établissement de propriétés.
Le Langage Tom est parfaitement adapté à la réalisation d'outils de
transformation et de prouveurs. Son intégration dans Java rend son
utilisation facile, aussi bien dans le milieu académique que dans le
milieu industriel. +, Je présenterai sur la base d'une démo une application des extensions
de langages, à savoir une extension Java pour l'optimisation. Cet
exemple montre la mise en oeuvre concrète dans Eclipse, les gains de
productivité et de qualité obtenus par rapport aux approches
classiques Java+DSL, la différence entre cette approche et un
générateur de code ou un préprocesseur. Il montre également une
utilisation originale d'un compilateur: la génération automatique
d'interface graphique.
Je parlerai aussi des futurs projets d'Ateji dans le domaine des
extensions de langage. +
Si une fonction φ promet de manipuler une valeur de type α sans
l'observer, on peut utiliser son code sans risque pour toutes les
affectations possibles de α : que la valeur soit entière (α = int) ou
qu'elle soit un arbre (α = tree), la fonction se comportera
toujours de façon identique. Cette propriété s'appelle le polymorphisme
paramétrique, l'essence de la généricité.
Promettre de ne pas observer de trop près son argument est un fardeau
parfois insupportable pour une fonction, pour des raisons
algorithmiques (comment prendre une décision sans savoir ce que vaut
mon argument ?), ou encore pour des raisons de performances de
bas-niveau (si je sais que α = int, je peux utiliser une primitive
dédiée de mon processeur). Même si le type d'une valeur est caché
derrière un type plus abstrait α, on peut fournir des mécanismes pour
« le redécouvrir » grâce à des tests dynamiques ou à des raisonnements
purement statiques. La propriété qui permet de diriger son calcul par
la forme des types est appelée le polymorphisme intentionnel.
Dans cet exposé, nous présenterons plusieurs versions du
polymorphisme intentionnel offertes par différents systèmes de types
et de preuves sûrs (c'est-à-dire garantissant que les programmes
ne peuvent pas planter et sont corrects vis-à-vis de leur spécification). +
Lisaac est un petit langage basé sur la technologie objet à base de
prototype. Plus flexible que l'objet à base de classe, elle permet un
dynamisme et un degré d'expressivité encore inégalés. Lisaac est
inspiré du langage Self pour les concepts d'objets à prototypes et du
langage Eiffel, pour les aspects d'ingénierie logicielle et notamment
pour la programmation par contrat. Enfin, l'objectif étant de
réaliser de la programmation de bas niveau à l'aide d'un langage de
haut niveau, un ensemble de concepts utiles à la programmation système
a été ajouté.
Le langage Lisaac utilise un nombre particulièrement restreint
d'idiomes orthogonaux rendant difficile l'élaboration d'un compilateur
efficace. Son compilateur en fait aujourd'hui l'unique langage à
prototype compilé. Les performances atteintes sont proche des
compilateurs C, voire même au-delà...
Pour étayer, approfondir et illustrer nos propos, nous ferons un
rapide tour d'horizon du développement du système d'exploitation
IsaacOS entièrement écrit en Lisaac.
Durant cet exposé, nous aborderons les thèmes suivants: concept à
prototype versus concept à classe; héritage multiple et dynamique et
autres particuliarité du Lisaac; technique de compilation et résultat
de performance; validation des concepts avec une brève présentation du
système d'exploitation IsaacOS. +, SmartEiffel, également connu sous le nom de GNU Eiffel, est à la fois
un langage et un ensemble d'outils de compilations, de documentation et
de validation.
Le langage SmartEiffel vise à favoriser la mise en pratique des
principales exigences liées au développement d'un gros logiciel par
une grande équipe. En plus d'exigences en terme de qualité, de
sécurité et de documentation, la définition de SmartEiffel est
également soucieuse de l'efficacité du programme à l'exécution. Ainsi,
le modèle des objets qui est à la base du langage intègre également
les types les plus élémentaires sans surcoût potentiel à l'exécution.
Pour sa part, le mécanisme de programmation par contrats qui est
essentiel en matière de documentation est également un bon moyen de
rechercher les meilleures performances à l'exécution.
Durant cet exposé, la visite guidée du langage présentera le modèle
d'objets, la programmation par contrats, la double forme d'héritage
multiple ainsi que le mécanisme des agents. +
Avec l'avènement du Web et des applications réparties, les machines
virtuelles applicatives sont devenues le support d'exécution de choix
pour la plupart des applications. Développer et optimiser une machine
virtuelle est un travail long et difficile qui requiert plusieurs
années. Il s'avère que la plupart des machines virtuelles possèdent
des composants communs: compilateur à la volée, ramasse-miettes,
vérifieur de type, gestionnaire de threads, gestionnaire
d'entrées/sorties, éditeur de liens paresseux, chargeur dynamique de
code.
AutoVM est une machine virtuelle générique qui factorise ces
composants communs et facilite le développement de nouvelles machines
virtuelles, ou l'amélioration de machines virtuelles existantes.
Dans cet exposé, je présenterai l'architecture logicielle de notre
prototype AutoVM et montrerai sa généricité et son extensibilité. +, La Low-Level Virtual Machine (LLVM) est un ensemble de bibliothèques
et d'outils qui facilitent le développement et l'optimisation de
compilateurs, de générateurs de code et de machines virtuelles. Clang
et VMKit utilisent LLVM pour leur générateur de code à différents
niveaux: l'un pour la compilation statique de langages de la famille C
(C/C++/ObjectiveC), et l'autre pour la compilation dynamique
d'applications Java ou .Net.
Dans cet exposé, je présenterai ces trois projets, et rentrerai dans
les détails de VMKit, que j'ai développée dans le cadre de ma
thèse. Je finirai par montrer les exemples de recherche auxquels
nous nous adressons avec l'aide de VMKit, au sein de l'équipe de
recherche INRIA/Regal. +
Nous décrirons brièvement l'état de l'art de l'utilisation des processeurs graphiques grand public (GPU) pour accélérer le traitement d'image, et nous en discuterons les limites. Puis, nous décrirons GpuCV, une bibliothèque logicielle libre et multi-plateforme pour accélérer par GPU les opérateurs de traitement d'image et de vision artificielle. GpuCV a été conçue pour être compatible avec la bibliothèque OpenCV et permettre d'intégrer facilement des opérateurs accélérés sur GPU dans des applications développées sur CPU. L'environnement GpuCV gère de façon transparente les caractéristiques du matériel, la synchronisation des données, l'activation à bas niveau des procédures GLSL ou CUDA, l'étalonnage et l'aiguillage vers la mise en oeuvre la plus performante et finalement offre un ensemble d'opérateurs de traiement accélérés par GPU. +
Malgré la grande variété des types de données que l'on rencontre dans
le domaine du traitement d'images (1D,2D,3D, scalaires, couleurs,
multi-spectrales, séquences, etc...), nous sommes souvent amenés à
appliquer des algorithmes très classiques, ou des variations de ces
algorithmes, pour le pré-traitement, l'analyse ou la visualisation de
ces données images. Par conséquent, les logiciels et les bibliothèques
que nous utilisons dans notre recherche quotidienne, devraient
également être génériques, afin de s'adapter le mieux possible aux
données à traiter. Dans ce séminaire, je présenterai quelques outils
développés dans cette optique (au laboratoire GREYC, équipe IMAGE),
qui possèdent différents niveaux d'utilisations. Je commencerai tout
d'abord par présenter CImg, une bibliothèque C++ "template" (donc
générique par nature), qui a pour but de faciliter l'implémentation
d'algorithmes de traitements d'images personnalisés. Puis,
j'introduirais G'MIC, un langage de script reprenant la plupart des
éléments de CImg, qui est dédié au traitement et à l'analyse d'images
"de tous les jours". J'essaierai de montrer comment ces différents
outils indépendants sont organisés et comment ils cherchent à aider le
chercheur ou le programmeur en traitement d'images, autant d'un point
de vue programmation pure que d'un point de vue plus haut niveau. +
La méthode multipôle rapide (Fast Multipole Method, FMM) permet de
résoudre en temps linéaire le problème à N-corps, en astrophysique ou
en dynamique moléculaire par exemple. Nous présentons ici
l'implémentation sur le processeur Cell du calcul du champ proche de
la FMM, ce qui constitue un premier pas vers une implémentation
complète de la FMM sur ce processeur. Nous détaillerons les problèmes
rencontrés, au niveau de l'architecture comme au niveau de
l'algorithmique, ainsi que les diverses optimisations mises en
place. Notre implémentation permet de calculer jusqu'à 8,5 milliards
d'interactions par seconde (115,8 Gflop/s) sur un processeur Cell, et
jusqu'à 17 milliards d'interactions par seconde sur un IBM QS20 (230,4
Gflop/s), pour des distributions uniformes ou non uniformes de
particules. +, Le processeur CELL BE développé par le consortium IBM, Sony et Toshiba
a eu un impact important dans le monde du calcul scientifique mais
aussi dans le monde du jeu. Il est le processeur de base de la
première machine à avoir atteint 1 Pflops et aussi celui de la Play
Station 3 de Sony. Pour arriver à ce niveau de performance, il intègre
9 coeurs hétérogènes interconnectés par un bus. Le coeur principal
(PPE) appartient à la famille des PowerPC. Les 8 autres coeurs (SPE)
sont spécialisés pour le calcul. Après une présentation détaillée de
l'architecture du processeur, nous développerons son mode de la
programmation : lancement de threads de calcul sur les SPE, échange de
données, programmation SIMD. +
Dans cet exposé, nous présenterons Yayi, une bibliothèque générique de
traitement morphologique d'image. Cette base logicielle, écrite en C++
et interfacée avec Python, fournit un nombre croissant de fonctions en
traitement d'image et en morphologie mathématique (distance,
segmentation, etc.). Nous discuterons de la mise en oeuvre générale,
des concepts génériques utilisés dans la bibliothèque, et de leurs
utilisations dans l'élaboration de nouveaux algorithmes. Enfin, nous
présenterons quelques pistes actuellement en développement dans Yayi
pour adresser certains des problèmes levés par la programmation
générique. +
Ce séminaire porte sur certains de mes travaux en matière de
généricité et réutilisation en traitement d'images. Ces travaux sont
présentés à une échelle algorithmique, bas-niveau, et à une échelle
logicielle, plutôt haut-niveau. À l'échelle de l'algorithme, nous
présentons une technique permettant d'étendre la généricité des
algorithmes de traitement d'images par rapport à la région d'intérêt
traitée, en complément de la généricité par rapport aux données
(1D, 2D, 3D, scalaires, couleurs, multi-spectrales, séquences,
etc.) Cette méthode repose sur une adaptation du patron de
conception « Iterator » et sur le polymorphisme de compilation en
C++. Au niveau logiciel, l'objectif de la généricité et de
réutilisation est de faciliter le couplage des algorithmes « purs »
avec des fonctionnalités supplémentaires telles que la visualisation,
l'interface homme-machine, les entrées-sorties... Dans ce cas, je
présente les principes d'une architecture flexible et évolutive
implémentée en C++, combinant la notion de (programmation par) rôle et
la notion de (programmation par) composants réutilisables. Ces travaux
sont illustrés par des applications dans le domaine médical. +, L'une des caractéristiques de la programmation objet est l'intégration
(introduite par Eiffel dans un article de la première conférence OOPSLA en
1986) entre les mécanismes d'héritage, permettant de structurer clairement
la description des systèmes, et de généricité, permettant le paramétrage de
ces descriptions. La combinaison de ces deux techniques d'architecture est
la clé de l'extensibilité et de la réutilisabilité permises par la
technologie objets. L'exposé montrera l'interaction entre la généricité et
l'héritage en Eiffel et l'application de ces concepts aux tâches d'analyse,
de conception et d'implémentation en génie logiciel. De nombreux exemples
illustreront l'application de ces idées, et compareront avec les solutions
adoptées dans des langages tels que Java et C\#. +
La plupart des frameworks de traitement d'images ne sont pas assez
génériques pour garantir une réutilisabilité effective des structures
de données et des algorithmes, tout en préservant performances et
facilité d'utilisation, et en restant proche de la théorie. Dans
cette présentation, nous proposons un cadre logiciel pour le
traitement d'images centré sur le paradigme de programmation
générique, cherchant à répondre tant aux besoins pratiques que
théoriques des scientifiques et des développeurs : la mise au point de
méthodes rapides et réutilisables, un niveau de généricité progressif,
la possibilité de traiter des ensembles de données volumineux, une
gestion de la mémoire automatique et efficace, la vérification
statique des types, l'orthogonalité des structures de données et des
algorithmes, etc. Cette approche permet aux utilisateurs de concevoir
et d'implémenter de nouvelles méthodes délivrées des contraintes
habituellement imposées pas les outils logiciels, de pratiquer des
expériences inter-domaines, de généraliser certains résultats et de
transformer facilement des prototypes en de vraies applications. +, Les Diagrammes de Décision (DDs) forment une vaste famille de
structures de données, qui permettent de représenter et manipuler très
efficacement de grandes quantités d'informations. Cependant, parmi les
nombreux types de DDs, l'utilisateur est souvent désemparé pour
choisir le bon. Souvent, aucun type ne répondant exactement à ce qu'il
cherche, l'utilisateur doit faire adapter ses données au type de DDs
choisi.
Le problème est que chaque type de DDs possède sa propre
définition. Il n'existe aucun socle commun qui permette de définir
n'importe quel type de DD. Ce problème se reflète au niveau des
opérations manipulant les DDs. Celles-ci sont aussi spécifiques à
chaque type.
Cet exposé présente les Polymorphic Decision Diagrams, un cadre assez
général permettant de spécifier de nombreux types de DDs
existants. L'utilisateur peut ainsi décrire simplement les DDs
correspondant le mieux aux données qu'il souhaite représenter. Ce
cadre permet de plus d'ajouter dans la spécification les informations
qui permettront de retrouver les performances des types définis
jusqu'à présent. Un exemple concret impliquant des loutres permettra
de montrer les possibilités offertes par ce cadre. +
Le projet BrainVISA (http://brainvisa.info) est en train de
développer, avec le soutien du projet européen HiPiP
(http://hipip.eu), une architecture générique pour la parallélisation
des applications. Cette architecture fournira un accès à divers moyens
de calculs (fermes de stations de travail, clusters, centres de
calculs, etc.) en s'appuyant sur des solutions existantes pour la
gestion des ressources (Sun Grid Engine, Condor, LSF, etc.) Cette
architecture est développée pour répondre aux besoins croissants de
moyens de calcul dans le monde de la recherche en neuroimagerie.
Au cours de ce séminaire, j'aborderai rapidement le contexte de la
recherche en neuroimagerie en me focalisant sur les besoins en
parallélisation d'applications. Ensuite, je détaillerai la solution
que nous avons choisie pour répondre à ces besoins. +, Le traitement d'images est par nature un procédé discret, au cours
duquel un signal continu est décomposé en un ensemble de pixels, ou de
voxels pour des images tri-dimensionnelles. Au niveau géométrique, cette
nature discrète pose peu de problèmes, car la plupart des opérations
géométriques sont indépendantes de la grille sous-jacente ; au niveau
topologique, le problème est tout autre. Deux des notions fondamentales
de la topologie, le voisinage et la connexité, sont radicalement
différentes entre un espace continu et un espace discret : il est entre
autres impossible de subdiviser un voisinage discret de façon infinie
comme c'est le cas dans un espace euclidien.
Bien que certaines bibliothèques de traitement d'images contiennent des
algorithmes topologiques, notamment de squelettisation, le type de
voisinage utilisé par ces algorithmes est généralement fixé par le code,
ce qui empêche une adaptation facile à un autre type de connexité ou à
un espace de dimension différente.
Ce séminaire présente une méthode générique pour intégrer les notions
discrètes de voisinage et de connexité à une bibliothèque de traitement
d'images programmée en C++. Je montrerai également comment obtenir de
façon simple un algorithme de squelettisation homotopique en utilisant
ces notions. +
Dans la recherche multimédia basée contenu, on distingue trois champs d'applications différents : la recherche de cible dans laquelle on désire retrouver un document particulier ; la recherche interactive, dans laquelle l'utilisateur définit l'objet de la requête au fil de son interaction avec le système ; et la catégorisation, où il s'agit d'étiqueter les données en un certain nombre de classes prédéfinies.
Cette présentation fera le tour d'horizon de mes travaux de recherche dans deux de ces domaines. Une première partie concernera la recherche de cible, où je présenterai le cas particulier de la recherche de quasi-copies dans de très grands volumes de données, et en particulier une application à la recherche de scènes urbaines identiques dans le cadre du projet iTowns.
Dans la deuxième partie, je développerai mes travaux récents sur la classification d'images. L'accent y sera mis sur la fusion de descripteurs multimédias et les techniques d'apprentissage statistique permettant d'apprendre conjointement l'opération de fusion avec la fonction de classification. +
L'idée d'une fonction est que la quantité d'entrée détermine complètement la quantité de sortie. En informatique, la quantité est une structure de données qui peut être simple, booléenne, entière, ou complexe, image, graphe, arbre. Dans ce domaine, un champ de recherche est de construire un ensemble de fonctions élémentaires, puis par composition d'en créer des plus compliquées. Pour cette dernière, une solution pratique est le langage Caméléon conçu par V. Tariel et O. Cugnon de Sevricourt, qui est un langage de flux de données génériques dont la sortie est prévue en janvier 2011. Générique signifie que tous les types de données peuvent être intégrés dans le langage. Pour cette première, ce séminaire couvrira quelques définitions de fonctions primaires reliées à l'image, incorporées à la bibliothèque standard de Caméléon. A la manière de l'implémentation de la bibliothèque standard du C++, il y aura l'utilisation d'un côté de l'algorithme générique for\_each en typage statique et de l'autre des opérateurs et des itérateurs organisés en programmation orientée objet. L'itérateur localise l'action suivant différents paradigmes : ensemble fini et dénombrable, voisinage, convolution, zone d'influence. L'opérateur agit suivant différents paradigmes : arithmétique, croissance de régions. +
Depuis 2000, on assiste à un regain d'intérêt pour les langages typés dynamiquement
regroupés sous la bannière "langage de script". Pour les langages de script les plus
populaires, comme PHP, Python ou Ruby, il existe, en plus des implantations
écrites en C, des implantations plus récentes utilisant des environnements
comme la machine virtuelle Java (JVM) ou la plateforme .Net.
Ces implantations sont souvent plus efficaces que les implantations historiques,
pourtant, ces environnements d'exécution utilisent des langages intermédiaires
typés statiquement qui sont peu propices à l'implantation de langage typé dynamiquement.
Partant de ce constat, le Java Community Process a créé la JSR 292 intitulée
"Supporting Dynamically Typed Languages on the JavaTM Platform" dont le but
est de proposer une API facilitant l'implantation et les performances des
langages de script sur une machine virtuelle Java.
Mon exposé se compose de deux parties.
Dans un premier temps, en tant que membre du groupe d'experts, j'essaierai de restituer
de façon didactique les concepts introduits par la JSR 292 en expliquant les tenants et les aboutissants.
La seconde partie, plus personnelle, montrera comment développer l'environnement
d'exécution d'un langage de script en utilisant les outils fournis par la JSR 292.
Je m'appuierai pour cela sur un prototype de langage que j'ai développé et nommé
PHP.reboot. +
Nous étudions la problématique du mélange de paradigmes de programmation
variés plongés dans un environnement concurrent. Dans cette
perspective, nous poursuivons
un cheminement similaire à celui qui conduit du lambda-calcul aux
langages fonctionnels, mais
en prenant comme point de départ le π-calcul. Nous proposons la
machine abstraite des π-threads
dont la principale originalité est l’absence de pile d’exécution.
Cette caractéristique
permet de nous reposer dans nos implémentations sur des algorithmes
simples et naturellement
concurrents, notamment pour ce qui concerne l’ordonnancement et le
ramasse-miettes. Pour ce
dernier, nous proposons un algorithme permettant de récupérer très
simplement les cycles de
processus en interblocage et autres structures bloquantes. +
La plupart des bibliothèques génériques en traitement d’images mettent l’accent sur la généricité, la mise en pipeline d’opérations basiques, mais peu mettent l’accent sur la sélection d’un sous-ensemble de pixels concerné par un algorithme. En pratique de nombreux algorithmes ne s’appliquent que sur un sous-ensemble simple (rectangle) ou complexe (forme contiguë quelconque) de pixels qui ne sont qu’une petite fraction d’une image. La création d’un masque précisant les pixels concernés ne semble pas une solution optimale (contrainte mémoire et calculatoire). Dans le cadre de développement d’algorithmes en traitement d’images et vidéos, le laboratoire Canon Research Centre France (localisé à Rennes) développe une bibliothèque générique de traitement d’images qui ajoute la notion de forme à toute manipulation basique ou complexe d’une image. Une « arithmétique » des formes permet une sélection précise de pixels et une exécution efficace d’algorithme complexe. Les motivations, la mise en œuvre de cette bibliothèque, les outils template utilisés seront présentés et illustrés d’exemples concrets. +
Pour encoder de manière efficace une séquence vidéo, la redondance
temporelle est souvent utilisée. Pour cela, le mouvement entre l'image
considérée et une image de référence est estimé. Cela permet de
générer une prédiction à partir de l'image de référence et seule la
différence entre la prédiction et l'image réelle est enregistrée. Pour
estimer ce mouvement, les codecs se contentent souvent de suivre
l'évolution spatiale de blocs dans l'image. Ils associent, pour chaque
bloc de l'image considérée, un bloc similaire dans un voisinage proche
dans l'image de référence. Nous présentons ici une méthode originale
pour réaliser cette prédiction par compensation de mouvement. Notre
méthode utilise les distances tangentes. Cela permet non seulement
d'estimer l'évolution de la position des blocs de l'image mais en
partie aussi l'évolution du bloc lui-même. Nos prédictions sont donc
de meilleure qualité. Utilisée dans l'encodage de séquences, on peut
espérer un gain de compression non négligeable. Pour valider
l'efficacité de la méthode, nous intégrons cette méthode dans le codec
Theora et mesurons son efficacité en comparant les résultats obtenus
avec notre méthode et ceux obtenus par une stratégie classique (le
block-matching). +
Ces dernières années ont vu exploser le nombre de vidéos disponibles
sur internet. Pour permettre leur exploitation, il est nécessaire de
mettre en place des systèmes analysant automatiquement ces données
multimédia. De tels systèmes permettent notamment d'indexer
automatiquement des vidéos en fonction de leurs contenus. Durant
cette présentation, je m'intéresserai aux récentes avancées effectuées
dans ce domaine. Je présenterai des descripteurs vidéos, développés
dans le cadre de ma thèse, qui capturent le mouvement et l'apparence
d'une vidéo pour les résumer dans une courte signature. Ces
signatures peuvent être utilisées a posteriori pour détecter
différents évènements ou concepts dans les vidéos. +, Conçus à l'origine pour le rendu 2D et 3D, les processeurs graphiques
(GPU) peuvent aujourd'hui être considérés comme des processeurs
génériques massivement parallèles. Mais ce parallélisme impose des
contraintes sur les algorithmes implantés et les types de données
utilisés. D'autre part, le bus de communication entre le processeur
central (CPU) et le GPU peut être un goulot d'étranglement.
Ce séminaire débutera par un aperçu des avantages et inconvénients de
la programmation GPU, puis je présenterai l'implantation d'un
algorithme temps réel de suivi de points dans une vidéo. Je terminerai
par l’introduction de deux petites boîtes à outils : Cuimg et Dige.
Cuimg utilise C++ pour simplifier l'écriture d'algorithmes de
traitement d'images avec CUDA, tandis que Dige, basée sur le framework
Qt, permet le prototypage rapide d'interfaces graphiques. +
Dans ce séminaire je présenterai un algorithme de résolution approchée
pour le problème du Compressive Sensing basé sur la programmation convexe.
Cet algorithme a la particularité d'avoir été pensé dès sa conception pour
tirer partie des architectures matérielles modernes, ce qui permet une
implémentation efficace et rapide sur celles-ci. Bien qu'une résolution
approchée soit en pratique suffisante pour obtenir rapidement une solution
de très bonne qualité, une variante exacte très rapide sera aussi
présentée. Cette dernière n'est toutefois utilisable que sous certaines
conditions. Trois types d'architectures parallèles sont ici envisagées :
des processeurs multi-cœurs avec unités de calcul vectoriel, des
processeurs graphiques (GPU) et le processeur Cell. +
Comment Javascript, un langage dynamique, interprété et non typé,
parvient à être aussi rapide ? Quelles sont les avancées qu'il reste
à faire pour obtenir des performances identiques au langage C ?
Pour illustrer cette présentation, on s’intéressera à l’évolution du
navigateur Mozilla Firefox et aux différentes approches pour résoudre
ce problème. +
The ilastik system developed by our group uses machine learning and
simple interaction techniques to empower users without special image
processing expertise to segment and analyze their 2- and 3-dimensional
image data on their own. It offers a number of easy-to-use workflows
for various common analysis tasks. The talk will present two of these
workflows (“interactive classification” and “region carving”), going
from an online demonstration of the high-level user experience down to
the algorithmic and software design details. Special emphasis will be
put on aspects of genericity and parallelization which facilitate
convenient adaptation of basic building blocks to different contexts
without loss of performance. Examples from challenging biological
applications will illustrate our system's capabilities. +
Nous traitons du problème de la conception d'un compilateur où des
informations sur le coût à l'exécution du code objet sont retournées
en tant qu'annotations de coût sur le code source, et ce de façon
certifiée correcte. Pour cela, nous avons besoin d'une idée souple et
précise : (i) du sens donné aux annotations de coût, (ii) de la
méthode pour les prouver correctes et précises, et (iii) de la manière
d'en composer les preuves. Nous proposons ce que nous appelons une
approche par étiquetage pour répondre à ces trois questions. Dans un
premier temps, nous montrons son application sur un compilateur jouet.
L'étude formelle qui en découle suggère que l'approche par étiquetage
a de bonnes propriétés de compositionnalité et de passage à l'échelle.
Afin de s'en convaincre davantage, nous rapportons notre retour
d'expérience sur l'implémentation d'un compilateur prototype écrit en
ocaml pour un large sous-ensemble du langage C. +, «The effective exploitation of his powers of abstraction must be
regarded as one of the most vital activities of a competent
programmer.» disait Dijsktra.
En effet, pour aborder la complexité d'un problème, l'explicitation
des concepts utiles à sa formalisation et à sa résolution est bien
souvent une étape clé. Lorsque que l'on étend ce processus à une
classe de problèmes qui partagent les mêmes concepts, il est naturel
de se doter d'un langage le plus approprié possible pour manipuler ces
abstractions spécifiques à un domaine (en anglais, «Domain Specific
Language»).
Comment implémenter ces DSLs? Une première approche classique reflète
les constructions du DSL sous la forme d'un jeu de fonctions de
bibliothèque. L'avantage de cette approche est d'utiliser directement
son langage généraliste préféré, et sa chaîne de compilation
optimisée, de façon à générer du code machine à moindre frais. Par
contre, dans ce cadre, l'écriture de passe d'optimisations spécifiques
au DSL - à moins d'utiliser des techniques pointues de
méta-programmation - est a priori impossible.
Une seconde approche, opposée, consiste à écrire un compilateur pour
le DSL à partir de zéro. Toute liberté est alors donnée à
l'implémenteur d'intégrer à son compilateur des passes d'optimisation
spécifiques… mais au prix d'une réimplémentation de passes de
compilation déjà présentes, et certainement plus abouties, dans le
compilateur de son langage généraliste favori.
Dans cet exposé, je présenterai les travaux de Martin Odersky et
son équipe sur la virtualisation de DSLs à l'intérieur du langage de
programmation Scala. La virtualisation de langage utilise
intensivement le polymorphisme et la composition mixin de Scala ainsi
que des techniques de génération de code à l'exécution pour embarquer
des langages spécifiques dans Scala dont la compilation peut
réutiliser des modules du compilateur mais aussi étendre ces derniers
par des optimisations spécifiques au domaine. +
L'industrie des effets spéciaux produit une grande quantité d'images
qu'il faut traiter et afficher. Dans le cadre de ses développements
internes, Mikros Image a développé et mis en Open Source un player
d'images temps réel : duke. Dans cet exposé je décrirai quels sont
les enjeux techniques d'un tel logiciel (allocation mémoire, accès
disque, multiplicité des formats, affichage, traitement...) puis
j'expliquerai plus en détails les étapes de la conception d'un
composant essentiel permettant de lire et décoder le plus rapidement
possible les images à afficher. Ce composant ayant pour but d'être
intégré dans d'autres outils, il doit être réutilisable. +
Une question fondamentale pour mes recherches est de savoir ce qu'est
une image. Cela peut sembler à première vue une question trop simple :
une image, c'est un ensemble de points. Mais ces points sont reliés
entre eux, c'est ce qu'on appelle une structure, et ils ont des
données de types multiples qui leur sont attachées. La bibliothèque
Milena, développée au LRDE, est une bibliothèque générique dédiée au
traitement d'images. Dans Milena, trois axes indépendants sont
développés : l'axe des structures, l'axe des données, et celui des
algorithmes, c'est-à-dire de ce qu'on peut faire avec une image.
Dans cet exposé, je vais développer plusieurs exemples dans lesquels
je choisirai un algorithme et un type de données, en faisant varier la
structure. Changer la structure, c'est penser les images d'une manière
différente, et c'est quelque chose d'extrêmement porteur en recherche.
- Un premier exemple est celui d'un algorithme classique de
segmentation : la ligne de partage des eaux. Originellement pensé sur
les pixels, sa traduction dans le cadre des arêtes donne le problème
classique d'arbre couvrant de poids minimum. Si la ligne de partage
des eaux est très connue en traitement d'images, les arbres de
poids minimum sont très utilisés en classification. Un pont naturel
est alors établi entre deux communautés différentes, et les idées
provenant de ces deux communautés peuvent être combinées.
- Un deuxième exemple est celui de la représentation arborescente des
images. Pour illustrer, tant les lignes de niveaux que les
composantes connexes des ensembles de niveaux (les coupes) des
images sont naturellement structurées en arbre : deux lignes ou deux
composantes sont soit disjointes soit emboîtées. On peut filtrer
une image en éliminant de l'arbre tous les nœuds qui ne vérifient
pas un critère. Mais on peut aussi considérer l'arbre lui-même comme
une image, et appliquer sur cet arbre un algorithme de traitement
d'images. C'est une idée récursive très riche.
D'autres exemples pourront être développés en fonction du temps : liens
entre ligne de partage des eaux topologique et segmentation
hiérarchique, topologie discrète dans divers cadres...
La bibliothèque Milena permet d’appliquer la plupart des algorithmes
existants à une nouvelle structure, ce qui est un gain de temps
incontestable. Cela permet de se concentrer sur ce qui fait le cœur
de mon métier: chercher un algorithme plus efficace, adapté à un type
de structure, ou encore chercher quelles sont les propriétés
mathématiques d’un algorithme sur une structure donnée.
Concilier généricité et performance des systèmes de vision a toujours
été au cœur des préoccupations scientifiques du laboratoire
d'Électronique et Informatique d'ENSTA-ParisTech. Nous y avons abordé
ce problème sous différents points de vue: électronique,
algorithmique, et logiciel. Depuis nos travaux sur les rétines
programmables et leur algorithmique exotique, nous avons
progressivement intégré la multiplicité des modèles et structures de
données, ainsi que l'emprise des architectures sur étagères, pour
appréhender l'hétérogénéité des systèmes multi-plateformes.
Dans cette présentation à deux voix, on abordera le problème sous deux
angles complémentaires, l'un touchant au modèle et aux algorithmes,
l'autre au logiciel et aux plateformes de calcul.
Ce premier exposé présente un modèle générique de traitement et de
représentation des images fondé sur les espaces de caractéristiques
"local jets" (LJ, ou dérivées partielles multi-échelles), comme
exemple de cadre algorithmique unifié. Grâce à un espace où la
métrique naturelle est directement liée à la similarité visuelle, ce
cadre permet d'aborder un grand nombre d'opérateurs de traitement
d'images de bas niveau, qui correspondent généralement à la
rétro-projection dans l'espace image de points de l'espace des
caractéristiques transformé. Il permet aussi d'aborder des
représentations visuelles de plus haut niveau (modèles d'objet par
exemple) à partir de statistiques globales extraites de l'espace des
caractéristiques. On justifiera cette représentation et on
l'illustrera par diverses applications : Moyennes non locales
(NL-Means) par Convolution dans l'espace LJ pour le débruitage de
vidéos, Calcul du flux optique par recherche du plus proche voisin
dans l'espace LJ, Modélisation de fond statique par échantillonnage de
l'espace LJ, Détection d'objets par transformée de Hough dense... +, Dans ce second exposé, Matthieu Garrigues parlera de ses travaux sur
l'analyse des mouvements apparents dans un flux vidéo. La primitive de
base, présentée dans un séminaire précédent, permet le suivi temps
réel (supérieur à 30 images par seconde) de plusieurs milliers de
particules. Ces travaux nous ont permis de développer un cadre
générique facilitant l'analyse de scènes dynamiques prises de caméras
fixes ou mobiles. Nous montrerons comment cette brique logicielle a
été utilisée dans deux exemples d'applications : l'extraction des
plans principaux et l'estimation de la profondeur dans un système
mono-caméra. Le suivi de particules a été implémenté sur processeurs
graphiques avec le framework CUDA, et sur CPU-multicœurs avec
OpenMP. Nous expliquerons comment C++ a été utilisé pour factoriser un
maximum de code entre ces deux implémentations. +
L'arrivée des GPU (Graphics Processing Unit) a profondément changé la
manière de concevoir la notion de coprocesseur. A moins de 500€, il est
désormais possible d'avoir à sa disposition une puissance de calcul qui
n'était réservée jusqu'à un passé récent qu'aux grands centres de calcul. La
société Nvidia, en mettant au point l'environnement CUDA, a fourni à la
communauté des développeurs des moyens simples et efficaces pour rendre
cette puissance de calcul accessible au plus grand nombre. Depuis, sous
l'impulsion de la société Apple, le standard OpenCL est venu ouvrir la voie
d'une véritable parallélisation des applications sur l'ensemble des
ressources processeur offertes aux développeurs.
Cet exposé décrira les différentes technologies permettant la programmation
parallèle des GPU en mettant l'accent sur les contraintes actuelles et les
progrès à venir des futures architectures comme le processeur Kepler. Des
démonstrations ainsi que des exemples de code viendront compléter cet
exposé. +
(Morphological Filtering in Shape Spaces: Applications using Tree-Based Image
Representations)
Connected operators are filtering tools that act by merging elementary
regions of an image. A popular strategy is based on tree-based image
representations: for example, one can compute a shape-based attribute on
each node of the tree and keep only the nodes for which the attribute is
sufficiently strong. This operation can be seen as a thresholding of the
tree, seen as a graph whose nodes are weighted by the attribute. Rather than
being satisfied with a mere thresholding, we propose to expand on this idea,
and to apply connected filters on this latest graph. Consequently, the
filtering is done not in the image space, but in the space of shapes built
from the image. Such a processing is a generalization of the existing
tree-based connected operators. Indeed, the framework includes classical
existing connected operators by attributes. It also allows us to propose a
class of novel connected operators from the leveling family, based on shape
attributes. Finally, we also propose a novel class of self-dual connected
operators that we call morphological shapings. +, Le model checking est une technique de vérification formelle
automatique. Prenant en entrée un modèle décrivant toutes les exécutions
possibles du système et une propriété exprimée sous la forme d'une formule
de logique temporelle, un algorithme de model checking répond si le modèle
satisfait ou non la formule. Le problème principal du model-checking est
l'explosion combinatoire de l'espace d'états décrivant le système.
Afin d'améliorer les performances, on a apporté les contributions suivantes
à l'approche automate du model checking. D'abord l'amélioration de
l'algorithme de vérification en deux passes de l'approche basée sur les
automates Testeur TA (Testing Automaton). Ensuite la proposition d'une
méthode permettant de transformer un automate TA en un automate vérifiable
en une seule passe, qu'on a appelé STA (Single-pass Testing
Automaton). Enfin, la contribution la plus significative est un nouveau type
d'automate baptisé TGTA (Transition-based Generalized Testing
Automaton). L'apport principal de cette nouvelle approche consiste à
proposer une méthode permettant de supprimer les transitions bégayantes dans
un TGTA sans avoir besoin, ni d'ajouter une seconde passe comme dans
l'approche TA, ni d'ajouter un état artificiel comme dans l'approche STA. +, Le model checking est une technique qui permet de s'assurer qu'un système
vérifie un ensemble de caratéristiques appelées propriétés. Le système et la
négation de la formule sont ensuite représentés de manière abstraite (ici un
automate) pour pouvoir détecter des comportements incohérents. Ces
propriétés ont été classifiées et possèdent des particularités qui peuvent
être exploitées afin de réduire la complexité du processus de
vérification. Nous montrerons ici comment tirer parti dynamiquement des
différentes classes de formules. +
Afin d'exploiter le potentiel des puces multi-cœurs pour une performance
évolutive et à haut rendement énergétique, le projet Apple-CORE a
co-conçu un modèle général d'architecture matérielle et une interface de
contrôle de parallélisme. Cette interface, appelée SVP, est réalisée par
du matériel sur puce dédié à la gestion de la concurrence de programmes
parallèles exécutés sur plusieurs cœurs. SVP se base sur les principes
de synchronisation de flux de données («data flow»), de programmation
impérative et d'exécution efficace du parallélisme en termes de budget
temps et énergie. Les composants matériels correspondants peuvent
coordonner plusieurs cœurs RISC équipés de multi-threading matériel,
organisés en clusters de calcul sur puce, dits «Microgrids».
Comparés à l'approche traditionnelle «accélérateurs», les Microgrids sont
destinés à être utilisés comme composants dans les systèmes distribués sur
puce contenant à la fois des grappes de petits cœurs et optionnellement de
gros cœurs –optimisés pour l'exécution séquentielle– disponibles en tant que
«services» pour les applications. Les principaux aspects de cette
architecture sont l'asynchronisme, c'est-à-dire la capacité à tolérer les
opérations irrégulières avec des temps de latence longs, un modèle de
programmation à échelle invariante, une vision distribuée de la puce, et une
mise à l'échelle transparente de la performance d'un seul code binaire à
plusieurs tailles de grappes de cœurs.
Cette présentation décrit le modèle d'exécution, la micro-architecture des
cœurs, sa réalisation au sein d'une plateforme et son environnement
logiciel. +, The Single-chip Cloud Computer (SCC) is a 48-core experimental processor
created by Intel Labs targeting the many-core research community. The 6x4
mesh Network-on-Chip provides 24 tiles with 2 cores each. All cores are
independent and run their own instance of an operating system. It has
hardware support (local buffers on the tiles) for sending short messages
between cores, and allows for voltage and frequency control at 8 and 2 cores
respectively.
We have already modified the SVP runtime system to use these on-chip buffers
for the communication between threads executed on separate cores. We also
created a visual application for manual process migration and scheduling on
the SCC as well as a library for customized voltage and frequency scaling on
the chip.
Currently we focus on automated parallelization and mapping of one or
multiple sequential programs onto the 48 cores by modifying the daedalus
framework to target the SCC. The daedalus framework parallelizes sequential
C programs using Kahn Process Networks (KPNs) and generates code to run the
KPN on multiple hardware platforms like for example an FPGA, SMP CPU or
GPU. The SCC backend, which is work in progress, should result in a tool
that utilizes the SCC cores in an optimal way by means of performance and
energy consumption. It should also allow the system to dynamically adapt on
changes in the computational or communicational needs of the processes by
scaling frequency and migrating processes. +
Avec l'avènement du Web et du besoin de protéger les utilisateurs contre des
logiciels malicieux, les machines virtuelles langages, comme les machines
virtuelles Java et .Net, sont devenues la norme pour exécuter des
programmes. Dans cet exposé, je vais présenter les travaux que j'ai menés
ces dernières années et qui se sont concentrés sur trois aspects des
machines virtuelles: leur design, leur sûreté de fonctionnement, et leur
performance sur les architectures multi-cœurs.
Ma première contribution est VMKit, une bibliothèque qui facilite le
développement de nouvelles machines virtuelles performantes en cachant leur
complexité dans un ensemble de composants réutilisables. Ma seconde
contribution est I-JVM, une machine virtuelle Java qui élimine les huit
vulnérabilités connues qu'un composant de la plateforme OSGi pouvait
exploiter. Ma troisième contribution vise à améliorer les performances des
machines virtuelles sur les architectures multi-cœurs en se focalisant sur
les verrous et les ramasse-miettes: avec un mécanisme de verrouillage qui
surpasse tous les autres mécanismes connus lorsque le nombre de cœurs
augmente, et avec avec une étude des goulets d'étranglement des
ramasse-miettes sur les architectures multi-cœurs. +
En morphologie mathématique, la représentation d'une image par l'arbre
des formes n'est en fait pas vraiment auto-duale: elle se heurte à la
dualité entre séparation et connexité (c4 vs. c8 en 2D) et au final
des aberrations apparaissent. À la recherche d'un algorithme original
pour le calcul de l'arbre des formes, une nouvelle représentation
discrète d'images 2D est apparue. Définie sur la grille de Khalimsky
avec la topologie d'Alexandroff et s'appuyant sur l'analyse
multivoque, cette représentation a la particularité de satisfaire à de
nombreuses propriétés du continu et de s'affranchir des problèmes
topologiques classiques. +
SMIL est une bibliothèque de traitement d'images 2D/3D. Elle a été
développée pour répondre à une demande de plus en plus forte (en
particulier dans le cas de projets industriels) en termes de
performances : taille d'images (2D ou 3D) et temps d'exécution.
Développée en C++ et utilisant les templates, elle peut être utilisée
avec n'importe quel type standard de données. Un effort important a
été porté sur la factorisation du code (par le biais de functors),
d'une part, pour faciliter l'intégration de nouvelles fonctions, et
d'autre part pour concentrer les parties du code permettant
l'optimisation. Ces "briques" communes optimisées utilisent le code
SIMD généré par l'auto-vectorisation de gcc et sont également
parallélisées grâce à l'utilisation d'OpenMP. +
Large distributed systems on the Internet are subject to hostile
environmental conditions such as node failures, erratic communications, and
partitioning, and global problems such as hotspots, attacks, multicast
storms, chaotic behavior, and cascading failures. How can we build these
systems to function in predictable fashion in such situations as well as
being easy to understand and maintain? In our work on building
self-managing systems in the SELFMAN project, we have discovered a useful
design pattern for building complex systems, namely as a set of Weakly
Interacting Feedback Structures (WIFS). A feedback structure consists of a
graph of interacting feedback loops that together maintain one global system
property. We give examples of biological and computing systems that use
WIFS, such as the human respiratory system and the TCP family of network
protocols. We then show the usefulness of the design pattern by applying it
to the Scalaris key/value store from SELFMAN. Scalaris is based on a
structured peer-to-peer network with extensions for data replication and
transactions. Scalaris achieves high performance: from 4000 to 14000
read-modify-write transactions per second on a cluster with 1 to 15 nodes
each containing two dual-core Intel Xeon processors at 2.66 GHz. Scalaris
is a self-managing system that consists of five WIFS, for connectivity,
routing, load balancing, replication, and transactions. We conclude by
explaining why WIFS are an important design pattern for building complex
systems and we outline how to extend the WIFS approach to allow proving
global properties of these systems. +
Le compilateur GCC est extensible via des greffons (plugins) depuis
plusieurs années. Mais c'est un logiciel libre complexe (de 10MLOC) et
encore en évolution, dont on décrira grossièrement l'architecture. Écrire
des greffons en C est fastidieux.
Le language d'extension MELT (domain specific language) permet d'étendre
moins péniblement le compilateur GCC. Il offre une syntaxe régulière et
simple, inspirée de LISP. MELT est traduit en du code C (ou C++) adapté aux
internes de GCC et son implémentation (en logiciel libre) est
auto-amorcée. Il offre des traits permettant des styles de programmation de
haut niveau (styles fonctionnel, objet, réflexif).
On décrira un peu l'implémentation de MELT, sa syntaxe et ses traits
caractéristiques, et les exemples d'extensions. +
Il existe de nombreux langages informatiques, et les débats concernant leurs
avantages et inconvénients respectifs sont nombreux, mais peu considèrent la
question du développement d'applications sécurisées, c'est-à-dire robustes
contre les actions d'agents malveillants. C'est l'optique abordée dans cette
présentation, qui rebondit sur de nombreuses illustrations dans différents
langages afin de pouvoir cerner ce que seraient les bonnes propriétés d'un
langage vis-à-vis de la sécurité, mais aussi des recommandations de codage
pertinentes ou encore des outils pertinents pour le développement et
l'évaluation d'applications de sécurité. +
Le réductionnisme est une technique réaliste de conception et implantation
de vrais langages de programmation, et conduit à des solutions plus faciles
à étendre, expérimenter et analyser. Je vais décrire la conception et
l'implantation de GNU epsilon, un langage de programmation extensible, basé
sur un langage-noyau minimaliste impératif du premier ordre, équipé de
mécanismes d'abstraction forts et avec des possibilités de réflexion et
auto-modification. Le langage peut être étendu à des niveaux très hauts: en
utilisant des macros à la Lisp et des transformations de code à code
réécrivant les expressions étendues en expressions-noyau, on arrive à
ajouter les clôtures et les continuations de première classe au dessus du
noyau.
Les programmes qui ne s'auto-modifient pas peuvent être analysés
formellement, grâce à la simplicité de la sémantique. Je vais parler
rapidement d'une analyse statique dont j'ai prouvé une propriété de
«soundness» par rapport à la sémantique dynamique. Le langage se prête à une
implantation efficace: je vais montrer un prototype de compilateur natif
particulièrement simple. +
Address & Thread sanitizer sont des outils destinés à détecter les
erreurs d'accès à la mémoire ainsi que les erreurs d'accès concurrents
en environnement multi-threads.
Ces outils sont constitués de deux parties logiques distinctes: une
partie instrumentant le code généré de manière statique, et un
environnement d'exécution.
Cet exposé présente l'implémentation de Address & Thread Sanitizer dans
GCC, les principes de fonctionnement de l'environnement d'exécution de
ces deux outils ainsi que les futures directions du projet. +
CPC est une extension concurrente du langage C. Le code CPC, en style à
threads, est traduit par le compilateur CPC en un code à style à événements;
ce code peut ensuite être exécuté, au choix du programmeur, par des threads
natifs « lourds » ou par un ordonnanceur à événements manipulant des
structures de données extrêmement légères. Cette technique d'implémentation
induit un style de programmation original, où les threads sont « gratuits ».
Cependant, le programmeur peut choisir d'utiliser des threads natifs
« lourds » lorsque c'est nécessaire, par exemple pour exploiter le
parallélisme du matériel ou utiliser des bibliothèques bloquantes.
La technique de compilation de CPC est basée sur des techniques formalisées
et bien connues de la communauté de la programmation fonctionnelle, telles
que la conversion en style à passage de continuations (CPS), le
lambda-lifting, ou l'introduction de fonctions terminales. La correction de
ces techniques a été prouvée formellement.
Dans cet exposé, je donnerai quelques exemples du style typique de
programmation en CPC tirées de Hekate, un seeder BitTorrent écrit en CPC.
Je décrirai ensuite la transformation en style à passage de continuations et
je décrirai la technique de traduction utilisée par le compilateur CPC. +
Component trees are essential tools in several morphological processing
methods, such as attribute filtering, or visualization, or the computation
of topological watersheds. Algorithms for computation of these trees fall
into two main categories: (i) Flood-filling algorithms, exemplified by the
algorithms of Salembier et al (1998), Hesselink (2003), and Wilkinson
(2011), and (ii) Union-find methods, such as Najman and Couprie (2006),
and Berger et al (2007). As images become larger, and parallel computers
become commonplace, there is an increased need for concurrent algorithms to
compute these trees. The first such algorithm was published by Wilkinson et
al in 2008, and was based on the divide-and-conquer principle. It splits up
the data spatially, computes local component trees using any arbitrary
algorithm which yields a union-find type representation of each node, and
glues these together hierarchically. The main drawback of this method is
that it does not work well on high-dynamic-range images, because the
complexity of the glueing phase scales linearly with the number of grey
levels.
In the current work, carried out by Moschini, Meijster, and Wilkinson within
the HyperGAMMA project, we develop a new algorithm for floating point or
high-dynamic-range integer images. It works in a two-tier process, in which
we first compute a pilot component tree at low dynamic range in parallel,
with one grey level per processor using dynamic quantization, and
Salembier's flood-filling method to build the local trees, and the previous
parallellization scheme. After this, a refinement stage is performed. This
refinement stage is based on the algorithm of Berger et al. As such, the new
algorithm combines the two main types of algorithm in a single framework.
Timings on images of up to 3.9 GPixel indicate a speed-up of up to 22 on 64
cores. The algorithm is more than 14x faster than the fastest sequential
algorithm on the same machine. We will apply the new algorithm to
astronomical data sets, including improvements to the SExtractor tool for
object detection. The importance of the new algorithm extends beyond
computation of component trees because it allows development of a fast
alpha-tree algorithm suitable for any pixel-difference metric in case of
vector images (i.e. not just $L_\infty$-based metrics on low dynamic range
colour images).
Le Web a subi en quelques années une évolution radicale, passant d'une
plateforme de données à une plateforme d'applications. Mais la plupart des
outils de programmation n'ont pas été conçus pour cette nouvelle vision du
Web.
Le projet Ocsigen a pour but d'inventer de nouvelles techniques de
programmation adaptées aux besoins des sites Web modernes et des
applications Web distribuées. Il permet de programmer les parties client et
serveur dans le même langage, et même, comme une seule et même
application. La puissance expressive du langage OCaml permet d'introduire
une abstraction des technologies sous-jacentes dans le but de simplifier la
programmation d'interactions Web complexes. Le système de types très avancé
du langage permet d'améliorer la fiabilité des programmes et le respect des
standards. Cela permet aussi de réduire beaucoup le temps de
développement.
Cet exposé donnera un aperçu global du projet et montrera comment écrire un
exemple d'application simple. +
Les automates acycliques sont utilisés dans tous les logiciels de traitement
de la langue naturelle essentiellement pour la représentation des lexiques,
des dictionnaires et des interprétations morpho-syntaxiques des textes.
Nous présenterons des résultats sur les stratégies de construction, de
manipulation et de stockage de ces automates. En particulier un algorithme
de construction dynamique. +
CLAIRE est un langage créé il y a une vingtaine d'années pour développer,
partager et enseigner des algorithmes pour la recherche
opérationnelle. Notre ambition première était de créer un pseudo-code
exécutable, qui permette à la fois de décrire simplement des algorithmes
complexes et de les exécuter facilement, grâce à un interprète, et
rapidement, grâce à un compilateur.
Après avoir brièvement rappelé l'histoire et les motivations de ce projet,
la deuxième partie de l'exposé donnera des exemples de fragments de code,
ainsi que quelques exemples d'applications réussies qui donnent un peu de
crédit à cette ambition.
La troisième partie fera un zoom sur certaines propriétés originales de
CLAIRE, qui font que ce langage de programmation conserve un certain intérêt
dans le paysage de 2014. En particulier, CLAIRE permet de décrire des
algorithmes d'exploration arborescents avec des mécanismes natifs de
raisonnement hypothétique. Un autre intérêt de ce langage est le haut niveau
de polymorphisme paramétrique, qui permet de traiter des fragments de code
comme des structures de données. CLAIRE a été utilisé pour développer
différents outils d'aide à la décision, de la résolution de problèmes
d'optimisation combinatoire à la simulation, en particulier dans le cadre de
GTES (simulation par jeux et apprentissage).
La dernière partie de cet exposé fera la liste des ressources disponibles
pour répondre à la question: pourquoi s'intéresser à un langage désuet ``20
ans après'' ? Le code de CLAIRE - méta-description, interprète et
plate-forme de compilation - est disponible. Une partie des fragments de
code disponibles peuvent soit servir de source d'inspiration (lorsqu'il
s'agit de fonctionnalités qui restent originales) soit de code réutilisable. +
Le Web a subi en quelques années une évolution radicale, passant d'une
plateforme de données à une plateforme d'applications. Mais la plupart des
outils de programmation n'ont pas été conçus pour cette nouvelle vision du
Web.
Le projet Ocsigen a pour but d'inventer de nouvelles techniques de
programmation adaptées aux besoins des sites Web modernes et des
applications Web distribuées. Il permet de programmer les parties client et
serveur dans le même langage, et même, comme une seule et même
application. La puissance expressive du langage OCaml permet d'introduire
une abstraction des technologies sous-jacentes dans le but de simplifier la
programmation d'interactions Web complexes. Le système de types très avancé
du langage permet d'améliorer la fiabilité des programmes et le respect des
standards. Cela permet aussi de réduire beaucoup le temps de
développement.
Cet exposé donnera un aperçu global du projet et montrera comment écrire un
exemple d'application simple. +
Nife est un langage de programmation ``Forth-like'': basé sur les principes du
langage Forth, défini par Charles H. Moore dans les années 1960, il n'en
reprend pas la totalité des fonctionnalités. Son ambition est d'offrir
aux non-informaticiens qui ont besoin de faire des mesures, de contrôler des
appareils distants, de surveiller des processus industriels, de manipuler
des grandes collections de données, de faire des calculs, des filtrages, des
statistiques, de pouvoir le réaliser facilement, dans un environnement Linux
à faible coût.
Simple, n'importe qui peut comprendre le fonctionnement de ce langage en
quelques minutes, et le maîtriser totalement en quelques heures - une
semaine tout au plus. Il peut aussi être utilisé plus modestement comme une
super calculatrice, pour faire ses comptes ou des calculs d'inversion de
matrice. Le public concerné est donc très large.
Une extension de Nife pour les systèmes embarqués lui permet de pouvoir être
directement chargé sur de petites ou moyennes unités de calcul. Pour cela,
on lui associe un noyau ``bootable'' et il devient Knife : Kernelable Nife.
Dans ce cas, il devient un outil puissant pour coder dans des environnements
où la mémoire est denrée rare, et où le côté ``langage dynamique'' va
permettre de résoudre des problèmes là où d'autres langages vont échouer. +
L'informatique graphique 3D, qu'il s'agisse de modélisation de formes,
d'analyse d'animation ou de synthèse d'images, exploite intensivement divers
types de structures spatiales telles que les hiérarchies volumes englobant,
les cages de déformation, les squelettes d'animation ou bien encore les
structures médianes.
Dans cette présentation, je reviendrai sur quelques uns de nos travaux
récents sur ce sujet. Je détaillerai notamment une nouvelle forme de
représentation d'objets 3D, les Sphere-Meshes, bien adaptés à
l'approximation extrême de forme et à l'auto-rigging pour la déformation
interaction. Je discuterai ensuite plusieurs projets liés à l'analyse de
formes, dont le système CageR pour l'ingénierie inverse de modèles issus
de performance capture. J'aborderai enfin le rendu temps-réel et le calcul
GPU dans le cadre l'éclairage global, qui s'appuie lui aussi sur la gestion
efficace d'une structure particulière : un arbre de radiance.
À chaque étape, je donnerai des éléments sur l'implémentation pratique de
ces approches et sur les nombreux défis qu'il reste à relever. +
Generic Tools, Specific Languages is an approach for developing tools and
applications in a way that supports easier and more meaningful adaptation to
specific domains. To achieve this goal, GTSL generalizes programming
language IDEs to domains traditionally not addressed by languages and
IDEs.
At its core, GTSL represents applications as documents / programs / models
expressed with suitable languages. Application functionality is provided
through an IDE that is aware of the languages and their semantics. The IDE
provides editing support, and also directly integrates domain-specific
analyses and execution services. Applications and their languages can be
adapted to increasingly specific domains using language engineering; this
includes developing incremental extensions to existing languages or creating
additional, tightly integrated languages. Language workbenches act as the
foundation on which such applications are built. +
Dans de nombreux domaines on cherche à améliorer les performances des
programmes en faisant appel au « GPGPU »: un ensemble d’outils et de
techniques permettant d’utiliser le GPU d’une machine afin de lui déléguer
d'autres calculs que les traditionnelles routines de dessins. Cependant,
écrire un programme qui exploite à la fois le GPU et le CPU n’est pas une
tâche facile. Même lorsque les algorithmes se prêtent bien à la
programmation GPU il arrive que le gain en performance soit décevant. L’un
des principaux problèmes reste la gestion de la mémoire et surtout du
transfert de données entre le GPU et le CPU. En effet l'optimisation des
temps de transfert est délicate et peut nécessiter plusieurs jours d’analyse
et de réécriture pour obtenir de bonnes performances.
CUDA offre de nouveaux outils pour résoudre ce problème. Des outils de
profilage de code permettent de voir où se situent les problèmes de
transfert. UVM (Unified Virtual Memory), le nouveau modèle de gestion de la
mémoire, permet de tirer pleinement parti de CUDA bien plus facilement que
par le passé.
C’est à l’utilisation de ces nouvelles techniques que nous nous intéressons
dans cette présentation. +
Au printemps 2014, j'ai animé un MOOC d'initiation à l'informatique, centré
sur la programmation récursive. Bien que loin d'être massif, ce MOOC a
permis d'expérimenter ce nouveau medium ainsi que de mettre à l'épreuve une
infrastructure de correction automatisée. L'exposé portera sur ces deux
aspects et présentera également les nouveautés prévues pour la prochaine
édition de ce MOOC. +
L’accroissement exponentiel de la complexité technique des logiciels métiers
a du mal à être compensée par les progrès du génie logiciel : les coûts et
les délais augmentent jusqu’à ce que l’intérêt de l’informatique soit
fondamentalement remis en cause dans certains cas, arguments rationnels et
légitimes à l’appui. Cette anomalie épistémologique s’explique pourtant par
des erreurs technologiques récurrentes dans l’histoire, des pièges et des
culs-de-sac ralentissant le progrès scientifique. Parmi ces freins : la
dette technique, l’utilisation de trop de technologies, trop élitistes pour
être correctement utilisées en général, et le niveau maximal de
compréhension et d’analyse de chaque humain, qui est fortement variable mais
toujours plafonné.
La technologie Faveod sert à éviter ces freins par la formalisation
structurée et factorisée des besoins métiers, applicatifs et techniques dans
un modèle générique et exhaustif. L’analyse continue des évolutions
collaboratives de ce modèle permet la production totalement automatisée et
instantanée de sa traduction technique : l’application cible en cohérence et
en qualité. La gestion de la complexité des facteurs influant sur la qualité
logicielle étant déléguée à la technologie, il devient possible d’augmenter
son niveau par accumulation linéaire sans dépendre des facteurs humains
limitants. +
Motivé par de nombreuses applications, allant de la cryptographie au
calcul mathématique, le calcul formel s'est fortement développé ces
dernières années tant au niveau des algorithmes que des implantations
efficaces. L'efficacité des calculs repose sur celle de bibliothèques
dédiées, pour certaines opérations de base, comme l'algèbre linéaire
dans un corps fini ou avec des entiers multi-précision. Devant la
multiplicité des domaines de calcul et des variantes algorithmiques
disponibles, la conception de ces bibliothèques doit concilier une
forte généricité avec l'efficacité.
Nous allons présenter comment cette problématique est abordée dans les
bibliothèques d'algèbre linéaire exacte FFLAS-FFPACK (2) et LinBox
(3). Après une présentation générale de ces projets, nous focaliserons
la présentation sur trois aspects représentatifs:
- l'exploitation des diverses arithmétiques de base (entière,
flottante, booléenne), de routines numériques optimisées et leur
intégration au sein d'algorithmes génériques haut niveau ;
- l'approche boîte-noire de la bibliothèque LinBox, proposant un
modèle algorithmique spécifique, particulièrement performant pour les
matrices creuses ou structurées ;
- La parallélisation de code dans FFLAS-FFPACK, basée sur un langage
spécifique (DSL) permettant d'utiliser de façon interchangeable
différents langages et moteurs exécutifs, et de tirer parti du
parallélisme de tâche avec dépendance par flot de données. +, Tout d'abord, nous présentons un cadre générique et rapide pour les
opérations SIMD (single instruction multiple data), écrit en C++ à
l'intérieur de la bibliothèque d'algèbre linéaire exacte FFLAS-FFPACK
(2).
Nous montrons aussi une technique de conception (modules "helper")
basée sur le patron de conception Strategy, qui permet une sélection
efficace d'algorithmes récursifs, des signatures de fonctions plus
simples et plus uniformes. Ensuite, nous appliquons ces techniques
pour accélérer la multiplication entre matrices creuses et vecteurs
denses (SpMV) sur des anneaux Z/pZ, en utilisant des formats conçus
pour les opérations vectorielles et en combinant diverses
représentations.
Finalement, nous généralisons ces techniques aux blocs de vecteurs
(matrices denses, SpMM) et étendons nos algorithmes aux entiers de
Z. Nous appliquons aussi ces briques de base au calcul du rang de
grandes matrices creuses avec l'algorithme bloc-Wiedemann. +
Le C++ est très impopulaire dans la communauté des développeurs web et ce
n'est pas sans raison. Le langage n'offre aucune introspection, ce qui
complique la sérialisation automatique de messages. De plus, l'injection de
dépendances, un design pattern très utile dans les frameworks web issus
d'autres langages, est complexe voire quasi impossible à implémenter en
C++98.
Nous verrons comment l'introspection statique et l'injection de dépendance
ont été implémentés en C++14 grâce à un concept innovant: les symboles de la
bibliothèque IOD (1). Nous verrons ensuite comment Silicon (2), un jeune
framework web, tire parti de ces abstractions et aide les développeurs à
construire des APIs web aussi simplement qu'ils le feraient en Go ou
JavaScript. +
Le traitement géométrique 3D temps-réel a progressivement atteint un niveau
de performance rendant un grand nombre de primitives inspirées du traitement
du signal compatible avec les applications interactives. Cela a souvent été
rendu possible grâce à la co-conception des opérateurs, des structures de
données et du support matériel d’exécution. Parmi les principales classes
d'opérateurs géométriques, le filtrage et le sur-échantillonnage (par
raffinement) ont été exprimés sous des contraintes temps-réel avec
succès. Cependant, l'opérateur de sous-échantillonnage - la simplification
adaptative - demeure un cas problématique pour les données non
triviales.
Dans ce contexte, nous proposons un nouvel algorithme de simplification
géométrique rapide basé sur un nouveau concept : les intégrales de
Morton. En sommant les quadriques d'erreurs associées aux échantillons
géométriques selon leur ordre de Morton, notre approche permet d'extraire de
manière concurrente les nœuds correspondants à une coupe adaptative dans la
hiérarchie implicite ainsi définie, et d'optimiser la position des sommets
du maillage simplifié en parallèle. Cette méthode est inspirée des images
intégrales et exploite les avancées récentes en construction et parcours
haute performance de hiérarchies spatiales.
L'implémentation GPU de notre approche peut simplifier des maillages
composés de plusieurs millions d'éléments à un taux de rafraîchissement
interactif, tout en fournissant une géométrie simplifiée de qualité
supérieure aux méthodes uniformes et en préservant notamment les structures
géométriques saillantes. Notre algorithme est compatible avec les maillages
indexés, les soupes polygonales et les nuages de points, et peut prendre en
compte des attributs de surfaces (normal ou couleur par exemple) et des
métriques d'erreurs alternatives. +
La cryptographie joue un rôle clé dans la sécurité des infrastructures
de communication. Il est donc d'une importance capitale de construire
des système cryptographiques apportant de fortes garanties de
sécurité. C'est dans ce but que les constructions cryptographiques
sont étudiées scrupuleusement et viennent avec une preuve de sécurité
bornant la probabilité qu'un adversaire casse le crypto-système.
La majorité des preuves de sécurité sont réductionnistes: elles
construisent, à partir d'un adversaire PPT (Probabilistic
Polynomial-Time) violant avec une probabilité écrasante la sécurité de
la construction cryptographique, un second adversaire PPT cassant une
hypothèse de sécurité. Cette approche, connue sous le nom de
"sécurité formelle", permet sur le principe de fournir des preuves
mathématiques rigoureuses et détaillées de sécurité.
Les récentes constructions cryptographiques (et donc leur analyse de
sécurité) sont de plus en plus complexes, et il n'est pas rare
qu'elles incluent maintenant la preuve sécurité de l'implémentation du
crypto-système, ou de sa résistance aux canaux cachés. En conséquence,
les preuves de sécurité de ces algorithmes présentent un niveau de
complexité tel qu'un grand nombre d'entre elles sont fausses -
prouvant la sécurité d'une construction qui ne l'est pas.
Une solution prometteuse pour pallier ce problème est de développer
des outils formels d'aide à la construction et vérification de
crypto-systèmes. Bien que de nombreux outils existent pour la
cryptographie symbolique, peu d'effort a été fait pour la
cryptographie calculatoire - pourtant utilisée largement parmi les
cryptographes.
Après avoir introduit le domaine de la preuve formelle et de la
sécurité formelle, je présenterai EasyCrypt, un outil d'aide à la
preuve des constructions cryptographiques dans le modèle
calculatoire. EasyCrypt adopte une approche reposant sur la
formalisation de constructions cryptographiques à partir de code
concret, dans laquelle la sécurité et les hypothèses de sécurité sont
modélisées à partir de programmes probabilistes et où les adversaires
sont représentés par du code non spécifié. Une telle approche permet
l'utilisation d'outils existants pour la vérification de programmes.
EasyCrypt est développé conjointement entre l'IMDEA Software
Institute et Inria.
Le cloud computing donne accès à des ressources de stockage et de
calcul quasiment illimitées, pour un coût toujours plus bas. Devant
l’explosion de la quantité des données générées et le besoin de réagir
toujours plus vite, il n’a jamais été aussi facile d’accéder aux
technologies de traitement massif.
Nous illustrerons de nombreux cas d’usage du cloud : Hadoop,
dataware-house de plusieurs Po, traitement temps réel de millions
d’événements par seconde, IOT, Machine Learning…
En particulier, l’utilisation d’algorithmes massivement parallèles
prend toute son importance et permet de tirer pleinement parti de
l’élasticité du cloud, par exemple: Monte-Carlo dans le domaine
financier, modélisation de protéines en 3D pour du screening, analyse
génomique, analyse de logs… +
Il y a un intérêt grandissant pour le développement d’outils de
traitements adaptés aux images multimodales (plusieurs images de la
même scène acquises avec différentes caractéristiques). Permettant une
représentation plus complète de la scène en question, ces images
multimodales ont de l'intérêt dans plusieurs domaines du traitement
d'images. Les exploiter et les manipuler de manière optimale soulève
cependant plusieurs questions.
Dans cet exposé, nous étendrons les représentations hiérarchiques,
outil puissant pour le traitement et l’analyse d’images classiques,
aux images multimodales afin de mieux exploiter l’information
additionnelle apportée par la multimodalité et améliorer les
techniques classiques de traitement d’images. En particulier, nous
nous concentrerons principalement sur deux modalités différentes,
fréquemment rencontrées dans le domaine de la télédétection:
- La modalité spectrale-spatiale, propre aux images hyperspectrales
(images à très haute résolution spectrale - plusieurs centaines de
canaux). Une intégration adaptée de cette information
spectrale-spatiale lors de l'étape de construction de la
représentation hiérarchique (en l’occurrence, un arbre de partition
binaire) nous permettra par la suite, via un processus de
minimisation énergétique, de proposer une carte de segmentation de
l'image optimale vis-à-vis de l'opération de démélange spectral.
- La modalité sensorielle, c'est-à-dire les images acquises par des
capteurs de différentes natures. Ces images "multisources",
porteuses d'informations à la fois redondantes et complémentaires,
sont particulièrement intéressantes pour des applications de
segmentation. Nous proposerons une méthode se basant sur le très
récent concept de tresses de partitions (extensions des hiérarchies
de partitions classiques) afin de réaliser l'analyse hiérarchique de
ces images multisources, et en obtiendrons une segmentation (là
encore) via un processus de minimisation énergétique.
- Enfin, nous décrirons très brièvement une méthode d'analyse d'images
multitemporelles permettant d'effectuer du suivi d'objet, en se
basant également sur les représentations hiérarchiques des
différentes images de la séquence.
Les extensions multimédia (SSE, AVX, NEON) sont une composante majeure des
processeurs d'aujourd'hui qui restent plus que sous-utilisées. Les
principales raisons de cette sous-utilisation sont la relative obscurité des
jeux d'instructions, leur variété entre et même au sein des différentes
familles de puces et surtout, une méconnaissance de la disponibilité des ces
unités de calculs.
Boost.SIMD est une bibliothèque permettant d'exploiter ces extensions de
manière efficace et expressive, facilitant l'utilisation, la diffusion et la
portabilité de tels codes, ouvrant la porte à des accélérations de l'ordre
de 4 à 10 sur un simple cœur.
Cet exposé présentera les fonctionnalités de Boost.SIMD, les challenges
posés par son implémentation, comment le C++ moderne répond à plusieurs de
ces problèmes et les éléments bloquants qu'il reste à résoudre. +
Julia est un langage de programmation relativement jeune, développé au
MIT, et vendu comme langage dynamique à haute performance pour le
calcul scientifique numérique. L'un des co-auteurs du langage a une
connaissance de Scheme, et Julia s'inspire en effet largement de Scheme,
Common Lisp et Dylan, au point qu'il pourrait presque revendiquer un
lien de parenté avec Lisp. Tout ceci est déjà suffisant pour capter
notre attention, mais il y a plus: Julia semble également tirer parti de
techniques modernes d'optimisation pour les langages dynamiques, en
particulier grâce à son compilateur « Just-in-Time » basé sur LLVM.
Dans cette présentation, nous ferons un tour des aspects les plus
saillants du langage, avec une légère emphase sur ce qui en fait (ou
pas) un Lisp, quelques fois même (pas toujours) un meilleur Lisp que
Lisp lui-même. +
Traditionnellement, la prospection commerciale B2B se fait grâce à des
listes d'entreprises classées manuellement, sur la base de données
administratives renseignées à la création des entreprises. Ces listes
sont donc souvent dépassées, très chères et peu qualifiées.
C-Radar, produit développé par la société Data Publica, veut
transformer la prospection commerciale en enrichissant ces données
administratives par des données issues du web. Ainsi, on obtient des
données fraîches, plus ciblées. Et grâce aux techniques de machine
learning et de clustering, on peut obtenir automatiquement des listes
d'entreprises pertinentes à faible coût.
Lors de cette présentation, nous aborderons les différentes techniques
de science des données mises en œuvre dans ce produit, en relation
avec les fonctionnalités du produit. +
L’analyse du mouvement, ou l’analyse d’une séquence d’images, est
l’extension naturelle de l’analyse d’images à l’analyse de séries temporelles d’images.
De nombreuses méthodes d’analyse de mouvement ont été développées dans le
contexe de vision par ordinateur, comprenant le suivi de caractéristiques, le flot
optique, l’analyse de points-clefs, le recalage d’image, etc.
Dans cet exposé, nous présenterons les outils que nous avons
développés pour l'analyse de mouvement adaptés à l’analyse de séquences
biomédicales, et en particulier pour les cellules ciliées. Ces cellules,
couvertes de cils qui battent, sont présentes chez l’homme dans les zones
nécessitant des mouvements de fluide. Dans les poumons et les voies
respiratoires supérieures par exemple, les cils sont responsables de l’épuration
muco-ciliaire, qui permet d’évacuer des poumons la poussière et autres
impuretés inhalées. Les altérations de l’épuration muco-ciliaire peuvent
être liées à des maladies génétiques ou acquises. Ces maladies, touchant les cils,
sont potentiellement handicapantes. Elles peuvent cependant être
caractérisées par l’analyse du mouvement des cils sous un microscope, avec
une résolution temporelle importante. Nous avons développé plusieurs outils
et techniques pour réaliser ces analyses de manière automatique et avec
une haute précision. +
La ville est un système complexe façonné par des dynamiques opérant à des
échelles différentes.
En tant que chercheur en sciences de l'information géographique travaillant
dans l'interdisciplinarité, je travaille en collaboration avec des
spécialistes du transport, des géographes, des urbanistes, des historiens,
des démographes, et des physiciens, afin de proposer de meilleurs outils,
modèles et données pour l'étude multi-échelle des dynamiques urbaines.
Je présente mes contributions dans un ordre correspondant à l'échelle
spatiale, de la plus large à la plus fine : la très grande échelle pour les
questions liées à la mobilité, la grande échelle pour celles liées à
l'urbanisme et la petite échelle pour les questions liées à l'évolution du
territoire sur le long terme.
Pour chaque partie, je vais m'attacher à proposer un cheminement commun :
tout d'abord la question des sources d'information, des connaissances
manipulées, leur représentation, leur stockage ; ensuite, la question de
l'analyse de ces données, de leur enrichissement, de leur croisement ;
enfin, l'interaction avec ces données, leur visualisation, leur
interprétation, leur validation, leur correction par des utilisateurs. +
La visualisation scientifique est un domaine qui vise à aider les utilisateurs
à (i) représenter, (ii) explorer et (iii) analyser des données géométriques
acquises ou simulées, à des fins d'interprétation, de validation ou de
communication. Parmi les techniques existantes, les algorithmes inspirés par
la théorie de Morse ont démontré leur utilité dans ce contexte pour
l'extraction efficace et robuste de structures d'intérêts, et ce, à plusieurs
échelles d'importance.
Dans cette présentation, je donnerai un bref tutoriel sur l'analyse
topologique de champs scalaires, en introduisant quelques concepts clés comme
celui de graphe de Reeb, de complexe de Morse-Smale ou de diagramme de
persistance. Par ailleurs, j'illustrerai ces notions par des cas
d'applications concrets en astrophysique, chimie moléculaire ou
encore en combustion.
Ensuite, je discuterai certaines problématiques pratiques ayant récemment
émergé avec le développement des ressources de calcul haute-performance. Ces
problématiques induisent non seulement des jeux de données d'une taille
inédite, mais également des types nouveaux de données, comme les champs
scalaires multivariés ou incertains. Ces difficultés ne sont pas uniquement
intéressantes pour la communauté de recherche à cause de leur forte importance
pratique, mais aussi parce qu'elles nécessitent un redémarrage complet de
l'effort de recherche entrepris dans ce domaine ces vingt dernières années. En
particulier, je présenterai de nouvelles directions de recherche, étayées par
des résultats préliminaires récents concernant l'analyse topologique dans un
contexte de calcul haute-performance, ainsi que l'analyse topologique de
champs scalaires incertains ou bivariés. +
Je présenterai un outil en ligne dont l'objectif est de manipuler et
tester des propriétés algébriques pour des automates. Une courte
présentation de la théorie algébrique des automates sera donnée à la
volée. Les seuls concepts nécessaires à la compréhension de l'exposé
sont les expressions régulières, ainsi que la minimisation et la
déterminisation d'automates finis. +, Vcsn est une plateforme consacrée aux automates et aux expressions
rationnelles. Parce qu'elle traite une large variété de natures
d'automates, elle place en son coeur le concept de "contexte", qui
type les automates, les expressions rationnelles, etc. La plateforme
repose sur une bibliothèque C++14 "templatée" par des contextes, au
dessus de laquelle la couche "dyn" qui, grâce à de l'effacement de
type et de la compilation à la volée, offre à l'utilisateur le confort
d'une bibliothèque traditionnelle avec la généricité et les
performances d'une bibliothèque templatée. Ces bibliothèques sont
ensuite exposées au travers d'outils en ligne de commande, mais aussi
Python et surtout IPython, qui permettent une exploration interactive
simple d'algorithmes.
La bibliothèque Vcsn repose sur un ensemble d'objets - automates,
étiquettes, poids, polynômes, expressions rationnelles et
développements rationnels - sur lesquels sont fournis plus de trois
cents algorithmes. Dans certains cas, Vcsn offre des fonctionalités
inégalées, et certains de ces algorithmes ont des performances
supérieures à celles des projets comparables.
Nous ferons une présentation de l'architecture générale de Vcsn, sous
la forme d'une démonstration guidée par les questions, ainsi qu'un
exposé des objectifs de Vcsn 3.0. +
L'Imagerie par Résonance Magnétique fonctionnelle (IRMf) est une source
prometteuse de biomarqueurs permettant le diagnostic de troubles
neuropsychiatriques sur des sujets non coopératifs.
L'IRMf s'étudie en établissant un atlas de régions cérébrales représentatif
de l'organisation fonctionnelle, puis en étudiant la corrélation entre leurs
signaux.
Pour les extraire, nous proposons une approche d'apprentissage de
dictionnaire multi-sujets intégrant une pénalité imposant compacité spatiale et
parcimonie.
Nous sélectionnons les unités de base des réseaux fonctionnels
extraits à l'aide de techniques de segmentation inspirées du domaine de la
vision. Nous montons à l'échelle sur de gros jeux de données en utilisant
une stratégie d'optimisation stochastique.
A défaut de vérité terrain, nous proposons d'évaluer les modèles générés
à l'aide de métriques de stabilité et de fidélité.
Nous intégrons ensuite notre méthode de définition de régions dans un
pipeline entièrement automatisé, afin de réaliser une tâche de diagnostic des troubles
autistiques à travers différents sites d'acquisition et sur des
sous-ensembles d'homogénéité variable. Nous montrons que nos modèles ont une meilleure
performance, à la fois relativement aux métriques d'évaluation mais également sur nos
résultats expérimentaux.
Enfin, par une analyse post-hoc des résultats, nous montrons que la
définition de région est l'étape la plus importante du pipeline et que l'approche que
nous proposons obtient les meilleurs résultats. Nous fournissons également
des recommandations sur les méthodes les plus performantes pour les autres
étapes du pipeline. +
Les algorithmes itératifs utilisés lors de la résolution de problèmes inverses portant sur des gros volumes de données requièrent
une accélération significative pour être utilisés en pratique. Sur des exemples d'applications en tomographie X et
en déconvolution de signaux 1D (enregistrement sur plusieurs années de données spectrales de Mars) ou 2D (flux vidéo d'une webcam),
nous présenterons notre recherche de solutions permettant la parallélisation des calculs la plus efficace possible
sur les processeurs de type "many cores" que sont les GPUs. Nous exposerons ainsi la triple adéquation entre
l'architecture des processeurs GPUs (CUDA de Nvidia), la (re)formulation des algorithmes et la (re)structuration
des données que nous avons mises en oeuvre sur différents types d'opérateurs utilisés dans les algorithmes
itératifs (projecteur, rétroprojecteur, convolution nD). Par ailleurs, nous montrerons l'attention particulière
qui doit être apportée au goulot d'étranglement lié au temps de transfert entre le PC et les cartes GPUs.
Enfin, nous présenterons le découpage des données que nous avons effectué afin de bénéficier pleinement
d'un serveur multi-GPUs et apporterons quelques éléments de réponse sur l'utilisation des GPUs couplés à Matlab
et des bibliothèques déjà existantes (CUBLAS, NVPP...). +
Nous proposons une approche auto-supervisée pour l’apprentissage de
représentations à partir de vidéos non supervisées, enregistrées à de
multiples points de vue. Cette approche est particulièrement pertinente en
robotique pour l’apprentissage par l’imitation, qui nécessite une
compréhension invariante par rapport au point de vue des relations
entre les humains et leur environnement (telles que les interactions
entre objets, les attributs et les poses corporelles). Nous entraînons
nos représentations à l’aide d’une stratégie de type triplet loss,
où les multiples points de vue simultanés de la même observation
sont attirés dans l’espace d’intégration, tout en étant repoussés
des voisins temporels qui sont souvent visuellement similaires mais
fonctionnellement différents. Ce signal encourage notre modèle à
découvrir des attributs invariants vis-à-vis du point de vue, mais
qui varient dans le temps, tout en ignorant les potentielles nuisances
telles que les occlusions, le flou de mouvement, l’éclairage et
l’arrière-plan. Nos expériences démontrent qu’une telle représentation
acquiert même un certain degré d’invariance vis-à-vis de l’instance
d’objet. Nous montrons que notre modèle peut correctement identifier
les étapes correspondantes dans les interactions complexes d’objets,
à travers différentes vidéos avec différentes instances. Nous montrons
également les premiers résultats, à notre connaissance, d’apprentissage
intégralement auto-supervisé pour l’imitation de mouvements humains
par un robot réel. +
MAQAO (Modular Assembly Quality Analyzer and Optimizer) est une suite d'outils d'analyse et d'optimisation des performances
à destination d'applications binaires. Le but principal de MAQAO est d'analyser des codes binaires puis de proposer aux
développeurs d'applications des rapports synthétiques les aidant à comprendre et optimiser les performances de leur application.
MAQAO combine des analyses statiques (évaluation de la qualité du code) et dynamiques (profiling) basées sur la capacité
à reconstruire des structures aussi bien bas niveau (basic blocks, instructions, etc.) que haut niveau (fonctions et boucles).
Un autre aspect important de MAQAO est son extensibilité. En effet les utilisateurs peuvent écrire leur propre plugin
grâce à un langage de script simple intégré (Lua). +
Frama-C est une plateforme d'analyse de code C visant à vérifier des programmes
C de taille industrielle. Elle fournit à ses utilisateurs une collection de
greffons effectuant notamment des analyses statiques par interprétation
abstraite et des méthodes déductives ou encore permettant des vérifications à
l'exécution. La plateforme permet également de faire coopérer les analyses grâce
au partage d'un noyau et d'un langage de spécification communs.
Cet exposé présente une vue générale de la plateforme, de ses principaux
analyseurs et de quelques applications industrielles. Il se concentre sur le
langage de spécification ACSL et sur différentes façons de vérifier des
spécifications ACSL avec des analyses statiques ou dynamiques. +
L'apprentissage automatique, ou "pattern recognition" multivarié, peut
identifier des motifs complexes, associés à une variable d'intérêt, et
ce, dans des données de grandes dimensions. Une fois l'apprentissage
effectué par l'algorithme, il est appliqué à un nouvel individu afin
de prédire l'évolution future de ce dernier. L'imagerie par résonance
magnétique (IRM) fournit une approche efficace et non invasive pour
étudier les changements structurels et fonctionnels du cerveau,
associés aux conditions cliniques des patients. En combinant
apprentissage automatique et imagerie cérébrale, il est possible de
considérer l'émergence d'une médecine personnalisée, où les
algorithmes ont appris du passé à prédire la réponse probable et
future d'un patient donné à un traitement spécifique. Ces nouvelles
informations guideront le clinicien dans ses choix thérapeutiques.
Nous présenterons la complexité des données IRM manipulées, les
algorithmes d'apprentissage et leurs applications aux maladies
cérébrales. +, La lecture des lignes de la main est une activité ancestrale sans
fondement scientifique, même si certains motifs sont associés à des
malformations congénitales comme la trisomie 21. Cette conférence
décrira l’émergence d’une véritable science de la lecture des « lignes
du cerveau humain », qu’il s’agisse des plissements de son cortex ou
de la trajectoire des faisceaux de fibres qui constituent son câblage
à longue distance. Des formes inhabituelles de ces plissements ou de
ces faisceaux sont parfois la trace d’anomalies développementales
susceptibles d’augmenter le risque de développer certaines
pathologies. +
Formal verification (aka Symbolic Model Checking) is becoming a
mainstream technology in system on a chip (SoC)/intellectual property
design and verification methodologies. In the past, the usage of
formal verification was limited to a small range of applications; it
was mainly used to verify complex protocols or intrinsic logic
functionality by formal verification experts. In recent years, we saw
a rapid adoption of formal verification technology and many new
application areas, such as checking of configuration and status
register accesses, SoC connectivity verification, low power design
verification, security applications, and many more. In this talk, we
give an overview of the JasperGold Formal Verification Platform. The
platform provides a wide range of formal apps, which ease adoption of
formal verification by offering property generation and other targeted
capabilities for specific design and verification tasks. In addition,
JasperGold offers a unique interactive debug environment (called
Visualize) that allows the user to easily analyze the verification
results. We present JasperGold from a user’s point of view, showcase
selected apps, and discuss features that were essential for their wide
adoption. +
Les réseaux de neurones convolutifs connaissent depuis quelques années
un franc succès dans de nombreuses applications de reconnaissance
visuelle. Nous reviendrons sur les premiers travaux en la matière en
segmentation sémantique (étiquetage de chaque pixel des images par une
catégorie sémantique). Nous explorerons ensuite une piste
d'amélioration visant à réduire la quantité de données labelisées
utilisée, à base d'entraînement de réseaux adversaires.
Dans un second temps, nous nous intéresserons au problème de la
prédiction d'images suivantes dans les vidéos: s'il nous parait
simple d'anticiper ce qu'il va se passer dans un futur très proche,
c'est un problème difficile à modéliser mathématiquement étant données
les multiples sources d'incertitude. Nous présenterons nos travaux de
prédiction dans le domaine des images naturelles, puis dans l'espace
plus haut niveau des segmentations sémantiques, nous permettant de
prédire plus loin dans le futur. +
We show a symbolic-execution-based algorithm computing the precise
effect of a program cycle on program variables. For a program variable,
the algorithm produces an expression representing the variable value
after the number of cycle iterations specified by parameters of the
expression. The algorithm is partial in the sense that it can fail to
find such an expression for some program variables (for example, it
fails in cases where the variable value depends on the order of paths in
the cycle taken during iterations).
We present two applications of this loop summarization procedure. The
first is the construction of a nontrivial necessary condition on program
input to reach a given program location. The second application is a
loop bound detection algorithm, which produces tighter loop bounds than
other approaches. +
Hierarchical image representations have become increasingly popular in
image processing and computer vision over the past decades. Indeed,
they allow a modeling of image contents at different (and
complementary) levels of scales, resolutions and semantics. Methods
based on such image representations have been able to tackle various
complex challenges such as multi-scale image segmentation, image
filtering, object detection, recognition, and more recently image
characterization and understanding. In this talk, we will focus on the
binary partition tree (BPT), which is a well-known hierarchical
data-structure, frequently involved in the design of image
segmentation strategies. In a first part, we will focus on the
construction of such trees by providing a generalization of the BPT
construction framework to allow one to embed multiple features, which
enables handling many metrics and/or many images. In a second part,
we will discuss how it may be possible to evaluate the quality of such
a structure and its ability to reconstruct regions of the image
corresponding to segments of reference given by a user. Finally, we
will see some examples of image analysis and recognition processes
involving these hierarchical structures. The main thematic application
is remote sensing and satellite image analysis. +
Dans ce travail en collaboration avec Axel Davy, Mauricio Delbracio et
Thibaud Ehret, je passerai en revue les classes d'algorithmes dont le
but est de détecter des anomalies dans les images digitales. Ces
détecteurs répondent au difficile problème de trouver automatiquement
des exceptions dans des images de fond, qui peuvent être aussi
diverses qu'un tissu ou une mammographie. Des méthodes de détection
ont été proposées par milliers car chaque problème nécessite un modèle
de fond différent. En analysant les approches existantes, nous
montrerons que le problème peut être réduit à la détection d'anomalies
dans les images résiduelles (extraites de l'image cible) dans
lesquelles prédominent le bruit et les anomalies. Ainsi, le problème
général et impossible de la modélisation d'un fond arbitraire est
remplacé par celui de modèliser un bruit. Or un modèle de bruit permet
le calcul de seuils de détection rigoureux. L'approche au problème
peut donc être non supervisée et fonctionner sur des images
arbitraires. Nous illustrerons l'usage de la théorie de détection dite
a contrario, qui évite la sur-détection en fixant des seuils de
détection prenant en compte la multiplicité des tests. +
Recent advances in medical image computing have resulted in automated systems that closely assist physicians in patient
therapy. Computational and personalized patient models benefit diagnosis, prognosis and treatment planning, with a
decreased risk for the patient, as well as potentially lower cost. HeartFlow Inc. is a successful example of a company
providing such a service in the cardiovascular context. Based on patient-specific vascular model extracted from X-ray CT
images, they identify functionally significant disease in large coronary arteries. Their combined anatomical and
functional analysis is nonetheless limited by the image resolution. At the downstream scale, a functional exam called
Myocardium Perfusion Imaging (MPI) highlights myocardium regions with blood flow deficit. However, MPI does not
functionally relate perfusion to the upstream coronary disease. The goal of our project is to build the functional
bridge between coronary and myocardium. To this aim we propose an anatomical and functional extrapolation. We produce an
innovative vascular network generation method extending the coronary model down to the microvasculature. In the
resulting vascular model, we compute a functional analysis pipeline to simulate flow from large coronaries to the
myocardium, and to enable comparison with MPI ground-truth data. +
Rendre la vue à ceux qui l’ont perdue a longtemps été considéré comme un sujet réservé à la science-fiction. Cependant,
sur les vingt dernières années les efforts intensifiés dans le domaine des prothèses visuelles ont abouti à des avancées
significatives, et plusieurs centaines de patients dans le monde ont reçu de tels dispositifs. Ce séminaire présentera
brièvement le domaine des prothèses rétiniennes avec une focalisation particulière sur les aspects de traitement
d’image. Nous exposerons les principales approches, les limitations connues et les résultats. +
Neural networks have been producing impressive results in computer vision these last years, in image classification or
segmentation in particular. To be transferred to remote sensing, this tool needs adaptation to its specifics: large
images, many small objects per image, keeping high-resolution output, unreliable ground truth (usually
mis-registered). We will review the work done in our group for remote sensing semantic segmentation, explaining the
evolution of our neural net architecture design to face these challenges, and finally training a network to register
binary cadaster maps to RGB images while detecting new buildings if any, in a multi-scale approach. We will show in
particular that it is possible to train on noisy datasets, and to make predictions at an accuracy much better than the
variance of the original noise. To explain this phenomenon, we build theoretical tools to express input similarity from
the neural network point of view, and use them to quantify data redundancy and associated expected denoising effects.
If time permits, we might also present work on hurricane track forecast from reanalysis data (2-3D coverage of the
Earth's surface with temperature/pressure/etc. fields) using deep learning. +
The Loci Auto-Parallelizing framework provides a Domain Specific
Language (DSL) for the creation of high performance numerical
models. The framework uses a logic-relation model to describe
irregular computations, provide guarantees of internal logical
consistency, and provides for automatic parallel execution. The
framework has been used to develop a number of advance computational
models used in production engineering processes. Currently Loci based
tools form the backbone of computational fluid dynamics tools used by
NASA Marshall and Loci based codes account for more than 20% of the
computational workload on NASA’s Pleiades supercomputer. This talk
will provide an overview of the framework, discuss its general
approach, and provide comparisons to other programming models through
a mini-app benchmark. In addition, future plans for developing
efficient schedules of fine-grained parallel and memory bandwidth
constrained computations will be discussed. Finally, some examples of
the range of engineering simulations enabled by the technology will be
introduced and briefly discussed. +
The relationship between neighboring pixels plays an
important role in many vision applications. A typical example of a
relationship between neighboring pixels is the intensity order, which
gives rise to some morphological tree-based image representations
(e.g., Min/Max tree and tree of shapes). These trees have been shown
useful for many applications, ranging from image filtering to object
detection and segmentation. Yet, these intensity order based trees do
not always perform well for analyzing complex natural images. The
success of deep learning in many vision tasks motivates us to resort
to convolutional neural networks (CNNs) for learning such a
relationship instead of relying on the simple intensity order. As a
starting point, we propose the flux or direction field representation
that encodes the relationship between neighboring pixels. We then
leverage CNNs to learn such a representation and develop some
customized post-processings for several vision tasks, such as symmetry
detection, scene text detection, generic image segmentation, and crowd
counting by localization. This talk is based on [1] and [2], as well
as extension of those previous works that are currently under review.
[1] Xu, Y., Wang, Y., Zhou, W., Wang, Y., Yang, Z. and Bai, X.,
2019. Textfield: Learning a deep direction field for irregular scene
text detection. IEEE Transactions on Image Processing.
[2] Wang, Y., Xu, Y., Tsogkas, S., Bai, X., Dickinson, S. and Siddiqi,
K., 2019. DeepFlux for Skeletons in the Wild. In Proceedings of the
IEEE Conference on Computer Vision and Pattern Recognition. +
Dans ce séminaire, nous parlerons d'une technologie émergente qu'est l'informatique quantique, exploitant les phénomènes quantiques de l'infiniment petit. Nous verrons que, quand dans le monde de l'informatique classique, les données sont représentées par des bits valant chacun 0 ou 1 exclusivement, alors que l'informatique quantique est déroutante dans le sens où les qubits (bits quantiques) peuvent valoir simultanément 0 et 1. Afin de pouvoir appréhender cette technologie, nous rappellerons ce que sont la dualité onde/corpuscule, la superposition d'états, ainsi que intrication quantique. Nous verrons aussi comment IBM a créé le premier processeur quantique (ou QPU) quelques dizaines d'années après l'idée révolutionnaire du père de l'informatique quantique, Richard Feynman, et quels sont les défis technologiques qui en découlent. Nous verrons que l’informatique quantique offre de nouvelles perspectives dans les domaines comme la cryptographie et l'intelligence artificielle pour ne citer qu'eux. Une étude des complexités des différents algorithmes vus durant le séminaire sera évoqué. Durant cette plénière interactive, une démonstration sera réalisée via l’environnement de développement Qiskit avec accès à distance à une machine quantique IBM. Merci donc d'apporter votre ordinateur portable ! +
In a partially observable system, diagnosis is the task of detecting certain events, for instance fault occurrences. In the presence of hostile observers, on the other hand, one is interested in rendering a system opaque, i.e. making it impossible to detect certain "secret" events. The talk will present some decidability and complexity results for these two problems
when the system is represented as a finite automaton or a Petri net. We then also consider the problem of active diagnosis, where the observer has some control over the system. In this context, we study problems such as the computational complexity of the synthesis problem, the memory required for the controller, and the delay between a fault occurrence and its detection by the diagnoser. The talk is based on joint work with B. Bérard, S. Haar, S. Haddad, T. Melliti, and S. Schmitz. +
In a partially observable system, diagnosis is the task of detecting certain events, for instance fault occurrences. In the presence of hostile observers, on the other hand, one is interested in rendering a system opaque, i.e. making it impossible to detect certain "secret" events. The talk will present some decidability and complexity results for these two problems
when the system is represented as a finite automaton or a Petri net. We then also consider the problem of active diagnosis, where the observer has some control over the system. In this context, we study problems such as the computational complexity of the synthesis problem, the memory required for the controller, and the delay between a fault occurrence and its detection by the diagnoser. The talk is based on joint work with B. Bérard, S. Haar, S. Haddad, T. Melliti, and S. Schmitz. +
We introduce iposets - posets with interfaces - equipped with a novel gluing
composition along interfaces and the standard parallel composition. We study
their basic algebraic properties as well as the hierarchy of gluing-parallel
posets generated from singletons by finitary applications of the two
compositions. We show that not only series-parallel posets, but also
interval orders, which seem more interesting for modeling concurrent and
distributed systems, can be generated, but not all posets. Generating posets
is also important for constructing free algebras for concurrent semi-rings
and Kleene algebras that allow compositional reasoning about such systems. +
Despite its NP-completeness, propositional Boolean satisfiability (SAT) covers a broad spectrum of applications. Nowadays, it is an active research area finding its applications in many contexts like planning decision, cryptology, computational biology, hardware and software analysis. Hence, the development of approaches allowing to handle increasingly challenging SAT problems has become a major focus: during the past eight years, SAT solving has been the main subject of my research work. This talk presents some of the main results we obtained in the field. +
Topological Data Analysis (TDA) is a recent area of computer science that focuses on discovering intrinsic structures hidden in data. Based on solid mathematical tools such as Morse theory and Persistent Homology, TDA enables the robust extraction of the main features of a data set into stable, concise, and multi-scale descriptors that facilitate data analysis and visualization. In this talk, I will give an intuitive overview of the main tools used in TDA (persistence diagrams, Reeb graphs, Morse-Smale complexes, etc.) with applications to concrete use cases in computational fluid dynamics, medical imaging, quantum chemistry, and climate modeling. This talk will be illustrated with results produced with the "Topology ToolKit" (TTK), an open-source library (BSD license) that we develop with collaborators to showcase our research. Tutorials for re-producing these experiments are available on the TTK website. +
Optimal transport (OT) has recently gained a lot of interest in machine learning. It is a natural tool to compare in a geometrically faithful way probability distributions. It finds applications in both supervised learning (using geometric loss functions) and unsupervised learning (to perform generative model fitting). OT is however plagued by the curse of dimensionality, since it might require a number of samples which grows exponentially with the dimension. In this talk, I will review entropic regularization methods which define geometric loss functions approximating OT with a better sample complexity. +
We present a framework for modelling and verifying epistemic properties over
parameterized multi-agent systems that communicate by truthful public
announcements. In this framework, the number of agents or the amount of certain
resources are parameterized (i.e. not known a priori), and the corresponding
verification problem asks whether a given epistemic property is true regardless
of the instantiation of the parameters. As in other regular model checking (RMC)
techniques, a finite-state automaton is used to specify a parameterized family
of systems.
Parameterized systems might also require an arbitrary number of announcements,
leading to the introduction of the so-called iterated public announcement.
Although model checking becomes undecidable because of this operator, we provide
a semi-decision procedure based on Angluin's L*-algorithm for learning finite
automata. Moreover, the procedure is guaranteed to terminate when some
regularity properties are met. We illustrate the approach on the Muddy Children
puzzle, and we further discuss dynamic protocol encodings through the Dining
Cryptographer example.
Initial publication at AAMAS21, joint work with Anthony Lin and Felix Thomas +