Synchronous block-diagram languages have long been formalized as fixpoints of equations defining stream functions. We apply this approach to a compiler verified in an interactive theorem prover, allowing us to restate its end-to-end correctness theorem: if a program is accepted and has no runtime errors, its input/output behavior is preserved in the generated code. In a functional semantics, it is necessary to model all possible behaviors, including erroneous ones. We show that static typing and dependency analyses correctly rule out all errors except those arising from logical and arithmetic operators. Our definitions supplement existing formal ones, especially for the reset operator, which is both useful in itself and a basis of advanced control structures.
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.
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.
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.
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.
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).
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.
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.
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.
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.
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.
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.
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.
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.