Relating Complexity and Precision in Control Flow Analysis

Relating Complexity and Precision in Control Flow Analysis, David Van Horn and Harry Mairson. ICFP 2007.

We analyze the computational complexity of kCFA, a hierarchy of control flow analyses that determine which functions may be applied at a given call-site. This hierarchy specifies related decision problems, quite apart from any algorithms that may implement their solutions. We identify a simple decision problem answered by this analysis and prove that in the 0CFA case, the problem is complete for polynomial time. The proof is based on a nonstandard, symmetric implementation of Boolean logic within multiplicative linear logic (MLL). We also identify a simpler version of 0CFA related to eta-expansion, and prove that it is complete for logarithmic space, using arguments based on computing paths and permutations.

For any fixed k > 0, it is known that kCFA (and the analogous decision problem) can be computed in time exponential in the program size. For k = 1, we show that the decision problem is NP-hard, and sketch why this remains true for larger fixed values of k. The proof technique depends on using the approximation of CFA as an essentially nondeterministic computing mechanism, as distinct from the exactness of normalization. When k = n, so that the "depth" of the control flow analysis grows linearly in the program length, we show that the decision problem is complete for exponential time.

In addition, we sketch how the analysis presented here may be extended naturally to languages with control operators. All of the insights presented give clear examples of how straightforward observations about linearity, and linear logic, may in turn be used to give a greater understanding of functional programming and program analysis.

There's ton of really good stuff in here; I was particularly fascinated by the fact that 0-CFA is exact for multiplicatively linear programs (ie, that use variables at most once), because linearity guarantees that every lambda can flow to at most one use site.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Neel, thanks for the notice

Neel, thanks for the notice and kind words. If you're interested in the correspondence between monovariant analyses and evaluation for linear programs, you might be interested in our recent paper, Linearity, flow analysis, and PTIME. Harry and I show that not only does this correspondence hold for 0CFA, but it holds for all of the approximations and restrictions of 0CFA that we could find in the literature. It also spells out in detail how exactly the result of evaluation can be "readback" from the result of flow analysis. Since this paper is currently in submission for publication, I especially welcome comments on it.

Harry and I have also been able to strengthen our ICFP results on the kCFA hierarchy, showing it to be complete for EXPTIME (rather than just NP-hard and contained in EXPTIME). He presented this work at CMU recently, where I assume you saw it, but I've also made the slides available here (PDF, 4.5Mb).