Séminaire, 5 avril 2012
Lieu
La rencontre aura lieu à l'École Normale Supérieure de Lyon, campus Jacques Monod, dans l'amphi B. Pour venir, voir les instructions sur le site du LIP ou sur un plan, par exemple chez Google Maps. À l'entrée, se présenter à la réception, qui aura la liste des inscrits.
Programme
- 10:30 – 12:00
-
Francesco Zappa Nardelli (Moscova, INRIA Paris-Rocquencourt)Invited talk: Verifying Fence Elimination Optimisations
(avec Viktor Vafeiadis, et Suresh Jagannathan, Jaroslav Sevcik, Peter Sewell)
A simple compiler optimisation for removing redundant memory fences in programs running on top of x86 multiprocessors turned out to be challenging to prove correct. In this talk, I will give a short overview of the challenges of the semantic design and verified compilation of high-level programming languages language above shared memory multiprocessors (focussing on x86 and Power/ARM), and will conclude by proving the fence optimisation correct by introducing a novel simulation technique.
- 14:00 – 15:00
-
Gabriel Kerneis (PPS, Université Paris Diderot)
Threads and events are two common techniques to implement concurrent programs. Events are often deemed harder to write and understand than threads, because their control flow is scattered across long chains of callbacks. But the programmer cannot always afford using threads, due to resource constraints (eg. embedded systems) or language limitation (eg. javascript). In such cases, it might be desirable to translate threads into events automatically.
We present several styles of event-driven programs and study how to generate them from a threaded description, in the particular case of C programs. Our translation steps are made of classical and proven transformation techniques, most notably lambda-lifting and conversion into continuation-passing style.
These techniques have been used to implement the <a href="http://www.pps.jussieu.fr/~kerneis/software/cpc">CPC translator</a>.
- 15:30 – 16:30
-
Alexandre Miquel (ENS Lyon)
