Bard College Mathematics, Computer Science, and Physics Talks

Static program analysis is a form of predicting the future: it's what a compiler does to predict the behavior of your program, so that at run-time, the compiled version of your code runs faster or better.

Control flow analysis (CFA) is a canonical form 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?" are used to optimize procedure calls. In the interest of compile-time tractability, these questions are answered approximately, possibly including false positives. Much experimental work has been done on flow analysis. Here we describe, instead, some analytic characterizations of how hard CFA is.

Different versions of CFA are parameterized by their sensitivity to calling contexts. We show that the simplest version of CFA, called 0CFA, is complete for PTIME. In other words, it is as difficult to solve as any problem requiring polynomial time. A family of generalizations of 0CFA providing better analyses, called kCFA (k a positive integer), has never been implemented efficiently. We prove that this is necessary: the problem solved by kCFA is complete for EXPTIME---it is as difficult to solve as any problem requiring exponential time.

Each proof depends on fundamental insights about the linearity of programs, appealing to ideas from linear logic and the geometry of interaction---a linear logic semantics that is effectively an exact form of control-flow analysis.

This is joint work with David Van Horn (Brandeis University), presented at the 2008 ACM International Conference on Functional Programming.

	How hard is static program analysis? Harry Mairson Brandeis University Computer Science Department Thursday, April 16, 2009 4:15 p.m. RKC 111
Static program analysis is a form of predicting the future: it's what a compiler does to predict the behavior of your program, so that at run-time, the compiled version of your code runs faster or better. Control flow analysis (CFA) is a canonical form 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?" are used to optimize procedure calls. In the interest of compile-time tractability, these questions are answered approximately, possibly including false positives. Much experimental work has been done on flow analysis. Here we describe, instead, some analytic characterizations of how hard CFA is. Different versions of CFA are parameterized by their sensitivity to calling contexts. We show that the simplest version of CFA, called 0CFA, is complete for PTIME. In other words, it is as difficult to solve as any problem requiring polynomial time. A family of generalizations of 0CFA providing better analyses, called kCFA (k a positive integer), has never been implemented efficiently. We prove that this is necessary: the problem solved by kCFA is complete for EXPTIME---it is as difficult to solve as any problem requiring exponential time. Each proof depends on fundamental insights about the linearity of programs, appealing to ideas from linear logic and the geometry of interaction---a linear logic semantics that is effectively an exact form of control-flow analysis. This is joint work with David Van Horn (Brandeis University), presented at the 2008 ACM International Conference on Functional Programming.

Bard College Mathematics and Computer Science Seminar