Harry Mairson (seminar)

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 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.  The key idea is to take the approximation mechanism inherent in CFA, and exploit its crudeness to do real computation.

Joint work with David Van Horn (Brandeis University)

Harry Mairson

Brandeis University