The goal of quantitative resource analysis is to provide developers with quantitative information about the runtime behavior of software at development time. With this extra information, programmers have early feedback to improve the efficiency of their code even before profiling.
Formal quantitative resource analysis also provides a well-designed framework to mathematically prove resource usage claims on programs. These strong guarantees are of tremendous importance for safety-critical and real-time systems.
This work presents a new framework to interactively and automatically derive certified, and compositional worst-case resource bounds.
We present here our tool C4B in a simple web interface. This automated
analysis is the first tool to successfully combine amortized analysis
reasoning with negative integer variables and imperative features like
assignment or non-linear control flow (like break and
return).
How to analyze a file?
If your input file contains only one function, the body of this function
will be analyzed. If multiple function definitions are available,
only the body of the function start will be analyzed. The
main function you analyze cannot be recursive, to analyze a recursive
function f, define it and call it from start.
You can use two metrics to analyze a file. Either the standard
back-edge metric that assigns a cost of 1 to every back edge in
the control-flow graph (including function returns). Or the
tick metric that assigns a cost n for calls
tick(n) of the builtin tick function.
To use the latter metric, include the #pragma tick
directive in your C code. For an example usage of this metric,
load the example
t46.
The prototype above is not yet feature complete for C. In particular:
return can only return variables.
goto is not supported.
We wrote a formal proof of soundness for our quantitative logic in the Coq proof assistant. The files in the archive below define precisely the semantics of a resource aware version of C and the rules of a logic to derive sound bounds for programs in this language.
You can also download a technical report that explains the details of our framework. The Section 2 of this file is a long informal explanation of both the logic and the automatic analysis. It features many examples with detailed explanations of our system. The Appendix A shows many other examples and features a comparison of different tools on these examples.
Quentin Carbonneaux, Jan Hoffmann, and Zhong Shao at Yale University