Subject
My manuscript: ICC and compilers
The implicit computational complexity (ICC) helps us to predict and control resources (Time and Space) consumed by programs. Static analysis on specific syntactic criterion allow us to categorize some of them. A common approach is to observe the program’s data’s behaviors.
For instance, the detection of Non Size Increasing programs is based on a simple principle : counting memory allocation and deallocation, particularly in loops. By this way, we can detect programs which computes within a constant amount of space. This method can be easily express as property on Control Flow Graph.
In practice, the system allocates a finite space of memory, if it’s not enough during the execution, the program needs to ask and wait for more space (waste of time). If it’s too many, it’s a waste of space.
The starting point of this thesis is to use the results of NSI Programs theories to generate a complexity certificate that provide the precise amount of space needed. This analysis is not always computable but if it is, we can provide a resource optimization.
Because it’s only syntactic, this analysis can be done during compilation, and the certificate can be gather with the executable file. Furthermore, compilers manipulates an intermediate representation language that’s close to assembly (Gimple/RTL for gcc or LLVM-IR) and gives access to the Control Flow Graph. Thereby we have all the required tools for realize some implicit complexity methods.
The first goal is to write a module in a chosen compiler to detect NSI programs and deduce potentials optimizations. After that, in one hand, we could continue to implement others implicit complexity methods (Size Change Termination or polynomial MWP).
Until now, theses implicit complexity theories were applied on more or less toys languages. We would like to apply theses theories on widely used languages/compilers to give the community a tool capable to treat a big amount of examples and give an accurate idea of the real expressivity of these analysis.