Difference Constraints: An adequate Abstraction for Amortized Complexity Analysis of Imperative Code

Details on the Experimental Evaluation

Tool Comparison

We compared the implementation of our approach (Loopus'15) to the tools KoAT (download 23.01.2015), CoFloCo (download 23.01.2015) and Loopus'14 (implementation of CAV'14 paper). For our experimental comparison we used the program and compiler optimization benchmark Collective Benchmark, which contains a total of 1027 different C files (after removing code duplicates) with 211.892 lines of code. The experiments were performed on a Linux system with an Intel dual-core 3.2 GHz processor and 16 GB memory. We used the following experimental set up:
  • We compiled all 1027 C files in the benchmark into the llvm intermediate representation using clang.
  • We extracted all 1751 functions which contain at least one loop using the tool llvm-extract (comes with the llvm tool suite). Extracting the functions to single files guarantees an intra-procedural setting for all tools.
  • We used the tool llvm2kittel to translate the 1751 llvm modules into 1751 text files in the Integer Transition System (ITS) format read in by KoAT. We ran llvm2kittel using the options '-only-loop-conditions -multi-pred-control' because with these options KoAT and CoFloCo performed better on the resulting ITS.
  • We used the transformation described here to translate the ITS format of KoAT into the ITS format of CoFloCo. This last step is necessary because there exists no direct way of translating C or the llvm intermediate representation into the CoFloCo input format.
  • We decided to exclude the 91 recursive functions in the set because we were not able to run CoFloCo on these examples (the transformation tool does not support recursion), KoAT was not successful on any of them and Loopus does not support recursion.
In total our example set thus comprises 1659 functions.

Our benchmark and the input files for the different tools are available here.

The new version of our tool (Loopus15) is available here.

Amortized Complexity

During our experiments we found the following examples for amortized complexity.

BenchmarkFileFunctionLine
cBenchsecurity_pgp_d/src/random.c cryptRandWriteFile1220
cBenchoffice_ghostscript/src/zfileio.c zwritehexstring_at1512
cBenchoffice_ghostscript/src/gxcht.c set_color_ht1703,1695,1674,1668
SPEC CPU2006hmmer/src/masks.c XNU
SPEC CPU2006perlbench/src/toke.c Perl_scan_vstring
SPEC CPU2006gcc/src/local-alloc.c local_alloc
SPEC CPU2006gcc/src/flow.c update_life_info
SPEC CPU2006gcc/src/loop.c load_mems
SPEC CPU2006gcc/src/reload1.c finish_spills
SPEC CPU2006gcc/src/reload1.c compute_use_by_pseudos
SPEC CPU2006gcc/src/real.c asctoeg
SPEC CPU2006gromacs/src/libxdrf.c xdr3dfcoord
SPEC CPU2006gromacs/src/index.c analyse_other196,193,182,184
SPEC CPU2006cactusADM/src/Cactus/ParseFile.c ParseFile
SPEC CPU2006cactusADM/RobinBoundary.c ApplyBndRobin
SPEC CPU2006h264ref/src/configfile.c Configure


The lines number for the cBench Benchmark refer to the version we prepared for the tool comparison (see above).

SPEC CPU2006 is a comercial benchmark, it can be obtained here.

Further examples for amortized complexity that can also be handled by our previous approach (Loopus'14):

BenchmarkFileFunctionLine
cBenchoffice_ghostscript/src/sfilter1.cs_SFD_process824
cBenchsecurity_pgp_d/src/zinflate.cinflate_stored1144
cBenchsecurity_pgp_d/src/zinflate.cinflate_dynamic1257
cBenchsecurity_pgp_d/src/ztrees.csend_tree1009
cBenchconsumer_jpeg_c/src/jcphuff.cencode_mcu_AC_first1293
cBenchconsumer_jpeg_c/src/jcphuff.cencode_mcu_AC_refine1386
cBenchconsumer_jpeg_c/src/jchuff.cencode_one_block1200
cBenchconsumer_jpeg_c/src/jchuff.chtest_one_block1319
cBenchconsumer_tiff2bw/src/tif_packbits.cPackBitsEncode1092
cBenchoffice_ghostscript/src/scfd.ccf_decode_eol995
cBenchbzip2d/src/compress.csendMTFValues936
cBenchoffice_ispell/src/dump.csubsetdump883