[MSLUG] Fwd: Séminaire DIRO 24 avril: Harry Mairson
Marc Feeley
feeley at iro.umontreal.ca
Mon Apr 21 09:29:37 EDT 2008
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 at iro.umontreal.ca>
> Date: April 17, 2008 3:03:36 PM GMT-04:00
> To: seminaires at 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.
More information about the MSLUG
mailing list