Validating Dominator Trees for a Fast, Verified Dominance Test
Proofs and experiments
Download the Coq development
and browse our experiments' results (please wait while loading).
- 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)
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.
- Unzip the archive
- Compile compcertSSA
- Run experiments (after having compiled compcertSSA)
cd compcertSSA_itp15 (if necessary)
then read benchs/bench_dom.html with a web browser.