[hofa] Pushdown Flow Analysis of First-Class Control

Olin Shivers shivers at ccs.neu.edu
Wed Jun 22 13:43:24 PDT 2011

Brown noser. 

On Jun 22, 2011, at 4:41 PM, David Van Horn <dvanhorn at ccs.neu.edu> wrote:

> Here's another interesting paper.  This one shows how to do pushdown analysis of a language with call/cc, which is difficult since first-class control destroys call/return matching.  It will appear at this year's ICFP.  (The link below is to a draft, not the final version.)
> David
> Pushdown Flow Analysis of First-Class Control
> Dimitrios Vardoulakis and Olin Shivers (Northeastern University)
> To appear, ICFP 2011
> http://www.ccs.neu.edu/home/dimvar/papers/callcc-cfa2.pdf
> Pushdown models are better than control-flow graphs for higher- order flow analysis. They faithfully model the call/return structure of a program, which results in fewer spurious flows and increased precision. However, pushdown models require that calls and returns in the analyzed program nest properly. As a result, they cannot be used to analyze language constructs that break call/return nesting such as generators, coroutines, call/cc, etc.
> In this paper, we extend the CFA2 flow analysis to create the first pushdown flow analysis for languages with first-class control. We modify the abstract semantics of CFA2 to allow continuations to escape to, and be restored from, the heap. We then present a summarization algorithm that handles escaping continuations via a new kind of summary edges. We prove that the algorithm is sound with respect to the abstract semantics.
> _______________________________________________
> HOFA mailing list
> HOFA at lists.lambda-calcul.us
> http://lists.lambda-calcul.us/listinfo.cgi/hofa-lambda-calcul.us

More information about the HOFA mailing list