Validating Dominator Trees for a Fast, Verified Dominance Test
Proofs and experiments

Paper

Validating Dominator Trees for a Fast, Verified Dominance Test. S. Blazy, D. Demange and D. Pichardie. ITP 2015. [.pdf].

Source code

Download the corresponding Coq development snapshot.

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

CompCertSSA main web page.

Main files

• DomTest.v: the main development that we describe in our paper (I-DT and I-DT-NATIVE)
• Dom.v: some libraries about dominance
• DomCompute.v: the AC algorithm as implemented in CompCertSSA (I-AC)
• DomAC.ml: the AC algorithm as implemented the CPP'12 paper (I-ACZ)
• DomKildallCHK.ml: the CHK algorithm as implemented the CPP'12 paper (I-CHK)

Experiments

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

The version of Coq used in this work is version 8.4pl2 (June 2013) compiled with OCaml 4.01.0.

1. Unzip the archive
2. Compile compcertSSA

   	  cd compcertSSA_itp15
   	  ./configure ia32-macosx 
   	  make all

   or

   	  cd compcertSSA_itp15
   	  ./configure ia32-linux
   	  make all

3. Run experiments (after having compiled compcertSSA)

   	  cd compcertSSA_itp15 (if necessary)
   	  make dom_benchs

   then read benchs/bench_dom.html with a web browser.