Verifying Fast and Sparse SSA-based Optimizations in Coq
Proofs and experiments

Paper

Verifying Fast and Sparse SSA-based Optimizations in Coq. Delphine Demange, David Pichardie, Léo Stefanesco. CC 2015.

Source code

Download the corresponding Coq development snapshot.

Browse our experiments' results (please wait while loading).

CompCertSSA main web page.

Experiments

As indicated on the paper, all tests were done on a MacBook OSX 10.8.5, 2.9GHz Intel Core i7, 8GB 1600MHz DDR3.

The version of Coq used in this work is version version 8.4pl2 (January 2014) compiled on Jan 28 2014 10:19:40 with OCaml 4.01.0.

Experiments have been made with the x86 back-end, on Mac OSX (otherwise, experimental results might slightly differ).

1. Unzip the archive
2. Benchmark results are available when opening compcertSSA_cc15/bench.html in your browser.
3. To re-run the experiments:
   1. Compile compcertSSA

      	  cd compcertSSA_cc15
      	  ./configure ia32-macosx 
      	  make depend
      	  make -j2 all

   2. Run experiments (after having compiled compcertSSA). Recent versions of Xcode (> 5.1.1) might require to invoke the compiler command with -D_VA_LIST flag.

      	  cd compcertSSA_cc15 (if necessary)
      	  cd test 
      	  ./run_benchs.sh 
      	

      then open compcertSSA_cc15/bench.html in your web browser.