Languages, Compilation, and Semantics LIP Seminar

Even though there has been a large number of proposals to accelerate databases using specialized hardware, often the opinion of the community is pessimistic: the performance and energy efficiency benefits of specialization are seen to be outweighed by the limitations of the proposed solutions and the additional complexity of including specialized hardware, such as field programmable gate arrays (FPGAs), in servers. Recently, however, as an effect of stagnating CPU performance, server architectures started to incorporate various programmable hardware components, ranging from smart network interface cards, through SSDs with offloading capabilities, to near-CPU accelerators. This availability of heterogeneous hardware brings new opportunities to databases and this talk makes the case that there is cause for optimism. In the light of a shifting hardware landscape and emerging analytics workloads, it is time to revisit our stance on hardware acceleration and to start exploring emerging research questions around programmability and integration.

Bio: Zsolt Istvan is an Assistant Research Professor at the IMDEA Software Institute in Madrid, Spain. In his research he explores how specialized hardware can be used to make data-intensive systems more efficient.

We propose a new static software analysis principle called Abstract Execution, generalizing Symbolic Execution: While the latter analyzes all possible execution paths of a specific program, Abstract Execution analyzes a partially unspecified program by permitting abstract symbols representing unknown contexts. There is a wide range of applications of Abstract Execution, especially for verifying relational properties of schematic programs. We implemented Abstract Execution in a deductive verification framework and proved correctness of eight well-known statement-level refactoring rules, including two with loops. For each refactoring we characterize the preconditions that make it semantics-preserving. Most preconditions were not mentioned in the literature.

I will first give a brief description of proof assistants: computer programs that make it possible to write and check proofs, and to exploit certified algorithms for some laborious subproofs.

Then I will spend most of the talk showing that graphs and tools from graph theory can be used to characterise certain equational theories, and to obtain decision procedures for some of them. There, a crucial point is to be able to characterise subclasses of graphs of treewidth at most two.

We formalised some of these ideas in the Coq proof assistant with C. Doczkal, which first required developing a general purpose library for graph theory (see the talk in the afternoon). We plan to pursue this effort in the future: not only this helps us in our daily research using graphs for equational theories, but this also opens the way to the formalisation of challenging results in graph theory.

The goal of this talk is to survey a classical method to prove theorems that describe the structure of graph classes. We will see several examples, such as the seminal theorem of Wagner on planar graphs from 1937 and the Strong perfect graph theorem from 2002. I will try to convince the audience that formal proofs are potentially interesting in this field, even if it not much used so far.

Computers are often used in combinatorics to determine if combinatorial objects with given structural or extremal properties exist as these existence problems are often too complex to solve by hand. This is done by designing and implementing generation algorithms which construct combinatorial objects from a given class (typically avoiding the generation of isomorphic copies) and analysing the resulting graphs.

In this talk we will give an introduction to the exhaustive isomorphism-free generation of graphs. We will also give concrete examples of how this has helped to gain new insights and solve problems in mathematics and chemistry.

Applications in mathematics include the generation of cubic graphs and snarks. We will present a new algorithm for the efficient generation of all non-isomorphic cubic graphs and show how this algorithm can be extended to generate snarks efficiently. A snark is a cyclically 4-edge-connected cubic graph with chromatic index 4. Snarks are of interest since for a lot of conjectures it can be proven that if the conjecture is false, the smallest possible counterexamples will be snarks. Our algorithm enabled us to generate all snarks up to 36 vertices, which was impossible with previous methods. This new list of snarks allowed us to find counterexamples to several published open conjectures.

An application of graph enumeration in chemistry is the generation of the Nobel Prize winning fullerenes (cubic plane graphs where all faces are pentagons or hexagons). We will sketch a new algorithm for the generation of all non-isomorphic fullerenes. Our implementation of this algorithm allowed us to generate all fullerenes up to 400 vertices, which enabled us to prove that the smallest counterexample to the spiral conjecture has 380 vertices.

