Realizing Implicit Computational Complexity.

Originalities in Implicit Computational Complexity. Automatic performance analysis and optimization is a critical for systems with strictly bounded resource constraints. The field of Implicit Computational Complexity (ICC) [9] pioneers in embedding in the program itself a guarantee of its resource usage, using e.g. bounded recursion [7, 16] or type systems [5, 15]. It drives better understanding of complexity classes, but also introduces original methods to develop resources-aware languages, static source code analyzers and optimizations techniques, often relying on informative and subtle type systems. Among the methods developed, the mwp-flow analysis [13] certifies polynomial bounds on the size of the values manipulated by an imperative program, obtained by bounding the transitions between states instead of focusing on states in isolation, and is not concerned with termination or tight bounds on values. It introduces a new way of tracking dependencies between “chunks” of code by typing each statement with a matrix listing the way variables relate to each others. Having introduced such novel analysis techniques, and, as opposed to traditional complexity, by utilizing models that are generally expressive enough to write down actual algorithms [20, p. 11], ICC provides a conceivable pathway to automatable complexity analysis and optimization. However, the approaches have rarely materialized into concrete programming languages or program analyzers extending beyond toy languages, with a few exceptions [4, 12]. Absence of realized results reduces ability to test the true power of these techniques, limits their application in general, and understanding their capabilities and potential expressivity remains underexplored. We present an ongoing effort to address this deficiency by applying the mwp-flow analysis, that tracks dependencies between variables, in three different ways, at different stages of maturation. The first and third projects bend this typing discipline to gain finer-grained view on statements independence, to optimize loops by hoisting invariant [21] and by splitting loops “horizontally” to parallelize them. The second project refines, extends and implements the original analysis to obtain a fast, modular static analyzer [3]. All three projects aim at pushing the original type system to its limits, to assess how ICC can in practice lead to original, sometimes orthogonal, approaches. We also discuss our intent and motivations behind formalizing this analysis using Coq proof assistant [22], in a spearheading endeavor toward formalizing complexity analysis.