Languages, Compilation, and Semantics LIP Seminar in 2017

Compiler code optimizations, and even manual code optimizations, rely on performance models, in general fairly simple analytic models, to drive the different optimization phases. They are certainly useful to provide methodologies, give ``grand principles'', but, when facing reality and approaching optimality, it is not clear how “good” they actually are. They can even drive us to wrong beliefs. In general, we (the community) are fairly bad at measuring the impact of these models, especially in today's context, with such a range of computer architectures (from FPGA, GPU, vector multi-cores, to future exascale), with many levels of parallelism and data storage, and where bandwidth, pipelining, and locality are more important than pure computing power. I will give several examples of code optimizations where, if analytic models can provide reassuring metrics for theoretical work, they give very little information on actual performance improvements. I will also quickly present a more heuristic performance model, introduced by physicists, the ECM model, that is fairly useful to optimize codes for vector machines. With Thierry Dumont (from ICJ), we are currently developing an alternative to standard stencil-like sparse computations with a better focus on exploiting vector operations as well as spatial and temporal data locality.“

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.

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.

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.

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.