Languages, Compilation, and Semantics LIP Seminar

Information

The seminar will be hold at Room 003, Site Buisson, ENS Lyon. The meeting is open to all members of the labs LIP, LIRIS, and CITI.

Program

9h00-9h30 Welcome
9h30-10h30 Simone Martini (U. Bologne/Collegium de Lyon 2018-2019) Towards a conceptual history of programming languages : Types
A Conceptual History of Programming Languages aims to be an organic tale of how some of the notions present in programming languages entered the field, how their semantics has been modified during the years, which linguistic mechanisms were proposed to “name” those concepts in specific languages. This evolution happened in dialogue and under the influence of important areas of mathematics, which, at some point across the sixties and the seventies, were identified with mathematical logic (and proof-theory in particular). Contrary to most folklore, however, the explicit recognition of the influence of mathematical logic on programming language design is not something that happens since the beginning. Moreover, concepts of the same name (e.g. types) have slightly different meanings in the two fields. I will describe this phenomenon for the notion of (data) type, starting with the fifties (Fortran and Algol), and arriving to the early eighties (abstract data types and objects oriented languages).
11h00-11h45 Emmanuel Coquery (U. LyonI/LIRIS) Securing Materialized Views: a Rewriting-based Approach
Views are named queries in databases. They can be used either for storing the result of costly queries in tables, this is called materialized views. They can also be used to restrict access to data, by allowing users to query only views and forbidding direct access to tables. We call such views « access control views ». We consider the problem of, given a set of access control views on tables and a set of materialized views on the same tables, to devise a set of access control view to protect the materialized views. This problem boils down to identify the information accessible from both sets of views. We give an overview of a sound but incomplete algorithm for the case where views are restricted to conjunctive queries.
11h45-12h30 Damiano Mazza (CNRS/LIPN) The Cook-Levin theorem via type systems
The Cook-Levin theorem (the statement that SAT is NP-complete) is a fundamental result of complexity theory. We will give a proof of this theorem entirely based on the properties of a certain type system for a simple Turing-complete programming language. Such a type system arises from very general considerations, formalized in the language of category theory, relating types and program approximations.

Information

The seminar will be hold at “Salle des Thèses”, ENS Lyon, Site Monod, Batiment MGN1, ENS Lyon, Monod site. The meeting is open to all members of the labs LIP, LIRIS, and CITI.

Program

Click on title for abstract.

9h00-9h30 Welcome
9h30-10h30 Nicolas Halbwachs (Verimag) Disjunctive relational abstract interpretation for interprocedural program analysis
This is a joint work with Rémy Boutonnet.

Program analysis by abstract interpretation using relational abstract domains — like polyhedra or octagons — easily extends from state analysis (construction of reachable states) to relational analysis (construction of input-output relations). In this talk, we exploit this extension to enable interprocedural program analysis, by constructing relational summaries of procedures. In order to improve the accuracy of procedure summaries, we propose a method to refine them into disjunctions of relations, these disjunctions being directed by preconditions on input parameters.

PDF
10h30-11h00 Coffee break
11h00-11h45 Matthieu Moy (LIP) Compilation and Real-Time Analysis of a Synchronous Data-Flow Application on the Kalray MPPA Many-Core Processor
Simple, single-core processors have been the main execution platform for critical real-time software for years. Such software can be handwritten in imperative languages, but code generation from higher-level languages such as the synchronous data-flow SCADE (industrial version of the Lustre language) are also used in production today.

Single-core processors are reaching their limits. Performance, or energy efficiency constraints are leading the industry towards multi-core or many-core including for critical systems. These architectures raise new major challenges for timing analysis.

In this talk, we present a code generation flow from SCADE that produces parallel and yet predictable code for Kalray MPPA architecture. The code generation scheme is designed together with a timing analysis that take into account interference between cores when they access the local memory.

This work was performed as part of the CAPACITES project: http://capacites.minalogic.net/

