Publications

2021

JFLA21
Timothy Bourke, Paul Jeanmaire, Basile Pesin, and Marc Pouzet. Normalisation vérifiée du langage lustre. In JFLA 2021 - Les trente-deuxièmes Journées Francophones des Langages Applicatifs, Saint Médard d'Excideuil, Dordogne, France, April 2021.
bib ]

Lustre is a synchronous dataflow language designed for programming embedded systems. In the Vélus project, we use Coq to develop and formalize a compiler that accepts a normalized form of the language and produces imperative code. While this restricted form is suitable for code generated from a user interface based on block diagrams, we wanted to allow programmers to use the complete language.

In this article, we present the normalization pass that transforms the complete language into the normalized one. This transformation is divided into three steps so as to simplify the correctness proofs. To show that the semantics is preserved, it is necessary to prove that the three steps preserve certain static and dynamic properties of the language. In particular, the relation between the clock types and the dynamic semantic must be established.

2020

POPL20
Timothy Bourke, Lélio Brun, and Marc Pouzet. Mechanized semantics and verified compilation for a dataflow synchronous language with reset. Proceedings of the ACM on Programming Languages, 4(POPL):1–29, January 2020.
bib | DOI | http | .pdf ]

Specifications based on block diagrams and state machines are used to design control software, especially in the certified development of safety-critical applications. Tools like SCADE Suite and Simulink/Stateflow are equipped with compilers that translate such specifications into executable code. They provide programming languages for composing functions over streams as typified by Dataflow Synchronous Languages like Lustre.

Recent work builds on CompCert to specify and verify a compiler for the core of Lustre in the Coq Interactive Theorem Prover. It formally links the stream-based semantics of the source language to the sequential memory manipulations of generated assembly code. We extend this work to treat a primitive for resetting subsystems. Our contributions include new semantic rules that are suitable for mechanized reasoning, a novel intermediate language for generating optimized code, and proofs of correctness for the associated compilation passes.

2019

JFLA19
Timothy Bourke and Marc Pouzet. Clocked arguments in a verified Lustre compiler. In JFLA 2019 - Les trentièmes Journées Francophones des Langages Applicatifs, Les actes des trentièmes Journées Francophones des Langages Applicatifs (JFLA 2019), page 16, Les Rousses, France, January 2019.
bib | http | .pdf ]

Lustre is a synchronous language for programming systems as block diagrams from which low-level imperative code is generated automatically. Recent work applies the Coq interactive proof assistant to specify a compiler from a core subset of Lustre to the Clight input language of CompCert from which assembly code is generated. The overall correctness proof connects the stream semantics of Lustre to the imperative semantics of the assembly code.

Every stream in a Lustre program is associated with a static ‘clock’ that represents when it is active. Compilation transforms the clocks into conditional statements that control when the corresponding value are calculated. Previous work made the simplifying assumption that the inputs and outputs of any given block shared the same static clock. This paper describes one way to lift this restriction. It requires enriching the static typing rules for clocks and the semantic model, and, to satisfy the Clight semantics, adding a compilation pass to ensure that any variable passed to a function call has been initialized.

2018

SCOPES18
Timothy Bourke, Lélio Brun, and Marc Pouzet. Towards a verified Lustre compiler with modular reset. In 21st International Workshop on Software and Compilers for Embedded Systems (SCOPES 2018), Proceedings of the 21st International Workshop on Software and Compilers for Embedded Systems (SCOPES 2018), page 4, Sankt Goar, Germany, May 2018. ACM Press.
bib | DOI | http | .pdf ]

This paper presents ongoing work to add a modular reset construct to a verified Lustre compiler. We present a novel formal specification for the construct and sketch our plans to integrate it into the compiler and its correctness proof.

2017

PLDI17
Timothy Bourke, Lélio Brun, Pierre-Evariste Dagand, Xavier Leroy, Marc Pouzet, and Lionel Rieg. A Formally Verified Compiler for Lustre. In PLDI 2017 - 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, Barcelone, Spain, June 2017. ACM.
bib | http | .pdf ]

The correct compilation of block diagram languages like Lustre, Scade, and a discrete subset of Simulink is important since they are used to program critical embedded control software. We describe the specification and verification in an Interactive Theorem Prover of a compilation chain that treats the key aspects of Lustre: sampling, nodes, and delays. Building on CompCert, we show that repeated execution of the generated assembly code faithfully implements the dataflow semantics of source programs.

We resolve two key technical challenges. The first is the change from a synchronous dataflow semantics, where programs manipulate streams of values, to an imperative one, where computations manipulate memory sequentially. The second is the verified compilation of an imperative language with encapsulated state to C code where the state is realized by nested records. We also treat a standard control optimization that eliminates unnecessary conditional statements.

JFLA17
Timothy Bourke, Pierre-Evariste Dagand, Marc Pouzet, and Lionel Rieg. Vérification de la génération modulaire du code impératif pour Lustre. In JFLA 2017 - Vingt-huitième Journées Francophones des Langages Applicatifs, Gourette, France, January 2017.
bib | http | .pdf ]

Synchronous languages are used to program critical control applications. The Scade language, used in industry for these applications, is based on the Lustre language introduced by Caspi and Halbwachs. In this article we treat the formalization and proof, in the Coq proof assistant, of a key compilation pass: the translation of programs from Lustre into an imperative language. The challenge is to change from a synchronous dataflow semantics, where programs manipulate streams, to an imperative semantics, where the program manipulates memory sequentially. We specify and verify a simple code generator that treats core Lustre features: sampling, nodes, and delays. The proof uses an intermediate semantic model that mixes dataflow and imperative characteristics and allows the statement of an essential inductive invariant. We exploit this formalization to verify a classic optimization that fuses conditional structures in the generated imperative code.