Back to compsys-tools (demo machine)
Back to Compsys Homepage

WTC Toolsuite Benchmarks

Compsys Team, LIP

Last updated : Feb., 11th 2015

WTC Compsys Benchmark - V2 2015

Looking for the WTC benchmarks V2 ? click here.

About this document

This document gives source code and results for INRIA research reports number 7037 ([ADF+09]) and [ADFG10], and for the SAS 2010 conference paper you can find there (preprint).

1  What does WTC tool suite compute ?

The toolsuite computes the estimated worst computational time complexity of a C code.

2  Quick Start

The tool suite is made of three parts :

More details of the techniques can be found in [ADF+09].

Usage

A typical use of the toolsuite on foo.c :

c2fsm foo -fst -cut -s// generates foo.fst
aspic -ranking foo.fst // generate invariants in foo.fstb
rank foo.fstb // termination and WTC

Or, equivalently, use the shell script :

./testone foo 

These tools have a demonstrator there

3  Benchmarks

Preliminary results

This tool chain has been tested on a large set of benchmarks from the literature. Most of the examples were collected in [CCG+08] from many other papers dealing with termination analysis. They can be found at the following web address:

http://www.eecs.qmul.ac.uk/~aziem/esop.html.

The results are summarized in Figure 13Experimental resultstable.1. All thise result files are now in this archive The test cases we developed for checking our algorithm are marked by ♣. The first two columns identify the test cases. The symbol ♣ indicates a test case we developed to check our algorithm. Columns 3 to 5 give statistics about the (generated) automaton: number of relevant variables, of control points, of transitions. The next column gives the dimension of the ranking function found by our algorithm. The next two columns give the timing measurements on a 2 GHz Pentium with 1 GByte of memory running Debian 2.6. When no time is given in the c2fsm column, it means that the translation was done by hand (mainly because c2fsm cannot handle recursive calls yet). The “Analysis” measures include the invariants computation time from the Aspic file, the computation of the ranking function, and the evaluation of the WCC. In general, the WCC is the maximum of several parametric expressions valid on different domains of the program imputs. To make the table simpler, the last column gives only the expression that can reach the maximum value.


NameRefVarsStatesTransdimρTime(c2fsm) (s)Time (Analysis)WCCC
easy1[CCG+08]34510.60.243
easy2[CCG+08]33310.40.07z0+3
ackermann[BAL07]2771N/A0.074m0+5
terminate[CS01]31110.60.08i0+j0+k0+102
gcd[]25110.80.2x0+y0+2
rsd33410.80.2ro2/2+5r0/2+5
nd_loop24610.60.0522
wcet223510.70.1555−12i0
relation124410.80.144
ndecr24410.40.08i0+2
random2d[CCG+08]5102111.71.16N0+3
random1d[CCG+08]34620.70.1max+3
wise261020.80.11|x0y0|+1
wcet136821.40.25n0+2
exmini43620.60.1104+k0j0x0
aaron2[CCG+08]361020.90.22(x0y0)+5
while233420.60.1N02+N0+3
cousot9[Cou05]34520.70.25/2 N2 + 7/2 N+3
loops[PR04]34520.80.15N2N+5
complex[GJK09]241121.30.281560−9b0−45a0
ax43630.90.16N02N0 + 2
perfect[]451231.10.35x02/2+3x0/2+2
nestedLoop[GJK09]651231.31.3n0m0+2N0+n0+3
counterex1451330.81.1x0+2
determinant[]4674N/A0.15N3/3+N2/2+N/6+3
maccarthy91[CS02]451821.61.21733/3 - 61/11 x
speedpldi2[GJK09]44920.90.12n0m0+3
speedpldi3[GJK09]4611310.3n0m0+n0+4
speedpldi4[GJK09]361120.80.32n0−2m0+5
speedFails4[GJK09]541020.70.4n0x0+4
Sorting programs
realselect751031.00.4N2/2+3N/2+1
insertsort36720.60.22N2/2+3N/2+1
sipmabubble[CCG+08]4101730.80.33N2+2N+3
realbubble651131.20.4N2+2
realshellsort881341.01.1N3/6−N/6
realheapsort101131332.84N2−11N+9
Table 1: Experimental results