PDF
11h45-12h30 Pierre Clairambault (LIP) Linearity in Higher-Order Recursion Schemes
Higher-Order Model-Checking (HOMC) has recently emerged as an approach to automated verification of higher-order programs, prompted by Ong's 2006 result that Monadic Second Order Logic (MSO) is decidable on infinite trees generated by Higher-Order Recursion Schemes (HORS). It is under active development, with implementations reporting encouraging results despite an awful theoretical worst case complexity.

In principle, HOMC algorithms work by reduction to Ong's theorem. In practice, this often involves CPS translations which are costly in terms of complexity, and so as to get tight complexity people have instead reproved variations of Ong's theorem for extensions of HORS (with data, or call-by-value) and drastically restricted fragments of MSO.

In this talk, I will introduce Linear HORS (LHORS), an extension of HORS with additional type constructors imported from Linear Logic. Data and call-by-value evaluation admit a finer translation to LHORS exploiting the idea of linearly-used continuations. Moreover LHORS enjoy a decidable model-checking problem, whose complexity essentially ignores linear types. In this way we recover and extend several developments that were originally proved independently of Ong's theorem.

This is joint work with Andrzej Murawski and Charles Grellois, presented at POPL'18.

PDF

Information

The seminar will be hold at the room at 1 place de l'école, ENS Lyon, Monod site. The meeting is open to all members of the labs LIP, LIRIS, and CITI.

Program

Click on title for abstract.

9h00-9h30 Welcome
9h30-10h30 Warwick Tucker (Uppsala University & LIP) Computer-aided proofs, interval arithmetic, and some (hard) conjectures
In this talk we will discuss some powerful techniques from the field of computer-aided proofs. The methods we will present are all based on set-valued mathematics (interval analysis) which is well-suited for computational proofs where the underlying problem is continuous rather than discrete. We will also talk about some concrete mathematical problems that we are currently trying to solve using the above-mentioned methods.
10h30-11h00 Coffee break
11h00-11h45 Ludovic Henrio (I3S) Programming and composing safely distributed applications with Active objects
Active objects is a programming paradigm strongly inspired from actors. In this talk, I will first present the active object programming model, and the different languages that implement it. In the Scale team we develop one particular active object language: the ASP model, and its reference implementation: ProActive. This will allow me to show how active objects can be used to implement software components, and how we extended the model to support local multi-threading. I will also illustrate how this model is efficient and expressive. Finally, I will present different efforts in applying formal methods to this programming model and to software components in order to ensure the correctness of programming languages and of distributed applications.
PDF PPTX
11h45-12h30 Laure Daviaud (Warwick University) First order and regular list functions.
We define two classes of functions, called regular (respectively, first-order) list functions, which manipulate objects such as lists, lists of lists, pairs of lists, lists of pairs of lists, etc. The definition is in the style of regular expressions: the functions are constructed by starting with some basic functions (e.g. projections from pairs, or head and tail operations on lists) and putting them together using four combinators (most importantly, composition of functions). Our main results are that first-order list functions are exactly the same as first-order transductions, under a suitable encoding of the inputs; and the regular list functions are exactly the same as MSO-transductions. This is a joint work with Mikolaj Bojanczyk and Krishna Shankara Naravanan.

Information

The seminar will be hold at Amphi J, ENS Lyon, Monod site. The meeting is open to all members of the labs LIP, LIRIS, and CITI.

Program

Click on title for abstract.

9h00-9h30 Welcome
9h30-10h30 Albert Cohen (Inria) Tensor Comprehensions: deep learning as a polyhedral compiler's killer app
Deep learning models with convolutional and recurrent networks are ubiquitous and analyze massive amounts of audio, image, video, text and graph data, with applications in automatic translation, speech-to-text, scene understanding, ranking user preferences, ad placement, etc. Competing frameworks for building these networks such as TensorFlow, Chainer, CNTK, Torch/PyTorch, Caffe1/2, MXNet and Theano, explore different tradeoffs between usability and expressiveness, research or production orientation and supported hardware. They operate on a DAG of computational operators, wrapping high-performance libraries such as CUDNN (for NVIDIA GPUs) or NNPACK (for various CPUs), and automate memory allocation, synchronization, distribution. Custom operators are needed where the computation does not fit existing high-performance library calls, usually at a high engineering cost. This is frequently required when new operators are invented by researchers. Such operators suffer a severe performance penalty, which limits the pace of innovation. Furthermore, even if there is an existing runtime call these frameworks can use, it often does not offer optimal performance for a user's particular network architecture and dataset, missing optimizations between operators as well as specialization to the size and shape of data.

