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.

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.

The implementation can also be tested via a web interface (see bottom of the page).

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:

  • Start Docker

  • You can download the latest version of the Docker image of KoAT (~150 MB) here. The link directs to the file-sharing system Sciebo, a joint project by 26 German universities. After downloading the file exact_runtime.zip, please change to the directory where you stored the file and execute:

      docker load --input=exact_runtime.zip

    If the Docker image was successfully imported (this may take a minute), Loaded image: aprove/exact_runtime:latest is prompted to your shell.

Input Format

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

  • The first line specifies that we want to compute the exact runtime of a CP program. Therefore, the first line should be: (GOAL EXACTRUNTIME)
  • The second line specifies the variables: (VAR (X1,X2))
  • In the third and fourth line, we specify the loop guard of the simple program. For instance, (GUARDPOLY X1-X2) specifies the scalar product of the vector a and the vector of variables as in 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.
  • As already mentioned, the fourth 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).
  • The fifth 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.
  • The sixth 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).
  • 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.
  • 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 7 parts, which are described in the following:

  • The first line contains either MAYBE (indicating that the expected termination time is infinite) or WORST_CASE(Omega(n^1),O(n^1)) indicating that the program has a linear expected runtime. Here, n is the sum of all absolute values of the program variables. This output format is taken from the annual Termination and Complexity Competition.
  • The second 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).
  • If an initial state was specified which violates the loop guard, the third 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.
  • The fourth line contains the time needed for the computation given in seconds. It starts with TIME. Note that the displayed time is the time SymPy needs to perform the steps of the algorithm presented in the paper. The times for starting the container and for starting Python are not taken into account.
  • If an initial state was specified, the next line contains the expected runtime evaluated in the given initial values. The line begins with EVALUATION.
  • 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.
  • 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:

  • Start Docker.

  • If you are using Windows, please go to the settings of Docker, select “Shared Drives”, and enable sharing for the local drive where you store the example programs that you want to analyze with KoAT.

  • To run KoAT on some example example.koat, please use a shell and change the current directory to the directory containing example.koat.

  • If you are using a Unix-based operating system (e.g., Linux or Mac) or if you are using PowerShell on Windows, just execute the following command in your shell. 
    docker run --mount type=bind,source="$(pwd)",target=/data aprove/exact_runtime -i /data/example.koat

    It executes the Docker image of KoAT on the file example.koat in the current directory. Your current directory is mounted into /data to enable file sharing. The result is printed on your console together with the time (in seconds) needed for computing the result.

  • If you are using cmd.exe on Windows, then instead of the above command, please execute the following command. 
    docker run --mount type=bind,source="%cd%",target=/data aprove/exact_runtime -i /data/example.koat

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

  • Start Docker.

  • To run KoAT on some example listed above, please get the name of the example by clicking on the hyperlink. Let us assume that you would like to analyze input_format.koat.

  • Execute the following command in your shell (independent of your operating system).

    docker run aprove/exact_runtime -i /data/examples/input_format.koat

    It executes the Docker image of KoAT on the file input_format.koat in the directory /data/examples of the Docker image. The result is printed on your console together with the time (in seconds) needed for computing the result.

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 CP that is currently analyzed. The user can modify the CP 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 CP to analyze.
  • After viewing the result of KoAT, “Return to program input” takes you back to the web page with the input CP.