le seminaire PPS aujourd'hui
Jeudi 7 Mai,
11h, salle 0C2:
Harry Mairson (Boston)
Linear Logic and the Complexity of Control Flow Analysis
ABSTRACT
Static program analysis is about predicting the future: it's what
compilers do at compile-time to predict and optimize what happens at
run-time. What is the tradeoff between the efficiency and the precision of
the computed prediction? Control flow analysis (CFA) is a canonical form
of program analysis that answers questions like "can call site X ever call
procedure P?" or "can procedure P ever be called with argument A?" 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 exact: 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), presented at
the 2008 ACM International Conference on Functional Programming.
Aucun commentaire:
Enregistrer un commentaire