BEGIN:VCALENDAR
PRODID:-//Google Inc//Google Calendar 70.9054//EN
VERSION:2.0
CALSCALE:GREGORIAN
METHOD:PUBLISH
X-WR-CALNAME:Inria Team Parkas
X-WR-TIMEZONE:Europe/Paris
X-WR-CALDESC:Shared PARKAS calendar (Inria Paris)
BEGIN:VTIMEZONE
TZID:Europe/Paris
X-LIC-LOCATION:Europe/Paris
BEGIN:DAYLIGHT
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
DTSTART:19700329T020000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
DTSTART:19701025T030000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20240315T140000
DTEND;TZID=Europe/Paris:20240315T150000
DTSTAMP;TZID=Europe/Paris:20240315T140000
UID:2024-03-15_Incer
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Inigo Incer: Towards Provably Safe and Secure Systems with Contr
act-Based Design
URL:http://parkas.di.ens.fr/seminars.html#2024-03-15_Incer
DESCRIPTION:The task of system design is shared by all engineering disci
plines, each \ncoming with its own techniques. In spite of their differe
nces in tools, \nthere is large intersection in their conceptual approac
h to design. In this \ntalk, we exploit this commonality to take an abst
ract view of systems and \ntheir composition. We understand systems and
subsystems in terms of their \nassume-guarantee specifications, or contr
acts.\n\nAssume-guarantee contracts are formal specifications that state
(i) the \nassumptions that a design element makes on its environment an
d (ii) the \nguarantees it delivers when the environment behaves accordi
ng to the \ncontract's assumptions. Contracts come with a rich algebra t
hat allows us to \ncarry out several design-relevant tasks: obtaining sy
stem-level \nspecifications from component specifications, finding speci
fications of \ncomponents that need to be added to a design in order to
meet an objective, \netc. We will introduce the algebra of contracts and
discuss how the various \nalgebraic operations relate to system-design
tasks. We will discuss \nhypercontracts, an extension of assume-guarante
e reasoning to support the \nformal analysis of key security and robustn
ess properties. We will also \ndiscuss the application of this methodolo
gy and Pacti, a software package \nthat supports system design using con
tracts, in applications ranging from \nspace-mission design to synthetic
biology.\n\n_Bio_: Inigo Incer is a postdoctoral researcher at Caltech
and UC Berkeley. \nHe obtained his PhD from UC Berkeley in 2022 under th
e guidance of Alberto \nSangiovanni-Vincentelli. He is interested in all
aspects of cyber-physical \nsystems, emphasizing formal methods and AI
that support their compositional \ndesign and analysis. Before pursuing
a PhD, Inigo was an IC designer in \nAustin. His work has been supported
by the NSF/ASEE eFellows program and the \nUC Berkeley Chancellor's Fel
lowship\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20240221T133000
DTEND;TZID=Europe/Paris:20240221T143000
DTSTAMP;TZID=Europe/Paris:20240221T133000
UID:2024-02-21_Schmidt
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Andreas Schmidt: Rust: Safe Beyond Memory
URL:http://parkas.di.ens.fr/seminars.html#2024-02-21_Schmidt
DESCRIPTION:Rust has established a reputation for providing both memory
and thread \nsafety. When it comes to dependable software, this is a for
midable \nfoundation but often not sufficient. In particular, correctly
handling \nunavoidable (but manageable) error conditions and managing re
sources (such \nas time) is essential. This talk sheds light on “stati
cally extracting error \nflows” as well as “automatic and dependable
resource management at run- and \ncompile-time”.\n\n[slides](https://
netzdoktor.eu/inria-intro/parkas.html)\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20240201T140000
DTEND;TZID=Europe/Paris:20240201T150000
DTSTAMP;TZID=Europe/Paris:20240201T140000
UID:2024-02-01_Stolze
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Claude Stolze: Composable Partial Multiparty Session Types
URL:http://parkas.di.ens.fr/seminars.html#2024-02-01_Stolze
DESCRIPTION:We introduce partial sessions and partial (multiparty) sessi
on types, in \norder to deal with open systems, i.e., systems with missi
ng components.\nPartial sessions can be composed, and the type of the re
sulting system is \nderived from those of its components without knowing
any suitable global \ntype nor the types of missing parts.\nWe apply th
ese types to a process calculus, for which we prove subject \nreduction
and progress, so that well-typed systems never violate the \nprescribed
constraints.\nTherefore, partial session types support the development o
f systems by \nincremental assembling of components.\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20231208T133000
DTEND;TZID=Europe/Paris:20231208T163000
DTSTAMP;TZID=Europe/Paris:20231208T133000
UID:2023-12-08_Pauget
LOCATION:CONF IV/E244 (2nd floor); 24 rue Lhomond; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY: Baptiste Pauget : Spécification de la mémoire dans un langage
synchrone flot de données doté de tableaux de taille statique
URL:http://parkas.di.ens.fr/seminars.html#2023-12-08_Pauget
DESCRIPTION:This PhD defense will be presented in French. The abstract i
n English can be \nfound below.\n\n_Soutenance de thèse (en français)_
\n\nScade est un langage de programmation synchrone utilisé depuis la f
in des \nannées 1990 pour concevoir et implémenter des systèmes criti
ques embarqués \ntels ceux que l'on trouve dans l'aviation. Cette criti
cité requiert la \nformalisation (i) des programmes, afin de garantir q
u'ils s'exécutent sans \nerreurs ou retards pendant une durée arbitrai
re et (ii) des outils de \ndéveloppement, en particulier le compilateur
, pour s'assurer de la \npréservation des propriétés des modèles lor
s de la génération de code. Ces \nactivités reposent sur une descript
ion flot de données des modèles, inspirée \ndes schémas-blocs, dont
la sémantique s'exprime par des fonctions de suites, \nainsi que d'une
compilation précisément documentée.\n\nScade descend de Lustre. La ve
rsion 6 a introduit des évolutions majeures, \ndans les pas de Lucid sy
nchrone, dont les automates hiérarchique et les \ntableaux. Pour ces de
rniers, leur taille est connue et vérifiée statiquement \nafin d'assur
er un temps d'exécution et une mémoire bornés. L'utilisation \ncroiss
ante des tableaux de Scade pour des opérations intensives a révélé \
nplusieurs axes d'amélioration: verbosité des modèles, manque de cont
rôle de \nla compilation ou description peu commode de certains algorit
hmes.\n\nDans cette thèse, ces trois aspects ont été étudiés à l'a
ide d'un prototype \nde compilateur. (i) Nous avons développé un syst
ème de types a la \nHindley-Milner spécifiant les tailles sous la form
e de polynômes \nmultivariés. Cette proposition permet de vérifier et
d'inférer la plupart \ndes tailles de manière modulaire. (ii) Nous av
ons exploré une méthode de \ncompilation alternative, fondée sur un l
angage déclaratif conscient de la \nmémoire. Il vise à concilier le s
tyle flot de données avec une spécification \nprécise des emplacement
s mémoire. La description modulaire des tailles en \nest un élément c
lé. (iii) Enfin, nous proposons une construction d'itération \ninspir
ée de Sisal qui complète les itérateurs actuels. En traitant les \nta
bleaux comme des suites finies, elle donne accès aux constructions \ns
équentielles de Scade (automates) lors d'itérations. De plus, elle per
met \nde décrire de manière déclarative des implémentations efficace
s \nd'algorithmes comme la décomposition de Cholesky. Cette compilation
\ncontrôlable est un premier pas nécessaire pour la compilation vers
des GPUs.\n\nLes membres du jury sont\n* [Albert Cohen](https://research
.google/people/106208/) (Rapporteur), Google\n* [François Pottier](http
s://pauillac.inria.fr/~fpottier/) (Rapporteur), Inria\n* [Jean-Louis Gia
vitto](https://www.ircam.fr/person/jean-louis-giavitto), IRCAM\n* [Yamin
e Ait-Ameur](https://www.researchgate.net/profile/Yamine-Ait-Ameur), Tou
louse INP\n* [Alain Girault](https://pop-art.inrialpes.fr/~girault/), In
ria Grenoble\n* [Laure Gonnord](https://laure.gonnord.org/pro/), Grenobl
e INP\n* [Jean-Louis Colaço](https://www.researchgate.net/profile/Jean-
Louis-Colaco), (Directeur de thèse), Ansys\n* [Marc Pouzet](https://www
.di.ens.fr/~pouzet/), (Directeur de thèse), École normale supérieure\
n\n__Memory Specification in a Data-flow Synchronous Language with Stati
cally Sized Arrays__\n\n_PhD thesis defense (in French)_\n\nThe synchron
ous programming language Scade has been used since the end of \nthe 1990
s to design safety critical embedded systems such as those found in \nav
ionics. This context requires to formally reason about (i) the programs,
\nto ensure that they run for an arbitrary long time without errors or
missed \ndeadlines and (ii) the tools, in particular the compiler, to gi
ve high \nconfidence in the preservation of model properties through the
code \ngeneration process. These activities build on a data-flow descri
ption of \nmodels, inspired by block diagrams, that enjoys a formal sema
ntics in terms \nof streams and a well-documented compilation process.\n
\nScade stems from Lustre. The Scade 6 version introduced major evolutio
ns \nfollowing Lucid synchrone, notably hierarchical automata and arrays
. For the \nlatter, sizes are statically known and checked, so as to ful
fill the bounded \nresources and execution time constraints. The increas
ing use of Scade arrays \nfor data-intensive computations has revealed a
reas for improve- ment: \nconcision of the models, control of the genera
ted code and idiomatic \ndescription of array computations.\n\nUsing a p
rototype implementation of a compiler, the present work \ninvestigates t
hese three aspects. (i) We designed a Hindley-Milner-like type \nsystem
for representing sizes with multivariate polynomials. This proposal \nal
lows to check and infer most sizes in a modular way. (ii) We explored an
\nalternative compilation process based on a memory-aware declarative \
nlanguage. It aims at reconciling the data-flow style with a precise \ns
pecification of memory locations. The underlying memory model builds on
our \nmodular description of sizes. (iii) Last, we propose an iteration
construct \ninspired by Sisal that supplements the available iterators.
By viewing \narrays as finite streams, iteration can benefit from the se
quential \nconstructs of Scade, e.g., automata. Moreover, it allows decl
arative \ndescriptions of efficient algorithm implementations such as th
e Cholesky \ndecomposition. This controllable compilation process is a m
andatory step \ntoward code generation for GPUs.\n\nThe members of the t
hesis commitee are\n* [Albert Cohen](https://research.google/people/1062
08/) (Reporter), Google\n* [François Pottier](https://pauillac.inria.fr
/~fpottier/) (Reporter), Inria\n* [Jean-Louis Giavitto](https://www.irca
m.fr/person/jean-louis-giavitto), IRCAM\n* [Yamine Ait-Ameur](https://ww
w.researchgate.net/profile/Yamine-Ait-Ameur), Toulouse INP\n* [Laure Gon
nord](https://laure.gonnord.org/pro/), Grenoble INP\n* [Alain Girault](h
ttps://pop-art.inrialpes.fr/~girault/), Inria Grenoble\n* [Jean-Louis Co
laço](https://www.researchgate.net/profile/Jean-Louis-Colaco), (Supervi
sor), Ansys\n* [Marc Pouzet](https://www.di.ens.fr/~pouzet/), (Superviso
r), École normale supérieure\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20231206T140000
DTEND;TZID=Europe/Paris:20231206T150000
DTSTAMP;TZID=Europe/Paris:20231206T140000
UID:2023-12-06_Sylvestre
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Loïc Sylvestre: Une approche synchrone pour la programmation ha
ut-niveau de FPGA
URL:http://parkas.di.ens.fr/seminars.html#2023-12-06_Sylvestre
DESCRIPTION:Les FPGA sont des circuits reprogrammables qui constituent u
ne cible de \nchoix, à la fois pour l'accélération matérielle d'appl
ications logicielles \net pour l'interaction avec un environnement exté
rieur (capteurs, \nactionneurs).\n\nDans cet exposé, je présenterai un
noyau de langage fonctionnel synchrone \npour la conception d'applicati
ons réactives embarquées sur FPGA. Chaque \napplication écrite dans c
e langage est une fonction « instantanée » \nmodélisant directemen
t un circuit synchrone qui reçoit des entrées et \nproduit des sorties
à chaque cycle d'horloge.\n\nJe proposerai ensuite une extension conse
rvative de ce langage avec des \ntraits de programmation de haut niveau
(récursion terminale, parallélisme à \ngros grain, tableaux implémen
tés en mémoire RAM, voire même des structures \nde données dynamique
s). Cette extension facilite la programmation \nd'applications réactive
s incorporant des calculs « longs » progressant, pas \nà pas, de fa
çon synchrone.\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20231013T133000
DTEND;TZID=Europe/Paris:20231013T163000
DTSTAMP;TZID=Europe/Paris:20231013T133000
UID:2023-10-13_Pesin
LOCATION:Salle W; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Basile Pesin: Verified Compilation of a Synchronous Dataflow Lan
guage with State Machines
URL:http://parkas.di.ens.fr/seminars.html#2023-10-13_Pesin
DESCRIPTION:_PhD thesis defense._\n\n_There will be a “pot-de-thèse
downstairs in the Cour aux Ernests after the \ndefense._\n_Extra infor
mation can be found on the dedicated [web \npage](https://vertmo.org/the
sis/)._\n\nSafety-critical embedded systems are often specified using bl
ock-diagram \nformalisms. SCADE Suite is a development environment for s
uch systems which \nhas been used industrially in avionics, nuclear plan
ts, automotive and other \nsafety-critical contexts for twenty years. It
s graphical formalism \ntranslates to a textual representation based on
the Lustre synchronous \ndataflow language, with extensions from later l
anguages like Lucid \nSynchrone. In Lustre, a program is defined as a se
t of equations that relate \ninputs and outputs of the program at each d
iscrete time step. The language \nof expressions at right of equations i
ncludes arithmetic and logic \noperators, delay operators that access th
e previous value of an expression, \nand sampling operators that allow s
ome values to be calculated less often \nthan others.\n\nThe Vélus proj
ect aims at formalizing a subset of the Scade 6 language in \nthe Coq Pr
oof Assistant. It proposes a specification of the dynamic \nsemantics of
the language as a relation between infinite streams of inputs \nand out
puts. It also includes a compiler that uses CompCert, a verified \ncompi
ler for C, as its back end to produce assembly code, and an end-to-end \
nproof that compilation preserves the semantics of dataflow programs.\n\
nIn this thesis, we extend Vélus to support control blocks present in S
cade 6 \nand Lucid Synchrone, which includes a construction that control
s the \nactivation of equations based on a condition (switch), a constru
ction that \naccesses the previous value of a named variable (last), a c
onstruction that \nre-initializes delay operators (reset), and finally,
hierarchical state \nmachines, which allow for the definition of complex
modal behaviors. All of \nthese constructions may be arbitrarily nested
in a program. We extend the \nexisting semantics of Vélus with a novel
specification for these constructs \nthat encodes their behavior using
sampling. We propose a generic induction \nprinciple for well-formed pro
grams, which is used to prove properties of the \nsemantic model such as
determinism and type system correctness. Finally, we \ndescribe the ext
ension of the Vélus compiler to handle these new constructs. \nWe show
that the existing compilation scheme that lowers these constructs \ninto
the core dataflow language can be implemented, specified and verified \
nin Coq. Compiling the reset and last constructs requires deeper changes
in \nthe intermediate languages of Vélus.\n\nThe members of the thesis
committee are\n* [Magnus Myreen](https://www.cl.cam.ac.uk/~mom22/) (Rep
orter),\n Chalmers\n* [Robert de Simone](http://www-sop.inria.fr/member
s/Robert.De_Simone/) (Reporter),\n Inria\n* Carlos Agon,\n IRCAM\n* [J
ulien Forget](https://pro.univ-lille.fr/julien-forget),\n Université d
e Lille\n* [Xavier Leroy](https://xavierleroy.org/),\n Collège de Fran
ce\n* [Timothy Bourke](https://www.tbrk.org) (Supervisor),\n Inria and
ENS\n* [Marc Pouzet](https://www.di.ens.fr/~pouzet/) (Supervisor),\n EN
S and Inria\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20231013T090000
DTEND;TZID=Europe/Paris:20231013T100000
DTSTAMP;TZID=Europe/Paris:20231013T090000
UID:2023-10-13_Myreen
LOCATION:salle Lions 1; bâtiment C; Inria Paris; 2 rue Simone Iff; Pari
s 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Magnus Myreen: The CakeML Project: Verified Compilation, Verifie
d Bootstrapping, Just-In-Time Compilation, and Applications
URL:http://parkas.di.ens.fr/seminars.html#2023-10-13_Myreen
DESCRIPTION:_Attention: This is a joint Parkas/Cambium seminar held at I
nria Paris in \nthe 12e_\n\nThis talk will be about the [CakeML](https:/
/cakeml.org/) project. The \nCakeML project centres around an impure fun
ctional programming language, for \nwhich we have developed a collection
of proofs and tools inside the \n[HOL4](https://hol-theorem-prover.org/
) theorem prover. The development \nincludes a proven-correct compiler t
hat can bootstrap itself.\n\nThis talk has two parts.\n\nIn the first pa
rt, I will explain the research questions the CakeML project \nhas tackl
ed and outline the main research ideas that have helped us address \nthe
m. The research questions include:\n\n- how can we transfer properties p
roved of logic functions to\n properties of machine code compiled from
those functions?\n- how can we use a verified compiler to compile itself
?\n- how can we reason about space usage of CakeML programs?\n- how can
we prove liveness properties for non-terminating code?\n\nIn the second
part, I will describe how the CakeML project strives to\nbuild meaningfu
l connections with other projects and our experience\nwith this so far.
We have:\n\n- built a proved-to-be-sound clone of the HOL light theorem
prover\n- produced a verified compiler for a Haskell-like language\n- co
nstructed several verified checkers, including checkers for UNSAT\n pro
ofs, floating-point error bounds, OpenTheory article files,\n pseudo-Bo
olean proofs, and Integer Programming proofs\n\nThe CakeML project is a
collaborative open source project and we are always \nkeen to explore ne
w directions and collaborations.\n\nThe CakeML webpage: \n\nThe CakeML project lives in the HOL4 theorem prover:\n\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20230718T153000
DTEND;TZID=Europe/Paris:20230718T163000
DTSTAMP;TZID=Europe/Paris:20230718T153000
UID:2023-07-18_Cohen
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Albert Cohen: Bidirectional Reactive Programming for Machine Lea
rning
URL:http://parkas.di.ens.fr/seminars.html#2023-07-18_Cohen
DESCRIPTION:Reactive programming languages are dedicated to the programm
ing of systems \nwhich react continuously with their environment. An env
ironment is commonly \nassociated with physical sensors in a control sys
tem, but it may also model \ninteractions with another program over time
, or even the concurrency of the \nunderlying hardware platform. Values
take the form of unbounded streams, \nmodeling the (discrete) passing of
time or the sequence of concurrent \ninteractions, and computations res
ult from the implicit application of the \n`fold_left` iterator over poi
ntwise reactions on streams. While `fold_left` \nimplements forward recu
rrences, we introduce symmetric reactive semantics \ncorresponding to th
e implicit application of the `fold_right` iterator, \nenabling what we
would like to refer to as bidirectional reactive \nprogramming. Constrai
nts on backward recurrences allow to preserve important \nproperties of
reactive languages, including and bounded memory and reaction \ntime. Ma
chine Learning (ML) systems provide numerous motivations for this: \nwe
demonstrate that reverse-mode automatic differentiation, backpropagation
, \nbatch normalization, bidirectional recurrent neural networks, traini
ng and \nreinforcement learning algorithms, are all naturally captured a
s \nbidirectional reactive programs. We will discuss our ongoing progres
s in the \narea.\n\n_(Joint work with Dumitru Potop-Butucaru and Hugo Po
mpougnac.)_\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20230627T160000
DTEND;TZID=Europe/Paris:20230627T170000
DTSTAMP;TZID=Europe/Paris:20230627T160000
UID:2023-06-27_Guatto
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Adrien Guatto: Permissions, fonctions, récursion, normalisation
URL:http://parkas.di.ens.fr/seminars.html#2023-06-27_Guatto
DESCRIPTION:(En collaboration avec C. Tasson.)\n\nPlusieurs travaux réc
ents et moins récents suggèrent d'intégrer une notion \nabstraite de
permission au cœur d'un langage de programmation. Les \npermissions doi
vent a minima pouvoir être comparées et combinées, \nc'est-à-dire ap
partenir à un préordre monoïdal.\n\nCet exposé traitera dans un prem
ier temps d'un λ-calcul simplement typé où \nla gestion des permissio
ns est présentée sous forme fonctionnelle, \nc'est-à-dire introduite
via une construction d'abstraction et éliminée via \nune construction
d'application. Le langage exhibe les propriétés attendues \ndes λ-cal
culs typés (réduction du sujet, confluence, normalisation) et ce \nque
l que soit le préordre monoïdal des permissions considéré.\n\nDans u
n second temps, j'instancierai ce langage générique sur le préordre \
nmonoïdal des horloges synchrones, et y ajouterai la récursion gardée
et les \nsuites infinies. Je conjecture que les programmes bien typés
du langage \nobtenu sont productifs et synchrones : toute sortie d'une f
onction de suites \ndéfinissable contient une infinité d'éléments do
nt chacun ne dépend que des \néléments de rang inférieur des entrée
s. Je discuterai enfin de la \npossibilité de formuler la productivité
comme un résultat de normalisation \ninfinitaire.\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20230621T143000
DTEND;TZID=Europe/Paris:20230621T153000
DTSTAMP;TZID=Europe/Paris:20230621T143000
UID:2023-06-21_Sankur
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Ocan Sankur: Model Checking Algorithms for Real-time Systems
URL:http://parkas.di.ens.fr/seminars.html#2023-06-21_Sankur
DESCRIPTION:Model checking is a technique for exhaustive verification. A
lthough recent \nalgorithms allow one to verify large models, the scalab
ility is still \nlimited for models with real-time constraints, that is,
when time delays, \nexecution times, and deadlines are modeled explicit
ly. In this talk, we \npresent some attempts to develop efficient algori
thms for model checking \ntimed automata with large discrete state space
s using techniques based on \npredicate abstraction, binary decision dia
grams, SMT solvers, and automata \nlearning algorithms.\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20230425T140000
DTEND;TZID=Europe/Paris:20230425T150000
DTSTAMP;TZID=Europe/Paris:20230425T140000
UID:2023-04-25_Broman
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:David Broman: Key aspects of the Miking framework: language comp
osition, probabilistic domain-specific languages, and statically resolva
ble ambiguity
URL:http://parkas.di.ens.fr/seminars.html#2023-04-25_Broman
DESCRIPTION:An essential benefit of domain-specific modeling languages i
s that engineers and scientists can describe problems declaratively at a
high level of abstraction. That is, users can focus on what to model ra
ther than how to create an efficient implementation. Although there are
many benefits with well-engineered modeling languages, the development a
nd maintenance cost can be very high. In this talk, I will give a brief
overview of a new framework called Miking that aims to address these cha
llenges. Specifically, I will discuss some key aspects of the framework,
including language fragments composition, DSLs for probabilistic progra
mming, and a new concept called statically resolvable ambiguity.\n\n_Bi
o:_\n\nDavid Broman is a Professor at the Department of Computer Science
, KTH Royal Institute of Technology and an Associate Director Faculty fo
r Digital Futures. He received his Ph.D. in Computer Science in 2010 fro
m Linköping University, Sweden. Between 2012 and 2014, he was a visitin
g scholar at the University of California, Berkeley, where he also was e
mployed as a part-time researcher until 2016. His research focuses on th
e intersection of (i) programming languages and compilers, (ii) real-tim
e and cyber-physical systems, and (iii) probabilistic machine learning.
David has received a Distinguished Artifact Award at ESOP (co-authored 2
022), an outstanding paper award at RTAS (co-authored 2018), a best pape
r award in the journal Software & Systems Modeling (SoSyM award 2018), t
he award as teacher of the year, selected by the student union at KTH (2
017), the best paper award at IoTDI (co-authored 2017), and awarded the
Swedish Foundation for Strategic Research's individual grant for future
research leaders (2016). He has worked several years within the software
industry, and is a member of IFIP WG 2.4, Modelica Association, a senio
r member of IEEE, and a board member of Forskning och Framsteg.\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20221124T090000
DTEND;TZID=Europe/Paris:20221124T100000
DTSTAMP;TZID=Europe/Paris:20221124T090000
UID:2022-11-24_Jeanin
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Jean-Baptiste Jeanin: Verification of Cyber-Physical Systems wit
h Synchronous Programming, Refinement Types and Active Corners
URL:http://parkas.di.ens.fr/seminars.html#2022-11-24_Jeanin
DESCRIPTION:Robots and other cyber-physical systems are held to high sta
ndards of safety \nand reliability. Formal verification can provide high
assurance, but \nprogramming languages and techniques that lend themsel
ves well to \nverification often do not produce executable code. We pres
ent MARVeLus, a \nstream-based approach to combining verification and ex
ecution in a \nsynchronous programming language with refinement types, b
ased on Zélus. Our \napproach allows formal guarantees to be made about
implementation-level \nsource code. We demonstrate the end-to-end proce
ss of developing a safe \nrobotics application, from modeling and verifi
cation to implementation and \nexecution.\n\nOne prominent example is th
e verification of collision avoidance between \nvehicles. When we do not
assume that the vehicles are point masses, the \nverification condition
s can often not be discharged fully automatically. We \nconsider a conve
x polygonal vehicle with nonzero area traveling along a \n2-dimensional
trajectory, and we derive an easily-checkable, quantifier-free \nformula
to check whether a given obstacle will collide with the vehicle \nmovin
g on the planned trajectory. Our technique compares favorably to \nquant
ifier elimination in several case studies.\n\n_Bio:_\n\n[Jean-Baptiste J
eannin](http://www-personal.umich.edu/~jeannin/) is an \nAssistant Profe
ssor in [Aerospace Engineering](https://aero.engin.umich.edu) \nat the [
University of Michigan](https://umich.edu), interested in Formal \nVerif
ication and Programming Languages, and their applications to providing \
nstrong guarantees to Aerospace, Robotics, and Cyber-Physical Systems. H
e \nreceived an Engineering degree from École polytechnique, and a Ph.D
. in \nComputer Science from Cornell University in 2013.\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20221123T100000
DTEND;TZID=Europe/Paris:20221123T110000
DTSTAMP;TZID=Europe/Paris:20221123T100000
UID:2022-11-23_Pasteur
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Cédric Pasteur: Scade One, Embedded Software Design Reinvented
URL:http://parkas.di.ens.fr/seminars.html#2022-11-23_Pasteur
DESCRIPTION:In this presentation, I will introduce Scade One, the next g
eneration of \nSCADE. I will present the high-level objectives and featu
res of Scade One, \nwith demo videos of the Technology Preview.\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20220520T160000
DTEND;TZID=Europe/Paris:20220520T170000
DTSTAMP;TZID=Europe/Paris:20220520T160000
UID:2022-05-20_Mendler
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Michael Mendler: Clocks Types for Synchronous Stream Processing
Revisited
URL:http://parkas.di.ens.fr/seminars.html#2022-05-20_Mendler
DESCRIPTION:Functional programming permits us to express complex computa
tional \nabstractions very efficiently while using types to force these
abstractions \nto remain well-behaved. E.g., in second-order polymorphic
lambda calculus \n(System F) we can define many standard inductive data
-types so that \nwell-typed programs using these data types are guarante
ed to be \ndeterministic and terminating.\n\nIt is natural to search for
a “System F” for computational domains where not \nevery data type
is inductive. An important such domain is reactive data-flow \nprogrammi
ng which is based on the co-inductive domain of polymorphic \nstreams. H
ere, affairs turn a twist. While determinism is still important it \nis
the behavioural property of “progress” that we are concerned about:
A \nreactive computation must not terminate but instead exhibit an infin
ite \nsequence of reaction cycles each of which should be finite (bounde
d) in \nmemory and time. The type-free functional model of stream-proces
sing by Kahn \nis very powerful but no "System K" is known that would un
iformly guarantee \nprogress for Kahn-style stream-programming like Syst
em F does for \nnon-interactive programming.\n\nHowever, interesting and
practically useful type systems are known for \nspecial cases. This tal
k revisits the type system proposed by Pouzet et al. \nfor the synchrono
us programming languages Lucid Synchrone/Velus. It extends \nthe predica
tive typing system of Hindley-Milner for data by “clock types” \nand
“causality types” as additional layers to control synchronisation.
A \nwell-typed program is then guaranteed to be progressive, i.e., deadl
ock-free \nand memory bounded, under a strictly synchronous model of sch
eduling. For \npractical applications within the given restricted class
of synchronous \nprograms this achieves its goals. However, it remains o
utside of a “System \nK” in the following sense: The typing system f
irstly exploits dependent \ntypes and secondly it uses separate type sys
tems, specifically, one for \neliminating deadlocks and another for elim
inating unbounded memory. In the \ntalk we will discuss a variation to a
void dependent types and to manage \ncausality and initialisation in one
and the same typing language, without \n(hopefully) losing expressivene
ss. The aim is to provide a more elementary \nreference calculus for tea
ching purposes and a simpler basis for discussion \nof approximations of
what might eventually become to be identified as \n“System K”.\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20211122T090000
DTEND;TZID=Europe/Paris:20211122T183000
DTSTAMP;TZID=Europe/Paris:20211122T090000
UID:2021-11-22_Synchron
LOCATION:La Rochette; 35 minutes by train from Paris; Paris 5e
SEQUENCE:2
STATUS:CONFIRMED
SUMMARY: Workshop : Synchron 2021 — 28th International Open Workshop o
n Synchronous Programming
URL:http://parkas.di.ens.fr/seminars.html#2021-11-22_Synchron
DESCRIPTION:The [PARKAS](https://parkas.di.ens.fr) team and Inria Paris
is organizing\n[Synchron 2021](http://synchron2021.inria.fr) over five d
ays at the end of \nNovember.\n\nThe Open Synchron Workshop is the annua
l meeting of experts and young \nresearchers in the area of synchronous
reactive programming. The main topics \ninclude executable specification
s, program analysis, operational semantics, \nmodel-based design, formal
methods, real-time programming, dedicated \narchitectures, timing predi
ctability, and controller synthesis.\n\nThe genuine format of the Open S
ynchron Workshop makes it unique in the \nmodern landscape: there is no
preliminary paper selection, and authors may \npresent their new work in
any available slot on a first-come/first-served \nbasis. While the audi
ence typically comprises a number of established \nresearchers in the to
pic, newcomers are more than welcome. The cosy seminar \natmosphere crea
ted by the venue in a single housing location is an \nopportunity for in
formal discussions and exchanges between researchers of \ndiffering seni
ority and expertise. Innovative contributions in blending \nreactive mod
eling and programming notions with neighboring research subjects \nand c
reative applicative domains, even at preliminary conceptual stages are \
nalways greatly appreciated.\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20201126T090000
DTEND;TZID=Europe/Paris:20201126T174500
DTSTAMP;TZID=Europe/Paris:20201126T090000
UID:2020-11-26_Synchron
LOCATION:online; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY: Online Workshop : Synchron 2020 — 27th International Open Wor
kshop on Synchronous Programming
URL:http://parkas.di.ens.fr/seminars.html#2020-11-26_Synchron
DESCRIPTION:The [PARKAS](https://parkas.di.ens.fr) team is organizing\n[
Synchron 2020](http://synchron2020.inria.fr) over two days at the end of
\nNovember. Please join us online for 18 presentations from all over th
e \nworld.\n\nThe Open Synchron Workshop is the annual meeting of expert
s and young \nresearchers in the area of synchronous reactive programmin
g. The main topics \ninclude executable specifications, program analysis
, operational semantics, \nmodel-based design, formal methods, real-time
programming, dedicated \narchitectures, timing predictability, and cont
roller synthesis.\n\nThe genuine format of the Open Synchron Workshop ma
kes it unique in the \nmodern landscape: there is no preliminary paper s
election, and authors may \npresent their new work in any available slot
on a first-come/first-served \nbasis. While the audience typically comp
rises a number of established \nresearchers in the topic, newcomers are
more than welcome. The cosy seminar \natmosphere created by the venue in
a single housing location is an \nopportunity for informal discussions
and exchanges between researchers of \ndiffering seniority and expertise
. Innovative contributions in blending \nreactive modeling and programmi
ng notions with neighboring research subjects \nand creative applicative
domains, even at preliminary conceptual stages are \nalways greatly app
reciated.\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20200706T083000
DTEND;TZID=Europe/Paris:20200706T123000
DTSTAMP;TZID=Europe/Paris:20200706T083000
UID:2020-07-06_Brun
LOCATION:salle Henri Cartan; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Lélio Brun: Mechanized Semantics and Verified Compilation for a
Dataflow Synchronous Language with Reset
URL:http://parkas.di.ens.fr/seminars.html#2020-07-06_Brun
DESCRIPTION:PhD thesis defense.\n\n_This will be an online thesis defens
e. Please \n[connect](https://global.gotomeeting.com/join/281254693) wit
h GoToMeeting \nusing your full name before the meeting is locked at 8:2
0am.\nIt may be possible to join us physically at the ENS and there may
also be a \n“pot” in the Cours Pasteur after the defense.\nWe don't
know yet. Watch this space (or contact \n[Lélio](mailto:Lelio.Brun@inri
a.fr))!_\n\nSpecifications based on block diagrams and state machines ar
e used to design \ncontrol software, especially in the certified develop
ment of safety-critical \napplications.\nTools like SCADE and Simulink/S
tateflow are equipped with compilers that \ntranslate such specification
s into executable code.\nThey provide programming languages for composin
g functions over streams as \ntypified by dataflow synchronous languages
like Lustre.\n\nIn this thesis we present Vélus, a Lustre compiler ver
ified in the \ninteractive theorem prover Coq.\nWe develop semantic mode
ls for the various languages in the compilation \nchain, and build on th
e verified CompCert C compiler to generate executable \ncode and give an
end-to-end correctness proof.\nThe main challenge is to show semantic p
reservation between the dataflow \nparadigm and the imperative paradigm,
and to reason about byte-level \nrepresentations of program states.\n\n
We treat, in particular, the modular reset construct, a primitive for \n
resetting subsystems.\nThis necessitates the design of suitable semantic
models, compilation \nalgorithms and corresponding correctness proofs.\
nWe introduce a novel intermediate language into the usual clock-directe
d \nmodular compilation scheme of Lustre.\nThis permits the implementati
on of compilation passes that generate better \nsequential code, and fac
ilitates reasoning about the correctness of the \nsuccessive transformat
ions of the modular reset construct.\n\nThe members of the thesis commit
tee are\n* [Gerwin Klein](https://www.cse.unsw.edu.au/~kleing/) (Reporte
r),\n Data61/University of NSW\n* [Xavier Thirioux](http://thirioux.per
so.enseeiht.fr/) (Reporter),\n ISAE-SUPAERO\n* Jean-Louis Colaço,\n A
NSYS\n* Emmanuel Ledinot,\n THALES Research & Technology\n* [Xavier
Leroy](https://xavierleroy.org/),\n Collège de France\n* [Pascal Raym
ond](http://www-verimag.imag.fr/~raymond/),\n Université Grenoble-Alpe
s, CNRS, and VERIMAG\n* [Timothy Bourke](https://www.tbrk.org) (Supervis
or),\n Inria and ENS\n* [Marc Pouzet](https://www.di.ens.fr/~pouzet/) (
Supervisor),\n Sorbonne Université, ENS, and Inria\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20200226T170000
DTEND;TZID=Europe/Paris:20200226T180000
DTSTAMP;TZID=Europe/Paris:20200226T170000
UID:2020-02-26_Lee
LOCATION:salle Henri Cartan; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Edward Lee: A Personal View of Real-Time Computing
URL:http://parkas.di.ens.fr/seminars.html#2020-02-26_Lee
DESCRIPTION:Computers are widely used in timing-sensitive applications s
uch as \ncontrolling vehicles, factories, and medical devices. Today, re
al-time \nbehavior of programs is a property that emerges from implement
ations rather \nthan a property that is specified in models. Control ove
r timing behavior of \nsoftware is difficult to achieve, and timing beha
vior is neither predictable \nnor repeatable. I will argue that this pro
blem can be solved by making a \ncommitment to deterministic models that
embrace temporal properties as an \nintegral part of the modeling parad
igm. I will explain how such models \ndiffer from the prevailing practic
e of modeling low-level computer \narchitectures and estimating worst-ca
se execution time. I will show moreover \nthat deterministic timing is p
ractical today without sacrificing performance \nfor many useful workloa
d models. Specifically, I will describe a class of \ncomputer architectu
res called PRET Machines that deliver deterministic \ntiming with no los
s of performance for a family of real-time problems \nconsisting of spor
adic event streams with hard deadlines.\n\n_This talk is part of the [se
minar series][1] of the Informatics Department \nat the ENS._\n\n[1]: ht
tps://www.di.ens.fr/seminars\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20200221T110000
DTEND;TZID=Europe/Paris:20200221T120000
DTSTAMP;TZID=Europe/Paris:20200221T110000
UID:2020-02-21_Kiselyov
LOCATION:Salle W; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Oleg Kiselyov: Even better stream fusion, as normalization-by-ev
aluation
URL:http://parkas.di.ens.fr/seminars.html#2020-02-21_Kiselyov
DESCRIPTION:The [strymonas library (POPL 2017)][1] is a high-performance
stream code \ngeneration library (DSL) that supports any combination of
zipping, nesting \n(or flat-mapping), sub-ranging, filtering, mapping
of finite or infinite \nstreams. Whatever the stream pipeline, strymo
nas delivers hand-written-like \ncode — but automatically, assuredly a
nd portably, with no reliance on \nblack-box optimizers or sufficiently
smart compilers. Not only is the \nstrymonas-produced code free from int
ermediate data structures of unbounded \nsize, in many cases, the code i
s free from any intermediate data structures \nwhatsoever; the main loop
can run without allocating any memory and without \nany use of GC.\n\nW
e report on the follow-up work, which clarifies the semantic model of \n
strymonas and views stream fusion as normalization-by-evaluation. As a \
nresult, we have reduced the number of core strymonas primitives and mad
e \nthem more general. In the original strymonas, when zipping two strea
ms both \ncontaining filtering or flat-mapping, fixed-size intermediate
data \nstructures seemed inevitable. We have already demonstrated truly
\nconstant-space zipping of filtered streams. Zipping of two flat-mapped
\nstreams is the only case that is still undecided (as of this writing)
.\n\nThis is a joint work with Kobayashi Tomoaki.\n\n[1]: https://strymo
nas.github.io\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20190621T140000
DTEND;TZID=Europe/Paris:20190621T160000
DTSTAMP;TZID=Europe/Paris:20190621T140000
UID:2019-06-21_Reddy
LOCATION:CONF IV/E244 (2nd floor); 24 rue Lhomond; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Chandan Reddy: Polyhedral Compilation for Domain Specific Langua
ges
URL:http://parkas.di.ens.fr/seminars.html#2019-06-21_Reddy
DESCRIPTION:PhD thesis defense.\n\nIn recent years the polyhedral model
has emerged as a powerful mathematical \nframework for loop transformati
ons in optimizing compilers. In this thesis, \nwe study the applicabilit
y of the polyhedral model to the compilation of \ndomain-specific langua
ges, focusing on image processing and deep learning \npipelines. We prop
ose new techniques to enhance the state-of-the-art \npolyhedral compilat
ion toolchain to achieve peak performance close to highly \ntuned libari
es. We extend a polyhedral toolchain to handle reductions which \nare a
key part of image processing and deep learning pipelines and often \nbec
ome the bottleneck if not parallelized. We also extend the Pluto \nalgor
ithm to account for the spatial locality in addition to the temporal \nl
ocality. We also propose a schedule specialization method for given prob
lem \nsizes. Finally, we propose techniques to reduce the autotuning t
ime from \nhours to minutes.\n\nThe members of the thesis committee are\
n* [Cédric Bastoul](http://icps.u-strasbg.fr/people/bastoul/public_html
/),\n University of Strasbourg (Reporter)\n* [Saman Amarasinghe](https:
//people.csail.mit.edu/saman/),\n Massachusetts Institute of Technology
(Reporter)\n* [Corinne Ancour](http://www.cri.ensmp.fr/people/ancourt/)
,\n MINES ParisTech (Examiner)\n* [Christine Eisenbeis](http://pages.sa
clay.inria.fr/christine.eisenbeis/)\n INRIA Saclay (Examiner)\n* [Grigo
ri Fursin](https://fursin.net/research.html),\n Divitditi (Examiner)\n*
[Albert Cohen](https://ai.google/research/people/106208),\n Google and
ENS (Supervisor)\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20190610T150000
DTEND;TZID=Europe/Paris:20190610T170000
DTSTAMP;TZID=Europe/Paris:20190610T150000
UID:2019-06-10_Beaugnon
LOCATION:Salle W; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Ulysse Beaugnon: Efficient Code Generation for Hardware Accelera
tors by Refining Partially Specified Implementations
URL:http://parkas.di.ens.fr/seminars.html#2019-06-10_Beaugnon
DESCRIPTION:PhD thesis defense.\n\n_English_:\nCompilers looking for an
efficient implementation of a function must find \nwhich optimizations a
re the most beneficial. This is a complex problem, \nespecially in the e
arly steps of the compilation process. Each decision may \nimpact the tr
ansformations available in subsequent steps. We propose to \nrepresent t
he compilation process as the progressive refinement of a \npartially sp
ecified implementation. All potential decisions are exposed \nupfront an
d commute. This allows for making the most discriminative \ndecisions fi
rst and for building a performance model aware of which \noptimizations
may be applied in subsequent steps. We apply this approach to \nthe gene
ration of efficient GPU code for linear algebra and yield \nperformance
competitive with hand-tuned libraries.\n\n\n_Français_: Les compilateur
s cherchant à améliorer l'efficacité des \nprogrammes doivent déterm
iner quelles optimisations seront les plus \nbénéfiques. Ce problème
est complexe, surtout lors des premières étapes de \nla compilation o
ù chaque décision influence les choix disponibles aux étapes \nsuivan
tes. Nous proposons de représenter la compilation comme le raffinement
\nprogressif d’une implémentation partiellement spécifiée. Les déc
isions \npossibles sont toutes connues dès le départ et commutent. Cel
a permet de \nprendre les décisions les plus importantes en premier et
de construire un \nmodèle de performance capable d'anticiper les potent
ielles optimisations. \nNous appliquons cette approche pour générer du
code d'algèbre linéaire \nciblant des GPU et obtenons des performance
s comparables aux bibliothèques \noptimisées à la main.\n\nThe member
s of the thesis committee are:\n\n* [Francesco Zappa Nardelli](https://w
ww.di.ens.fr/~zappa/),\n (Examinateur and Président)\n* [Ratislav Bodi
k](https://homes.cs.washington.edu/~bodik/),\n University of Washington
(Rapporteur)\n* [Christophe Dubach](http://homepages.inf.ed.ac.uk/cduba
ch/),\n University of Edinburgh (Rapporteur)\n* [Anton Lokhmotov](http
s://uk.linkedin.com/in/lokhmotov),\n [Dividity](https://www.dividiti.co
m) (Examinateur)\n* [Jacques Pienaar](https://www.linkedin.com/in/jacque
spienaar),\n Google (Examinateur)\n* [Albert Cohen](https://ai.google/r
esearch/people/106208),\n [Google]() (Directeur de thèse)\n* [Marc Pou
zet](https://www.di.ens.fr/~pouzet/),\n ENS et Université Paris 6 (Cod
irecteur de thèse)\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20190515T150000
DTEND;TZID=Europe/Paris:20190515T160000
DTSTAMP;TZID=Europe/Paris:20190515T150000
UID:2019-05-15_Mercadier
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Darius Mercadier: Usuba: high-throughput & constant-time ciphers
, by construction
URL:http://parkas.di.ens.fr/seminars.html#2019-05-15_Mercadier
DESCRIPTION:Cryptographic primitives are subject to diverging imperative
s. The necessity \nof functional correctness and auditability pushes for
using a high-level \nprogramming language. The performance requirements
and the threat of timing \nattacks push for using no more abstract than
an assembler to exploit (or \navoid!) the intricate micro-architectural
features of a given machine. We \nbelieve that a suitable programming l
anguage can reconcile both views and \nactually improve on the state of
the art in both directions. In this work, \nwe introduce Usuba, an opini
onated dataflow programming language in which \nblock ciphers become so
simple as to be “obviously correct” and whose types \ndocument and e
nforce valid parallelization strategies at the bit-level \ngranularity.
We then present Usubac, its optimizing compiler that produces \nhigh-thr
oughput, constant-time implementations performing on par with \nhand-tun
ed reference implementations. The cornerstone of our approach is a \nsys
tematization and generalization of bitslicing, an implementation trick \
nfrequently used by cryptographers. We thus show that Usuba can produce
code \nthat executes between 5% slower to 22% faster than hand-tuned ref
erence \nimplementations while gracefully scaling across a wide range of
\narchitectures and automatically exploiting Single Instruction Multipl
e Data \n(SIMD) instructions whenever the cipher’s structure allows it
.\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20190510T133000
DTEND;TZID=Europe/Paris:20190510T143000
DTSTAMP;TZID=Europe/Paris:20190510T133000
UID:2019-05-10_Forget
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Julien Forget: Data-dependencies in real-time multi-task program
s
URL:http://parkas.di.ens.fr/seminars.html#2019-05-10_Forget
DESCRIPTION:A real-time system is a computer system that controls a phys
ical device in \nits environment, at a rate adapted to the evolution of
the device. These \nsystems are often critical, as a malfunction can lea
d to dramatic \nconsequences. Therefore, real-time system developers mus
t ensure that their \nimplementations are safe, both functionally (produ
cing the correct outputs) \nand temporally (producing outputs at the rig
ht time).\n\nDeveloping a safe real-time system involves methods of two
rather\ndistinct research domains:\n\n1. formal methods, formal language
s and compilation, for the functional \n part;\n\n2. real-time schedul
ing and Worst-Case Execution Time, for the temporal \n part.\n\nThe ob
jective of this talk is to focus on one specific area where both \ndomai
ns meet, namely: *real-time data-dependencies*. A real-time system is \n
typically programmed as a set of concurrent tasks, each with its own \nr
eal-time constraints (periods, deadlines, ...). The talk will focus on t
he \nsemantics, timing analysis, and implementation of inter-task \ndata
-dependencies in such programs.\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20190417T100000
DTEND;TZID=Europe/Paris:20190417T113000
DTSTAMP;TZID=Europe/Paris:20190417T100000
UID:2019-04-17_Todorov
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Vassil Todorov: Méthodes formelles au service de la voiture aut
onome
URL:http://parkas.di.ens.fr/seminars.html#2019-04-17_Todorov
DESCRIPTION:La part croissante des fonctions d'assistance à la conduite
, leur criticité, \nainsi que la perspective d'une certification de ces
fonctions, rendent \nnécessaire leur vérification et leur validation
avec un niveau d'exigence \nque le test seul ne peut assurer. Depuis que
lques années déjà d'autres \ndomaines comme l'aéronautique ou le fer
roviaire sont soumis à des contextes \néquivalents. Pour répondre à
certaines contraintes ils ont localement mis en \nplace des méthodes fo
rmelles. Le groupe PSA expérimente différentes \ntechniques formelles
afin de déterminer celles qui seraient pertinentes, \npour quel type de
développement, ainsi que l'impact de leur déploiement sur \nle proces
sus. Cette présentation fait un tour d'horizon des techniques \nformell
es expérimentées sur du code embarqué réellement utilisé en \nprodu
ction, donne une synthèse des résultats obtenus et propose quelques \n
perspectives pour l'avenir.\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20181213T100000
DTEND;TZID=Europe/Paris:20181213T123000
DTSTAMP;TZID=Europe/Paris:20181213T100000
UID:2018-12-13_Zhao
LOCATION:Salle W; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Jie Zhao: A Combined Language and Polyhedral Approach for Hetero
geneous Parallelism
URL:http://parkas.di.ens.fr/seminars.html#2018-12-13_Zhao
DESCRIPTION:PhD thesis defense. The room is on the very top floor, see [
this \nmap](http://gdt.ludics.eu/index.php/Salle_W).\n\nThe work being p
roposed concerns parallelization and optimizations for two \nimportant c
lasses of applications: sparse computations and iterated \nstencils, tha
t appear frequently in scientific simulation, learning \napplications, i
mage processing, etc.\n\nNowadays, optimizing compilers are increasingly
challenged by the diversity \nof programming languages and heterogeneit
y of architectures.\nThe polyhedral model is a powerful mathematical fra
mework for programs to \nexploit automatic parallelization and locality
optimization, playing an \nimportant role in the field of optimizing com
pilers.\nA long standing limitation of the model has been its restrictio
n to static \ncontrol affine programs, resulting in an emergent demand f
or the support of \nnon-affine extensions.\nThis is particularly acute i
n the context of heterogeneous architectures \nwhere a variety of comput
ation kernels need to be analyzed and transformed \nto match the constra
ints of hardware accelerators and to manage data \ntransfers across memo
ry spaces.\nWe explore multiple non-affine extensions of the polyhedral
model, in the \ncontext of a well-defined intermediate language combinin
g affine and \nsyntactic elements.\nOn the one hand, we explain how tran
sformations and code generation for \nloops with non-affine, data-depend
ent and dynamic loop bounds are integrated \ninto a polyhedral framework
, extending the applicable domain of polyhedral \ncompilation in the rea
lm of non-affine applications.\nOn the other hand, we describe the integ
ration of overlapped tiling for \nstencil computations into a general po
lyhedral framework, automating \nnon-affine transformations in polyhedra
l compilation.\nWe evaluate our techniques on both CPU and CPU architect
ures, validating the \neffectiveness of the optimizations by conducting
an in-depth performance \ncomparison with state-of-the-art frameworks an
d manually-written libraries.\n\nThe members of the thesis committee ar
e:\n\n* [Mary W. Hall](http://www.cs.utah.edu/~mhall/)\n Professor, Uni
versity of Utah (Reviewer)\n* [Cédric Bastoul](http://icps.u-strasbg.fr
/people/bastoul/public_html/),\n Professor, Université de Strasbourg (
Reviewer)\n* Bill McColl, CTO/Fellow, Huawei Research/University of Oxfo
rd (Examiner)\n* [Francesco Zappa Nardelli](https://www.di.ens.fr/~zappa
/),\n Senior Researcher, ENS Paris/INRIA (Examiner)\n* [Claude Tadonki]
(https://www.cri.ensmp.fr/~tadonki/),\n Senior Researcher, Mines ParisT
ech/CRI (Examiner)\n* [Albert Cohen](https://who.rocq.inria.fr/Albert.Co
hen/),\n Research Scientist, Google (Advisor)\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20181115T103000
DTEND;TZID=Europe/Paris:20181115T113000
DTSTAMP;TZID=Europe/Paris:20181115T103000
UID:2018-11-15_Abadi
LOCATION:Inria Paris; Salle Kions 1; bâtiment C; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Martín Abadi: On the Theory and Practice of Software that Learn
s
URL:http://parkas.di.ens.fr/seminars.html#2018-11-15_Abadi
DESCRIPTION:*This is joint Parkas/Gallium seminar to be held at the Inri
a Paris offices*\n\nAs machine learning becomes more powerful and pervas
ive, it has an impact on\nthe many software systems that rely on it and
on the underlying software and\nhardware platforms. The resulting questi
ons should concern virtually all\naspects of the theory and practice of
software, as they relate to software\nengineering, security and trust, p
rogramming, tools, foundations, and\nmore. This talk will discuss some o
f those questions. In particular, it will\npresent recent research on th
e semantics of programming languages suitable for\nlearning by gradient
descent and on adversarial machine learning.\n\n_(This talk is a lightly
updated version of one given at ETAPS 2018.)_\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20180926T140000
DTEND;TZID=Europe/Paris:20180926T150000
DTSTAMP;TZID=Europe/Paris:20180926T140000
UID:2018-09-26_Nobre
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Nuno Miguel Nobre: Polyhedral compilation of dataflow programs
URL:http://parkas.di.ens.fr/seminars.html#2018-09-26_Nobre
DESCRIPTION:Polyhedral techniques are an effective instrument in automat
ic loop tiling \nfor data locality optimisation of sequential programs.
In this presentation, \nI will provide an example of how these technique
s can be applied to \nautomatically adjust the granularity of work in a
one-dimensional \nGauss-Seidel kernel implemented in \n[OpenStream](htt
p://openstream.cs.manchester.ac.uk/), a task-parallel \ndataflow languag
e. Next, I will extend these ideas to the more \nrepresentative two-dime
nsional case and compare the performance of these \npolyhedral-tiled Ope
nStream programs against other implementations, e.g., a \nsequential C i
mplementation, a parallel C implementation using OpenMP, and \nan implem
entation using less convoluted OpenStream routines. Preliminary \nresult
s show that our polyhedral-tiled versions are significantly faster \ntha
n manually tiled OpenStream implementations, and thus demonstrate the \n
value of polyhedral tiling for dataflow programming models. Given enough
\nparallelism, our implementations also outperform polyhedral-tiled Ope
nMP \nimplementations, suggesting that both polyhedral optimisations and
the use \nof a task-parallel dataflow model contribute to better perfor
mance.\n\n_Bio_: Nuno Migeul Nobre is currently a postgraduate research
student in the \nSchool of Computer Science at the University of Manches
ter, UK, where he is \nstudying for a Ph.D. His research interests are f
ocused on scheduling for \nheterogeneous multi-core architectures, langu
ages and compilers for parallel \ncomputing and numerical algorithms. H
e also holds a master's degree in \nPhysics Engineering, awarded in 2016
by the University of Coimbra, Portugal.\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20180903T103000
DTEND;TZID=Europe/Paris:20180903T113000
DTSTAMP;TZID=Europe/Paris:20180903T103000
UID:2018-09-03_Hall
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Mary Hall: Bringing Sparse Computations into the Optimization Li
ght
URL:http://parkas.di.ens.fr/seminars.html#2018-09-03_Hall
DESCRIPTION:Scalable computations where the data is sparse — that is,
a tiny subset\nof the data is populated — are widely represented in sc
ientific\ncomputing and big data analytics. Sparse data are typically r
epresented\nby sparse matrices and graphs, which reduce data storage and
computation\nrequirements (e.g., by storing only nonzero data elements)
through the\nuse of indirection matrices such as `B` in `A[B[i]]`. Thi
s indirection\nimpacts performance on modern architectures. Whether the
code is\noptimized by human programmer, compiler or hardware, any optim
izations\nthat must understand the memory access patterns for A require
the values\nof B, which are not known until runtime. Over time, many op
timizations\nof sparse computations have been developed that simplify th
e code and\nreduce the amount of indirection through custom data represe
ntations,\nbut these representations must also rely on runtime knowledge
of the\nnonzero structure of the sparse data. In this talk, we describ
e a\nframework for composing compile-time and runtime optimizations of s
parse\ncodes, and demonstrate its effectiveness at achieving performance
\ncomparable to manually-tuned code for applications in scientific\ncomp
uting and data analytics.\n\n_Bio_: Mary Hall is a professor in the Scho
ol of Computing at University of\nUtah. She received a PhD in Computer S
cience from Rice University. Her\nresearch focus brings together compil
er optimizations targeting current\nand future high-performance architec
tures on real-world applications.\nHall's prior work has developed compi
ler techniques for exploiting\nparallelism and locality on a diversity o
f architectures: automatic\nparallelization for SMPs, superword-level pa
rallelism for multimedia\nextensions, processing-in-memory architectures
, FPGAs and more recently\nmany-core CPUs and GPUs. Professor Hall is an
ACM Distinguished\nScientist and ACM’s representative on the Computin
g Research Association\nBoard of Directors. She is deeply interested in
computing history,\nhaving served on the ACM History Committee for a dec
ade and as chair\nfrom 2009-2014. She also actively participates in outr
each programs to\nencourage the participation of women and underrepresen
ted minorities in\ncomputer science.\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20180413T110000
DTEND;TZID=Europe/Paris:20180413T120000
DTSTAMP;TZID=Europe/Paris:20180413T110000
UID:2018-04-10_Champion
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Adrien Champion: ICE-based Refinement Type Discovery for Higher-
Order Functional Programs
URL:http://parkas.di.ens.fr/seminars.html#2018-04-10_Champion
DESCRIPTION:We propose a method for automatically finding refinement typ
es of \nhigher-order function programs. Our method is an extension of th
e ICE \nframework of Garg et al. for finding invariants. In addition to
the usual \npositive and negative samples in machine learning, their ICE
framework uses \nimplication constraints, which consist of pairs (x, y)
such that if x \nsatisfies an invariant, so does y. From these constrai
nts, ICE infers \ninductive invariants effectively. We observe that the
implication \nconstraints in the original ICE framework are not suitable
for finding \ninvariants of recursive functions with multiple function
calls. We thus \ngeneralize the implication constraints to those of the
form\n({x1,...,xk}, y), which means that if all of x1, ... , xk satis
fy an \ninvariant, so does y. We extend their algorithms for inferring l
ikely \ninvariants from samples, verifying the inferred invariants, and
generating \nnew samples. We have implemented our method and confirmed i
ts effectiveness \nthrough experiments.\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20180322T110000
DTEND;TZID=Europe/Paris:20180322T120000
DTSTAMP;TZID=Europe/Paris:20180322T110000
UID:2018-03-22_Brisk
LOCATION:salle Henri Cartan; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Philip Brisk: Language and Compiler Design for Laboratories-on-a
-Chip
URL:http://parkas.di.ens.fr/seminars.html#2018-03-22_Brisk
DESCRIPTION:Microfluidics is a multidisciplinary field at the intersecti
on of \nengineering, physics, chemistry, biochemistry, nanotechnology, a
nd \nbiotechnology. It has practical applications to the design of integ
rated \nsystems that process sub-microliter-scale volumes of fluid. Micr
ofluidics \nhas enabled the emergence of a Laboratories-on-a-Chip (LoCs)
, which \nintegrate multiple laboratory functions into devices whose phy
sical size \nranges from square millimeters to square centimeters. Compa
red to \ntraditional benchtop chemistry methods, LoCs offer the benefits
of \nautomation and miniaturization; software-programmable LoCs offer a
n \nimportant additional benefit: programmability.\n\nThis talk will int
roduce BioScript, a domain-specific language for \nprogrammable LoCs, an
d its compiler. Extensibility is particularly important \nfor language d
esign, as each LoC target features a unique set of \ncapabilities, and t
here is no universal functionality among LoCs akin to \nTuring completen
ess. The BioScript compiler presently targets a specific \nclass of semi
conductor-based LoCs which manipulate discrete liquid droplets \non a 2D
electrode grid. The language, compiler, and runtime leverage \nadvances
in sensor integration to execute biochemical procedures that \nfeature
online decision-making based on sensory data acquired during assay \nexe
cution. The compiler features a novel hybrid intermediate representation
\n(IR) that interleaves fluidic operations with computations performed
on \nsensor data. The IR extends the traditional notions of liveness and
\ninterference to fluidic variables and operations, as needed to target
the \nLoC, which itself can be viewed as a spatially reconfigurable arr
ay. The \ncode generator converts the IR into the following:\n\n 1. a s
et of electrode activation sequences for each basic block in the \n con
trol flow graph (CFG);\n 2. a set of computations performed on sensor d
ata, which dynamically \n determine the result of each control flow
operation; and\n 3. a set of electrode activation sequences for each co
ntrol flow transfer \n operation (CFG edge).\n\nThe compiler is validat
ed using a software simulator which produces animated \nvideos of realis
tic bioassay execution on the device. \n\n_Bio_: Philip Brisk received,
the BS, MS, and PhD Degrees, all in Computer \nScience, from UCLA in 200
2, 2003, an 2006 respectively. From 2006-2009 he \nwas a Postdoctoral Sc
holar at EPFL in Switzerland. He has been with UC \nRiverside since 2009
. His research interests include programmable \nmicrofluidics and lab-on
-a-chip technology, FPGAs and reconfigurable \ncomputing, and other forw
ard-looking applications of computer engineering \nprinciples.\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20171025T170000
DTEND;TZID=Europe/Paris:20171025T180000
DTSTAMP;TZID=Europe/Paris:20171025T170000
UID:2017-10-25_Mandel
LOCATION:salle Henri Cartan; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Louis Mandel: Prototyping a Query Compiler using Coq
URL:http://parkas.di.ens.fr/seminars.html#2017-10-25_Mandel
DESCRIPTION:Designing and prototyping new features is important in indus
trial\nprojects. I will present our experience using the Coq proof assis
tant\nas a prototyping environment for building a query compiler for use
in\nIBM's ODM Insights. I will discuss the pros and cons of using Coq f
or\nthis purpose and describe our methodology for porting the compiler t
o\nJava for product integration.\n\nThe initial Coq prototype has evolve
d into [Q*cert][1], an open-source \nplatform for the specification, ver
ification, and implementation of query \ncompilers. This platform includ
es support for SQL and OQL. It can generate \ncode for execution on Java
Script, Spark and Cloudant. It internally relies \non familiar database
intermediate representations, notably the nested \nrelational algebra an
d calculus. The platform also comes with a simple but \nfunctional and e
xtensible query optimizers.\n\nThis is joint work with Joshua Auerbach,
Martin Hirzel, Avi Shinnar and \nJérôme Siméon.\n\n_This talk is [par
t][2] of the seminar series of the Informatics Department \nat the ENS._
\n\n[1]: https://querycert.github.io/\n[2]: http://www.di.ens.fr/Seminai
reGeneral.html.fr#Mercredi_25_octobre_2017_17h00_L\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20170928T103000
DTEND;TZID=Europe/Paris:20170928T113000
DTSTAMP;TZID=Europe/Paris:20170928T103000
UID:2017-09-28_DeBacker
LOCATION:Salle W; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Bruno De Backer: EXEgesis: Understanding CPUs to speed up code
URL:http://parkas.di.ens.fr/seminars.html#2017-09-28_DeBacker
DESCRIPTION:Google's [EXEgesis project][1] takes a principled approach t
o generating \ncode for modern processors. This talk will start with a r
efresher on modern \ncomputer architectures. We shall see why it is impo
rtant to have precise \ninstruction itineraries. We will then turn to th
e combinatorial optimization \nmodels for obtaining these itineraries. W
e will then touch on some gains \nthat we've obtained so far.\n\nThe EXE
gesis team is based in the Google Paris office. Many of us have a \nback
ground in combinatorial optimization, and we are passionate about CPUs.\
n\n(NB: The [salle W][2] is well hidden. Please don't hesitate to come t
o the \n[PARKAS][3] area beforehand. We will leave together at 10:20.)\n
\n[1]: https://opensource.google.com/projects/exegesis\n[2]: http://gdt.
ludics.eu/index.php/Salle_W\n[3]: http://parkas.di.ens.fr/#where
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20170608T110000
DTEND;TZID=Europe/Paris:20170608T120000
DTSTAMP;TZID=Europe/Paris:20170608T110000
UID:2017-06-08_Nicolet
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Victor Nicolet: Synthesis of Divide And Conquer Parallelism for
Loops
URL:http://parkas.di.ens.fr/seminars.html#2017-06-08_Nicolet
DESCRIPTION:We focus on the automated synthesis of divide-and-conquer pa
rallelism,\nwhich is a common parallel programming skeleton supported by
many\ncross-platform multithreaded libraries. The challenges of produci
ng\n(manually or automatically) a correct divide-and-conquer parallel pr
ogram\nfrom a given sequential code are two-fold:\n\n1. assuming that in
dividual worker threads execute a code identical to the \n sequential
code, the programmer has to provide the extra code for \n dividing the
tasks and combining the computation results, and\n\n2. sometimes, the s
equential code may not be usable as is, and may need to \n be modified
by the programmer.\n\nWe address both challenges in this paper. We pres
ent an automated synthesis\ntechnique for the case where no modification
s to the sequential code are\nrequired, and we propose an algorithm for
modifying the sequential code to\nmake it suitable for parallelization w
hen some modification is necessary.\nFinally, we present theoretical res
ults for when this modification is\nefficiently possible, and experiment
al evaluation of the technique and the\nquality of the produced parallel
programs.\n\n(This work will appear in [PLDI 2017](http://pldi17.sigpla
n.org/event/pldi-2017-papers-automated-synthesis-of-divide-and-conquer-p
arallelism).)\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20170405T140000
DTEND;TZID=Europe/Paris:20170405T170000
DTSTAMP;TZID=Europe/Paris:20170405T140000
UID:2017-04-05_Morisset
LOCATION:salle 236; 29 rue d'Ulm; ENS; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Robin Morisset: Compiler Optimisations and Relaxed Memory Consis
tency Models
URL:http://parkas.di.ens.fr/seminars.html#2017-04-05_Morisset
DESCRIPTION:PhD thesis defense.\n\nThere will be a “pot-de-thèse” a
fter the defense at 45 rue d'Ulm. Please \nRSVP to Robin by [email](mail
to://robin.morisset@normalesup.org) if you will \nattend.\n\nModern mult
iprocessor architectures and programming languages exhibit weakly \ncons
istent memories. Their behaviour is formalised by the memory model of \n
the architecture or programming language; it precisely defines which wri
te \noperation can be returned by each shared memory read. This is not a
lways the \nlatest store to the same variable, because of optimisations
in the \nprocessors such as speculative execution of instructions, the c
omplex \neffects of caches, and optimisations made by compilers.\n\nIn t
his thesis we focus on the C11 memory model that is defined by the 2011
\nedition of the C standard. Our contributions are threefold.\n\nFirst,
we focused on the theory surrounding the C11 model, formally studying \n
which compiler optimisations it enables. We show that many common compil
er \noptimisations are allowed, but, surprisingly, some important ones a
re \nforbidden.\n\nSecondly, building on our results, we developed a ran
dom testing methodology \nfor detecting when mainstream compilers such a
s GCC or Clang perform an \nincorrect optimisation with respect to the m
emory model. We found several \nbugs in GCC, all promptly fixed. We als
o implemented a novel optimisation \npass in LLVM, that looks for specia
l instructions that restrict processor \noptimisations—called fence in
structions—and eliminates the redundant ones.\n\nFinally, we developed
a user-level scheduler for lightweight threads \ncommunicating through
first-in first-out single-producer single-consumer \nqueues. This progra
mming model is known as Kahn process networks, and we \nshow how to effi
ciently implement it, using C11 synchronisation primitives. \nThis shows
that despite its flaws, C11 can be usable in practice.\n\nThe members o
f the thesis committee are:\n\n* [Andrew Appel](https://www.cs.princeton
.edu/~appel/),\n Princeton University (Examiner)\n* [Mark Batty](https:
//www.cs.kent.ac.uk/people/staff/mjb211/),\n University of Kent\n* [Der
ek Dreyer](https://people.mpi-sws.org/~dreyer/),\n Max Planck Institute
for Software Systems\n* [Doug Lea](http://gee.cs.oswego.edu/dl/index.ht
ml),\n State University of New York at Oswego (Examiner)\n* [Marc Pouze
t](http://www.di.ens.fr/~pouzet/),\n UPMC/ENS/Inria Paris\n* [Dmitry Vy
ukov](http://www.1024cores.net),\n Google\n* [Francesco Zappa Nardelli]
(http://www.di.ens.fr/~zappa/),\n Inria Paris (Director)\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20170313T150000
DTEND;TZID=Europe/Paris:20170313T173000
DTSTAMP;TZID=Europe/Paris:20170313T150000
UID:2017-03-13_Baudart
LOCATION:Salle W; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Guillaume Baudart: A Synchronous Approach to Quasi-Periodic Syst
ems
URL:http://parkas.di.ens.fr/seminars.html#2017-03-13_Baudart
DESCRIPTION:PhD thesis defense. The room is on the very top floor, see [
this \nmap](http://gdt.ludics.eu/index.php/Salle_W).\nThere will be a
pot-de-thèse” downstairs after the defense in\n[Salle S16](https://w
ww.di.ens.fr/AccesDI.html.fr) in the Rataud Wing at the \nENS.\nThe [man
uscript](http://guillaume.baudart.eu/thesis/) and supporting \nmaterials
are available online.\n\nIn this thesis we study embedded controllers i
mplemented as sets of \nunsynchronized periodic processes.\nEach process
activates quasi-periodically, that is, periodically with \nbounded jitt
er, and communicates with bounded transmission delays.\nSuch reactive sy
stems, termed _quasi-periodic_, exist as soon as two \nperiodic processe
s are connected together.\nIn the distributed systems literature they ar
e also known as synchronous \nreal-time models.\nWe focus on techniques
for the design and analysis of such systems without \nimposing a global
clock synchronization.\n\nSynchronous languages were introduced as domai
n specific languages for the \ndesign of reactive systems.\nThey offer a
n ideal framework to program, analyze, and verify quasi-periodic \nsyste
ms.\nBased on a synchronous approach, this thesis makes contributions to
the \ntreatment of quasi-periodic systems along three themes: verificat
ion, \nimplementation, and simulation.\n\nVerification: The _quasi-synch
ronous abstraction_ is a discrete abstraction \nproposed by Paul Caspi f
or model checking safety properties of \nquasi-periodic systems.\nWe sho
w that this abstraction is not sound in general and give necessary and \
nsufficient conditions on both the static communication graph of the \na
pplication and the real-time characteristics of the architecture to reco
ver \nsoundness.\nWe then generalize these results to multirate systems.
\n\nImplementation: _Loosely time-triggered architectures_ are protocols
\ndesigned to ensure the correct execution of an application running on
a \nquasi-periodic system.\nWe propose a unified framework that encompa
sses both the application and the \nprotocol controllers.\nThis framewor
k allows us to simplify existing protocols, propose optimized \nversions
, and give new correctness proofs.\nWe instantiate our framework with a
protocol based on clock synchronization \nto compare the performance of
the two approaches.\n\nSimulation: Quasi-periodic systems are but one ex
ample of timed systems \ninvolving real-time characteristics and toleran
ces.\nFor such nondeterministic models, we propose a _symbolic simulatio
n_ scheme \ninspired by model checking techniques for timed automata.\nW
e show how to compile a model mixing nondeterministic continuous-time an
d \ndiscrete-time dynamics into a discrete program manipulating sets of
possible \nvalues.\nEach trace of the resulting program captures a set o
f possible executions of \nthe source program.\n\nThe members of the the
sis committee are:\n\n* [Albert Benveniste](http://people.rennes.inria.f
r/Albert.Benveniste/),\n Inria Rennes (Co-supervisor)\n* [Timothy Bourk
e](http://www.tbrk.org),\n Inria Paris (Supervisor)\n* [Nicolas Halbwac
hs](http://www-verimag.imag.fr/~halbwach/),\n Vérimag (Reporter)\n* [M
arc Pouzet](https://www.di.ens.fr/~pouzet/),\n ENS, UPMC, Inria Paris (
Director)\n* [Xavier Rival](http://www.di.ens.fr/~rival/),\n Inria Pari
s (Examiner)\n* [Alberto Sangiovanni-Vincentelli](http://people.eecs.ber
keley.edu/~alberto/),\n University of California Berkeley (Examiner)\n*
[Cesare Tinelli](http://homepage.cs.uiowa.edu/~tinelli/),\n University
of Iowa (Reporter)\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20170202T110000
DTEND;TZID=Europe/Paris:20170202T120000
DTSTAMP;TZID=Europe/Paris:20170202T110000
UID:2017-02-02_Beaugnon
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Ulysse Beaugnon: Optimization space pruning without regrets
URL:http://parkas.di.ens.fr/seminars.html#2017-02-02_Beaugnon
DESCRIPTION:Many computationally-intensive algorithms benefit from the w
ide\nparallelism offered by Graphical Processing Units (GPUs). However,
the\nsearch for a close-to-optimal implementation remains extremely tedi
ous due\nto the specialization and complexity of GPU architectures.\n\nW
e present a novel approach to automatically discover the best performing
\ncode from a given set of possible implementations. It involves a branc
h\nand bound algorithm with two distinctive features: (1) an analytic\np
erformance model of a lower bound on the execution time, and (2) the\nab
ility to estimate such bounds on a partially-specified implementation.\n
\nThe unique features of this performance model allow to aggressively pr
une\nthe optimization space without eliminating the best performing\nimp
lementation. While the space considered in this paper focuses on GPUs,\
nthe approach is generic enough to be applied to other architectures.\n\
nWe implemented our algorithm in a tool called Telamon} and demonstrate
its\neffectiveness on a huge, architecture-specific and input-sensitive\
noptimization space.\n\n\nThis will be a practice run for Ulysse's prese
ntation at\n[CC 2017](http://conf.researchr.org/event/CC-2017/cc-2017-pa
pers-optimization-space-pruning-without-regrets).\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20170127T110000
DTEND;TZID=Europe/Paris:20170127T120000
DTSTAMP;TZID=Europe/Paris:20170127T110000
UID:2017-01-27_Morisset
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Robin Morisset: Partially redundant fence elimination for x86, A
RM and Power processors
URL:http://parkas.di.ens.fr/seminars.html#2017-01-27_Morisset
DESCRIPTION:We show how partial redundancy elimination (PRE) can be inst
antiated to \nperform provably correct fence elimination for multi-threa
ded programs \nrunning on top of the x86, ARM and IBM Power relaxed memo
ry models.\nWe have implemented our algorithm in the backends of the LLV
M compiler \ninfrastructure.\nThe optimisation does not induce an observ
able overhead at compile-time and \ncan result in up-to 10% speedup on s
ome benchmarks.\n\nThis will be a practice run for Robin and Francesco's
presentation at\n[CC 2017](http://conf.researchr.org/event/CC-2017/cc-2
017-papers-partially-redundant-fence-elimination-for-x86-arm-and-power-p
rocessors).\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20161209T140000
DTEND;TZID=Europe/Paris:20161209T153000
DTSTAMP;TZID=Europe/Paris:20161209T140000
UID:2016-12-09_MinhLe
LOCATION:salle Celan; 45 rue d'Ulm; ENS; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Nhat Minh Lê: Kahn Process Networks as Concurrent Data Structur
es: Lock Freedom, Parallelism, Relaxation in Shared Memory
URL:http://parkas.di.ens.fr/seminars.html#2016-12-09_MinhLe
DESCRIPTION:PhD thesis defense. The room is on the ground floor, at numb
er 14 on\n[this map](http://www.ens.fr/IMG/pdf/Plan_45ULM_RDC.pdf).\n\nI
n this thesis, we are interested in Kahn process networks, a simple\nyet
expressive model of concurrency, and its parallel implementation\non mo
dern shared-memory architectures. Kahn process networks expose\nconcurre
ncy to the programmer through an arrangement of sequential\nprocesses an
d single-producer single-consumer channels.\n\nThe focus is on the imple
mentation aspects. Of particular importance\nto our study are two parame
ters: lock freedom and relaxed memory. The\ndevelopment of fast and effi
cient lock-free algorithms ties into\nconcerns of controlled resource co
nsumption (important in embedded\nsystems) and reliable performance on c
urrent and future platforms with\nunfair or skewed scheduling such as vi
rtual machines and GPUs. Our\nwork with relaxed memory models complement
s this more theoretical\napproach by offering a window into realistic sh
ared-memory\narchitectures.\n\nWe present a new lock-free algorithm for
a Kahn process network\ninterpreter. It is disjoint-access parallel: we
allow multiple threads\nto work on the same shared Kahn process network,
fully utilizing the\nparallelism exhibited by independent processes. It
is non-blocking in\nthat it guarantees global progress in bounded memor
y, even in the\npresence of (possibly infinite) delays affecting the exe
cuting\nthreads. To our knowledge, it is the first lock-free system of t
his\nsize, and integrates various well-known non-blocking techniques and
\nconcepts (e.g., safe memory reclamation, multi-word updates,\nassistan
ce) with ideas and optimizations specific to the Kahn network\nsetting.
We also discuss a blocking variant of this algorithm,\ntargetted at high
-performance computing, with encouraging experimental\nresults.\n\nThe m
embers of the thesis committee are:\n\n* [Albert Cohen](https://who.rocq
.inria.fr/Albert.Cohen/),\n Inria Paris (Directeur)\n* [Mike Dodds](htt
ps://www-users.cs.york.ac.uk/~miked/),\n University of York (Rapporteur
)\n* [Alastair F. Donaldson](http://multicore.doc.ic.ac.uk),\n Imperial
College (Examinateur)\n* [Tim Harris](https://timharris.uk),\n Oracle
Labs Cambridge (Examinateur)\n* [Francesco Zappa Nardelli](http://www.di
.ens.fr/~zappa/),\n Inria Paris (Président)\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20161124T140000
DTEND;TZID=Europe/Paris:20161124T150000
DTSTAMP;TZID=Europe/Paris:20161124T140000
UID:2016-11-24_Rajopadhye
LOCATION:salle Aimé Césaire; 2ème escalier A; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Sanjay Rajopadhye: Thirty Years of the Polyhedral Model and Wher
e are We?
URL:http://parkas.di.ens.fr/seminars.html#2016-11-24_Rajopadhye
DESCRIPTION:Even after thirty years, the polyhedral model is far from be
ing an unequivocal success, even on the restricted domain where it is ap
plicable. We do not (yet) have compilers for general-purpose processors
that can generate code approaching either the machine peak, or the algo
rithmic peak of the source program, or hand tuned libraries developed by
“heroes of high performance computing.” I will try to explain why
this is so, and suggest a plan of how we can improve this state of affai
rs.
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20161107T110000
DTEND;TZID=Europe/Paris:20161107T120000
DTSTAMP;TZID=Europe/Paris:20161107T110000
UID:2016-11-07_Pai
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Sreepathi Pai: A Compiler for Throughput Optimization of Graph P
rograms on GPUs
URL:http://parkas.di.ens.fr/seminars.html#2016-11-07_Pai
DESCRIPTION:Graphics Processing Units (GPUs) are an attractive target fo
r graph\nalgorithms because they support massively parallel execution an
d\npossess much higher memory bandwidths than CPUs and FPGAs. However,\n
graph programs are also highly irregular and low-level GPU programming\n
models make writing high-performance implementations very challenging.\n
\nIn this talk, I will describe the Galois GPU compiler that we have\nbu
ilt to generate high-performance implementations of graph\nalgorithms on
GPUs. Beginning with a high-level representation of\ngraph algorithms,
which we call IrGL, our compiler generates\noptimized CUDA code for NVID
IA GPUs by applying three key\noptimizations that I argue are fundamenta
l to high-performance\nimplementations of graph algorithms on GPUs. Eval
uation on eight\ngraph applications shows that our compiler produces cod
e that\noutperforms all current state-of-the-art handwritten CUDA\nimple
mentations.\n\nGraph program performance strongly depends on the inputs,
and this\nmakes picking the right set of optimizations for a given inpu
t very\ndifficult. We show how our compiler can exploit queuing network\
nmodels generated from IrGL source code to customize optimizations\nfor
combinations of applications and inputs.\n\nParts of this work will appe
ar in OOPSLA 2016.
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20161027T100000
DTEND;TZID=Europe/Paris:20161027T110000
DTSTAMP;TZID=Europe/Paris:20161027T100000
UID:2016-10-27_Janin
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:David Janin: Semantic models for timed programing languages
URL:http://parkas.di.ens.fr/seminars.html#2016-10-27_Janin
DESCRIPTION:In this talk, I consider temporally causal functions of time
d streams, i.e., \nfunctions that produce output values at a given insta
nt that only depend on \nthe input values that have been received till t
hat instant. Defining partial \ntimed streams that form a directed compl
ete partial order (DCPO), I will \nshow how causal functions are nicely
captured as limits of continuous and \nsynchronous functions over these
DCPO offering thus a denotational model of \ncausal timed functions. Rel
axing the synchronous hypothesis to a \npre-synchronous hypothesis, I wi
ll show how every causal function admits a \nlattice of possible denotat
ions such that:\n\n * the least element can be understood as the latest
semantics of that \n function: output values are computed when they
need to be outputted,\n * the greatest element can be understood as the
earliest semantics of that \n function: output values are computed a
s soon as all the input values \n they depend have been received.\n
* other elements in between can be understood as the various possible \n
computation schedules that can still be followed in order to run the
\n causal function.\n\nThe categorical properties of these continuou
s functions will then be \ndetailed, offering various relevant operators
for programing with them.\nLastly, I will show that a notion of causal
function residual is available \nso that a minimal (possibly continuous)
IO-automaton can be associated to \nevery causal function, providing th
us an abstract operational (latest) \nsemantics. Open perspectives and q
uestions will conclude this presentation.\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20161018T110000
DTEND;TZID=Europe/Paris:20161018T120000
DTSTAMP;TZID=Europe/Paris:20161018T110000
UID:2016-10-18_Champion
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Adrien Champion: Kind 2: Contract-based Compositional Reasoning
URL:http://parkas.di.ens.fr/seminars.html#2016-10-18_Champion
DESCRIPTION:Contract-based software development is a leading methodology
for the \nconstruction of safety- and mission-critical embedded systems
. Contracts are \nan effective way to establish boundaries between compo
nents and can be used \nefficiently to verify global properties by using
compositional reasoning \ntechniques. A contract specifies the assumpti
ons a component makes on its \ncontext and the guarantees it provides. R
equirements in the specification of \na component are often case-based,
with each case describing what the \ncomponent should do depending on a
specific situation (or mode) the \ncomponent is in. This talk introduces
CoCoSpec, a mode-aware \nassume-guarantee-based contract language for e
mbedded systems built as an \nextension of the Lustre language. CoCoSpec
lets users specify mode behavior \ndirectly, instead of encoding it as
conditional guarantees, thus preventing \na loss of mode-specific inform
ation. Mode-aware model checkers supporting \nCoCoSpec can increase the
effectiveness of the compositional analysis \ntechniques found in assume
-guarantee frameworks and improve scalability. \nSuch tools can also pro
duce much better feedback during the verification \nprocess, as well as
valuable qualitative information on the contract itself. \nI will presen
ts the CoCoSpec language and illustrate the benefits of \nmode-aware mod
el-checking on a case study involving a flight-critical \navionics syste
m. The evaluation uses [Kind 2][1], a collaborative, parallel, \nSMT-bas
ed model checker developed at the University of Iowa that provides \nful
l support for CoCospec. \n\n[1]: https://github.com/kind2-mc\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20161018T100000
DTEND;TZID=Europe/Paris:20161018T110000
DTSTAMP;TZID=Europe/Paris:20161018T100000
UID:2016-10-18_Bekooij
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Marco Bekooij: A Refinement Theory for Timed-Dataflow Analysis w
ith Support for Reordering
URL:http://parkas.di.ens.fr/seminars.html#2016-10-18_Bekooij
DESCRIPTION:Real-time stream processing applications executed on embedde
d multiprocessor systems often have strict throughput and latency constr
aints. Violating these constraints is undesired and temporal analysis me
thods are therefore used to prevent such violations. These analysis meth
ods use abstractions of the analyzed applications to simplify their temp
oral analysis.\n\nRefinement theories have enabled the creation of deter
ministic abstractions of stream processing applications that are execute
d on multiprocessor systems. Prominent examples of such abstract models
are deterministic timed-dataflow models which can be efficiently analyze
d because they only have one behavior.\n\nAn important aspect of a strea
m processing application can be that it makes use of reordered data stre
ams between tasks. An example is the bit-reversed ordered stream produce
d by a FFT task. Another example is reordering that is a result of data-
parallelism. However, existing abstraction/refinement theories do not su
pport such reordering behavior or do not handle this type of behavior co
rrectly. This is because existing refinement theories assume that the te
mporal behavior of applications is orthogonal to their functional behavi
or, whereas this orthogonality does not always hold in the case of reord
ered data streams.\n\nIn this talk I will present a new refinement theor
y in which the potential interaction between temporal and functional beh
avior is taken into account. The introduced theory supports reordering o
f data and can therefore be used to validate existing systems with such
reordering. Furthermore, the theory enables showing that deterministic d
ataflow models that do not apply reordering can be used as valid abstrac
tions of systems in which reordering takes place.\n\nNote 1: Marco will
also serve on the thesis committee of Khanh Xuan Do, CEA List, NanoInnov
, Monday October 17 at 14:30.\n\nNote 2: we will continue with the semin
ar of Adrien Champion in the same room after a short coffee break.
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20161014T163000
DTEND;TZID=Europe/Paris:20161014T173000
DTSTAMP;TZID=Europe/Paris:20161014T163000
UID:2016-10-14_Mandel
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Louis Mandel: A Compiler Driver in Coq / Un gestionnaire de chem
ins de compilation en Coq
URL:http://parkas.di.ens.fr/seminars.html#2016-10-14_Mandel
DESCRIPTION:[Q*cert][1] is a query compiler written in Coq. Initially d
edicated to the \ncompilation of jRule to Cloudant, it is now able to co
mpile several source \nlanguages (e.g., OQL, NRA) and to generate code f
or Java or Spark. \nInternally, Q*cert uses 14 languages and 27 unitary
translation functions to \ngo directly from one language to another. In
this talk, I will present how \nwe handle all these compilation paths an
d how proofs help to maintain the \noptions of the command line compiler
.\n\nJoint work with Joshua Auerbach, Martin Hirzel, Avraham Shinnar and
\nJérôme Siméon.\n\n* * *\n\n[Q*cert][1] est un compilateur de requê
tes écrit en Coq. Initialement dédié \nà la compilation de jRule ver
s Cloudant, il est maintenant capable de \ncompiler plusieurs langages s
ources (e.g., OQL, NRA) et de générer du code \npour Java ou Spark. En
interne, Q*cert utilise 14 langages et 27 fonctions \nde traductions un
itaires permettant de passer directement d'un langage à un \nautre. Dan
s cet exposé, je présenterai comment nous faisons pour gérer tous \nc
es chemins de compilation et comment les preuves nous aident à mainteni
r à \njour les options de la ligne de commande du compilateur.\n\nTrava
il réalisé en collaboration avec Joshua Auerbach, Martin Hirzel,\nAvra
ham Shinnar et Jérôme Siméon.\n\n[1]: https://querycert.github.io/\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20160930T130000
DTEND;TZID=Europe/Paris:20160930T140000
DTSTAMP;TZID=Europe/Paris:20160930T130000
UID:2016-09-30_Iooss
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Guillaume Iooss: Detection of Linear Algebra Operations in Polyh
edral Programs
URL:http://parkas.di.ens.fr/seminars.html#2016-09-30_Iooss
DESCRIPTION:Writing code which uses an architecture at its full capabili
ty has become an \nincreasingly difficult problem. For some key operatio
ns, a dedicated \naccelerator or a finely tuned implementation exists an
d delivers the best \nperformance. When compiling code, identifying thes
e operations and issuing \ncalls to their high-performance implementatio
ns is thus attractive. In this \ntalk, we focus on the problem of detect
ing such operations. We propose a \nframework which detects linear algeb
ra subcomputations within a polyhedral \nprogram. The main idea of this
framework is to partition the computation in \norder to isolate differen
t subcomputations in a regular manner, then we \nconsider each portion o
f the computation and try to recognize it as a \ncombination of linear a
lgebra operations.\n\nWe perform the partitioning of the computation by
using a program \ntransformation called monoparametric tiling. This tran
sformation partitions \nthe computation into blocks, whose shape is some
homothetic scaling of a \nfixed-size partitioning. We show that the til
ed program remains polyhedral \nwhile allowing a limited amount of param
etrization: a single size parameter. \nThis is an improvement compared t
o the previous work on tiling, that forced \na choice between these two
properties.\n\nThen, in order to recognize computations, we introduce a
template \nrecognition algorithm built built on a state-of-the-art progr
am equivalence \nalgorithm. We also propose several extensions in order
to manage some \nsemantic properties.\n\nFinally, we combine these two c
ontributions into a framework which detects \nlinear algebra subcomputat
ions. A part of this framework is a library of \ntemplates based on the
BLAS specification. We demonstrate our framework on \nseveral applicatio
ns.\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20160817T103000
DTEND;TZID=Europe/Paris:20160817T120000
DTSTAMP;TZID=Europe/Paris:20160817T103000
UID:2016-08-17_Amarasinghe
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Saman Amarasinghe: Halide and Simit: Domain Specific Languages w
hen Performance Matters
URL:http://parkas.di.ens.fr/seminars.html#2016-08-17_Amarasinghe
DESCRIPTION:Achieving high performance is no easy task. From the early d
ays of\ncomputing, many researchers have spent their lifetime trying to
extract more\nFLOPS out of critical codes. Hardcore performance enginee
rs try to get to\nthis performance nirvana single handedly without any h
elp from languages,\ncompilers or tools. In this talk I'll argue that pr
ogramming languages and\ncompiler technology can take on most of the per
formance optimization\nburden... at least in certain domains.\nWe will d
emonstrate the performance optimization ability of compilers and\nlangua
ges in the domains of image processing and physical simulation. Most\nth
ese applications are performance critical, and programmers spend many\nm
onths optimizing them.\nIn the first part of this talk, I will describe
Halide, a language and\ncompiler for image processing. Halide explicitly
separates the description\nof the algorithm, the task of the domain exp
ert, from the choices of\nexecution structure which determine parallelis
m, locality, memory footprint,\nand synchronization, the domain of the p
erformance engineer. We show how\nthis separation simplifies the problem
for both the domain expert and the\nperformance engineer. Using machine
learning we can even eliminate the\nperformance engineer entirely from
the process. The end result is much\nsimpler programs, delivering perfor
mance often many times faster than the\nbest prior hand-tuned C, assembl
y, and CUDA implementations, while scaling\nacross radically different a
rchitectures, from ARM cores to massively\nparallel GPUs.\n\nIn the seco
nd part of the talk, I will introduce Simit, a new language for\nphysica
l simulations. Simit lets the programmer seamlessly work on a\nphysical
system both in its individual geometric elements as a hypergraph as\nwel
l as the behavior of the entire system as set of global tensors. Simit\n
provides a novel assembly construct that makes it conceptually easy and\
ncomputationally efficient to move between these two abstractions. Using
the\ninformation provided by the assembly construct, the compiler gener
ates\nefficient in-place computation on the graph. We demonstrate that S
imit is\neasy to use: a Simit program is typically shorter than a Matlab
program;\nthat it is high performance: a Simit program running sequenti
ally on a CPU\nperforms comparably to hand-optimized simulations; and th
at it is portable:\nSimit programs can be compiled for GPUs with no chan
ge to the program,\ndelivering 4 to 20x speedups over our optimized CPU
code.\n\nBio: Saman P. Amarasinghe is a Professor in the Department of E
lectrical\nEngineering and Computer Science at Massachusetts Institute o
f Technology\nand a member of the Computer Science and Artificial Intell
igence Laboratory\n(CSAIL) where he leads the Commit compiler group. Und
er Saman's guidance,\nthe Commit group has developed the StreamIt, PetaB
ricks, StreamJIT, Halide,\nSimit, and MILK programming languages and com
pilers, DynamoRIO dynamic\ninstrumentation system, Superword level paral
lelism for SIMD vectorization,\nProgram Shepherding to protect programs
against external attacks, the\nOpenTuner extendable autotuner, and the K
endo deterministic execution\nsystem. He was the co-leader of the Raw ar
chitecture project. His research\ninterests are in discovering novel app
roaches to improve the performance of\nmodern computer systems and make
them more secure without unduly increasing\nthe complexity faced by the
end users, application developers, compiler\nwriters, or computer archit
ects. Saman was the founder of Determina\nCorporation and a co-founder o
f Lanka Internet Services Ltd. Saman received\nhis BS in Electrical Engi
neering and Computer Science from Cornell\nUniversity in 1988, and his M
SEE and Ph.D from Stanford University in 1990\nand 1997, respectively.
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20160623T130000
DTEND;TZID=Europe/Paris:20160623T140000
DTSTAMP;TZID=Europe/Paris:20160623T130000
UID:2016-06-23_GallegoArias
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Emilio J. Gallego Arias: Experiments in Certified Digital Audio
Processing
URL:http://parkas.di.ens.fr/seminars.html#2016-06-23_GallegoArias
DESCRIPTION:We will present recent developments in Wagner, a functional\
nprogramming language geared towards real-time digital audio\nprocessing
with formal, machine-checkable semantics.\n\nWagner can be seen as eith
er a very simple synchronous language of a\nfunctional reactive one, usi
ng coeffects for history tracking,\nallowing a natural coding of filter
and digital waveguide\noscillators.\n\nIn order to relate programs with
their mathematical model three main\ncomponents are needed:\n\n1. A Coq
library with some facts about the Discrete Fourier Transform and \n un
itary transforms. The formalization is constructive and heavily relies \
n on the Mathematical Components library.\n\n2. An embedding of Wagner
into Coq, crucially allowing a lightweight \n mechanization style as
we can reuse most of Mathcomp's linear algebra \n libraries. The funct
ional nature of Wagner allows the use of typical PL \n techniques such
as for example logical relations to characterize the \n subset of Wag
ner programs that are “linear processors”.\n\n3. Finally, a call-by-
value abstract machine with a heap provides the \n efficient execution
model. Basic ideas from the focusing literature are \n used to distin
guish “positive” and “negative” types.\n\n We embed the machin
e in Coq using the standard monadic CBV translation \n and we link it
to the semantics in 2) by relating well-formed heaps with \n typing en
vironments.\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20160613T110000
DTEND;TZID=Europe/Paris:20160613T120000
DTSTAMP;TZID=Europe/Paris:20160613T110000
UID:2016-06-13_Talbot
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Pierre Talbot: Spacetime Programming
URL:http://parkas.di.ens.fr/seminars.html#2016-06-13_Talbot
DESCRIPTION:Search heuristics are of utter importance for solving Constr
aint \nSatisfaction Problems (CSP) efficiently. However, the implementer
s will \nstruggle to choose between a full-fledged but low-level constra
int library \nor high-level languages proposing a limited amount of pre-
built heuristics. \nWe introduce Spacetime Programming (STP), a paradigm
based on concurrent \nconstraint programming and synchronous languages,
where both time and space \nare part of the language. The variables are
characterized by a “spacetime”\nproperty describing how their value
s evolve through time and space. We will \npresent preliminary work demo
nstrating how STP, in the context of CSP \nsolving, can be used for writ
ing and composing search strategies.\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20160606T150000
DTEND;TZID=Europe/Paris:20160606T160000
DTSTAMP;TZID=Europe/Paris:20160606T150000
UID:2016-06-06_Sjolund
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Martin Sjölund: Tools and Methods for Analysis, Debugging, and
Performance Improvement of Equation-Based Models
URL:http://parkas.di.ens.fr/seminars.html#2016-06-06_Sjolund
DESCRIPTION:Equation-based object-oriented (EOO) modeling languages such
as Modelica\nprovide a convenient, declarative method for describing mo
dels of\ncyber-physical systems. Because of the ease of use of EOO langu
ages, large\nand complex models can be built with limited effort.\n\nHow
ever, current state-of-the-art tools do not provide the user with enough
\ninformation when errors appear or simulation results are wrong. It is
of\nparamount importance that such tools should give the user enough inf
ormation\nto correct errors or understand where the problems that lead t
o wrong\nsimulation results are located. However, understanding the mode
l translation\nprocess of an EOO compiler is a daunting task that not on
ly requires\nknowledge of the numerical algorithms that the tool execute
s during\nsimulation, but also the complex symbolic transformations bein
g performed.\n\nAs part of this work, methods have been developed and ex
plored where the EOO\ntool, an enhanced Modelica compiler, records the t
ransformations during the\ntranslation process in order to provide bette
r diagnostics, explanations,\nand analysis. This information is used to
generate better error-messages\nduring translation. It is also used to p
rovide better debugging for a\nsimulation that produces unexpected resul
ts or where numerical methods fail.\n\nMeeting deadlines is particularly
important for real-time applications. It\nis usually essential to ident
ify possible bottlenecks and either simplify\nthe model or give hints to
the compiler that enable it to generate faster\ncode. When profiling an
d measuring execution times of parts of the model the\nrecorded informat
ion can also be used to find out why a particular system\nmodel executes
slowly.\n\nCombined with debugging information, it is possible to find
out why this\nsystem of equations is slow to solve, which helps understa
nding what can be\ndone to simplify the model. A tool with a graphical u
ser interface has been\ndeveloped to make debugging and performance prof
iling easier. Both debugging\nand profiling have been combined into a si
ngle view so that performance\nmetrics are mapped to equations, which ar
e mapped to debugging information.\n\nThe algorithmic part of Modelica w
as extended with meta-modeling constructs\n(MetaModelica) for language m
odeling. In this context a quite general\napproach to debugging and comp
ilation from (extended) Modelica to C code was\ndeveloped. That makes it
possible to use the same executable format for\nsimulation executables
as for compiler bootstrapping when the compiler\nwritten in MetaModelica
compiles itself.\n\n_Bio:_ Martin Sjölund is doing a postdoc at Linkö
ping University where he\nfinished his PhD in 2015. The thesis is mostly
focused on debugging\nand profiling of an equation-based object-oriente
d (EOO) language called\nModelica. He has worked on various parts of the
\n[OpenModelica](https://openmodelica.org/) compiler since 2009, both do
ing\nresearch (resulting in the PhD) and development work for the Open
Source\nModelica Consortium (resulting in improved portability, performa
nce,\nscalability, and new features in OpenModelica).\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20160601T140000
DTEND;TZID=Europe/Paris:20160601T150000
DTSTAMP;TZID=Europe/Paris:20160601T140000
UID:2016-06-01_Zinenko
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Oleksandr Zinenko: Polyhedral program transformations via intera
ctive visualization
URL:http://parkas.di.ens.fr/seminars.html#2016-06-01_Zinenko
DESCRIPTION:_Context:_ part of the PhD thesis work of Oleksandr Zinenko.
\n\nThe Polyhedral model is a powerful framework for program\ntransforma
tion, yet it remains complex for direct use, even by\nexperts. We lever
age the inherent geometric nature of the model to\nvisualize programs an
d to support code transformation by directly\nmanipulating these visuali
zations with automatic code generation and\nfeedback on semantics preser
vation. Besides manual transformation, the\nuser of our interactive too
l, Clint, is able to recover, visually\nreplay and adjust an automatical
ly computed optimization using a set\nof syntactic-level directives with
strong semantics. Combining this\nvisualization with existing polyhedr
al tools introduces visual aid for\nschedule and transformation construc
tion. Empirical user studies\ndemonstrated that visual representations
allow to extract and express\nparallelism faster and with more success.
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20160412T103000
DTEND;TZID=Europe/Paris:20160412T120000
DTSTAMP;TZID=Europe/Paris:20160412T103000
UID:2016-04-12_Llopard
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Ivan Llopard: Programming Embedded Manycore: Refinement and Opti
mizing Compilation of a Parallel Action Language for Hierarchical State
Machines
URL:http://parkas.di.ens.fr/seminars.html#2016-04-12_Llopard
DESCRIPTION:Context: presentation of the PhD thesis work of Ivan Llopard
; the\nthesis was prepared at CEA Leti and will be defended on April 26t
h in\nGrenoble.\n\nModeling languages propose convenient abstractions an
d transformations\nto harness the complexity of today's embedded systems
. These\nlanguages are often based on the formalism of Hierarchical Sta
te\nMachines, such as the widely known Statecharts. While they naturall
y\ncapture the concurrency of control systems, they face two important\n
challenges when it comes to modeling data-intensive applications on\nmod
ern parallel architectures: the absence of a unified approach that\nalso
accounts for (data) parallel actions; and the lack of an\neffective opt
imization and code generation flow. We propose a modeling\nlanguage exte
nded with parallel action semantics and indexed state\nmachines suitable
for computationally intensive applications. Together\nwith its formal s
emantics, we present an optimizing compiler aiming\nfor the generation o
f efficient parallel implementations. Following a\nmodel-driven methodol
ogy, the compilation flow has been successfully\napplied to manycore arc
hitectures such as GPGPU platforms.
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20160401T130000
DTEND;TZID=Europe/Paris:20160401T140000
DTSTAMP;TZID=Europe/Paris:20160401T130000
UID:2016-04-01_Bodin
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Bruno Bodin: Performance analysis of dataflow models
URL:http://parkas.di.ens.fr/seminars.html#2016-04-01_Bodin
DESCRIPTION:Synchronous Dataflow graphs, an equivalent of weighted petri
-nets\nintroduced by Lee and Messerschmitt in 1987, is a well-known form
alism\ncommonly used to model data-exchanges between parallel programs.
This\nmodel has been extensively studied in the last two decades because
of\nthe importance of its applications. However, the determination of a
\nmaximal throughput is a difficult question, for which no polynomial\nt
ime algorithm exists up to now. Several authors proved that it\nexists
a schedule which reaches the maximum throughput but with a no\npolynomia
lly bounded size. On the other hand a strictly periodic\nschedule may be
built polynomially, but without any guarantee on the\nthroughput achiev
ed. In this context, we investigate the trade-off\nbetween schedules si
ze and their corresponding\nthroughput. Additionally, the applicability
of these models on SLAM\nalgorithms is explored.
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20160316T170000
DTEND;TZID=Europe/Paris:20160316T180000
DTSTAMP;TZID=Europe/Paris:20160316T170000
UID:2016-03-16_Raymond
LOCATION:salle Henri Cartan; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Pascal Raymond: Analyse de pire temps d'exécution et programmat
ion synchrone
URL:http://parkas.di.ens.fr/seminars.html#2016-03-16_Raymond
DESCRIPTION:[Séminaire du DI](http://www.di.ens.fr/SeminaireGeneral.htm
l.fr#Mercredi_16_mars_2016_17h00_Pasc).\n\nLes systèmes embarqués sont
des dispositifs informatisés dédiés à une tâche \nspécifique, typ
iquement le contrôle/commande d'un processus physique. On en \ntrouve d
ans le domaine des transports (freinage assisté, allumage moteur, \ncom
mande de vol), du contrôle de processus industriel, ou de la production
\nd'énergie. Les termes de systèmes réactifs, systèmes temps-réel
(dur) \ncouvrent à peu près la même réalité.\n\nUne caractéristiqu
e principale de ces systèmes est la criticité : les \ndéfaillances pe
uvent être catastrophiques. Il faut donc s'assurer de la \ncorrection d
e ses systèmes avant leur mises en service.\n\nPour être considéré c
omme correct, un tel système doit essentiellement : - \ncalculer juste
: il réalise bien la fonctionnalité attendue, sans bogue de \nconcept
ion ni erreur à l'exécution ; - calculer (suffisamment) vite : la \nvi
tesse de réaction du système doit être en adéquation avec la dynamiq
ue du \nprocessus physique qu'il contrôle.\n\nL'approche synchrone, for
malisée dans le courant des années 80, s'intéresse \nspécifiquement
aux aspects fonctionnels. Elle propose un cadre idéalisé pour \nla con
ception des systèmes (concurrence déterministe), et fournit les outils
\nnécessaires pour la programmation, la validation, la compilation et
\nl'implantation du logiciel embarqué. L'outil Scade (Esterel technolog
ies) \nest un exemple typique d'un environnement de programmation synchr
one, \nutilisé en production dans l'industrie (commandes de vol Airbus
et bien \nautres).\n\nL'analyse temporelle cherche à vérifier que le t
emps de réaction du système \nimplanté est conforme aux contraintes t
emps-réel de son environnement. Aux \nméthodes dynamiques classiques,
basées sur le test et la mesure, se sont \najoutées à partir des ann
ées 90 des méthodes d'analyse statiques qui \ncherchent à déterminer
des bornes supérieures garanties aux temps de \nréaction. Le problèm
e de base de ces méthodes est l'estimation du pire temps \nd'exécution
d'un code séquentiel donné sur une architecture donnée (Worst \nCase
Execution Time, ou WCET).\n\nCet exposé présente les complémentarit
és des deux domaines, puis aborde plus \nspécifiquement des travaux r
écents qui visent à analyser la sémantique des \nprogrammes synchrone
s pour découvrir des chemins d'exécutions infaisables \nsur le code co
mpilé, et donc, potentiellement, d'affiner les estimations de \npire te
mps d'exécution.
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20160113T170000
DTEND;TZID=Europe/Paris:20160113T180000
DTSTAMP;TZID=Europe/Paris:20160113T170000
UID:2016-01-13_Pagano
LOCATION:salle Henri Cartan; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Bruno Pagano: Scade 6: Conception d'un langage de programmation
synchrone et réalisation de son compilateur pour les systèmes embarqu
és critiques
URL:http://parkas.di.ens.fr/seminars.html#2016-01-13_Pagano
DESCRIPTION:[Séminaire du DI](http://www.di.ens.fr/SeminaireGeneral.htm
l.fr#Mercredi_13_janvier_2016_17h00_B).\n\nDans le contexte des système
s embarqués critiques, l'objectif principal du logiciel n'est pas d'eff
ectuer des calculs extrêmement longs et complexes à partir d'une donn
ée qui lui est fournie initialement, mais de réagir de façon sure et
déterministe aux évènements externes qui lui sont communiqués de man
ière régulière tout au long de son exécution. La réalisation de tel
s logiciels peut se faire en utilisant des langages de programmation dé
diés dont la conception et les techniques de compilation sont un sujet
de recherche actif depuis une trentaine d'années. Les langages de progr
ammation synchrones, comme Esterel ou Lustre, ont prouvé leur utilité
dans la réalisation des systèmes réactifs. Après une introduction au
x principes des langages synchrones, cet exposé présentera à travers
le langage de programmation Scade 6 (dialecte de Lustre) les travaux de
recherche d'Esterel Technologies sur la réalisation et la compilation d
'un langage textuel et graphique. Nous évoquerons les mécanismes parti
culiers à Scade qui ont été introduit ainsi qu'un travail en cours su
r l'utilisation de Scade pour la simulation de systèmes physiques.
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20160113T104500
DTEND;TZID=Europe/Paris:20160113T114500
DTSTAMP;TZID=Europe/Paris:20160113T104500
UID:2016-01-13_Beaugnon
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Ulysse Beaugnon: A Quest for the Optimal Matrix-Matrix Multiplic
ation Code
URL:http://parkas.di.ens.fr/seminars.html#2016-01-13_Beaugnon
DESCRIPTION:Finding a near-optimal implementation of a program on a GPU
is a daunting task. The programmer or the compiler must not only explore
regular code optimizations but also handle the placement of the data in
the memory hierarchy and choose a parallelism scheme. The solution we p
ropose explores a set of possible implementation to find the optimal one
for a given input and GPU model. The problem with this approach is that
the search space has an exponential size. We thus propose a performance
model to trim the search space and drive the search.\n\nThe seminar is
based on the work conducted during an internship at Google.
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20160107T103000
DTEND;TZID=Europe/Paris:20160107T120000
DTSTAMP;TZID=Europe/Paris:20160107T103000
UID:2016-01-07_Guatto
LOCATION:salle Jean Jaurès; 29 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Adrien Guatto: A Synchronous Functional Language with Integer Cl
ocks
URL:http://parkas.di.ens.fr/seminars.html#2016-01-07_Guatto
DESCRIPTION:PhD thesis defense.\n\nThis thesis addresses the design and
implementation of a\nprogramming language for real-time stream processin
g\napplications, such as video decoding. The model of Kahn process\nnetw
orks is a natural fit for this area and has been used\nextensively. In t
his model, a program consists in a set of\nparallel processes communicat
ing through single reader, single\nwriter queues. The strength of the mo
del lies in its determinism.\n\nSynchronous functional languages like Lu
stre are dedicated to\ncritical embedded systems. A Lustre program defin
es a Kahn\nprocess network which is synchronous, that is, which can be\n
executed with finite queues and without deadlocks. This is\nenforced by
a dedicated type system, the clock calculus, which\nestablishes a global
time scale throughout a program. The global\ntime scale is used to defi
ne clocks: per-queue boolean sequences\nindicating, for each time step,
whether a process produces or\nconsumes a token in the queue. This infor
mation is used both for\nenforcing synchrony and for generating finite-s
tate software or\nhardware.\n\nWe propose and study integer clocks, a ge
neralization of boolean\nclocks featuring arbitrarily big natural number
s. Integer clocks\ndescribe the production or consumption of several val
ues from the\nsame queue in the course of a time step. We then rely on i
nteger\nclocks to define the local time scale construction, which may\nh
ide time steps performed by a sub-program from the surrounding\ncontext.
These principles are integrated into a clock calculus\nfor a higher-or
der functional language. We study its properties,\nproving among other t
hings that well-typed programs do not\ndeadlock. We compile typed progra
ms to digital synchronous\ncircuits by adapting the clock-directed code
generation scheme of\nLustre. The typing information controls certain tr
ade-offs\nbetween time and space in the generated circuits.\n\nThe membe
rs of the thesis committee are:\n\n* [Gérard Berry](http://www.college-
de-france.fr/site/gerard-berry),\n Collège de France (Président)\n* [
Mary Sheeran](http://www.cse.chalmers.se/~ms),\n Chalmers University (R
apporteur)\n* [Robert de Simone](http://www-sop.inria.fr/members/Robert.
De_Simone),\n INRIA Nice - Sophia Antipolis (Rapporteur)\n* [Stephen Ed
wards](http://www.cs.columbia.edu/~sedwards),\n Columbia University (Ex
aminateur)\n* [Dan R. Ghica](http://www.cs.bham.ac.uk/~drg),\n Birmingh
am University (Examinateur)\n* [Albert Cohen](https://who.rocq.inria.fr/
Albert.Cohen),\n INRIA Rocquencourt (Directeur de thèse)\n* [Marc Pouz
et](http://www.di.ens.fr/~pouzet),\n ENS et Université Paris 6 (Codire
cteur de thèse)\n* [Louis Mandel](https://www.lri.fr/~mandel),\n IBM R
esearch (Encadrant)\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20150929T110000
DTEND;TZID=Europe/Paris:20150929T120000
DTSTAMP;TZID=Europe/Paris:20150929T110000
UID:2015-09-29_Baudard
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Guillaume Baudard: Loosely Time-Triggered Architectures: Improve
ments and Comparisons
URL:http://parkas.di.ens.fr/seminars.html#2015-09-29_Baudard
DESCRIPTION:Loosely Time-Triggered Architectures (LTTAs) are a proposal
for\nconstructing distributed embedded control systems. They build on th
e\nquasi-periodic architecture, where computing units execute ‘almost\
nperiodically’, by adding a thin layer of middleware that facilitates\
nthe implementation of synchronous applications.\n\nWe show how the depl
oyment of a synchronous application on a\nquasi-periodic architecture ca
n be modeled using a synchronous\nformalism. Then we detail two protocol
s, Back-Pressure LTTA,\nreminiscent of elastic circuits, and Time-Based
LTTA, based on\nwaiting. Compared to previous work, we present controlle
r models that\ncan be compiled for execution and a new version of the Ti
me-Based\nprotocol that neither requires broadcast communication nor imp
oses\nglobal synchronization. We also compare the LTTA approach with\nar
chitectures based on clock synchronization.\n\nBased on an [EMSOFT 2015]
(http://www.emsoft.org) presentation.
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20150925T151700
DTEND;TZID=Europe/Paris:20150925T173000
DTSTAMP;TZID=Europe/Paris:20150925T151700
UID:2015-09-25_Baghdadi
LOCATION:salle Cavaillès; 45 rue d'Ulm; ENS; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Riyadh Baghadi: Improving Tiling, Reducing Compilation Time, and
Extending the Scope of Polyhedral Compilation
URL:http://parkas.di.ens.fr/seminars.html#2015-09-25_Baghdadi
DESCRIPTION:PhD thesis defense.\n\nWe are interested in enabling compile
rs to automatically optimize and\nparallelize code. The polyhedral frame
work is showing promising\nresults in this area. In this thesis, we addr
ess three limitations in\nthe polyhedral framework and we present a prac
tical solution to each\none of these limitations. First, we address the
problem of tiling code\nthat has false dependences. Compilers cannot til
e such code without\nprivatization or expansion. To avoid this problem,
we propose a new\nrelaxed permutability criterion that allows a compiler
to ignore false\ndependences between iteration-private live ranges and
thus enables the\ncompiler to tile the loops without privatization or ex
pansion. Second,\nwe address the problem of compilation time. To reduce
the long\ncompilation time of large programs, we introduce a technique t
hat we\ncall statement clustering and in which the original representati
on of\nthe program is transformed into a new program representation (whe
re\neach group of statements is represented as a macro-statement). The n
ew\nrepresentation of the program can be optimized faster than the\norig
inal representation. The third limitation is related to the\nability of
compilers to automatically parallelize irregular code and\nto generate e
fficient code when information is missing to the\ncompiler. To address t
his limitation, we introduce PENCIL, an\nintermediate language for DSL c
ompilers and for accelerator\nprogramming. PENCIL is a subset of the C99
language carefully designed\nto capture static properties essential to
enable more precise data\ndependence analysis. It provides also a set of
language constructs\nthat enable parallelizing compilers to generate mo
re efficient\ncode. The use of PENCIL would enable the compiler to gener
ate\noptimized code that is quite difficult to generate otherwise.\n\nTh
e members of the thesis committee are:\n\n* Stef Graillat, Professor, Un
iversity Pierre et Marie Curie (President)\n* Cédric Bastoul, Professor
, University of Strasbourg (Rapporteur)\n* Paul H J Kelly, Professor, Im
perial College London (Rapporteur)\n* J. Ramanujam, Professor, Louisiana
State University (Examinateur)\n* Albert Cohen, Senior Research Scienti
st, INRIA, France (Directeur de thèse)\n* Sven Verdoolaege, Associate R
esearcher, Polly Labs and KU Leuven (Encadrant)
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20150907T163000
DTEND;TZID=Europe/Paris:20150907T173000
DTSTAMP;TZID=Europe/Paris:20150907T163000
UID:2015-09-07_vonHanxleden
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Reinhard von Hanxleden: Code-Generation for Sequential Construct
iveness
URL:http://parkas.di.ens.fr/seminars.html#2015-09-07_vonHanxleden
DESCRIPTION:The Sequentially Constructive Language (SCL) is a minimal sy
nchronous\nlanguage that captures the essence of the Sequentially Constr
uctive model of\ncomputation (SC MoC), a recently proposed extension of
the classical\nsynchronous model of computation. The SC MoC uses sequent
ial scheduling\ninformation to increase the class of constructive (legal
) synchronous\nprograms. This should facilitate the adoption of synchron
ous programming by\nusers familiar with sequential programming in C or J
ava, thus simplifying\nthe design of concurrent reactive/embedded system
s with deterministic\nbehavior. In this presentation, I focus on how to
compile SCL down to\ndata-flow equations, which ultimately can be synth
esized to hardware or\nexecuted in software.\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20150904T130000
DTEND;TZID=Europe/Paris:20150904T140000
DTSTAMP;TZID=Europe/Paris:20150904T130000
UID:2015-09-04_Andreani
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Virgile Andreani: Distributed Simulation of Hybrid Systems
URL:http://parkas.di.ens.fr/seminars.html#2015-09-04_Andreani
DESCRIPTION:The task of modelling and simulating a complex physical syst
em is often a\nchallenge to engineers and researchers since the applicat
ions of interest\nroutinely involve several time-scales, multiple sub-sy
stems strongly or\nloosely coupled, and components whose behaviours are
very distinct. The\nsimulation of such systems is done in most software
by a single numeric\nsolver, which is often an inelegant solution, comp
ared to harvesting the\nresults of a herd of specialised solvers, certai
nly more efficient in their\nrespective tasks than a general purpose sol
ver. This talk will explore a\nfew leads to help shepherd several solve
rs on the same simulation. Emphasis\nwill be placed on the role of 0th-o
rder value holders in the computation,\nand on the compilation of a dist
ributed simulation.\n\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20150703T150000
DTEND;TZID=Europe/Paris:20150703T163000
DTSTAMP;TZID=Europe/Paris:20150703T150000
UID:2015-07-03_Gramoli
LOCATION:Amphi Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Vincent Gramoli: Contention: can theory meet practice?
URL:http://parkas.di.ens.fr/seminars.html#2015-07-03_Gramoli
DESCRIPTION:With the growing core count on chip multiprocessors, content
ion has\nbecome an important factor of performance degradation. Yet, lit
tle\nefforts have been devoted to understanding how it affects performan
ce of\ndata structures. Some were devoted to introducing different defin
itions\nof contention whereas others were devoted to the implementation
of\nefficient data structures with terrible complexity. In the first par
t of\nthis talk, I motivate the mismatch between some complexity metrics
and\nperformance measurements by presenting a technique to reduce conte
ntion\nin logarithmic data structures. In the second part of this talk,
I show\nthat definitions of contention can be considered equivalent in s
ome\ncontext and illustrate this with an efficient concurrent linked lis
t.
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20150626T103000
DTEND;TZID=Europe/Paris:20150626T120000
DTSTAMP;TZID=Europe/Paris:20150626T103000
UID:2015-06-26_Sarkar
LOCATION:salle Jean Jaurès; 29 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Vivek Sarkar: Structured Parallel Programming Primitives and the
ir use in Compilers, Runtimes and Debuggers for Parallel Systems
URL:http://parkas.di.ens.fr/seminars.html#2015-06-26_Sarkar
DESCRIPTION:[Séminaire du DI](http://www.di.ens.fr/SeminaireGeneral.htm
l.fr#Vendredi_26_juin_2015_10h30_Vive).\n\nIn this talk, we claim that s
tructured parallel programming greatly\nsimplifies the task of writing c
orrect and efficient parallel programs,\nwhile also capturing the flexib
ility of expressing asynchronous\ncomputations. We support this claim b
y introducing a family of structured\nparallel programming primitives de
veloped in the\n[Habanero Extreme Scale Software Research project](http:
//habanero.rice.edu)\nat Rice University, and discussing semantic guaran
tees (e.g., deadlock freedom,\ndata race freedom, determinism, serial el
ision) for different subsets of\nparallel programs that can be construct
ed with these primitives. We will then\nsummarize results for\n[compile
r optimizations](http://dl.acm.org/citation.cfm?id=2450138),\n[runtime s
ystems](http://link.springer.com/chapter/10.1007%2F978-3-662-44202-9_25)
,\n[repair](http://dl.acm.org/citation.cfm?id=2254127) and\n[datarace de
tection](http://dl.acm.org/citation.cfm?id=2594335) for these\nsubsets.
If time permits, we will briefly discuss future directions for\ndata-dri
ven repair and synthesis of parallel programs in the new\n[Pliny project
](http://pliny.rice.edu).\n\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20150611T130000
DTEND;TZID=Europe/Paris:20150611T140000
DTSTAMP;TZID=Europe/Paris:20150611T130000
UID:2015-06-11_Zhang
LOCATION:salle R; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Zhen Zhang: Time Mixed-Critical, Multi-Core Embedded Systems Des
ign, Modeling and Implementation
URL:http://parkas.di.ens.fr/seminars.html#2015-06-11_Zhang
DESCRIPTION:The cost efficient integration of different applications wit
h different\nlevels of safety and security on a single computing platfor
m has become a\nmajor industrial challenge. Such a platform would prefer
ably be an\noff-the-shelf shared memory multicore processor. The perform
ance\nrequirements of individual applications and components also push f
or their\nparallelization. Focusing on the safety-critical domain, we wo
rk on\nextending to multicore processors with the established modular de
sign and\nimplementation methods used for synchronous applications. In t
his talk, I\nwill describe our approach to the modular composition of sy
nchronous\ncomponents with hard real-time constraints. Preserving time-p
redictability\nis the most difficult barrier to the adoption of multicor
es in\nsafety-critical systems. Our solution is compatible with off-the-
shelf\nembedded shared-memory multiprocessors, introducing minor modific
ations to\nthe syntax and semantics of Heptagon, a synchronous programmi
ng dialect of\nLustre. It is demonstrated on an industrial use case from
Alstom Transport,\ninvolving a time-triggered software stack designed o
n top of Linux and\nbare-metal components running on a Xilinx Zynq multi
core platform. Our\nsolution involves an original methodology for the de
sign of\n"mixed-time-critical" applications. The safety levels and corre
ctness by\nconstruction of synchronous designs is preserved. Performance
and time\npredictability can be traded off against each other. This inv
olves the\npartitioning of an application into modes of different time c
riticality, and\nis supported by time-critical backup scenarios when bes
t-effort components\nmiss their deadline. This work takes place in the c
ontext of the EMC2\nproject.\n\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20150601T130000
DTEND;TZID=Europe/Paris:20150601T140000
DTSTAMP;TZID=Europe/Paris:20150601T130000
UID:2015-06-01_Baghdadi
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Riyadh Baghdadi: PENCIL: a Platform-Neutral Compute Intermediate
Language for DSL Compilers and for Accelerator Programming
URL:http://parkas.di.ens.fr/seminars.html#2015-06-01_Baghdadi
DESCRIPTION:Programming accelerators such as GPUs with low-level APIs an
d languages like\nOpenCL and CUDA is difficult, error prone, and not per
formance-portable.\nAutomatic parallelization and domain specific langua
ges (DSLs) have been\nproposed to hide this complexity and to regain som
e performance portability.\nIn this presentation, I will present PENCIL
(Platform-Neutral Compute\nIntermediate Language) and present some detai
ls about how it is compiled.\nPENCIL is a rigorously defined subset of G
NU C99 with specific programming\nrules and few extensions. Adherence to
this subset and the use of these\nextensions enable compilers to exploi
t parallelism and to better optimize\ncode when targeting accelerators.
We intend PENCIL both as a portable\nlanguage to facilitate accelerator
programming, and as an intermediate\nlanguage for DSL compilers. We vali
date the potential of PENCIL on a\nstate-of-the-art polyhedral compiler,
extending the applicability of the\ncompiler to dynamic, data-dependent
control flow and non-affine array\naccesses. We use the polyhedral comp
iler to generate highly optimized\nOpenCL code for a set of standard ben
chmark suites (Rodinia and SHOC),\nimage processing kernels, and for two
DSL compilers: a linear algebra (BLAS)\nDSL compiler and a DSL for sign
al processing radar applications (SpearDE).\nTo assess performance porta
bility, we present experimental results on many\nGPU platforms: AMD Rade
on HD 5670, Nvidia GTX470, and ARM Mali-T604 GPU.\n\nBased on a [PACT 20
15](http://www.pactconf.org) presentation.
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20150427T130000
DTEND;TZID=Europe/Paris:20150427T140000
DTSTAMP;TZID=Europe/Paris:20150427T130000
UID:2015-04-27_KroahHartman
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Greg Kroah-Hartman: An Introduction to Greybus
URL:http://parkas.di.ens.fr/seminars.html#2015-04-27_KroahHartman
DESCRIPTION:Greybus is the name for a new application layer protocol on
top of Unipro\nthat controls the Ara Phone from Google. This protocol t
urns a phone into a\nmodular device, allowing any part of the system to
be hotplugged while the\nphone is running. This talk will describe what
this protocol is, why it was\ndesigned, and give the basics for how it
works. It will discuss how this is\nimplemented in the Linux kernel, an
d how it easily bridges existing hardware\nlike USB, I2C, GPIO and other
s with little to no changes needed to existing\nkernel drivers.\n\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20150413T130000
DTEND;TZID=Europe/Paris:20150413T140000
DTSTAMP;TZID=Europe/Paris:20150413T130000
UID:2015-04-13_MinhLe
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Nhat Minh Lê: Kahn process networks in the world of task parall
elism
URL:http://parkas.di.ens.fr/seminars.html#2015-04-13_MinhLe
DESCRIPTION:This talk presents libkpn, a high-performance runtime system
for task\nparallel programming, based on Kahn process networks (KPNs).
Away from the\nusual perception of KPNs as a high-level programming mode
l compiled into\ngeneral-purpose languages, we explore how KPNs can be u
sed directly as\nconcurrency specifications to guide dynamic scheduling
in a runtime system.\nThrough a comparison with existing models, we expl
ain how features of KPNs\ncan be taken advantage of to allow more logica
l parallelism to be expressed,\nand to create an efficient implementatio
n.\n\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20150407T130000
DTEND;TZID=Europe/Paris:20150407T140000
DTSTAMP;TZID=Europe/Paris:20150407T130000
UID:2015-04-07_Bondhugula
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Uday Bondhugula: High-performance compilation through Domain-Spe
cific Languages: the case of Image Processing Pipelines
URL:http://parkas.di.ens.fr/seminars.html#2015-04-07_Bondhugula
DESCRIPTION:This talk addresses the well-known challenge involved in sim
ultaneously\ndelivering high productivity and high parallel performance
on modern\nmulticore architectures—through the development of domain-s
pecific languages\n(DSLs) and their optimizing code generators. It prese
nts the domain of Image\nProcessing Pipelines as the motivating case by
presenting PolyMage, our DSL\nand its code generator for automatic and e
ffective optimization of image\nprocessing pipelines. PolyMage takes an
image processing pipeline expressed\nin a high-level language (embedded
in Python) and generates an optimized\nC/C++ implementation of the pipel
ine. We show how certain techniques\nincluding those based on the polyhe
dral compiler framework need to be\nspecialized in order to provide sign
ificant improvements in parallel\nperformance over existing approaches i
ncluding manual, library-based, and\nthat of another state-of-the-art DS
L (Halide). More information at\nhttp://mcl.csa.iisc.ernet.in/polymage.h
tml. Experimental results on a modern\nmulticore system and a short demo
will also be presented.\n\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20150324T130000
DTEND;TZID=Europe/Paris:20150324T140000
DTSTAMP;TZID=Europe/Paris:20150324T130000
UID:2015-03-24_Mendler
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Michael Mendler: Constructive Semantics of Instantaneous Reactio
ns
URL:http://parkas.di.ens.fr/seminars.html#2015-03-24_Mendler
DESCRIPTION:The synchronous model of programming, which emerged in the 1
980s and has led\nto the development of well-known languages such as Sta
techarts, Esterel,\nSignal, and Lustre, has made the programming of conc
urrent systems with\ndeterministic and bounded reaction a routine exerci
se. The synchronous\napproach draws its success from the fact that it i
s founded on a simple and\nwell-understood mathematical model of computa
tion, the Mealy automaton.\nHowever, the validity of this model is not f
or free. It depends on the\nSynchrony Hypothesis according to which a sy
stem is invariably faster than\nits environment. Yet, this raises a tang
led compositionality problem. Since\na node is in the environment of eve
ry other node, it follows that each node\nmust be faster than every othe
r and hence faster than itself!\n\nThis talk presents some results towar
ds solving this paradox, refining the\nclassical Mealy model by construc
tive notions of input-output causality.\nSpecifically, we propose a game
-theoretic interpretation of the constructive\nsemantics of step respons
es for synchronous languages, providing a coherent\nsemantic framework e
ncompassing both non-deterministic Statecharts (as per\nPnueli & Shalev)
and deterministic Esterel. In particular, it is shown that\nEsterel ari
ses from a finiteness condition on strategies whereas Statecharts\npermi
ts infinite games. Beyond giving a novel and unifying account of these\n
concrete languages the talk sketches a general theory for obtaining\ndif
ferent notions of constructive responses in terms of winning conditions\
nfor finite and infinite games and their characterisation as maximal\npo
st-fixed points of functions in directed complete lattices of intensiona
l\ntruth-values.\n\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20150309T140000
DTEND;TZID=Europe/Paris:20150309T153000
DTSTAMP;TZID=Europe/Paris:20150309T140000
UID:2015-03-09_Adve
LOCATION:salle U/V; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Vikram Adve: Automated Bug Diagnosis and Virtual Instruction Set
Computing
URL:http://parkas.di.ens.fr/seminars.html#2015-03-09_Adve
DESCRIPTION:The presentation has two parts:\n\n PART 1: AUT
OMATED BUG DIAGNOSIS\n PART 2: VIRTUAL INSTRUCTION SET COMP
UTING\n\nI will present our work on two ongoing projects: (1) automated\
ndiagnosis of software failures, and (2) the benefits of using rich\nvir
tual instruction sets as a persistent representation of _all_\nsoftware.
If time permits, I will discuss a mythical connection\nbetween the two
projects.\n\nIn the first part of the talk, I will describe new insight
s into\nanalyzing the root causes of software failures automatically. W
e use\ndynamically observed likely invariants to identify candidate loca
tions\nfor the root cause of a failure, and then use novel static and dy
namic\nanalyses to filter out false positives and to extract valuable\ni
nformation relevant to understanding the failure. Experimental\nresults
show that we are able to narrow down the locations of root\ncauses to j
ust a few (e.g., 2-10) program locations, even in large\nprograms, for n
early all bugs we have tested. We are now exploring how\nto automate th
e process fully using dynamic symbolic execution, and how\nto apply thes
e fault isolation techniques for diagnosis and triaging of\nsoftware fai
lures in production software.\n\nNext, I will discuss a project on Virtu
al Instruction Set Computing\n(VISC). Despite extensive advances in mana
ged run-time systems and\ndynamic compilation, high performance applicat
ions and security\nsensitive systems software are almost universally com
piled and shipped as native machine code. In the VISC project, we are e
xploring the\nsecurity, reliability, and performance implications of shi
pping *all*\nsuch software in virtual instruction set form. We use the
LLVM bitcode\nlanguage as the shipping representation to enable advanced
"lifelong"\nprogram analysis and transformation for such programs. We
have shown\nthat shipping operating systems in LLVM form enables powerfu
l security\nguarantees to be enforced using compiler techniques. We are
now\nexploring how the approach could be used to improve programmabilit
y and\nportability for heterogeneous parallel systems, and to enable nov
el\nperformance optimization techniques.
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20141217T100000
DTEND;TZID=Europe/Paris:20141217T110000
DTSTAMP;TZID=Europe/Paris:20141217T100000
UID:2014-12-17_Janin
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:David Janin: Flux média tuilés polymorphes: une expérimentati
on en Haskell
URL:http://parkas.di.ens.fr/seminars.html#2014-12-17_Janin
DESCRIPTION:De nombreux outils sont aujourd'hui disponibles pour l'analy
se et la\nproduction temps réel de flux média temporisés : sons,
vidéo, animations,\netc. Néanmoins, la coordination de ces outils, la
synchronisation des flux\nqu'ils analysent et produisent, sur des éche
lles de temps de valeurs et même\nde nature différentes, reste une aff
aire délicate.\n\nLe modèle des Tiled Polymorphic Temporal Media (ou T
PTM), qui combine en un\nmême formalisme le contenu media de ces flux e
t leurs marqueurs de\nsynchronisations, vise à remédier à cela. Dans
le modèle, le produit de deux\nflux ainsi enrichi, paramétré par ces
marqueurs de synchronisations, est\ntout à la fois séquentiel et paral
lèle : c’est un produit tuilé.\n\nEn théorie, la sémantique de ces
flux tuilés peut être décrite dans la\nthéorie des monoïdes invers
ifs. En pratique, nous avons réalisé, en Haskell,\nla première implé
mentation réellement polymorphe et inversive de ces Tiled\nPolymorphic
Temporal Media. Notre implémentation permet en outre, via le\nmécanism
e d’évaluation paresseuse d’Haskell, de distinguer simplement la\ns
yntaxe de ces flux – un système d’équations tuilées – de leur s
émantique\nopérationnelle – la résolution de ce système à la vol
ée.\n\nNous montrerons aussi comment nos constructions se généralisen
t simplement\naux tuiles infinies.\n\nCe travail a été partiellement r
éalisé en collaboration avec Paul Hudak\n(Yale) et Théis Bazin (Stagi
aire, ENS Cachan).
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20140630T103000
DTEND;TZID=Europe/Paris:20140630T113000
DTSTAMP;TZID=Europe/Paris:20140630T103000
UID:2014-06-30_Tinelli
LOCATION:salle Jules Ferry; 29 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Cesare Tinelli: SMT-based Unbounded Model Checking with IC3 and
Approximate Quantifier Elimination
URL:http://parkas.di.ens.fr/seminars.html#2014-06-30_Tinelli
DESCRIPTION:The IC3 procedure by A. Bradley is a recent model checking p
rocedure for proving safety properties of finite-state systems that has
shown to be quite effective in practice. This talk presents an SMT-based
version of IC3 that works with both finite- and infinite-state systems.
A distinguishing feature of our approach is the use of approximate quan
tifier elimination to generalize counterexamples. We provide experimenta
l evidence that for linear integer arithmetic our method is superior in
practice to full-blown quantifier elimination, and that our IC3 implemen
tation is competitive with a state-of-the-art k-induction model checker
for infinite-state systems. Our experiments also show that IC3 and k-ind
uction have complementary strengths and so can be combined advantageousl
y in a multi-engine parallel checker.
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20140623T100000
DTEND;TZID=Europe/Paris:20140623T110000
DTSTAMP;TZID=Europe/Paris:20140623T100000
UID:2014-06-23_Tinelli
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Cesare Tinelli: SMT-based Model Checking
URL:http://parkas.di.ens.fr/seminars.html#2014-06-23_Tinelli
DESCRIPTION:The field of model checking owes much of its great success a
nd impact to the use of symbolic techniques to reason efficiently about
functional properties of hardware or software systems. Traditionally, th
ese techniques have relied on propositional encodings of transition syst
ems and on propositional reasoning engines such as binary decision diagr
ams and SAT solvers. More recently, a number of these techniques have be
en adapted, and new ones have been devised, based instead on encodings i
nto fragments of first-order logic supported by Satisfiability Modulo Th
eories (SMT) solvers. These are highly efficient solvers specialized on
checking the satisfiability of formulas in certain logical theories such
as the theory of linear arithmetic, bit-vectors, arrays, algebraic data
types, and so on.\nSMT-based model checking methods blur the line betwe
en traditional (propositional) model checking and traditional (first or
higher order) deductive verification. More crucially, they combine the b
est features of both by offering the scalability and scope of deductive
verification while maintaining comparable levels of automations as propo
sitional model checking.\nThis talk will briefly introduce SMT and then
give an overview of SMT-based model checking, focusing on a number of no
table approaches and techniques.
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20140526T103000
DTEND;TZID=Europe/Paris:20140526T120000
DTSTAMP;TZID=Europe/Paris:20140526T103000
UID:2014-05-26_Pessaux
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:François Pessaux: The FoCaLiZe language: mixing program and pro
ofs
URL:http://parkas.di.ens.fr/seminars.html#2014-05-26_Pessaux
DESCRIPTION:FoCaLiZe is a programming language allowing to state in a sa
me framework\nalgorithms (programming aspects), properties (logical aspe
cts) that these\nalgorithms must satisfy and proofs these latter hold. I
t provides high-level\nconstructs to ease development structuring and re
use (modularity,\ninheritance, late-binding, parameterization) and a pro
of language allowing\nto write proofs in a hierarchical way, using a nat
ural deduction style, which\nrely on the Zenon automated theorem prover
to discharge goals ... and the\nburden of the user. The core programming
language is a pure functional\nlanguage while properties are stated a f
irst-order logic formulae.\nA FoCaLiZe development is compiled in two ta
rget languages: one OCaml source\ncode leading to an executable (or obje
ct file) and one Coq source code\ncontaining the complete model of the d
evelopment (i.e. definitions, properties\nand proofs) that will be ultim
ately checked by Coq as assessment. A crucial\ncare in this process is t
o avoid any error from the target languages being\nreturned to the user:
a program accepted by the FoCaLiZe compiler must be\naccepted by both O
Caml and Coq. To increase confidence in "what is ran is\nwhat is proved"
despite two target languages, the compiler has to use a\ncode generatio
n model identical and traceable for both of them.\n\nIn this presentatio
n we will introduce the motivations, design and\nfeatures choices that i
mpacted the language semantics. The presentation\nof the language featur
es and the development style will also be addressed\non the basis of exa
mples, trying to illustrate advantages (and disavantages)\nof such a sys
tem compared to other existing formal proofs systems.\n\n[Slides](slides
/2014-05-26_Pessaux.pdf)
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20140429T103000
DTEND;TZID=Europe/Paris:20140429T120000
DTSTAMP;TZID=Europe/Paris:20140429T103000
UID:2014-04-29_Schneider
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Sigurd Schneider: Translating In and Out of a Functional Interme
diate Language
URL:http://parkas.di.ens.fr/seminars.html#2014-04-29_Schneider
DESCRIPTION:A functional intermediate language is a simple and effective
\nformalization of static single assignment (SSA) for the purpose of\nve
rified compilation of an imperative language. Two translations are of\np
articular importance:\nTranslating from the imperative source language (
e.g. C) to the\nfunctional language, and translating from the functional
intermediate\nlanguage to an imperative target language (e.g. assembly)
.\n\nThis talk discusses the above translations in the context of the\ni
ntermediate language IL.\nIL comes with an imperative and a functional i
nterpretation.\nIL/I (imperative interpretation) is a register transfer
language close\nto assembly.\nIL/F (functional interpretation) is a firs
t-order functional language\nwith a tail-call restriction.\nWe devise th
e decidable notion of coherence to identify programs on\nwhich the seman
tics of IL/I and IL/F coincide.\nTranslations between the interpretation
s are obtained from\nequivalence-preserving translations to the coherent
fragment.\nThe translation from IL/I to IL/F corresponds to SSA constru
ction.\nThe translation from IL/F to IL/I corresponds to SSA deconstruct
ion and\ninvolves register assignment.\n\nThe translations are implement
ed and proven correct using the proof\nassistant Coq. Extraction yields
translation-validated implementations\nof SSA construction and deconstru
ction.
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20140418T103000
DTEND;TZID=Europe/Paris:20140418T120000
DTSTAMP;TZID=Europe/Paris:20140418T103000
UID:2014-04-18_Ding
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Chen Ding: Program Interaction in Shared Cache: Theory and Appli
cations
URL:http://parkas.di.ens.fr/seminars.html#2014-04-18_Ding
DESCRIPTION:On modern multicore systems, the interaction between co-run
programs\nlargely depends on cache sharing, and cache sharing depends on
the\nlocality, i.e. the active data usage, in co-run programs. This tal
k\nintroduces a newly developed locality theory based on a concept calle
d\nthe footprint. The theory shows the composability of footprint and th
e\nconversion between footprint and other locality metrics. It enables\n
accurate characterization and analysis of the dynamics of cache sharing.
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20140415T103000
DTEND;TZID=Europe/Paris:20140415T120000
DTSTAMP;TZID=Europe/Paris:20140415T103000
UID:2014-04-15_KrishnaRamanathan
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Murali Krishna Ramanathan: Multithreaded Test Synthesis for Dead
lock Detection
URL:http://parkas.di.ens.fr/seminars.html#2014-04-15_KrishnaRamanathan
DESCRIPTION:Designing and implementing thread-safe multithreaded librari
es can be a\ndaunting task as developers of these libraries need to ensu
re that their\nimplementations are free from concurrency bugs including
deadlocks. The\nusual practice involves employing software testing and/o
r dynamic\nanalysis to detect deadlocks. Their effectiveness is dependen
t on\nwell-designed multithreaded test cases. Unsurprisingly, developing
\nmultithreaded tests is easily an order of magnitude harder than\ndevel
oping single threaded tests for obvious reasons.\n\nIn this talk, we wil
l address the problem of automatically synthesizing\nmultithreaded tests
that can induce deadlocks. The key insight to our\napproach is that a s
ubset of the properties observed when a deadlock\nmanifests in a concurr
ent execution can also be observed in a single\nthreaded execution. We d
esign a novel, automatic, scalable and directed\napproach that identifie
s these properties and synthesizes a\nmultithreaded test that realizes t
hese properties simultaneously\nrevealing a potential deadlock. The inpu
t to our approach is only the\nlibrary implementation under consideratio
n and the output is a set of\ndeadlock revealing multithreaded tests. We
will present the results of\nour analysis on synthesizing multithreaded
tests for Java libraries. We\nfind 35 real deadlocks in thread safe cla
sses in COLT, a popular high\nperformance scientific computing library.
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20140331T103000
DTEND;TZID=Europe/Paris:20140331T120000
DTSTAMP;TZID=Europe/Paris:20140331T103000
UID:2014-03-31_Oz
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Işıl Öz: Portable and Predictable Performance of Task-Based P
arallel Applications
URL:http://parkas.di.ens.fr/seminars.html#2014-03-31_Oz
DESCRIPTION:Multicore systems yield high performance by the execution of
multiple concurrent software processes in the system in a power and are
a efficient way. While multicore systems are promising architectures for
higher performance, the soft error reliability of these systems becomes
a major concern due to smaller transistor sizes and low power operating
modes.\n\nMy talk will include work during my Phd and recent work, rela
ted to reliability and performance analysis of multicore systems.\n\nI a
m currently working on ARTEMIS PaPP project. PaPP (Portable and Predicta
ble Performance on Heterogeneous Embedded Manycores) aims to achieve pre
dictable performance portability of software running on different parall
el platforms. We focus on performance analysis modelling for task-based
parallel applications within multicore systems. Our modelling targets to
find out minimal resources which satisfy performance requirements of an
application and to develop task scheduling strategies as an input to ru
n-time for better resource management and performance optimization.\n\nI
n my PhD study, I was working on reliability analysis of multicore syste
ms. I propose Thread Vulnerability Factor metric, to quantify vulnerabil
ity of thread and to qualify the relative vulnerability of parallel appl
ications to soft errors, and utilize the metric for performance-vulnerab
ility analysis of parallel programs, reliability-aware core partitioning
schemes for multicore architectures, and critical thread identification
for redundant execution in a partial fault tolerance method.
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20140324T103000
DTEND;TZID=Europe/Paris:20140324T120000
DTSTAMP;TZID=Europe/Paris:20140324T103000
UID:2014-03-24_Balabonski
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Thibaut Balabonski: Data-race freedom by typing in Mezzo
URL:http://parkas.di.ens.fr/seminars.html#2014-03-24_Balabonski
DESCRIPTION:Mezzo is a typed programming language in the ML family whose
static\ndiscipline controls aliasing and ownership. This rules out cert
ain\nmistakes, including representation exposure and data races, and ope
ns up\nnew opportunities, such as gradual initialization or (more genera
lly,\nand somewhat speculatively) the definition and enforcement of obje
ct\nprotocols.\n\nIn this talk, I will explain the basic design of Mezzo
on examples, and\nshow how its type system gives a simple way of tracki
ng ownership of\nfragments of shared memory between concurrent threads.
Beyond the usual\nclaim that "well-typed programs do not go wrong", we g
uarantee that\nwell-typed Mezzo programs have no data-races.
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20140213T103000
DTEND;TZID=Europe/Paris:20140213T120000
DTSTAMP;TZID=Europe/Paris:20140213T103000
UID:2014-02-13_Bhati
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Khurram Bhati: Predictable Execution of Task-Based Applications
on Multicore Systems
URL:http://parkas.di.ens.fr/seminars.html#2014-02-13_Bhati
DESCRIPTION:The presentation will have two parts. In the first part, we
will present\nan on-going research project to provide a run-time system
with\n"guidelines", using task graph properties, and a static analysis p
hase\nto prioritize certain tasks of a given application over the others
. The\norder in which tasks of an application task graph are considered
has a\nsignificant influence on the resulting schedule length. Gauging t
he\nimportance of the tasks with a priority scheme is therefore a\nfunda
mental part of scheduling schemes. We have used the concept of\npaths an
d path lengths to gauge the importance of tasks in an offline\nstatic an
alysis phase and provide guidelines to the run-time system for\npriority
assignment.\n\nIn the second part of my presentation, we will present e
arlier research\nresults that focuses on power/energy efficient real-tim
e scheduling. We\nwill discuss at least one such technique to elaborate
the concept.
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20131004T103000
DTEND;TZID=Europe/Paris:20131004T120000
DTSTAMP;TZID=Europe/Paris:20131004T103000
UID:2013-10-04_LeeHung
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Prof. Jenq Kuen Lee and Dr. Ming-Yu Hung: Probabilistic Pointer
analysis in SSA Form and its Applications
URL:http://parkas.di.ens.fr/seminars.html#2013-10-04_LeeHung
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20130919T140000
DTEND;TZID=Europe/Paris:20130919T150000
DTSTAMP;TZID=Europe/Paris:20130919T140000
UID:2013-09-19_Bhaskaracharya
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Somashekaracharya Bhaskaracharya: PolyGLoT - A Polyhedral Loop T
ransformation Framework for a Graphical Dataflow Language
URL:http://parkas.di.ens.fr/seminars.html#2013-09-19_Bhaskaracharya
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20130719T133000
DTEND;TZID=Europe/Paris:20130719T143000
DTSTAMP;TZID=Europe/Paris:20130719T133000
UID:2013-07-19_Rahli
LOCATION:salle R; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Vincent Rahli: EventML
URL:http://parkas.di.ens.fr/seminars.html#2013-07-19_Rahli
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20130613T111500
DTEND;TZID=Europe/Paris:20130613T121500
DTSTAMP;TZID=Europe/Paris:20130613T111500
UID:2013-06-13_Sheeran
LOCATION:Salle Dussane; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Mary Sheeran: Obsidian: generating GPU kernels from Haskell
URL:http://parkas.di.ens.fr/seminars.html#2013-06-13_Sheeran
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20130610T100000
DTEND;TZID=Europe/Paris:20130610T110000
DTSTAMP;TZID=Europe/Paris:20130610T100000
UID:2013-06-10_Govindarajan
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:R. Govindarajan: Compiling for Heterogeneous Multi-Core Architec
tures with GPUs
URL:http://parkas.di.ens.fr/seminars.html#2013-06-10_Govindarajan
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20130603T100000
DTEND;TZID=Europe/Paris:20130603T110000
DTSTAMP;TZID=Europe/Paris:20130603T100000
UID:2013-06-03_Hughes
LOCATION:salle U/V; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:John Hughes: Property-based testing with QuickCheck
URL:http://parkas.di.ens.fr/seminars.html#2013-06-03_Hughes
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20130527T103000
DTEND;TZID=Europe/Paris:20130527T113000
DTSTAMP;TZID=Europe/Paris:20130527T103000
UID:2013-05-27_Chargueraud
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Arthur Charguéraud: Verification of Concurrent Programs Targeti
ng the x86-TSO Weak Memory Model
URL:http://parkas.di.ens.fr/seminars.html#2013-05-27_Chargueraud
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20130424T140000
DTEND;TZID=Europe/Paris:20130424T150000
DTSTAMP;TZID=Europe/Paris:20130424T140000
UID:2013-04-24_Keryell
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Ronan Keryell: SMECC: compiling the SME-C language for heterogen
eous computing
URL:http://parkas.di.ens.fr/seminars.html#2013-04-24_Keryell
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20130114T103000
DTEND;TZID=Europe/Paris:20130114T113000
DTSTAMP;TZID=Europe/Paris:20130114T103000
UID:2013-01-14_Grosser
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Tobias Grosser: Geometric time tiling of stencil computations
URL:http://parkas.di.ens.fr/seminars.html#2013-01-14_Grosser
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20130107T103000
DTEND;TZID=Europe/Paris:20130107T113000
DTSTAMP;TZID=Europe/Paris:20130107T103000
UID:2013-01-07_Sun
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Wei-Tsun Sun: The DynamicGALS approach to designing dynamic reac
tive systems
URL:http://parkas.di.ens.fr/seminars.html#2013-01-07_Sun
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20121217T103000
DTEND;TZID=Europe/Paris:20121217T113000
DTSTAMP;TZID=Europe/Paris:20121217T103000
UID:2012-12-17_Serpette
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Bernard Serpette: Une définition CPS d'Esterel
URL:http://parkas.di.ens.fr/seminars.html#2012-12-17_Serpette
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20121105T103000
DTEND;TZID=Europe/Paris:20121105T113000
DTSTAMP;TZID=Europe/Paris:20121105T103000
UID:2012-11-05_Bagnol
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Marc Bagnol: Synchronous Machines: a Traced Category
URL:http://parkas.di.ens.fr/seminars.html#2012-11-05_Bagnol
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20120907T110000
DTEND;TZID=Europe/Paris:20120907T120000
DTSTAMP;TZID=Europe/Paris:20120907T110000
UID:2012-09-07_Inoue
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Jun Inoue: High-Level Programming That Works
URL:http://parkas.di.ens.fr/seminars.html#2012-09-07_Inoue
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20120724T103000
DTEND;TZID=Europe/Paris:20120724T113000
DTSTAMP;TZID=Europe/Paris:20120724T103000
UID:2012-07-24_Cong
LOCATION:Amphi Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Jason Cong: High-Level Synthesis Revisited: Progress and Applica
tions
URL:http://parkas.di.ens.fr/seminars.html#2012-07-24_Cong
DESCRIPTION:[Slides](slides/2012-07-24_Cong.pdf).\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20120626T103000
DTEND;TZID=Europe/Paris:20120626T113000
DTSTAMP;TZID=Europe/Paris:20120626T103000
UID:2012-06-26_Edwards
LOCATION:salle B14; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Stephen A. Edwards: From Recursive Functions to Real FPGAs
URL:http://parkas.di.ens.fr/seminars.html#2012-06-26_Edwards
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20120523T140000
DTEND;TZID=Europe/Paris:20120523T150000
DTSTAMP;TZID=Europe/Paris:20120523T140000
UID:2012-05-23_Guatto
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Adrien Guatto: Code generation for Lucy-n: Issues and Perspectiv
es
URL:http://parkas.di.ens.fr/seminars.html#2012-05-23_Guatto
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20120419T103000
DTEND;TZID=Europe/Paris:20120419T113000
DTSTAMP;TZID=Europe/Paris:20120419T103000
UID:2012-04-19_DavidDelchini
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Vincent David et Hugo Delchini: Systèmes temps réel embarqués
déterministes et sûrs de fonctionnement – OASIS & PharOS
URL:http://parkas.di.ens.fr/seminars.html#2012-04-19_DavidDelchini
DESCRIPTION:Cohabitation PharOS/EmbeddedC dans une application de contr
ôle/commande de\nmoteur électrique pour du steer-by-wire avec retour d
'effort Démonstration.\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20120319T103000
DTEND;TZID=Europe/Paris:20120319T113000
DTSTAMP;TZID=Europe/Paris:20120319T103000
UID:2012-03-19_Chapoutot
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY: Alexandre Chapoutot : Vers un moteur de simulation ensembliste
de modèles Simulink
URL:http://parkas.di.ens.fr/seminars.html#2012-03-19_Chapoutot
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20120305T103000
DTEND;TZID=Europe/Paris:20120305T113000
DTSTAMP;TZID=Europe/Paris:20120305T103000
UID:2012-03-05_Kerneis
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY: Gabriel Kerneis : From threads to events through classical prog
ram transformations
URL:http://parkas.di.ens.fr/seminars.html#2012-03-05_Kerneis
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20120220T103000
DTEND;TZID=Europe/Paris:20120220T113000
DTSTAMP;TZID=Europe/Paris:20120220T103000
UID:2012-02-20_Delaval
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY: Gwenaël Delaval : Musical programming with Lucid Synchrone
URL:http://parkas.di.ens.fr/seminars.html#2012-02-20_Delaval
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20120213T103000
DTEND;TZID=Europe/Paris:20120213T113000
DTSTAMP;TZID=Europe/Paris:20120213T103000
UID:2012-02-13_Conchon
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Sylvain Conchon: Cubicle: A Parallel SMT-based Model Checker for
Parameterized Systems
URL:http://parkas.di.ens.fr/seminars.html#2012-02-13_Conchon
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20120130T103000
DTEND;TZID=Europe/Paris:20120130T113000
DTSTAMP;TZID=Europe/Paris:20120130T103000
UID:2012-01-30_Bouillard
LOCATION:salle B14; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Anne Bouillard: Algorithmic Issues in Network Calculus
URL:http://parkas.di.ens.fr/seminars.html#2012-01-30_Bouillard
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20120116T133000
DTEND;TZID=Europe/Paris:20120116T143000
DTSTAMP;TZID=Europe/Paris:20120116T133000
UID:2012-01-16_Filliatre
LOCATION:salle U/V; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Jean-Christophe Filliâtre: Deductive Program Verification with
Why3
URL:http://parkas.di.ens.fr/seminars.html#2012-01-16_Filliatre
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20111205T103000
DTEND;TZID=Europe/Paris:20111205T113000
DTSTAMP;TZID=Europe/Paris:20111205T103000
UID:2011-12-05_Plaice
LOCATION:salle B14; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY: John Plaice : TransLucid
URL:http://parkas.di.ens.fr/seminars.html#2011-12-05_Plaice
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20111102T103000
DTEND;TZID=Europe/Paris:20111102T113000
DTSTAMP;TZID=Europe/Paris:20111102T103000
UID:2011-11-02_Nicolau
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Alex Nicolau: Variability, Accuracy, and Performance evaluation
URL:http://parkas.di.ens.fr/seminars.html#2011-11-02_Nicolau
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20110919T103000
DTEND;TZID=Europe/Paris:20110919T113000
DTSTAMP;TZID=Europe/Paris:20110919T103000
UID:2011-09-19_Ishii
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Daisuke Ishii: An Execution Algorithm for a Hybrid Modeling Lang
uage HydLa
URL:http://parkas.di.ens.fr/seminars.html#2011-09-19_Ishii
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20110819T103000
DTEND;TZID=Europe/Paris:20110819T113000
DTSTAMP;TZID=Europe/Paris:20110819T103000
UID:2011-08-19_Gammie
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Peter Gammie: Verified Synthesis of Knowledge-Based Programs in
Finite Synchronous Environments
URL:http://parkas.di.ens.fr/seminars.html#2011-08-19_Gammie
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20110720T100000
DTEND;TZID=Europe/Paris:20110720T113000
DTSTAMP;TZID=Europe/Paris:20110720T100000
UID:2011-07-20_Giavitto
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Jean-Louis Giavitto: MGS : construire des représentations spati
ales de processus musicaux
URL:http://parkas.di.ens.fr/seminars.html#2011-07-20_Giavitto
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20110720T100000
DTEND;TZID=Europe/Paris:20110720T113000
DTSTAMP;TZID=Europe/Paris:20110720T100000
UID:2011-07-20_Echeveste
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:José Echeveste et Arshia Cont: Antescofo : formalisation des re
lations temporelles entre une partition et une performance musicale
URL:http://parkas.di.ens.fr/seminars.html#2011-07-20_Echeveste
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20110720T100000
DTEND;TZID=Europe/Paris:20110720T113000
DTSTAMP;TZID=Europe/Paris:20110720T100000
UID:2011-07-20_Bresson
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Jean Bresson: OpenMusic : programmation visuelle et composition
assistée par ordinateur
URL:http://parkas.di.ens.fr/seminars.html#2011-07-20_Bresson
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20110711T103000
DTEND;TZID=Europe/Paris:20110711T113000
DTSTAMP;TZID=Europe/Paris:20110711T103000
UID:2011-07-11_Encrenaz
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Emmanuelle Encrenaz: A Symbolic Model-Checking Framework for Tra
nsient Fault Robustness Classification and Quantification
URL:http://parkas.di.ens.fr/seminars.html#2011-07-11_Encrenaz
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20110630T110000
DTEND;TZID=Europe/Paris:20110630T123000
DTSTAMP;TZID=Europe/Paris:20110630T110000
UID:2011-06-30_Darte
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Alain Darte: Program Analysis and Source-Level Communication Opt
imizations for High-Level Synthesis
URL:http://parkas.di.ens.fr/seminars.html#2011-06-30_Darte
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20110630T100000
DTEND;TZID=Europe/Paris:20110630T110000
DTSTAMP;TZID=Europe/Paris:20110630T100000
UID:2011-06-30_Carle
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Thomas Carle: Throughput optimization by software pipelining of
conditional reservation tables
URL:http://parkas.di.ens.fr/seminars.html#2011-06-30_Carle
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20110614T150000
DTEND;TZID=Europe/Paris:20110614T160000
DTSTAMP;TZID=Europe/Paris:20110614T150000
UID:2011-06-14_Vitek
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Jan Vitek: Virtualizing Real-time Embedded Systems with Java
URL:http://parkas.di.ens.fr/seminars.html#2011-06-14_Vitek
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20110606T110000
DTEND;TZID=Europe/Paris:20110606T120000
DTSTAMP;TZID=Europe/Paris:20110606T110000
UID:2011-06-06_MunierKordon
LOCATION:salle U/V; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Alix Munier-Kordon: Etude de la minimisation de la surface des m
émoires-buffers pour une application modélisée par un graphe « Synch
ronous Data-Flow »
URL:http://parkas.di.ens.fr/seminars.html#2011-06-06_MunierKordon
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20110523T103000
DTEND;TZID=Europe/Paris:20110523T113000
DTSTAMP;TZID=Europe/Paris:20110523T103000
UID:2011-05-23_Lowinger
LOCATION:salle U/V; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Hélène Lowinger: Présentation des outils de l'information sci
entifique et technique de l'INRIA
URL:http://parkas.di.ens.fr/seminars.html#2011-05-23_Lowinger
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20110513T103000
DTEND;TZID=Europe/Paris:20110513T120000
DTSTAMP;TZID=Europe/Paris:20110513T103000
UID:2011-05-13_Najjar
LOCATION:Salle W; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Prof. Walid Najjar: Performance, Productivity and Programmabilit
y: The Coming of Age of FPGA Code Accelerators
URL:http://parkas.di.ens.fr/seminars.html#2011-05-13_Najjar
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20110328T113000
DTEND;TZID=Europe/Paris:20110328T123000
DTSTAMP;TZID=Europe/Paris:20110328T113000
UID:2011-03-28_Upadrasta
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Ramakrishna Upadrasta: Potential and Challenges of Two-Variable-
Per-Inequality Sub-Polyhedral Compilation
URL:http://parkas.di.ens.fr/seminars.html#2011-03-28_Upadrasta
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20110328T103000
DTEND;TZID=Europe/Paris:20110328T113000
DTSTAMP;TZID=Europe/Paris:20110328T103000
UID:2011-03-28_Park
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Eunjung Park: Predictive Modeling in a Polyhedral Optimization S
pace
URL:http://parkas.di.ens.fr/seminars.html#2011-03-28_Park
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20110321T083000
DTEND;TZID=Europe/Paris:20110321T093000
DTSTAMP;TZID=Europe/Paris:20110321T083000
UID:2011-03-21_Li
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Feng Li: Advances in Parallel-stage Decoupled Software Pipelinin
g
URL:http://parkas.di.ens.fr/seminars.html#2011-03-21_Li
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20110307T103000
DTEND;TZID=Europe/Paris:20110307T113000
DTSTAMP;TZID=Europe/Paris:20110307T103000
UID:2011-03-07_Bourke
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Timothy Bourke: OCaml/Sundials
URL:http://parkas.di.ens.fr/seminars.html#2011-03-07_Bourke
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20110131T143000
DTEND;TZID=Europe/Paris:20110131T153000
DTSTAMP;TZID=Europe/Paris:20110131T143000
UID:2011-01-31_ZappaNardelli
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Francesco Zappa-Nardelli: Shared Memory: an Elusive Abstraction
URL:http://parkas.di.ens.fr/seminars.html#2011-01-31_ZappaNardelli
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20101213T103000
DTEND;TZID=Europe/Paris:20101213T113000
DTSTAMP;TZID=Europe/Paris:20101213T103000
UID:2010-12-13_Pasteur
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Cédric Pasteur: Programming agents in ReactiveML
URL:http://parkas.di.ens.fr/seminars.html#2010-12-13_Pasteur
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20101213T103000
DTEND;TZID=Europe/Paris:20101213T113000
DTSTAMP;TZID=Europe/Paris:20101213T103000
UID:2010-12-13_Boudeville
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Olivier Boudeville: Présentation de SimDiasca (Simulation of Di
screte Systems of All Scales)
URL:http://parkas.di.ens.fr/seminars.html#2010-12-13_Boudeville
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20101124T133000
DTEND;TZID=Europe/Paris:20101124T143000
DTSTAMP;TZID=Europe/Paris:20101124T133000
UID:2010-11-24_Gerard
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Léonard Gérard: The basis of a bursty synchronous language, it
s clock system and a causality analysis
URL:http://parkas.di.ens.fr/seminars.html#2010-11-24_Gerard
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20101115T103000
DTEND;TZID=Europe/Paris:20101115T113000
DTSTAMP;TZID=Europe/Paris:20101115T103000
UID:2010-11-15_MandelPlateau
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Louis Mandel et Florence Plateau: Typage d'horloges périodiques
en Lucy-n
URL:http://parkas.di.ens.fr/seminars.html#2010-11-15_MandelPlateau
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20101011T150000
DTEND;TZID=Europe/Paris:20101011T160000
DTSTAMP;TZID=Europe/Paris:20101011T150000
UID:2010-10-11_Donaldson
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Alastair F. Donaldson: An Induction-based Method for Complete Bo
unded Model Checking of Programs
URL:http://parkas.di.ens.fr/seminars.html#2010-10-11_Donaldson
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
END:VCALENDAR