WTC Toolsuite BenchmarksCompsys Team, LIPLast updated : Feb., 11th 2015 |
Looking for the WTC benchmarks V2 ? click here.
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).
The toolsuite computes the estimated worst computational time complexity of a C code.
The tool suite is made of three parts :
More details of the techniques can be found in [ADF+09].
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
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:
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.
Name Ref Vars States Trans dimρ Time(c2fsm) (s) Time (Analysis) WCCC easy1 [CCG+08] 3 4 5 1 0.6 0.2 43 easy2 [CCG+08] 3 3 3 1 0.4 0.07 z0+3 ackermann [BAL07] 2 7 7 1 N/A 0.07 4m0+5 terminate [CS01] 3 1 1 1 0.6 0.08 i0+j0+k0+102 gcd [] 2 5 1 1 0.8 0.2 x0+y0+2 rsd ♣ 3 3 4 1 0.8 0.2 ro2/2+5r0/2+5 nd_loop ♣ 2 4 6 1 0.6 0.05 22 wcet2 ♣ 2 3 5 1 0.7 0.15 55−12i0 relation1 ♣ 2 4 4 1 0.8 0.14 4 ndecr ♣ 2 4 4 1 0.4 0.08 i0+2 random2d [CCG+08] 5 10 21 1 1.7 1.1 6N0+3 random1d [CCG+08] 3 4 6 2 0.7 0.1 max+3 wise ♣ 2 6 10 2 0.8 0.11 |x0−y0|+1 wcet1 ♣ 3 6 8 2 1.4 0.25 n0+2 exmini ♣ 4 3 6 2 0.6 0.1 104+k0−j0−x0 aaron2 [CCG+08] 3 6 10 2 0.9 0.2 2(x0−y0)+5 while2 ♣ 3 3 4 2 0.6 0.1 N02+N0+3 cousot9 [Cou05] 3 4 5 2 0.7 0.2 5/2 N2 + 7/2 N+3 loops [PR04] 3 4 5 2 0.8 0.15 N2−N+5 complex [GJK09] 2 4 11 2 1.3 0.28 1560−9b0−45a0 ax ♣ 4 3 6 3 0.9 0.16 N02 − N0 + 2 perfect [] 4 5 12 3 1.1 0.35 x02/2+3x0/2+2 nestedLoop [GJK09] 6 5 12 3 1.3 1.3 n0m0+2N0+n0+3 counterex1 ♣ 4 5 13 3 0.8 1.1 x0+2 determinant [] 4 6 7 4 N/A 0.15 N3/3+N2/2+N/6+3 maccarthy91 [CS02] 4 5 18 2 1.6 1.2 1733/3 - 61/11 x speedpldi2 [GJK09] 4 4 9 2 0.9 0.1 2n0−m0+3 speedpldi3 [GJK09] 4 6 11 3 1 0.3 n0m0+n0+4 speedpldi4 [GJK09] 3 6 11 2 0.8 0.3 2n0−2m0+5 speedFails4 [GJK09] 5 4 10 2 0.7 0.4 n0−x0+4 Sorting programs realselect ♣ 7 5 10 3 1.0 0.4 N2/2+3N/2+1 insertsort ♣ 3 6 7 2 0.6 0.22 N2/2+3N/2+1 sipmabubble [CCG+08] 4 10 17 3 0.8 0.33 N2+2N+3 realbubble ♣ 6 5 11 3 1.2 0.4 N2+2 realshellsort ♣ 8 8 13 4 1.0 1.1 N3/6−N/6 realheapsort ♣ 10 11 31 3 3 2.8 4N2−11N+9
Table 1: Experimental results
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.
This document was translated from LATEX by HEVEA.