Hello MSLUGers! This thursday the DIRO is happy to get the visit of Harry Mairson who will be giving a presentation on Control Flow Analysis (CFA). So if you ever wanted to know about advanced Scheme (or Haskell, or any language actually) compiler optimization, this is your chance. Below are the details.
Marc
Begin forwarded message:
From: Pierre McKenzie mckenzie@iro.umontreal.ca Date: April 17, 2008 3:03:36 PM GMT-04:00 To: seminaires@iro.umontreal.ca Subject: Séminaire DIRO 24 avril: Harry Mairson
Cordiale bienvenue au prochain séminaire du DIRO! http://www.iro.umontreal.ca/~mckenzie/ColloquesDIRO/H2008
CONFÉRENCIER: Harry Mairson, Brandeis University TITRE: Linear Logic and the Complexity of Control Flow Analysis
QUAND: le jeudi 24 avril à 15:30 OÙ: salle (*attention*) 3195, pavillon André-Aisenstadt, U de Montréal
RÉSUMÉ: 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).
POUR INFORMATION: Marc Feeley, DIRO.