Room 206 (2nd floor, badged access)
8 juin 2023 - 14h00
Verifying a compiler for a synchronous dataflow language with state machines in Coq
par Basile Pesin de Inria PARKAS - ENS-Ulm
Abstract: The Velus project is a formalization of a synchronous block-diagram language, based on elements from Lustre and Scade 6, in the Coq interactive theorem prover.
It includes a relational formalization of the dataflow semantics of the language, a compiler that uses the CompCert C compiler as a backend to produce assembly code, and an end-to-end proof that the dataflow semantics of the source program is preserved by the trace-based semantics of the generated assembly. Our recent work extends Velus with higher-level constructs that are useful to define modal behaviors: switched blocks, shared variables (eg last x), reset blocks, and state machines.
This talk will present this work, including the novel semantic model we developed to integrate these block-based constructions into the existing stream-based model. We will discuss the dynamic properties of this model, that we were able to prove using a verified dependency analysis and a custom induction scheme for programs that do not contain dependency cycles. We will also show how we compile these constructs. We will outline the adaptations that must be done to the standard source-to-source rewriting schemes, and the invariants necessary to prove them correct in the context of an interactive theorem prover. Finally, we will explain how the backend of the compiler also needs to be adapted for efficient compilation of these constructs.