This talk is based on joint work with Gunnar Brinkmann (Ghent University) and Brendan McKay (Australian National University).

Over the last couple of years we have developed a library of graph theory results in the interactive theorem prover Coq. This was motivated by the wish to formalize recent results on axiomatizations of graph isomorphism for treewidth-two graphs. Given the lack of a general-purpose graph theory library for Coq when we started our project, our second goal, right from the start, was to improve upon the state of the art in formalized graph theory by building a reusable library.

In my talk, I will report on our experience building the library, highlighting key design choices, selected results, and some directions for future extensions.

This talk is based on joint work with Damien Pous.

For analyzing the behaviour of concurrent value-passing systems, classical temporal logics must be extended with data-handling primitives. Since the early days of formal verification, many such extensions were proposed, both in the linear/branching time and the state/action based settings. We present MCL (Model Checking Language), an extension of the alternation-free modal mu-calculus with data-handling features, generalized regular expressions over transition sequences, and fairness operators expressed using omega-regular expressions. MCL was designed for a versatile and succinct formulation of temporal properties interpreted on labeled transition systems (LTSs) containing data values, i.e., state-transition graphs modeling the behaviour of concurrent systems. We illustrate the usage of MCL by means of classical examples of properties (safety, liveness, and fairness) and discuss its expressiveness and model checking complexity. We also briefly describe the implementation of MCL provided by the EVALUATOR model checker of the CADP verification toolbox, which evaluates an MCL formula on an LTS on the fly and produces diagnostics (counterexamples and witnesses). Finally, we illustrate the recent extension of MCL with a probabilistic operator, which computes on the fly the probability measure of a transition sequence in a probabilistic transition system (PTS). Combined with data-handling features, this probabilistic operator enables the quantitative analysis of sequences having peak cost values (e.g., number of operations, energy consumption, etc.).

This is a joint work with Cyril Six and Sylvain Boulmé.

CompCert (compcert.inria.fr) is a compiler for the C language with a machine-checked proof of correctness: if it succeeds in compiling a program, then the semantics of the assembly code should match that of the source code. This is ensured by giving semantics to all intermediate languages, and proofs that all transformations preserve the semantics. It is mainly developed in Coq.

Extending CompCert to a new architecture is not so hard, albeit tedious, assuming that architecture is sufficiently similar to those already supported. We did so for the upcoming Kalray MPPA3 processor.

CompCert however had no optimization pass for instruction scheduling — that is, reordering instruction to exploit instruction-level parallelism (e.g. posting memory reads sufficiently in advance before using their results, so as to avoid stalling waiting for the read value). This is not much important on highly out-of-order processors such as x86, but is of great importance on in-order processors. MPPA3 is a VLIW (very large instruction word) in-order processor, meaning that the compiler can specify multiple instructions to be executed at the same cycle, according to certain well-formedness rules.

We designed a highly modular and parametric system for scheduling instructions in the backend, after register allocation. This system is composed of a transformation pass, itself calling a scheduler among a choice of several, and a checker, verifying that the semantics of the results of the transformation matches that of the input. We can also add extra transformation passes to implement other transformations (in our case, coalescing of multiple-word reads and writes). Only the checker needs to be implemented in Coq proved correct; the transformation phases and schedulers do not (in fact, one of the schedulers calls an external solver).

When dealing with large graphs, classical algorithms for finding paths such as Dijkstra's Algorithm are unsuitable, because they require to perform too many disk accesses. To avoid the cost of this expensive accesses, while keeping a data structure of size quasi-linear in the size of the graph, we propose to guide the path search with a distance oracle, obtained from a topological embedding of the graph. I will present fresh experimental research on this topic, in which we obtain graph embeddings using learning algorithms from natural language processing. On some graphs, such as the graph of publications of DBLP, our topologically-guided path search allows us to visit a small portion of the graph only, in average. This is joint work with Charles Paperman.

