Non-polynomial Worst-Case Analysis of Recursive Programs

Krishnendu Chatterjee, Hongfei Fu, Amir Kafshdar Goharshady

Guide to the Artifact submitted for evaluation

Update: The artifact successfully passed CAV 2017 artifact evaluation

For questions or clarifications, or if there were any problems in running the artifact, feel free to write to:

# General Information

Our artifact gets a recursive program as its input and attempts to synthesize a bound for its worst-case execution time using the sound method explained in the paper.

The artifact is entirely written in Java and depends on JavaILP and lpsolve for solving linear programs.

# Supported Language

Our tool supports input in a C-like language. The examples are the best starting point for seeing how this works. The artifact includes a parser that verifies the input code and produces relevant errors when it’s in invalid form. Note that this is different from the syntax we use in the paper for demonstrating our approach.

In this section, we explain the language supported in our implementation. Other parts of this guide are not dependant on this section and it can be safely skipped.

A program in our language consists of a number of functions. Each function starts with a header of the form

fname(arguments)
Where
fname is the function’s name, which should start with the lowercase letter f and arguments is a comma-seperated list of its arguments. Arguments can either be normal (integer) variables or arrays. By convention, names of normal variables should begin with the lowercase letter p and arrays with a. The functions do not return a value as in the paper. Normal variables are sent to functions by value, while arrays are by reference. For example, the fibonacci function in our examples starts with:

f_fibo(pn)
The statements inside each function then appear inside curly braces. As in C, our statements, except for while and if, end with a semicolon.
Each statement can be in one of the following forms:

1. Skip: A skip (or null) statement is a single semicolon.
2. Assignment: We use = to denote assignment. Note that the right hand side of an assignment should always be a polynomial as in the paper and that one cannot assign values from arrays to normal variables.
3. Block: A block is a sequence of statements put in curly braces. A block is considered a statement in its own right and can appear whenever a statement is permitted.
4. Function calls, if and while statements: These are exactly like C.

Note: Unlike C, we do not use || and && to denote the logical operations. We use and and or instead. Parenthesization is always allowed and recommended, but generally and has a higher priority than or.

As an example, here is a simplified binary-search program in our language:

f_binary_search(aArray, pn, px)
{
if(pn>=2)
{
pmid = pn / 2;
if(pmid>=px)
f_binary_search(aArray, pmid, px);

else
f_binary_search(aArray, pn-pmid, px);
}
}

Our parser tries to find errors in the code, but does not terminate in case of errors and tries to ignore them. If the program fails with an exception, check the stderr for errors. (If it’s long just search for the word Error.) The parser will usually point to the exact point in code where something has gone wrong.

# Invariants and Templates

The program in input should also supply program invariants and templates at every significant label (cut point) of the program. These include the first statements of each function and while statements. Our approach works reasonably well with very simple invariants and by default, a template of the form in equation (1), page 8 of the paper, leads to the most general case where the algorithm would try to obtain the most general upper-bound.

When including a template in the input, you can use c-variables, i.e. variables whose names start with the lowercase letter c as values to be synthesized by the algorithm.

At each significant label, enclose the template in \$ signs and the invariant in #s. For example, the full input for the binary search code above would be:

f_binary_search(aArray, pn, px)
{
#pn>=0#
\$cmain * ln(pn) + c2\$
if(pn>=2)
{
pmid = pn / 2;
if(pmid>=px)
f_binary_search(aArray, pmid, px);
Else
f_binary_search(aArray, pn-pmid, px);
}
}

See the examples to get a feel of how templates can be written. The parser is quite picky about parenthesization in the templates. Try to follow the format as demonstrated in examples.

# Running the Artifact

To run the artifact on a given input file code.prog, simply run

java -jar main.jar code.prog

Our implementation usually writes a great deal of reports to stderr. It is a good idea to avoid seeing these by sending them to a file

java -jar main.jar code.prog 2>log.txt

This will run the artifact step by step (according to the paper) and produce a final output if a bound can be synthesized or reports failure if not.

In many cases, one would like to maximize or minimize one of the c-variables inside the templates. For example, in the binary search program above, we might be interested in finding the smallest cmain possible. One can do this by running:

java -jar main.jar code.prog min cmain

Of course, max is also allowed in place of min. In all our examples, we are interested in minimizing a c-variable called cmain.

# Artifact’s Output

The main output is written to stdout. In case of success, the output will contain a list of functions in the code along with the bounds synthesized for them.

The artifact also writes a great deal of reports to stderr. These match the steps as explained in the paper and can be used for debugging purposes. Especially, values synthesized for other c-variables can be found in this log.

# Obtaining Reported Results

The artifact comes with several examples. Four of these have appeared in the paper. All examples are put in .prog files. Our examples include:

1. Binary Search
2. Closest Pair
3. Fibonacci
4. Karatsuba
5. Merge Sort
6. Quick Sort
7. Strassen

In all cases the result can be obtained by running:

java -jar main.jar example.prog min cmin 2>log.txt

Where example.prog is replaced with the suitable file name containing the example codes.

Note that in our approach, assignments to array elements are treated just like skip statements. Therefore, in several examples semicolons have been put instead of array assignments for brevity.

Unfortunately, we have made an error in reporting the result for Strassen’s algorithm in the paper. The correct result is: 954.2 n2.9 + 1. We apologize for the mistake and will correct it in the final version of the paper. Since this is simply a change in constants, it does not change any of the results we have claimed.