Chers collègues,
La prochaine session du séminaire Performance et Généricité du LRDE
(Laboratoire de Recherche et Développement de l'EPITA) aura lieu le
Mercredi 15 février 2012 (14h-17h). Nous sommes heureux de vous
annoncer qu'un second exposé est programmé !
Au programme:
* 14h: Des performances dans les nuages avec la virtualisation des langages
-- Yann Régis-Gianas
http://www.pps.jussieu.fr/~yrg/
«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.
-- Yann Régis-Gianas est un ancien élève de l'EPITA, promo CSI 2003. À sa
sortie de l'école, il a poursuivi un troisième cycle en passant un DEA à
l'Université Paris Diderot et une thèse à l'INRIA Rocquencourt. Il est
aujourd'hui maître de conférence à Paris Diderot et travaille sur le
design des langages de programmation et de preuve.
* 15h30: Certification d'annotations de coût dans les compilateurs
-- Nicolas Ayache
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.
-- Nicolas Ayache, ancien doctorant Université Paris-Sud / CEA-LIST, est
actuellement Post-doc au laboratoire PPS (Preuves, Programmes et
Systèmes) à l'université Paris Diderot.
Pour plus de renseignements, consultez
http://seminaire.lrde.epita.fr/.
L'entrée du séminaire est libre. Merci de bien vouloir diffuser cette
information le plus largement possible.
_______________________________________________
Seminaire mailing list
Seminaire(a)lrde.epita.fr
https://www.lrde.epita.fr/mailman/listinfo/seminaire