Field Programmable Gate Array (FPGA) architec-tures are suitable hardware platforms for systems that need high performance and flexibility, because they support dynamic partial reconfiguration (DPR) to implement adaptive hardware algorithms e.g., for performance or energy efficiency. They are used for example in embedded systems such as UAV, e.g. for video processing. It is a challenge to design Autonomic Managers for such highly dynamic systems, taking into account the combina-torial design space of configurations and criteria and policies to decide on whether to reconfigure, and what next configuration to choose. In this paper, we propose a Domain Specific Language (DSL) called Ctrl-DPR, allowing designers to easily generate Autonomic Managers. They can describe their system and their management strategies, in terms of the entities composing the system : tasks, versions, applications, ressources, policies. The DSL relies on a behavioural modelling of these entities, targeted at the design of autonomic managers to control the reconfigurations in such a way as to enforce given policies and strategies. The models we use involve automata to describe the state space of configurations, and the transitions representing reconfigurations; they also involve discrete control techniques exploiting such models in order to obtain a correct runtime manager. These model-based control techniques are embedded in a compiler, connected to a reactive language and discrete controller synthesis tool, which enables to generate a C implementation of the controller enforcing the management strategies. We apply our DSL for the management of a video application on a UAV.

OpenMP (http://www.openmp.org) est un standard de facto qui est piloté par l’ARB (Architecture Review Board) composé de la plupart des grands constructeurs en HPC ainsi que par certains représentants universitaires. L’objectif d’OpenMP est d’offrir un ensemble de directives pour annoter du code séquentiel afin d'exploiter tous les niveaux de parallélisme qui sont offerts par les matériels, i.e. multi-cœurs, unités vectorielles et accélérateurs. Dans cette présentation nous nous attacherons à re-positionner les évolutions actuelles de la norme 4.x entre son passé (pré 3.0) et son futur (5.0) en s’intéressant plus particulièrement au modèle de tâches.

Nous présenterons la manière dont sont définies les tâches et leurs dépendances dans le modèle OpenMP. Nous verrons qu'un tel programme OpenMP est fonctionnellement portable mais que l'obtention des performances doit aussi prendre en compte l'implementation à disposition. Nous illustrerons sur quelques exemples typiques en HPC l'impact de quelques runtimes (GCC, ICC/LLVM, …) sur les performances dont certains choix d'implémentation restentcritiquables.

In this talk, we present a survey on multi-core timing analyses including delays due to interferences (shared memory, shared bus). We show that interference analysis is possible (scalability and precision). We illustrate this point with our interference analysis where the delay is integrated into schedulability analysis. We show that applying this analysis to a real platform (Kalray MPPA2) comes with a necessary smart software implementation and hardware configuration.

With the emergence of large-scale virtualized distributed infrastructures, such as Cloud, Fog and Edge computing, for instance, the automation of the deployment of distributed software is of great importance for IT administrators and developers. While many production tools already help developers automate their deployment tasks, academic research is interested in safe and verified modeling to ensure the correct behavior of a software configuration or reconfiguration. In this talk I will present Madeus, a formal component model for the deployment of distributed software that enhances the efficiency of deployment. Madeus puts forward more concurrency than other deployment models. This implies a greater complexity and a greater propensity for error. Hence, I will also introduce ongoing work regarding the verification of properties on Madeus deployments by model checking. Finally, I will rapidly present ongoing work regarding the extension of Madeus to dynamic software reconfiguration.

This talk surveys a Curry-Howard perspective on Rabin's Tree Theorem, the decidability of Monadic Second-Order Logic (MSO) on infinite trees.

Rabin's Tree Theorem proceeds by effective translations of MSO-formulae to tree automata. We show that the operations on automata used in these translations can be organized in a deduction system based on intuitionistic linear logic (ILL). We propose a computational interpretation of this deduction system along the lines of the Curry-Howard proofs-as-programs correspondence. This interpretation, relying on the usual technology of game semantics, maps proofs to strategies in two-player games generalizing usual acceptance games of tree automata.