| ResAna: A Tool for Resource-Consumption Analysis | |
ResAna is a tool that can perform three types of resource analysis: loop-bound analysis, heap-space usage analysis and stack analysis. It works on Java and is implemented as an Eclipse plug-in. It utilises several third-party tools. Loop and heap bounds must be verified using KeY. Heap-space usage analysis requires COSTA. Stack-space analysis requires the proprietary VeriFlux tool, therefore this analysis is unfortunately only available to owners of this software. ResAna was developed as part of the EU CHARTER project. Note that it is in the experimental prototype phase.
ResAna can be downloaded separately from the required third-party tools as an Eclipse plug-in. However, the recommended option is to download the VirtualBox image with all EU CHARTER tools (except VeriFlux) pre-installed.
ResAna is the work of the Radboud University Resource Analysis team, lead by Marko van Eekelen.
Given a program with a loop, the corresponding ranking function expresses an upper bound on the number of the loop iterations depending on (some of) the numerical program variables and data sizes. For instance, for the loop while (i<10) i++;, 10-i is the most precise ranking function.
The concept of ranking functions for loops and the theory behind ResAna's loop-bound analysis are described in the following paper, presented at the PPPJ'10 conference:
The current version of ResAna (0.3) implements the basic method as described in the paper, as well as the features DNF-splitting, branch-splitting and steps, described as extensions and future work, respectively, in the paper. Also implemented is support for arrays and field-access in loop guards.
When the ResAna plug-in is installed and a Java file is open, three CHARTER icons are shown in the menu bar. The ones that are used for loop-bound analysis are the one without text and the one with the overlay "ALL". The former analyses the first loop above the current position of the cursor. The latter analyses all loops in the file with the same options. The options are the same for both possibilities, so will be discussed only once here.
Under "Expected degree" the user inputs the maximal degree she expects for the polynomial loop ranking function. Usually, one/linear is just fine here. More complex loops may have a ranking function of a higher degree. If the inferred bound for degree one is incorrect, a user may go back and try a higher degree. In case a degree is chosen which is higher than the actual degree, the inference method will still find the correct loop-bound, but will take a lot longer to run.
When a program variable is increased/decreased with n > 1 on each iteration, care must be taken. The ranking funtion will probably have rational coefficients in this case. For instance, a loop with guard i < 10 and body i += 4 will have raking function ceil((10 - i)/4). The plug-in can search for these increments itself by looking for assignments in the loop body. This succeeds in most cases. In some cases, for instance if a variable is increased twice, this method may fail. A user can then input the so-called step (in the example: 4) herself.
Even though there is a JML specification, most tools that use JML only implement a subset of this specification and/or some of their own statements. In other words, each tool generally has its own JML dialect. This is also the case for KeY. Under "Annotations" the user is given the choice to output JML that is correct with respect to the JML specification, which contains statements that are not usable by KeY. The default mode is to output JML which KeY can verify.
The second option under "Annotations" can be used to overwrite existing decreases clauses. The default is to keep the existing anotation and give a warning to the user in the console.
There may be branches (if-then-else statements) in the body of a loop. In some cases, executing one of the branches has a different effect on the loop variables than executing the other. The way this can be treated by ResAna is to execute the analysis separately for each branch, then taking the maximum of the resulting loop bounds. This approach is called branch-splitting and can be turned on or off in the options dialog. It should only be used when the normal method results in an incorrect bound.
These options allow for finetuning the search for test nodes. In general, the default options are fine. The algorithm starts at the given start point and looks for nodes within the given minimal and maximal values. If the loop variables run for instance from -10.000 to -9.900 then these options should be used to make sure that test-values are found in this range.
In the beginning of this section we state that it is assumed that the code is already refactored to the limitations of the prototype. The plug-in version of the prototype actually also has an experimental feature in which it refactors the code automatically. This can be tried by switching this option.
When an annotated Java class is loaded into KeY, it generates several 'proof obligations'. Since the 'ensuresPost' proof obligation includes proving termination, proving this for a method will prove the decreases clause for all loops in that method. Select 'ensuresPost' for the method for which you want to prove the LBFs in the 'Proof Obligation Browser', click 'Start proof' and then 'Ok'. KeY will be able to prove the more simple examples automatically (press 'play' button). For more complex LBFs (degree > 1, or containing divisions), manual steps will be needed. See the KeY book and website for more information on how to use KeY (and how it works!).
ResAna's heap consumption analysis is based on the COSTA tool, which provides a generic analysis infrastructure for Java byte code. The symbolic upper bound that COSTA generates for a method, depends on the logical sizes of the method's parameters and structures pointed to by the class fields, and the costs of the called library methods.
The icon annotated with "MEM" starts ResAna's heap and stack analysis dialog. We discuss the available options here.
Select for which methods to perform the analysis.
Switch between heap or stack analysis.
Select how to output heap bounds. The option Costa heap bound outputs the symbolic bound exactly as COSTA generates it. A simplified, human-readable version of this bound can be output by selecting the option Simple heap bound. The third option, concrete heap bound outputs a numerical bound, specific for a certain virtual machine. ResAna can generate sound concrete heap bounds for JamaicaVM or estimate heap bounds for other virtual machines (host option).
Stack-space analysis requires the proprietary VeriFlux tool, therefore this analysis is unfortunately only available to owners of this software.
To perform the stack analysis, select the 'stack' option in ResAna's memory analysis dialog (click on the icon annotated with "MEM"). VeriFlux can now use the generated annotations for stack analysis.
We offer ResAna binaries, sources and pre-installed, with all the other tools in the CHARTER toolchain in a VirtualBox image. The latter is the recommended option, since multiple third-party tools are required as well.
The ResAna Eclipse plug-in can be downloaded here: ResAna_0.3.jar
Simply copy the JAR to your Eclipse plugins folder (for instance '/usr/lib/eclipse/plugins/') and restart Eclipse. You will now see three CHARTER icons appear when a Java file is open: one regular, one with the word 'ALL' and one with the word 'MEM'.
ResAna is distributed under the FreeBSD license. Source can be downloaded here.
A VirtualBox image with Ubuntu, Eclipse and all the CHARTER tools (except VeriFlux) pre-installed is available here. This is the recommended way to use ResAna.
NOTE: The image contains JamaicaVM Personal Edition. This is proprietary software of Aicas GMBH and is intended for personal use only. Please see http://www.aicas.com/jamaica-pe.html for more information.
For examples, try the classes in this zip file: resana-examples.zip