On this web page, we provide the experimental data supporting our claims.
Runtime_Complexity_Innermost_Rewriting.
Our benchmark files are available here:
benchmarks.zip(GOAL COMPLEXITY)(STARTTERM CONSTRUCTOR-BASED)(STRATEGY INNERMOST)
To indicate that runtime complexity of parallel-innermost
rewrite strategies is supposed to be analysed, replace this line by:
(STRATEGY PARALLELINNERMOST)
We used the all.q computer queue
and a timeout of 300 seconds per example.
As far as we are aware, so far there have not been any automated tools able to analyse runtime complexity of parallel-innermost rewriting. However, an upper bound on runtime complexity of innermost rewriting is always also an upper bound on runtime complexity of parallel-innermost rewriting: pircR(n) ≤ ircR(n) holds for all TRSs R.
Thus, as the state of the art for upper bounds of runtime complexity of parallel-innermost rewriting with which to compare our contributions, we used the complexity analysis tools AProVE and TcT (Starexec URL for TcT) from the Termination and Complexity Competition in 2021 to analyse runtime complexity for innermost rewriting. We used the "tct_rci" configuration of TcT from StarExec. The corresponding tool configurations are labelled "AProVE irc" and "TcT irc" in our tables.
We have assessed the following configurations of AProVE and TcT as the state of the art in searching for upper bounds of parallel-innermost complexity. You can find the resulting data from these experiments downloaded from StarExec here:
We implemented our contributions in the complexity analysis tool AProVE. The configuration "AProVE pircR(n) Section 3" includes the techniques from Section 3, and the configuration "AProVE pircR(n) Sections 3 & 4" includes the techniques from both Section 3 and Section 4. We used these configurations to obtain upper and lower bounds on the runtime complexity of parallel-innermost rewriting for the TRSs from our benchmark suite. You can find the data from these experiments here:
| Tool | O(1) | ≤ O(n) | ≤ O(n2) | ≤ O(n3) | ≤ O(n≥4) |
|---|---|---|---|---|---|
| TcT irc | 19 | 145 | 173 | 188 | 188 |
| AProVE irc | 26 | 193 | 301 | 330 | 338 |
| AProVE pirc Section 3 | 26 | 210 | 317 | 346 | 353 |
| AProVE pirc Sections 3 and 4 | 26 | 212 | 318 | 346 | 351 |
The first table
gives an overview over our experimental results for upper bounds.
For each configuration, we state the number of examples for
which the corresponding asymptotic complexity bound could be inferred.
A row "≤ O(nk)" means that the corresponding tools proved a bound
"≤ O(nk)" (e.g., in Table 1 right below, the configuration
"AProVE irc" proved constant or linear upper bounds in 193 cases).
We observe that upper complexity bounds improve in a
noticeable number of cases, e.g., linear bounds on pirc can now be inferred
for 212 TRSs rather than for 193 TRSs (using upper bounds on
ircR as a correct but imprecise over-approximation
for pircR).
The improvement from irc to pirc can be drastic:
for example, for the TRS TCT_12/recursion_10, the
bounds found by AProVE change from an upper bound of sequential
complexity of O(n10) to a (tight) upper bound for
parallel complexity of O(n).
(This TRS models a specific recursion structure, with rules
{ f0(x) → a } ∪
{ fi(x) → gi(x,x), gi(s(x), y) → b(fi-1(y), gi(x,y)) | 1 ≤ i ≤ 10 }, and is highly amenable to parallelisation.)
We observe that adding the
techniques from Section 4 to the techniques from
Section 3 leads to only few examples for which better
upper bounds can be found.
| Tool | Confluent | ≥ Ω(n) | ≥ Ω(n2) | ≥ Ω(n3) | ≥ Ω(n≥4) |
|---|---|---|---|---|---|
| AProVE pirc Sections 3 and 4 | 447 | 307 | 38 | 8 | 1 |
The second table shows our results for lower bounds on pirc. Here we evaluated only our own implementation in AProVE. The reason is that a lower bound on irc is not necessarily also a lower bound for pirc (the whole point of performing innermost rewriting in parallel is to reduce the asymptotic complexity!), so using results by tools that compute lower bounds on irc for comparison would not make sense. We observe that non-trivial lower bounds can be inferred for 307 out of 633 examples. This shows that our transformation from Section 4 produces relative TRSs that are generally amenable to analysis by existing program analysis tools. (A standard concern with transformations for program analysis is that, although correct, their output might be hard to analyse for existing tools. Our experimental results alleviate this concern for the contributions of this paper, both for upper and for lower bounds on pirc.)
| Tool | Θ(1) | Θ(n) | Θ(n2) | Θ(n3) | Total |
|---|---|---|---|---|---|
| AProVE pirc Sections 3 and 4 | 26 | 103 | 5 | 6 | 140 |
Finally, the third table shows that for overall 140 TRSs, the bounds that were found are asymptotically precise.
| Tool | O(1) | ≤ O(n) | ≤ O(n2) | ≤ O(n3) | ≤ O(n≥4) |
|---|---|---|---|---|---|
| TcT irc | 4 | 28 | 39 | 44 | 44 |
| AProVE irc | 5 | 50 | 110 | 123 | 127 |
| AProVE pirc Section 3 | 5 | 65 | 125 | 140 | 142 |
| AProVE pirc Sections 3 and 4 | 5 | 69 | 125 | 139 | 141 |
We again observe that upper complexity bounds improve in a
noticeable number of cases, e.g., linear bounds on pirc can now be inferred
for 69 TRSs rather than for 50 TRSs, an improvement by 38%.
A closer inspection of the results shows that our dedicated analysis
for complexity of parallel rewriting improves upper bounds obtained from
state-of-the-art tools sequential-complexity analysis for 27 TRSs.
Of these 27 TRSs, 15 cannot be handled by tools for sequential complexity
at all. This gives tighter bounds for 27/(127+15) = 19.0% of TRSs
with (now) known upper bounds.
| Tool | Confluent | ≥ Ω(n) | ≥ Ω(n2) | ≥ Ω(n3) | ≥ Ω(n≥4) |
|---|---|---|---|---|---|
| AProVE pirc Sections 3 and 4 | 186 | 133 | 23 | 5 | 1 |
We observe that non-trivial lower bounds can be inferred for 133 out of 294 examples (45.2%).
| Tool | Θ(1) | Θ(n) | Θ(n2) | Θ(n3) | Total |
|---|---|---|---|---|---|
| AProVE pirc Sections 3 and 4 | 5 | 32 | 1 | 3 | 41 |
Finally, the third table shows that for overall 41 of the 234 TRSs, the bounds that were found are asymptotically precise.