Harry
Mairson
Brandeis University
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).
Wednesday, January 30, 2008
2:00 p.m.
PPB 300
Principles
of Programming Seminars