An efficient and parallel abstract interpreter in Scala
Abstract interpretation is a static program analysis technique that can be used to reason over programs and their behavior. It consists of building an interpreter that works with abstract values: concrete values are approximated by sets of values (e.g., 5 can be approximated by the interval [0, 10], or by its type: Int). A frequently used approach to perform abstract interpretation is to describe the interpreter as an abstract state machine, and to abstract this machine. This is the AAM (Abstracting Abstract Machines) approach .
In an abstract interpreter following the AAM approach, the interpreter explores a graph where each state approximates a possible state of the concrete evaluation. A transition function is defined, allowing the interpreter to transition from one state to its successors. The abstract interpretation therefore consists of exploring the successors of each state, starting from an
initial state containing the program to analyze. This builds up a state graph that over-approximates every possible behavior of the program.
However, abstract interpretation does not scale well to analyze large programs. Because each transition represent a small increment in the evaluation of the program, many states have to be explored, and the state graph computed can be complex and contain many cycles. In order to support larger programs, it is important to improve performance of such abstract interpreters. Some work exists on improving the efficiency of abstract machines , but not much research has been done in parallelizing these abstract machines. A notable exception is .
The goal of this thesis is to investigate the parallelization of a Scheme abstract interpreter that follows the AAM approach. The student can start by implementing a simple abstract abstract machine for Scheme, or use the abstract interpretation framework developped at the Software Languages Lab . The machine has to be implemented in a language supporting modern concurrency features (such as actors). Our framework is implemented in Scala and can make use of the Akka actor library.
The student should investigate which are the slow parts of the abstract machine, and parallelize them. Multiple parallelization strategies will have to be considered, including the strategies described in . Other optimizations, such as better representation of states, can be investigated as well. The thesis will be validated by experimentally showing that:
- The time spent for the exploration of the state graph is reduced, and the speedup increases with the number of worker threads.
- Larger benchmarks can be handled in a decent amount of time, bringing the AAM approach to real-world programs.
Also, the final thesis should include the following
- A comparison of the impact of the different parallelization strategies
- A discussion on how to go from a sequential abstract machine to an efficient parallel abstract machine, and how the strategies implemented could be adapted to other abstract machines.
: Abstacting Abstract Machines, M. Might, D. Van Horn, 2010. http://matt.might.net/papers/vanhorn2010abstract.pdf
: Optimizing Abstract Abstract Machines, I. Johnson et al., 2013. http://arxiv.org/pdf/1211.3722
: scala-am: http://github.com/acieroid/scala-am