We will survey the work-in-progress design of

(1) a language close to the mathematics of deep learning called Tensor Comprehensions, featuring interesting developments in the areas of automatic range inference, declarative array programming, and data-flow modeling of recurrent networks;

(2) a polyhedral Just-In-Time compiler to convert a mathematical description of a deep learning DAG into a CUDA kernel with delegated memory management and synchronization, also providing optimizations such as operator fusion and specialization for specific sizes;

(3) a high level metaprogramming environment and compilation cache populated by an autotuner, acting as a built-to-order library.

In a first paper, we demonstrate the suitability of the polyhedral framework to construct a domain-specific optimizer effective on state-of-the-art deep learning models on GPUs. Our flow reaches up to 4x speedup over NVIDIA libraries on kernels relevant to the Machine Learning Community, and on an actual model used in production at Facebook. TC also facilitates algorithmic exploration, exposing up to 2 orders of magnitude speedup on research layers. It is open source, integrated with mainstream frameworks Caffe2 (production-oriented) and PyTorch (research-oriented). TC is still at an early stage, and looking for contributions and collaboration.

https://research.fb.com/announcing-tensor-comprehensions

http://pytorch.org/2018/03/05/tensor-comprehensions.html

https://arxiv.org/abs/1802.04730

PDF
10h30-11h00 Coffee break
11h00-11h45 Abdallah Arioua (LIRIS) User-guided Repairing of Inconsistent Knowledge Bases
Repairing techniques for relational databases have leveraged integrity constraints to detect and then resolve errors in the data. User guidance has started to be employed in this setting to avoid a prohibitory exploration of the search space of solutions. In this paper, we present a user-guided repairing technique for Knowledge Bases (KBs) enabling updates suggested by the users to resolve errors. KBs exhibit more expressive constraints with respect to relational tables, such as tuple-generating dependencies (TGDs) and negative rules (a form of denial constraints). We consider TGDs and a notable subset of denial constraints, named contradiction detecting dependencies (CDDs). We propose user-guided polynomial-delay algorithms that ensure the repairing of the KB in the extreme cases of interaction among these two classes of constraints. To the best of our knowledge, such interaction is so far unexplored even in repairing methods for relational data. We prove the correctness of our algorithms and study their feasibility in practical settings. We conduct an extensive experimental study on synthetically generated KBs and a real-world inconsistent KB equipped with TGDs and CDDs. We show the practicality of our proposed interactive strategies by measuring the actual delay time and the number of questions required in our interactive framework.
PDF
11h45-12h30 Guilhem Jaber (LIP) Model-checking contextual equivalence of higher-order programs with references.
This talk will present SyTeCi, the first general automated tool to check contextual equivalence for programs written in an higher-order language with references (i.e. local mutable states), corresponding to a fragment of OCaml.

After introducing the notion of contextual equivalence, we will see on some examples why it is hard to prove such equivalences (reentrant calls, private states). As we will see, such examples can be found in many different programming languages.

Then, we will introduce SyTeCi, a tool to automatically check such equivalences. This tool is based on a reduction of the problem of contextual equivalence of two programs to the problem of reachability of “error states” in transition systems of memory configurations.

Contextual equivalence being undecidable (even in a finitary setting), so does the non-reachability problem for such transition systems. However, one can apply model-checking techniques (predicate abstraction, summarization of pushdown systems) to check non-reachability via some approximations. This allows us to prove automatically many non-trivial examples of the literature, that could only be proved by hand before. We will end this talk by the presentation of a prototype implementing this work.

PDF

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.

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.

Program

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.

Program

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