velus.bib
@inproceedings{JFLA17,
title = {{V{\'e}rification de la g{\'e}n{\'e}ration modulaire du code imp{\'e}ratif pour Lustre}},
author = {Bourke, Timothy and Dagand, Pierre-Evariste and Pouzet, Marc and Rieg, Lionel},
url = {https://hal.inria.fr/hal-01403830},
booktitle = {{JFLA 2017 - Vingt-huiti{\`e}me Journ{\'e}es Francophones des Langages Applicatifs}},
address = {Gourette, France},
year = 2017,
month = jan,
keywords = {Langages synchrones (Lustre) ; Compilation ; Assistants de Preuve (Coq)},
pdf = {https://hal.inria.fr/hal-01403830/file/bourke%20%281%29.pdf},
hal_id = {hal-01403830},
hal_version = {v1},
abstract = {
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.
}
}
@inproceedings{PLDI17,
title = {{A Formally Verified Compiler for Lustre}},
author = {Bourke, Timothy and Brun, L{\'e}lio and Dagand, Pierre-Evariste and Leroy, Xavier and Pouzet, Marc and Rieg, Lionel},
url = {https://hal.inria.fr/hal-01512286},
booktitle = {{PLDI 2017 - 38th ACM SIGPLAN Conference on Programming Language Design and Implementation}},
address = {Barcelone, Spain},
organization = {{ACM}},
year = 2017,
month = jun,
keywords = {Synchronous Languages (Lustre) ; Verified Compilation ; Interactive Theorem Proving (Coq)},
pdf = {https://hal.inria.fr/hal-01512286/file/velus-pldi17.pdf},
hal_id = {hal-01512286},
hal_version = {v1},
abstract = {
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.
}
}
@inproceedings{JFLA19,
title = {{Clocked arguments in a verified Lustre compiler}},
author = {Bourke, Timothy and Pouzet, Marc},
url = {https://hal.inria.fr/hal-02005639},
booktitle = {{JFLA 2019 - Les trenti{\`e}mes Journ{\'e}es Francophones des Langages Applicatifs}},
address = {Les Rousses, France},
series = {Les actes des trenti{\`e}mes Journ{\'e}es Francophones des Langages Applicatifs (JFLA 2019)},
pages = 16,
year = 2019,
month = jan,
pdf = {https://hal.inria.fr/hal-02005639/file/bourke-pouzet-jfla2019.pdf},
hal_id = {hal-02005639},
hal_version = {v1},
abstract = {
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.
}
}
@inproceedings{SCOPES18,
title = {{Towards a verified Lustre compiler with modular reset}},
author = {Bourke, Timothy and Brun, L{\'e}lio and Pouzet, Marc},
url = {https://hal.inria.fr/hal-01817949},
booktitle = {{21st International Workshop on Software and Compilers for Embedded Systems (SCOPES 2018)}},
address = {Sankt Goar, Germany},
publisher = {{ACM Press}},
series = {Proceedings of the 21st International Workshop on Software and Compilers for Embedded Systems (SCOPES 2018)},
pages = 4,
year = 2018,
month = may,
doi = {10.1145/3207719.3207732},
keywords = {Compilers ; Formal software verification ; Semantics ; Synchronous Languages (Lustre) ; Verified Compilation},
pdf = {https://hal.inria.fr/hal-01817949/file/paper.pdf},
hal_id = {hal-01817949},
hal_version = {v1},
abstract = {
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.
}
}
@phdthesis{Brun20,
author = {L{\'{e}}lio Brun},
title = {Mechanized Semantics and Verified Compilation for a
Dataflow Synchronous Language with Reset},
school = {PSL Research University},
year = 2020,
month = jun,
pdf = {https://theses.hal.science/tel-03068862/file/Brun-2020-These.pdf},
abstract = {
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 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.
In this thesis we present Vélus, a Lustre compiler verified in the
interactive theorem prover Coq. We develop semantic models for the
various languages in the compilation chain, and build on the verified
CompCert C compiler to generate executable code and give an end-to-end
correctness proof. The main challenge is to show semantic preservation
between the dataflow paradigm and the imperative paradigm, and to reason
about byte-level representations of program states.
We treat, in particular, the modular reset construct, a primitive for
resetting subsystems. This necessitates the design of suitable semantic
models, compilation algorithms and corresponding correctness proofs. We
introduce a novel intermediate language into the usual clock-directed
modular compilation scheme of Lustre. This permits the implementation of
compilation passes that generate better sequential code, and facilitates
reasoning about the correctness of the successive transformations of the
modular reset construct.
}
}
@article{POPL20,
title = {{Mechanized semantics and verified compilation for a dataflow synchronous language with reset}},
author = {Bourke, Timothy and Brun, L{\'e}lio and Pouzet, Marc},
url = {https://hal.inria.fr/hal-02426573},
journal = {{Proceedings of the ACM on Programming Languages}},
publisher = {{ACM}},
volume = {4},
number = {POPL},
pages = {1-29},
year = {2020},
month = jan,
doi = {10.1145/3371112},
keywords = {CCS Concepts: $\bullet$ Software and its engineering $\rightarrow$ Formal language definitions ; Software verification ; Compilers ; $\bullet$ Computer systems organization $\rightarrow$ Embedded software Additional Key Words and Phrases: stream languages ; verified compilation ; interactive theorem proving},
pdf = {https://dl.acm.org/doi/pdf/10.1145/3371112?download=true&.pdf},
hal_id = {hal-02426573},
hal_version = {v1},
abstract = {
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.
}
}
@inproceedings{JFLA21,
title = {Normalisation v{\'{e}}rifi{\'{e}}e du langage {Lustre}},
author = {Timothy Bourke
and Paul Jeanmaire
and Basile Pesin
and Marc Pouzet},
booktitle = {{JFLA 2021 - Les trente-deuxi{\`e}mes Journ{\'e}es Francophones des Langages Applicatifs}},
pages = {117--133},
year = 2021,
month = apr,
address = {Online},
url = {https://hal.inria.fr/hal-03287572},
pdf = {https://hal.inria.fr/hal-03287572/file/jfla.pdf},
hal_id = {hal-03287572},
hal_version = {v1},
abstract = {
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.
}
}
@article{EMSOFT21,
author = {Timothy Bourke
and Paul Jeanmaire
and Basile Pesin
and Marc Pouzet},
title = {Verified {Lustre} Normalization with Node Subsampling},
journal = {ACM Transactions on Embedded Computing Systems},
year = 2021,
month = oct,
volume = {20},
number = {5s},
pages = {Article 98},
url = {https://velus.inria.fr/emsoft2021/},
pdf = {https://hal.inria.fr/hal-03370264/file/paper.pdf},
hal_id = {hal-03370264},
hal_version = {v1},
doi = {10.1145/3477041},
note = {ESWEEK special issue including presentations at the 21st
Int. Conf. on Embedded Software (EMSOFT 2021)},
abstract = {
Dataflow languages allow the specification of reactive systems by
mutually recursive stream equations, functions, and boolean activation
conditions called clocks. Lustre and Scade are dataflow languages for
programming embedded systems. Dataflow programs are compiled by a
succession of passes. This article focuses on the normalization pass
which rewrites programs into the simpler form required for code
generation.
Vélus is a compiler from a normalized form of Lustre to CompCert's
Clight language. Its specification in the Coq interactive theorem prover
includes an end-to-end correctness proof that the values prescribed by
the dataflow semantics of source programs are produced by executions of
generated assembly code. We describe how to extend Vélus with a
normalization pass and to allow subsampled node inputs and outputs. We
propose semantic definitions for the unrestricted language, divide
normalization into three steps to facilitate proofs, adapt the clock
type system to handle richer node definitions, and extend the end-to-end
correctness theorem to incorporate the new features. The proofs require
reasoning about the relation between static clock annotations and the
presence and absence of values in the dynamic semantics. The
generalization of node inputs requires adding a compiler pass to ensure
the initialization of variables passed in function calls.
}
}
@inproceedings{TYPES22,
author = {Timothy Bourke
and Paul Jeanmaire
and Marc Pouzet},
title = {Towards a denotational semantics of streams for a verified
{Lustre} compiler (short talk)},
booktitle = {28th International Conference on Types for Proofs and
Programs},
year = 2022,
month = jun,
address = {Nantes, France},
pdf = {https://types22.inria.fr/files/2022/06/TYPES_2022_paper_28.pdf},
abstract = {
This short talk presents work in progress to develop a denotational
semantics in the Coq proof assistant for the Vélus verified Lustre
compiler. It describes the current correctness theorem and proposes an
approach to mitigate certain of its limitations by building on an
existing library for Complete Partial Orders (CPOs).
}
}
@inproceedings{JFLA23,
title = {Analyse de d{\'{e}}pendance v{\'{e}}rifi{\'{e}}e pour
un langage synchrone {\`{a}} flot de donn{\'{e}}es},
author = {Timothy Bourke
and Basile Pesin
and Marc Pouzet},
pages = {101--120},
booktitle = {{JFLA 2023 - Les trente-quatri{\`e}mes Journ{\'e}es
Francophones des Langages Applicatifs}},
year = 2023,
month = jan # {/} # feb,
editor = {Timothy Bourke
and Delphine Demange},
address = {Praz-sur-Arly, France},
url = {https://velus.inria.fr/jfla2023/},
pdf = {https://hal.inria.fr/hal-03936656/file/jfla23_paper_6388.pdf},
hal_id = {hal-03936656},
hal_version = {v1},
abstract = {
Vélus is a formalisation of a synchronous dataflow language and
compiler in the Coq proof assistant.
It includes a definition of the source language's dynamic semantics,
a compiler that produces imperative code,
and an end-to-end proof that the compiler preserves the semantics of
programs.
In this article, we extend Vélus with the semantics of two activation
structures that are provided by modern compilers:
switchs and local declarations.
These new constructions require adapting the static dependency analysis
of Vélus, which produces an acyclic graph as a witness that a program is
well formed.
We use this witness to construct an induction schema and apply it to
show, in Coq, that the semantic model is deterministic.
}
}
@article{EMSOFT23,
title = {Verified Compilation of Synchronous Dataflow with State
Machines},
author = {Timothy Bourke
and Basile Pesin
and Marc Pouzet},
journal = {ACM Transactions on Embedded Computing Systems},
year = 2023,
month = sep,
pages = {137:1--137:26},
note = {ESWEEK special issue including presentations at the 23rd
Int. Conf. on Embedded Software (EMSOFT 2023)},
volume = 22,
number = {5s},
doi = {10.1145/3608102},
url = {https://velus.inria.fr/emsoft2023/},
pdf = {https://inria.hal.science/hal-04201401v1/file/velus-emsoft2023.pdf},
abstract = {
Safety-critical embedded software is routinely programmed in
block-diagram languages. Recent work in the Vélus project specifies such
a language and its compiler in the Coq proof assistant. It builds on the
CompCert verified C compiler to give an end-to-end proof linking the
dataflow semantics of source programs to traces of the generated
assembly code. We extend this work with switched blocks, shared
variables, reset blocks, and state machines; define a relational
semantics to integrate these block- and mode-based constructions into
the existing stream-based model; adapt the standard source-to-source
rewriting scheme to compile the new constructions; and reestablish the
correctness theorem.
}
}
@phdthesis{Pesin23,
author = {Basile Pesin},
title = {Verified Compilation of a Synchronous Dataflow Language
with State Machines},
school = {PSL University},
year = 2023,
month = oct,
pdf = {https://inria.hal.science/tel-04830529v1/file/pesin_phd.pdf},
abstract = {
Safety-critical embedded systems are often specified using block-diagram
formalisms. SCADE Suite is a development environment for such systems
which has been used industrially in avionics, nuclear plants, automotive
and other safety-critical contexts for twenty years. Its graphical
formalism translates to a textual representation based on the Lustre
synchronous dataflow language, with extensions from later languages like
Lucid Synchrone. In Lustre, a program is defined as a set of equations
that relate inputs and outputs of the program at each discrete time
step. The language of expressions at right of equations includes
arithmetic and logic operators, delay operators that access the previous
value of an expression, and sampling operators that allow some values to
be calculated less often than others.
The Vélus project aims at formalizing a subset of the Scade 6 language
in the Coq Proof Assistant. It proposes a specification of the dynamic
semantics of the language as a relation between infinite streams of
inputs and outputs. It also includes a compiler that uses CompCert, a
verified compiler for C, as its back end to produce assembly code, and
an end-to-end proof that compilation preserves the semantics of dataflow
programs.
In this thesis, we extend Vélus to support control blocks present in
Scade 6 and Lucid Synchrone, which includes a construction that controls
the activation of equations based on a condition (switch), a
construction that accesses the previous value of a named variable
(last), a construction that re-initializes delay operators (reset), and
finally, hierarchical state machines, which allow for the definition of
complex modal behaviors. All of these constructions may be arbitrarily
nested in a program. We extend the existing semantics of Vélus with a
novel specification for these constructs that encodes their behavior
using sampling. We propose a generic induction principle for well-formed
programs, which is used to prove properties of the semantic model such
as determinism and type system correctness. Finally, we describe the
extension of the Vélus compiler to handle these new constructs. We show
that the existing compilation scheme that lowers these constructs into
the core dataflow language can be implemented, specified and verified in
Coq. Compiling the reset and last constructs requires deeper changes in
the intermediate languages of Vélus.
}
}
@phdthesis{Jeanmaire24,
author = {Paul Jeanmaire},
title = {Une sémantique dénotationnelle pour un compilateur
synchrone v{\'{e}}rifi{\'{e}}},
school = {PSL University},
year = 2024,
month = dec,
abstract = {
Lustre is a synchronous dataflow language. Its discrete temporal
structure and clocking system guarantee statically bounded execution
time and memory consumption, favoring its adoption in mission-critical
systems, notably within the Scade industrial tool. Vélus, developed at
Inria, is a verified Lustre compiler. Based on the definition of formal
semantics for each intermediate language, it provides a proof that a
Lustre program and its translation into Clight (the language supported
by CompCert) exhibit identical behaviors.
In this thesis, we develop a new model of the input language's dataflow
kernel, based on synchronous denotational semantics, and give the exact
conditions for its equivalence with the existing relational model in
Vélus. This constructive approach results in an executable semantics,
reinforcing the main correctness theorem of the compilation. Thanks to
Scott's induction principle, specific to denotational semantics, we are
able to conduct very natural reasoning on program dynamics, but with
explicit treatment of errors that may occur at runtime. Finally, we
explore the possibility of freeing ourselves from language
synchronization constraints by proposing a formal correspondence between
our model and that of Kahn's networks. We outline the principles of the
infrastructure required for an end-to-end verified reasoning on
compilable programs.
}
}