A program equivalence checker
|
Description
The tar ball zyva.tar.gz contains source code
and exemples for the program equivalence checker.
After uncompressing (using gunzip) and untaring (using
tar xf), build is done by simply typing “make”,
this produces the checker “zyva”.
Benchmark
Timings are wall-clock times in seconds, measured on a lightly loaded 1GHz
PC, running Linux Red-Had 7.2.
One program in directory inputs is compared with the
(equivalent) program with the same name in directory opt.
For some of the inputs used during the contest judging phase, the
following table shows its approximate size and the number of variables
in it, and
the running times of zyva, both with optimizations enabled
and disabled.
| |
alpha2 |
ifjarboe |
ifparrot |
mips0 |
pentium |
sim-intel.rtl0 |
sim-sparc.rtl0 |
sparc3 |
| Size (Kb) |
96 |
24 |
8 |
40 |
2936 |
1044 |
140 |
136 |
| nvars |
13 |
3 |
8 |
16 |
25 |
609 |
1112 |
12 |
| zyva -O |
0.05 |
0.01 |
0.01 |
0.05 |
8.14 |
0.54 |
0.31 |
0.08 |
| zyva |
0.23 |
0.01 |
0.01 |
7.95 |
N/A |
0.81 |
N/A |
527.24 |
Only some signifant timings are shown above, here are the timings of
another run of the checker (with optimizations enabled) on all contest inputs:
alpha0.icfp: 0.00
alpha1.icfp: 0.00
alpha2.icfp: 0.05
busker.icfp: 0.01
cat.icfp: 0.00
ifbusker.icfp: 0.01
ifcat.icfp: 0.01
ifjarboe.icfp: 0.01
ifparrot.icfp: 0.01
jarboe.icfp: 0.01
mips0.icfp: 0.05
parrot.icfp: 0.01
pentium0.icfp: 0.00
pentium1.icfp: 0.00
pentium2.icfp: 0.00
pentium3.icfp: 0.01
pentium4.icfp: 0.00
pentium.icfp: 8.14
pessbusker.icfp: 0.01
pesscat.icfp: 0.01
pessjarboe.icfp: 0.04
pessparrot.icfp: 0.02
sim-intel.rtl0.icfp: 0.54
sim-sparc.rtl0.icfp: 0.31
sim-sparc.rtl1.icfp: 0.01
sim-sparc.rtl2.icfp: 0.01
sparc0.icfp: 0.00
sparc1.icfp: 0.00
sparc2.icfp: 0.00
sparc3.icfp: 0.08
xs.rtl0.icfp: 0.01
xs.rtl0.mc.icfp: 0.01
This document was translated from LATEX by
HEVEA.