"Computing Expected Runtimes for Constant Probability Programs" - Experiments and Proofs

We introduce the class of constant probability (CP) programs and show that classical results from probability theory directly yield a simple decision procedure for (positive) almost sure termination of programs in this class. Moreover, asymptotically tight bounds on their expected runtime can always be computed easily. Based on this, we present an algorithm to infer the exact expected runtime of any CP program.


References

Here is the full version of our paper Computing Expected Runtimes for Constant Probability Programs (including all proofs and a collection of examples to demonstrate the application of our algorithm).


Implementation in KoAT

We implemented our algorithm to determine the exact expected runtime of CP programs in our tool KoAT, which was already one of the leading tools for complexity analysis of (non-probabilistic) integer programs, cf. our corresponding ACM TOPLAS paper. The implementation is written in OCaml and uses the open source Python libraries SymPy and MpMath as back-end for computing the roots of the characteristic polynomial numerically, for solving linear equations, and for the transformation of the complex roots to polar representation. Furthermore, the full version of KoAT also uses the SMT solver Z3 and the invariant generator APRON. However, these tools are not called when computing exact expected runtimes.


Downloading KoAT

We provide our implementation (i.e., a special-purpose version of KoAT) as a Docker container. To use it, you first have to install Docker CE. Docker is available for Windows, Mac, and Linux. After installing Docker CE, please proceed as follows:


Input Format

Our tool uses a special input format. The input is a file with the ending .koat. This file consists of 7 parts, which are described in the following:

  1. The first line specifies that we want to compute the exact runtime of a CP program. Therefore, the first line should be: (GOAL EXACTRUNTIME)

  2. In the second and third line, we specify the loop guard of the simple program. For instance, (GUARDVEC (1,-1)) specifies the vector a from the paper, i.e., it means that we have two program variables x1 and x2 and the guard of the loop is 1*x1 +(-1)*x2 > b where b will be specified in the next line. Note that GUARDVEC has to be a tuple. So it has to be enclosed by round brackets, even if it is one-dimensional.

  3. As already mentioned, the third line specifies the value b in the loop guard, which is an arbitrary integer number. For instance, to set b=2, one has to write (GUARDVAL 2).

  4. The fourth line contains the updates of the program variables in the loop body. The updates are of the form p:c, where p is a rational probability and c is the update tuple which is added to the variables with probability p. As c is a tuple, it has to be enclosed by round brackets, even if it is one-dimensional. The updates are separated by ":+:". For example (UPDATES 1/5:(1,2) :+: 4/5:(-3,0)) means that in each loop iteration, x1 is increased by 1 and x2 is increased by 2 with probability 1/5, whereas x1 is decreased by 3 and x2 stays unchanged with probability 4/5.

  5. The fifth line is optional and specifies the probability for direct termination. It has the form p':d, where p' is a rational probability and d are integer values which lead to direct termination. As d is a tuple, it has to be enclosed by round brackets, even if it is one-dimensional. If the program does not have direct termination, one can omit this line or just write (DIRECTTERMINATION 0:(0,0)). Note that the probabilities of the updates in the fourth line and the probability p' must add up to 1. Otherwise, our implementation stops with an error message. Moreover, it also gives an error message if p' > 0 and d satisfies the loop condition (i.e., if setting the program variables to d does not lead to direct termination).

  6. The next line is used for adjusting the precision. For example, (PRECISION 10) means that our algorithm performs floating point operations with a precision of 10 decimal places (i.e., in this way the user can select the precision used by MpMath for approximating the roots of the characteristic polynomial). This line is optional as well and the default precision is 100 decimal places.

  7. The last line is used for giving an initial state in which we would like to evaluate the exact_runtime. For example, (INITIAL (4,1)) specifies that we are interested in the expected runtime of the program when started in the initial state x1=4 and x2=1. This line is optional. When it is provided, in addition to the general expected runtime the expected runtime evaluated in the initial state is computed.
Below, we provide input files for all examples mentioned in the paper. "Input Format-Example" is the example that we used to explain the input format above.


Output Format

Our tool generates an output prompted to the console. This output consists of up to 6 parts, which are described in the following:

  1. The first line begins with RESULT and contains the expected runtime expressed in the program variables. Here, we only consider the expected runtime for inputs that satisfy the loop condition (for other inputs, the runtime is always 0).

  2. If an initial state was specified which violates the loop guard, the second line is WARNING: For the given initial values the program is not executed at all. If no initial state was specified or the entered initial state does not violate the loop guard, this line is of course omitted.

  3. The third line contains the time needed for the computation given in seconds. It starts with TIME. Note that the displayed time is the time SageMath needs to perform the steps of the algorithm presented in the paper. The times (one or two seconds) for starting the container and for starting SageMath are not taken into account.

  4. If an initial state was specified, the next line contains the expected runtime evaluated in the given initial values. The line begins with EVALUATION.

  5. The next line contains the upper bound we gave in our paper for the given program, i.e., a constant if the program has direct termination (cf. Thm. 10) and an affine term if the program has no direct termination (cf. Thm. 21). The line starts with UPPER BOUND.

  6. If the program has no direct termination, the last line presents the linear lower bound (cf. Thm. 21) for the expected runtime, which is made clear by the keyword LOWER BOUND.


Example Files

Below are all examples from the paper, including the examples in the appendix. They are provided in KoAT's input format that we described above. Moreover, we also provide the resulting output of our implementation for each of the examples when running the tool on an Intel Core i7-6500 with 8 GB memory. In fact, each example could be handled in less than 1 second.


Executing KoAT

To run KoAT, please proceed as follows:


You can also test our implementation on the examples listed above without file sharing. To do so please proceed as follows: