Inferring Expected Runtimes Using Sizes

This website contains additional information on our article “Inferring Expected Runtimes of Probabilistic Integer Programs Using Expected Sizes”:

Abstract

We present a novel modular approach to infer upper bounds on the expected runtime of probabilistic integer programs automatically. To this end, it computes bounds on the runtime of program parts and on the sizes of their variables in an alternating way. To evaluate its power, we implemented our approach in a new version of our open-source tool KoAT.

References

The full version of our paper can be found on arXiv. The paper itself will appear at TACAS 2021.

Examples

The examples can be downloaded here. The provided zip file contains all inputs for KoAT, Absynth, and eco-imp as well as plots of the corresponding transition systems automatically generated by our tool KoAT and Graphviz.

Artifact

An artifact including the examples from the paper and a static binary can be downloaded here. The provided zip-file contains a documentation on how to reproduce our experimental evaluation.

The version of the artifact which was accepted at the TACAS 21 Artifact Evaluation can be found here. This version contains five examples less. Additionally, in this version we did not compare with eco-imp since it was not yet published.

Both versions of “artifact.zip” can be used with the TACAS VM.

Executing the Implementation

Docker

A Docker image containing our implementation can be downloaded here. The image can be loaded into Docker (provided Docker is installed, see here for installation instructions) by changing to the directory where you stored koat_docker.tar and executing:

docker load --input=koat_docker.tar

The Docker image already contains all provided examples. For instance, KoAT can be executed on the example leading.koat by running:

docker run --rm -t koat:probabilistic -i leading.koat

Recall that while we over-approximated the maximum of expressions by their bounds to simplify the presentation in our paper, KoAT also constructs expressions with “max”, which may lead to slightly more precise bounds.

If you want to save KoATs output in a file, this can be achieved by the usual command line instruction, e.g., docker run --rm -t koat:probabilistic -i leading.koat > output.txt.

Moreover, when executing the Docker image with run-all instead of -i leading.koat, i.e., docker run --rm -t koat:probabilistic run-all, KoAT analyzes all provided examples.

Additional examples can be added by mounting a directory. Assume that the directory /home/user/examples contains an example named myExample.koat. Then

docker run --rm -v '/home/user/examples:/home/koat2/examples:ro' -t koat:probabilistic -i myExample.koat

first mounts the directory in the Docker container and then executes KoAT on myExample.koat.

Static Binary

A static ELF binary, containing all necessary dependencies, can be downloaded here. Please make sure that the binary is executable by running chmod +x koat-static. KoAT can then be run on an example by executing

/PATH/TO/KOAT/koat-static analyse -i /PATH/TO/EXAMPLES/example.koat

Additional Flags

Both the Docker image and the static binary can be invoked with additional flags, e.g., for choosing only certain preprocessors, for choosing a different output format, for getting information on the computation process, and many more. To see a detailed description of these flags run

docker run koat:probabilistic --help

when using the Docker image or

/PATH/TO/KOAT/koat-static analyse --help

when using the static binary.

For instance, to obtain the automatically generated proof of KoAT instead of just the result of the analysis, one has to add the flag -r all at the end of the command (and to get an output in the format of the Termination and Complexity Competition, one has to add the flag -r termcomp).

Source Code

The most current version of KoAT is available on GitHub. The source code of our official release version is here.

Web Interface

Our implementation can also be tested via a web interface using the input format described below. (This web interface is provided via a special version of the web site of our tool AProVE).

  • The window “Load Example” shows the PIP that is currently analyzed. The user can modify the PIP or replace it by a new one.
  • Moreover, via the “Load Example” button, you can directly choose any of the examples from the collection used in our evaluation, and run KoAT on it.
  • In addition, one can also “Upload a File” of a PIP to analyze.
  • By choosing “Detailed Format”, one can obtain the automatically generated proof of KoAT instead of just the result of the analysis.
  • After viewing the result of KoAT, “Return to program input” takes you back to the web page with the input PIP.

Input Format

We use an adapted version of the format for Integer Transition Systems (see for example here or here) from the Termination and Complexity Competition for our PIPs. The leading example from our paper is represented by the following code, where the first and the third transition have the cost 0.

