A Fast Verified Liveness Analysis in SSA form
Proofs and experiments

Paper

Jean-Christophe Léchenet, Sandrine Blazy, David Pichardie. A Fast Verified Liveness Analysis in SSA form. IJCAR 2020. To appear.
[.pdf]

Source code

Download the Coq development and browse our experiments' results.

Main files

• The following files implement liveness checking.
  • The precomputation part is made up of three files. Each file is accompanied by two files: one containing lemmas ("proof") and one containing the main theorems ("thm") about the objects defined in the file. Only these main theorems are used in the rest of the Coq development, so reading the (sometimes technical) lemmas is not necessary.
    • SSAfastliveprecomputeRT (proof, thm): the first step of the precomputation that computes R and T↑
    • SSAfastliveprecomputeTT (proof, thm): the second step of the precomputation that computes T from T↑
    • SSAfastliveprecompute (proof, thm): the precomputation step, based on the two preceding files
  • SSAfastlive (proof): the online part, based on the precomputation part
• SSAfastliveutils: definitions and properties of objects used in the other files
• SSAlive: the reference data-flow based liveness analysis
• SSAfastlivewrap and SSAlivewrap: files that artificially add the liveness analyses as passes in CompCertSSA, for testing purposes

Experiments

As indicated in the paper, all tests were done on a Dell Latitude 7490 with an Intel Core i7-8650U processor at 1.90GHz and 16 GB of memory.

The version of Coq used in this work is version 8.7.2 (February 2018) compiled with OCaml 4.07.1. Our development depends on library menhir, version 20180528 (please note that recent versions of menhir are not compatible).

0. Install the dependencies
   We recommend using the opam package manager. The following snippet creates a new environment (called a "switch") named "CompCertSSA", with OCaml version 4.07.1, and installs the correct versions of coq and menhir inside this environment.

         opam switch create CompCertSSA 4.07.1
         eval $(opam env)
         opam install coq.8.7.2 menhir.20180528

1. Decompress the archive
2. Compile compcertSSA
   configure must be given the target architecture. For instance,

         cd compcertSSA_ijcar20/compcertSSA
         ./configure x86_64-linux
         make all

   or

         cd compcertSSA_ijcar20/compcertSSA
         ./configure x86_64-macosx
         make all

3. Run experiments (after having compiled compcertSSA)
   Note that running the experiments takes about 30 minutes.

         cd compcertSSA_ijcar20/benchs
         ./make_ten_benchs.sh

4. Display experiments
   Due to security restrictions of web browsers, just opening the html file does not work. The file has to be delivered by a server. Here is one way to do it.

         cd compcertSSA_ijcar20/benchs
         python3 -m http.server --bind localhost

   Then access with your favorite browser the address http://localhost:8000/benchs.html.