Comments

In all test cases of Table 13Experimental resultstable.1, we were able to prove termination, even for nondeterministic examples like random2d. Nested loops are correctly handled, and we find multi-dimensional rankings for them. The case of recursion is often handled by making assumptions about (the values of) the variables after a recursive call (for instance we assume the result of ackermann is positive).

We were also able to prove the termination of some classical sortings algorithms. The rankings for these codes may seem of the wrong dimensions, but the additional dimensions have constant values and the order of magnitude of the WCC are still as expected, e.g., O(N2) for bubblesort. For heapsort, our algorithm finds an O(N2) WCC instead of the correct O(N log2N), see the research report for an explanation. However, we are for the moment unable to prove the termination of mergesort due to scalability reasons. We also point out that our algorithm for the elimination of useless variables is still rudimentary. We therefore manipulate polyhedra of dimensions higher than needed. In addition, since the termination of concurrent programs sometimes depends on a fairness hypothesis, we were unable to solve some of the examples of [PR04]. We found the precision of our algorithm to be strongly dependent on the quality of the invariants, and also the quality of the affine approximation of some (non affine) affectations in the C programs.

References

[ADF+09]
Christophe Alias, Alain Darte, Paul Feautrier, Laure Gonnord, and Clément Quinson. Program Termination and Worst Time Complexity With Multi-Dimensional Affine Ranking Functions. Research Report 7037, INRIA, september 2009.
[ADFG10]
Christophe Alias, Alain Darte, Paul Feautrier, and Laure Gonnord. Bounding the computational complexity of flowchart programs with multi-dimensional rankings. Research Report 7235, INRIA, 03 2010.
[BAL07]
Amir M. Ben-Amram and Chin Soon Lee. Program termination analysis in polynomial time. ACM Transactions on Programming Languages and Systems (TOPLAS), 29(1):5, 2007.
[Brad:05b]
Aaron A. Bradley, Zohar Manna, and Henny B. Sipma. The polyranking principle. In 32nd International Colloquium on Automata, Languages and Programming (ICALP), volume 3580 of Lecture Notes in Computer Science, pages 1349–1361. Springer Verlag, July 2005.
[manna:termination2005]
Aaron R. Bradley, Zohar Manna, and Henny B. Sipma. Termination analysis of integer linear loops. In 16th International Conference on Concurrency Theory (CONCUR), volume 3653 of Lecture Notes in Computer Science, pages 488–502. Springer Verlag, August 2005.
[CCG+08]
Aziem Chawdhary, Byron Cook, Sumit Gulwani, Mooly Sagiv, and Hongseok Yang. Ranking abstractions. In 17th European Symposium on Programming (ESOP’08), volume 4960 of Lecture Notes in Computer Science, pages 81–92, Budapest, April 2008. Springer Verlag.
[Cou05]
Patrick Cousot. Proving program invariance and termination by parametric abstraction, Lagrangian relaxation, and semidefinite programming. In 6th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI’05), volume 3385 of Lecture Notes in Computer Science, pages 1–24, Paris, January 2005. Springer Verlag.
[CS01]
Michael Colón and Henny Sipma. Synthesis of linear ranking functions. In 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’01), volume 2031 of Lecture Notes in Computer Science, pages 67–81. Springer Verlag, 2001.
[CS02]
Michael A. Colón and Henny B. Sipma. Practical methods for proving program termination. In 14th International Conference on Computer Aided Verification (CAV), volume 2404 of Lecture Notes in Computer Science, pages 442–454. Springer Verlag, January 2002.
[GJK09]
Sumit Gulwani, Sagar Jain, and Eric Koskinen. Control-flow refinement and progress invariants for bound analysis. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’09), pages 375–385, Dublin, 2009. ACM.
[PR04]
Andreas Podelski and Andrey Rybalchenko. A complete method for the synthesis of linear ranking functions. In Bernhard Steffen and Giorgio Levi, editors, Verification, Model Checking, and Abstract Interpretation (VMCAI’03), volume 2937 of Lecture Notes in Computer Science, pages 239–251. Springer Verlag, 2004.

This document was translated from LATEX by HEVEA.