(GOAL EXPECTEDCOMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS f))
(VAR x y)
(RULES
  f(x,y) -{0}> g(x,y)
  g(x,y) -> 0.5:g(x-1,y+x) :+: 0.5:g(x,y+x) :|: x>0
  g(x,y) -{0}> h(x,y)
  h(x,y) -> h(x,y-1) :|: y>0
)
  • The first line (GOAL EXPECTEDCOMPLEXITY) indicates that we would like to compute upper bounds on the expected runtime of the given PIP.
  • The second line (STARTTERM (FUNCTIONSYMBOLS f)) specifies that f is the start location of the PIP.
  • The third line (VAR x y) specifies that the variables used in the system are x and y.
  • The fourth line (RULES ... indicates that we now state the general transitions of our system. It is ended by a closing parenthesis ) in the last line of the example code above.
  • The remaining lines contain the general transitions of the program in the form LHS -{COST}> RHS (:|: GUARD) or LHS -> RHS (:|: GUARD).
    • LHS is the start location of the general transition including the variables to be updated here, e.g., f(x,y). Locations are arbitrary alpha-numerical strings.
    • COST is a non-negative integer constant that bounds the cost of the general transition. This is optional. If omitted, the cost defaults to 1.
    • RHS specifies the distribution over transitions in the general transition.
      • Elements of the transition are given by p:target(up1,...,upn) and are separated by :+:. This means that the variable x1 is updated to up1,…, the variable xn is updated to upn, and the system transitions to location target with probability p.
      • Probabilities are rational numbers strictly greater than 0 which must add up to 1.
      • In case of a singleton general transition, the probability can be omitted and then defaults to 1, e.g., f(x,y) -{0}> g(x,y).
      • Updates are polynomial expressions. If the updates contain variables which are not given on the left-hand side, they are treated as non-deterministic (those variables can be restricted in the guard).
        • For example, g(x,y) -> 0.5:g(x-1,y+x) :+: 0.5:g(x,y+x) means that from the start location g, with probability 0.5 x is set to x-1 and y is set to y+x, and with the remaining probability 0.5 x is set to x and y is set to y+x.
        • For example, g(x,y) -> 1:g(z,y) means that from the start location g, the PIP chooses the transition to location g where the first variable x is updated non-deterministically and the second variable y stays the same.
      • Updates can also be distribution functions. In our semantics, the value drawn from this distribution is added to the current value of the variable.
        • For example, g(x,y) -> g(x,GEOMETRIC(0.5)) means that in the transition from the location g, the variable x stays the same whereas y is increased by a value drawn from a geometric distribution with parameter 0.5.
        • At the moment, we support the following discrete distributions. Here, parameters are integer polynomial expressions, i.e., they may depend on variables, whereas constants are non-negative integers or non-negative rationals. The user has to ensure that their values meet the stated constraints:
    • GUARD is a conjunction (using the connective &&) of linear (in)equalities representing the guard of the transition, e.g., x > 0 or x > 0 && 2 * x + 3 * y = 0. This is optional. If omitted, GUARD defaults to true, e.g., g(x,y) -{0}> h(x,y).

Results

The tables below contain the results of our experiments with our tool KoAT and the tools Absynth, and eco-imp. The output of KoAT always has the form WORST_CASE(a,b) where a is a lower bound and b is an upper bound on the expected (worst-case) runtime. Depending on the output format chosen, KoAT only depicts asymptotic bounds or both concrete and asymptotic bounds. Currently, KoAT can only infer upper bounds (i.e., the lower bound is always constant).

By clicking on a result in the table, the corresponding output of the tool is shown. Here, the result of KoAT also contains a visualization of the corresponding PIP as a graph. We refer to Sect. 6 in our paper and Sect. A.2 in our technical report for a description of the experiments.

Results on Absynth’s examples

