journée des groupes de travail LaMHA/LTP- Automne 2017

Motivated by applications to security and high efficiency, we propose an automated methodology for validating on low-level intermediate representations the results of a source-level static analysis. Our methodology relies on two main ingredients: a relative-safety checker, an instance of a relational verifier which proves that a program is “safer” than another, and a transformation of programs into defensive form which verifies the analysis results at runtime. We prove the soundness of the methodology, and provide a formally verified instantiation based on the Verasco verified C static analyzer and the CompCert verified C compiler. We experiment with the effectiveness of our approach with client optimizations at RTL level, and static analyses for cache-based timing side-channels and memory usage at pre-assembly levels.

JIT compilers for dynamic langage crucially rely on *speculative* optimizations, that generate code under optimistic assumptions that may be invalidated later during the program run. The generated code contains dynamic tests (guards) to check that the hypotheses hold, and enough information to de-optimize (bail out) when they fail.
It is not easy for implementers to determine which optimizations remain correct on code that contains guards and de-optimization points.We designed a toy language to serve as a model of existing JIT implementations, a bytecode with an explicit bailout instruction, to study the correctness of code transformations in this setting.

Les compilateurs Just-in-time (JIT) pour langages dynamiques reposent de façon essentielle sur les optimisations *spéculatives*, qui consistent à générer du code sous des hypothèses optimistes qui peuvent être contredites pendant l'exécution du programme. Le code généré contient des tests dynamiques les hypothèses sont valides, et des informations pour dé-optimiser (bail out) si les tests échouent.
Nous avons conçu un petit langage pour servir de modèle des implémentations JIT existantes, avec une instruction spécifique de déoptimisation, afin de pouvoir étudier la correction des optimisations classiques en présence de points de déoptimisation: quelles sont les transformations de programme qui restent valides ?

Les langages synchrones sont utilisés pour programmer des logiciels de contrôle-commande d'applications critiques. On s'intéresse ici à la formalisation et la preuve, dans l'assistant de preuve Coq, d'un générateur de code impératif pour un noyau du langage Lustre. Nous spécifions et vérifions un générateur de code simple qui gère les traits principaux de Lustre: l'échantillonnage, les nœuds et les délais. Le générateur intègre le compilateur CompCert pour produire un code assembleur qui calcule successivement les valeurs spécifiées par le modèle sémantique flot de données. Les garanties offertes par CompCert nous permettent d'étendre notre théorème de correction sur toute la chaîne de compilation des programmes Lustres jusqu'à l'assembleur.

Ce travail est fait en collaboration avec Lélio Brun, Pierre-Évariste Dagand, Xavier Leroy, Marc Pouzet et Lionel Rieg.

Bulk Synchronous Parallel (BSP) is a model for parallel computing with predictable scalability. BSP has a cost model: programs can be assigned a cost which describes its behavior on any parallel machine. However, the programmer has to manually derive this cost. This paper describes an automatic method for the derivation of BSP program costs, based on classic cost analysis and approximation of polyhedral integer volumes. Our method requires and analyzes programs with textually aligned synchronization and textually aligned, polyhedral communication. We obtain cost-formulas that are parametric in the input parameters of the program and the parameters of the BSP computer.