Mechanized Semantics and Verified Compilation for a Dataflow Synchronous Language with Reset
These source files contain the implementation, models, and proof of correctness of a formally verified Lustre compiler backend.
This file contains instructions for (i) using the compiler, (ii) running from local opam installation or from docker, and (iii) cross-references from material presented in the paper to the source files.
The examples/
subdirectory contains another readme file presenting several
example programs that can be used to test the compiler.
We are still working on the normalization pass, which means that Lustre
source programs must currently be manually normalized (each fby
and
application
must be given its own equation; merge
and if
constructs
may only appear at the top level of an expression; output variables cannot
be defined directly by fby
equations). Also, the ->
and pre
operators
used in many Lustre programs are not yet treated. An equation like
x = e1 -> e2
must instead be "manually compiled" into
x = if init then e1 else e2
init = true fby false
and an uninitialized delay pre e
must be replaced by an initialized one
0 fby e
.
Compiler error messages are still very brutal. In particular the parser only reports syntax errors with a line number and character offset. We will implement more helpful messages when we have finalized one or two remaining details of the final (unnormalized) language.
Building the compiler
We describe two ways of building Vélus:
- using a Docker container environment, which is easier and still allows read/write access to the source files, or
- using a manual local installation, which is better if one wants to interactively run the Coq proofs.
If you cloned the repository, do not forget to run git submodule update --init
to update the sub-module CompCert.
In both cases be aware that the building process can take almost 25min on a dual core Intel Core i7-6600U.
Docker
The script rundocker.sh
retrieves a container from the Docker Hub (~1Gb),
starts the container, compiles the development (thus checking the proofs) and
gives you access to a Bash shell from which you will be able to run the
compiler.
The container accesses the present files: you can transparently edit them from the host and compile them in the guest.
Local installation
Prerequisites
Vélus builds on the following dependencies:
- 4.03 ≤ OCaml ≤ 4.07.1
- Coq = 8.9.0
- 20161201 ≤ Menhir ≤ 20181113
- OCamlbuild ≥ 0.14.0
We recommend installing the opam OCaml package manager to install the dependencies as follows. In the case where the version of OCaml available in your system package manager is too old, you should still be able to install a newer version by using an opam switch.
opam init # if running opam for the first time
opam switch create 4.07.1 # create a global switch
eval $(opam env) # update PATH
opam update # sync opam database
opam install coq.8.9.0 menhir.20181113 ocamlbuild # install dependencies
Build
Type ./configure [options] <target>
where <target>
is one of the list given
in the CompCert manual,
e.g., x86_64-linux
.
The configuration script uses the same options as CompCert's, except one
optional -compcertdir
to specify the CompCert directory.
This will set up the configuration for both the Vélus development and the
CompCert development (in the subdirectory CompCert/
by default).
Then, typing make
will launch the building process of CompCert and Vélus.
Invocation
The compiler can be called with:
./velus <options> <sourcefile.ext>
Options are described in the output of ./velus -h
.
In particular, the flags -dstc
, -dobc
and -dclight
enable the generation
of Stc, Obc and Clight intermediate files.
The flag -nofusion
is used to disable the fusion optimization.
On success, the compiler will output an assembly file <sourcefile.s>
.
The compiler can be tested against two test suites:
make runexamples # run the compiler on programs in ./examples/
make runtests # run the compiler on programs in ./tests/
The programs in ./examples/
are described in a dedicated readme.md
.
In particular, the examples nav.lus
, ppdp00.lus
and stopwatch_reset.lus
use the modular reset construct, as well as the test ok_resetsoup.lus
.
If generated with the -sync
option, the generated assembly file can be further
compiled to executable code with user IO loop by calling:
CompCert/ccomp -stdlib CompCert/runtime <sourcefile>.sync.c <sourcefile>.s
Thus the example of the paper can be executed with the following:
./velus -sync examples/nav.lus
CompCert/ccomp -stdlib CompCert/runtime examples/nav.sync.c examples/nav.s
./a.out
Lemmas references
The following table gives the names of the Coq results corresponding to the numbered lemmas in the paper, and the files where the are stated and proved. Note that the lemma 3.5 does not correspond to a particular Coq result: it is given in the paper for clarity but only appear inside another proof in the development.
Lemma | Name | Link |
---|---|---|
2.1 | sem_msem_node | NLustre/NLMemSemantics.v |
2.2 | msem_sem_node | NLustre/NLMemSemantics.v |
2.3 | msem_node_absent_until | NLustre/NLMemSemantics.v |
3.1 | sem_system_absent | Stc/StcSemantics.v |
3.2 | msem_node_initial_state | NLustreToStc/Correctness.v |
3.3 | correctness | NLustreToStc/Correctness.v |
3.4 | correctness_loop | NLustreToStc/Correctness.v |
3.6 | exp_correct | StcToObc/Correctness.v |
3.7 | reset_spec | StcToObc/Correctness.v |
3.8 | correctness | StcToObc/Correctness.v |
3.9 | correctness_loop_call | StcToObc/Correctness.v |