Example KoAT Absynth eco-imp
2drwalk O(n) : 7.69 s O(n) : 1.55 s O(n) : 0.05 s
bayesian O(n) : 6.90 s O(n) : 0.22 s O(n) : 0.01 s
ber O(n) : 0.19 s O(n) : 0.02 s O(n) : 0.01 s
bin O(n) : 0.20 s O(n) : 0.23 s O(n) : 0.02 s
C4B_t09 O(n) : 0.46 s O(n) : 0.05 s O(n) : 0.02 s
C4B_t13 O(n) : 1.13 s O(n) : 0.03 s O(n) : 0.02 s
C4B_t15 O(n) : 0.43 s O(n) : 0.04 s ∞ : 0.34 s
C4B_t19 O(n) : 0.49 s O(n) : 0.04 s O(n) : 0.01 s
C4B_t30 O(n) : 27.49 s O(n) : 0.03 s ∞ : 0.03 s
C4B_t61 O(n) : 0.26 s O(n) : 0.03 s O(n) : 0.02 s
complex O(n²) : 1.52 s O(n²) : 2.49 s O(n²) : 0.05 s
condand O(n) : 0.27 s O(n) : 0.01 s O(n) : 0.01 s
cooling O(n) : 0.79 s O(n) : 0.06 s O(n) : 0.03 s
coupon O(1) : 1.66 s O(1) : 0.08 s O(1) : 0.01 s
cowboy_duel O(1) : 0.38 s O(1) : 0.03 s O(1) : 0.01 s
cowboy_duel_3way O(1) : 2.27 s O(1) : 0.16 s O(1) : 0.01 s
fcall O(n) : 0.64 s O(n) : 0.02 s O(n) : 0.01 s
filling O(n) : 2.67 s O(n) : 0.41 s O(n) : 0.02 s
geo O(1) : 0.35 s O(1) : 0.02 s O(1) : 0.01 s
hyper O(n) : 0.19 s O(n) : 0.03 s O(n) : 0.01 s
linear01 O(n) : 0.22 s O(n) : 0.02 s O(n) : 0.01 s
miner O(n) : 1.91 s O(n) : 0.06 s O(n) : 0.01 s
multirace O(n²) : 0.73 s O(n²) : 6.72 s O(n²) : 0.03 s
no_loop O(1) : 0.33 s O(1) : 0.02 s O(1) : 0.00 s
pol04 ∞ : 0.87 s O(n²) : 0.04 s O(n²) : 0.02 s
pol05 ∞ : 0.63 s O(n²) : 1.11 s O(n²) : 0.02 s
pol06 ∞ : 2.95 s O(n²) : 5.72 s O(n²) : 0.06 s
pol07 O(n²) : 0.66 s O(n²) : 3.16 s O(n²) : 0.03 s
prdwalk O(n) : 0.33 s O(n) : 0.05 s O(n) : 0.01 s
prnes O(n) : 1.56 s O(n) : 0.06 s O(n²) : 0.24 s
prseq O(n) : 0.46 s O(n) : 0.05 s O(n) : 0.02 s
prseq_bin O(n) : 1.54 s O(n) : 0.09 s O(n) : 0.03 s
prspeed O(n) : 1.43 s O(n) : 0.05 s O(n) : 0.03 s
race O(n) : 0.31 s O(n) : 0.19 s O(n) : 0.05 s
rdbub ∞ : 0.59 s O(n²) : 0.16 s O(n²) : 0.02 s
rdseql O(n) : 0.44 s O(n) : 0.03 s O(n) : 0.02 s
rdspeed O(n) : 0.58 s O(n) : 0.04 s O(n) : 0.03 s
rdwalk O(n) : 0.39 s O(n) : 0.02 s O(n) : 0.01 s
rfind_lv O(1) : 0.26 s O(1) : 0.02 s O(1) : 0.01 s
rfind_mc O(n) : 0.45 s O(n) : 0.04 s O(n) : 0.01 s
robot O(n) : 27.93 s O(n) : 1.76 s O(n) : 0.02 s
roulette O(n) : 1.21 s O(n) : 0.65 s O(n) : 0.09 s
sampling O(n) : 1.78 s O(n) : 2.29 s O(n) : 0.01 s
simple_recursive O(n) : 0.36 s O(n) : 0.02 s O(n) : 0.01 s
sprdwalk O(n) : 0.19 s O(n) : 0.02 s O(n) : 0.01 s
trader ∞ : 1.29 s O(n²) : 0.92 s O(n²) : 0.87 s

Results on our examples

Example KoAT Absynth eco-imp
Fig. 5 O(n) : 0.22 s ∞ : 0.46 s ∞ : 0.44 s
Fig. 6 O(1) : 0.70 s ∞ : 0.10 s O(1) : 0.03 s
Fig. 7 O(1) : 0.17 s O(1) : 0.01 s O(1) : 0.00 s
alain.c O(n³) : 35.47 s TO ∞ : 0.33 s
C4B_t132 O(n) : 1.03 s ∞ : 0.10 O(n) : 0.02 s
complex2 O(n²) : 1.21 s ∞ : 85.78 O(n²) : 0.05 s
cousot9 O(n²) : 1.79 s TO TO
ex_paper1.c O(n²) : 28.01 s TO O(n²) : 0.22 s
fib_exp_size EXP : 0.69 s ∞ : 15.32 s ∞ : 0.01 s
geo_race O(n) : 0.25 s ∞ : 0.14 s ∞ : 23.29 s
knuth_morris_pratt.c O(n) : 20.79 s ∞ : 0.40 TO
leading O(n²) : 0.49 s ∞ : 0.74 s ∞ : 30.64 s
leading.1 O(n²) : 0.56 s ∞ : 0.62 s ∞ : 1.25 s
multirace2 O(n²) : 0.68 s TO O(n²) : 0.03 s
neg_init_upd O(n) : 0.40 s ∞ : 0.09 ∞ : 0.03 s
nested_break O(n²) : 1.17 s ∞ : 0.12 ∞ : 0.14 s
nested_rdwalk O(n) : 0.55 s O(n) : 0.03 s O(n) : 0.02 s
nested_size O(n⁵) : 1.53 s TO ∞ : 3.25 s
nondet_countdown O(n) : 0.41 s ∞ : 0.31 s O(n) : 0.02 s
prob_loop ∞ : 0.72 s O(n) : 0.43 s ∞ : 0.03 s
prseq2 O(n) : 0.64 s ∞ : 0.16 s O(n) : 0.02 s
rank3.c O(n²) : 55.88 s TO ∞ : 0.14 s
rdseql2 O(n) : 0.64 s ∞ : 0.12 O(n) : 0.02 s
realheapsort O(n²) : 21.47 s TO ∞ : 0.81 s
selectsort O(n²) : 4.46 s O(n²) : 93.77 s O(n²) : 1.75 s
simple_nested ∞ : 0.72 s ∞ : 1.85 s O(n²) : 0.05 s
spctrm O(n²) : 21.47 s TO TO
trunc_selectsort O(n²) : 3.99 s TO O(n²) : 1.74 s
two_arrays2 O(n) : 7.76 s O(n) : 0.61 s O(n) : 0.03 s