Linear Logic and the Complexity of Control Flow Analysis

Abstract

Control flow analysis (CFA) is a kind of static program analysis performed by compilers, where the answers to questions like "can call site X ever call procedure P?" or "can procedure P ever be called with argument A?" can be used to optimize code output by the compiler. Such questions can be answered exactly by Girard's geometry of interaction (GoI), but in the interest of efficiency and time-bounded computation, control flow analysis computes a crude approximation to GoI, possibly including false positives.

Different versions of CFA are parameterized by their sensitivity to calling contexts, as represented by a contour--- a sequence of k labels representing these contexts, analogous to Lévy's labelled lambda calculus. CFA with larger contours is designed to make the approximation more precise. A naive calculation shows that 0CFA (i.e., with k=0) can be solved in polynomial time, and kCFA (k>0, a constant) can be solved in exponential time. We show that these bounds are tight, namely, that the decision problem for 0CFA is PTIME-hard, and for kCFA is EXPTIME-hard. Each proof depends on fundamental insights about the linearity of programs. In both the linear and nonlinear case, contrasting simulations of the linear logic exponential are used in the analysis. The key idea is to take the approximation mechanism inherent in CFA, and exploit its crudeness to do real computation.

This is joint work with David Van Horn (Brandeis University), to be presented later this month at the annual ACM International Conference on Functional Programming.