Table of Contents

Languages, Compilation, and Semantics LIP Seminar in 2017

4th Edition, 2017, June, 1st

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.

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.