Languages, Compilation, and Semantics LIP Seminar

Information

The seminar will be hold at the Seminar room of the Centre Blaise Pascal (Access plan) The meeting is open to all members of the labs LIP, LIRIS, and CITI.

Preliminary Program

Click on title for abstract.

9h00-9h30 Welcome
9h30-10h15 Alain Darte (LIP) Performance models for (automatic) code optimizations: can we trust them?
10h15-10h45 Coffee break
10h45-11h30 Eric Rutten et Gwenael Delaval (LIG) Programming with controller synthesis, and application to autonomic managers of reconfigurable software components
Heptagon is a synchronous programming language, whose compilation involves discrete controller synthesis. It allows the programmer to express non determinism, by the use of controllable variables, associated with temporal properties the final program will satisfy. These temporal properties are enforced by a controller, automatically generated by a controller synthesis tool. We will present he Heptagon language, its semantics and compilation, and illustrates its use as a back-end for Ctrl-F, a DSL for autonomic managers of reconfigurable software components.
11h30-13h30 Lunch
13h30-14h00 Xavier Urbain (LIRIS) Towards Formal Proof for Swarms of Mobile Robots
Mobile robot networks emerged in the past few years as a promising distributed computing model, and received increasing attention from the Distributed Computing community. On the one hand, the use of cooperative swarms of inexpensive robots to achieve various complex tasks in potentially hazardous environments is a promising option to reduce human and material costs and assess the relevance of Distributed Computing in a practical setting. On the other hand, execution model differences warrant extreme care when revisiting “classical results” from Distributed Computing, as very small changes in assumed hypotheses may completely change the feasibility of a particular problem.

I will present a formal proof framework for localised distributed protocols in mobile robotic networks, based on the Coq Proof Assistant. The framework allows for a relatively easy specification of context, protocols, and properties. It was successfully used to certify impossibility results, and to establish formally the correctness of distributed protocols.

14h00-14h30 Jérôme Richard (LIP) COMET: A High-Performance Model for Fine-Grain Composition
Task-based models are known to greatly enhance performance and performance portability while component models ease the separation of concerns and thus improves modularity and adaptability. In this talk, we present the COMET programming model, a component model for HPC extended with task concepts, and its implementation built on top OpenMP and L2C.

We evaluate the approach on five synthetic use-cases representative of common patterns from HPC applications. Experimental results show that the approach is very efficient on the use-cases. On one hand, independent software codes can be easily composed. On the other hand, fine-grained composition supports very good performance. It sometimes even outperforms classical hand-written OpenMP implementations thank to better task interleaving. The presentation will also presents previous results conducted on a real-world use-case analysis of a sub-part of the production application GYSELA.

14h30-15h00 Coffee break
15h00-15h30 Anupam Das (LIP) Circular reasoning and relational algebra
Relational algebras provide important languages for reasoning about programs. In this talk I will present some axiomatisations and proof systems for Kleene algebra, in particular focussing on the importance of “analytic”systems, towards automated reasoning with relational expressions. I will present a methodology for handling least fixed points, such as transitive closure, that has recently become significant in proof theory: non-wellfounded reasoning. While this can be fallacious in general, correct reasoning can be ensured by 'fairness' criteria, and we can thus design classes of systems suitable for reasoning in these frameworks.

Information

The seminar will be hold at the Seminar room of the Centre Blaise Pascal (Access plan) The meeting is open to all members of the labs LIP, LIRIS, and CITI.

Preliminary Program

9h-9h30 Welcome
9h30-10h15 Guillaume Salagnac (CITI) Peripheral State Persistence For Transiently Powered Systems PDF
10h15-10h45 Coffee break
10h45-11h30 Olivier Muller (TIMA) An OpenMP flow targeting HPC systems with FPGA
11h30-13h00 Lunch
13h00-13h45 Paul Feautrier (LIP) Toward a polynomial model, with application to the OpenStream Language (cont'd) PDF
13h45-14h30 Christophe Alias et Laure Gonnord (LIP) Estimation of Parallel Complexity with Rewriting Techniques PDF
14h30-15h00 Coffee break
15h00-15h45 Romuald Thion (LIRIS) Inference leakage detection for authorization policies over RDF data PDF
15h45-16h30 Patrick Baillot (LIP) On a type-based time complexity analysis of subrecursive programs PDF

Information

The seminar will be hold at the Buisson site of ENS Lyon, allée de Fontenay. The meeting is open to all members of the labs LIP, LIRIS, and CITI.

Preliminary Schedule

9h-9h30 Welcome
9h30-10h15 Damien Pous (LIP) Tutorial Coq PDF
10h15-11h00 Angela Bonifati (LIRIS) Schema matching and mapping systems PDF
11h-11h30 Coffee break
11h30-12h15 Matteo Mio (LIP) Tutorial Markov Decision Processes / Stochastic Games PDF
12h15-13h45 Lunch break at Descartes CROUS
13h45-14h30 Paul Feautrier (LIP) Toward a polynomial model, with application to the OpenStream Language PDF
14h30-15h15 Tomofumi Yuki (LIP) Static Analysis of Parallel Programs with Loops, Tasks, and Synchronizations PDF
15h15-15h45 Coffee break
15h45-16h30 Tanguy Risset (CITI) Compilation de dataflow parametrique pour machines multi-core heterogènes PDF
16h30-17h15 Adrien Basso-Blandin (LIP) Model instantiation in KAMI PDF

Information

The seminar had gathered 31 people, Thursday 17 March 2016, at résidence Villemanzy, 21 montée St Sébastien at Lyon, 1er arr. (http://www.belambra-villemanzy.fr/fr/seminaires). The meeting was open to all members of the labs CITI-LIP-LIRIS.

Schedule

9h-9h15 Welcome
9h15-10h Laure Gonnord et Lionel Morel (LIP/CITI) Les langages flot de données dans tous leurs états PDF
10h-10h30 Coffee break
10h30-11h15 Emmanuel Coquery (LIRIS) Langages de requêtes en bases de données: tour d’horizon des différents paradigmes PDF
11h15-11h45 Hélène Coullon (LIP) The Multi-Stencil Language PDF
11h45-12h15 Christian Perez (LIP) Des langages d'assemblages dans les modèles à composants logiciels PDF
12h15-13h45 Lunch break
13h45-14h30 Russ Harmer (LIP) Executable knowledge PDF
14h30-15h Thierry Gautier (LIP) Programmation et exécution d’algorithmes parallèles PDF
15h-15h30 Coffee break
15h30-16h Simon Castellan (LIP) Weak memory models using event structures PDF
16h-16h30 Arnaud Lefray (LIP) Formalisation of security requirements PDF