Informations
A denotational semantics for a verified synchronous compiler
defended on December 20, 2024. Jury:
| advisors | Timothy Bourke | Inria |
| Marc Pouzet | ENS | |
| reviewers | Sylvain Boulmé | Grenoble INP |
| Christine Paulin-Mohring | Université Paris-Saclay | |
| examiners | Michael Mendler | Bamberg University |
| César Muñoz | NASA | |
| Xavier Rival | Inria | |
| Yannick Zakowski | Inria |
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.
The source code of the associated formal development is available here under Inria non-commercial license.