Matthew Might
ABSTRACT
We present two independent and complementary improvements for flow-based analysis of higher-order languages: (1) abstract garbage collection and (2) abstract counting, collectively titled ΓCFA.Abstract garbage collection is an analog to its concrete counterpart: we determine when an abstract resource has become unreachable, and then reallocate it as fresh. This prevents flow sets from merging in the abstract, which has two immediate effects: (1) the precision of the analysis is increased, and (2) the running time of the analysis is frequently reduced. In some nontrivial cases, we achieve an order of magnitude improvement in precision and time simultaneously.In abstract counting, we track how many times an abstract resource has been allocated. A count of one implies that the abstract resource momentarily represents only one concrete resource. This, in turn, allows us to perform environment analysis and to expand the kinds (rather than just the degree) of optimizations available to the compiler.
- AGESEN, O. The cartesian product algorithm: Simple and precise type inference of parametric polymorphism. In Proceedings of ECOOP 1995 (1995), pp. 2--26. Google Scholar
Digital Library
- CHASE, D. R., WEGMAN, M., AND ZADECK, F. K. Analysis of Pointers and Structures. In ACM SIGPLAN Conference on Programming Language Design and Implementation (White Plains, New York, June 1990), pp. 296--310. Google ScholarDigital Library
- COUSOT, P., AND COUSOT, R. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In ACM SIGPLAN Symposium on Principles of Programming Languages (Los Angeles, California, Jan. 1977), vol. 4, pp. 238--252. Google ScholarDigital Library
- HANNAN, J. Type Systems for Closure Conversion. In Workshop on Types for Program Analysis (1995), pp. 48--62.Google Scholar
- HUDAK, P. A semantic model of reference counting and its abstraction (detailed summary). In Proceedings of the 1986 ACMConference on LISP and Functional Programming (Cambridge, Massachusetts, Aug. 1986), pp. 351--363. Google ScholarDigital Library
- JAGANNATHAN, S., THIEMANN, P., WEEKS, S., AND WRIGHT, A. K. Single and loving it: Must-alias analysis for higher-order languages. In ACM SIGPLAN Symposium on Principles of Programming Languages (San Diego, California, January 1998), pp. 329--341. Google ScholarDigital Library
- MIGHT, M., AND SHIVERS, O. Environment Analysis via ΔCFA. In ACM SIGPLAN Symposium on Principles of Programming Languages (Charleston, South Carolina, January 2006), pp. 127--140. Google ScholarDigital Library
- SHIVERS, O. Control-Flow Analysis of Higher-Order Languages. PhD thesis, School of Computer Science, Carnegie-Mellon University, Pittsburgh, Pennsylvania, May 1991. Technical Report CMUCS-91--145. Google ScholarDigital Library
- SHIVERS, O., AND MIGHT, M. Continuations and transducer composition. In ACM SIGPLAN Conference on Programming Language Design and Implementation (Ottawa, Canada, June 2006). Google ScholarDigital Library
- STEELE JR., G.L. RABBIT: a compiler for SCHEME. Master's thesis, Artificial Intelligence Laboratory, Massachusetts Institute of Technology, Cambridge, Massachusetts, May 1978. Technical report AI-TR-474. Google ScholarDigital Library
- WAND, M., AND STECKLER, P. Selective and lightweight closure conversion. In ACM SIGPLAN Symposium on Principles of Programming Languages (Portland, Oregon, January 1994), vol. 21, pp. 435--445. Google ScholarDigital Library
- WRIGHT, A.K., AND JAGANNATHAN, S. Polymorphic splitting: An effective polyvariant flow analysis. ACM Transactions on Programming Languages and Systems 20, 1 (January 1998), 166--207. Google ScholarDigital Library
Index Terms
- Improving flow analyses via ΓCFA: abstract garbage collection and counting
Recommendations
Improving flow analyses via ΓCFA: abstract garbage collection and counting
Proceedings of the 2006 ICFP conferenceWe present two independent and complementary improvements for flow-based analysis of higher-order languages: (1) abstract garbage collection and (2) abstract counting, collectively titled ΓCFA.Abstract garbage collection is an analog to its concrete ...
Model checking via ΓCFA
VMCAI'07: Proceedings of the 8th international conference on Verification, model checking, and abstract interpretationWe present and discuss techniques for performing and improving the model-checking of higher-order, functional programs based upon abstract interpretation [4]. We use continuation-passing-style conversion to produce an abstractable state machine, and ...
Logic-flow analysis of higher-order programs
Proceedings of the 2007 POPL ConferenceThis work presents a framework for fusing flow analysis and theorem proving called logic-flow analysis (LFA). The framework itself is the reduced product of two abstract interpretations: (1) an abstract state machine and (2) a set of propositions in a ...
Comments