Many tools rely on symbolic evaluation to reduce programming tasks, such as verification and synthesis, to satisfiability queries. Identifying, diagnosing, and fixing performance bottlenecks in these tools is challenging even for experts, as the all-paths execution model of symbolic evaluators defies both human intuition and standard profiling techniques.
This project develops symbolic profiling, a new approach to identifying and diagnosing performance bottlenecks in programs under symbolic evaluation. To help with diagnosis, we develop a catalog of common performance anti-patterns in solver-aided code. To locate these bottlenecks, we develop SymPro, a new profiling technique for symbolic evaluation. SymPro identifies bottlenecks by analyzing two implicit resources at the core of every symbolic evaluation engine: the symbolic heap and symbolic evaluation graph. These resources form a novel performance model of symbolic evaluation that is general (encompassing all forms of symbolic evaluation), explainable (providing programmers with a conceptual framework for understanding symbolic evaluation), and actionable (enabling precise localization of bottlenecks). Performant solver-aided code carefully manages the shape of these implicit structures; SymPro makes their evolution explicit to the programmer.
James Bornholt and Emina Torlak. Finding Code That Explodes Under Symbolic Evaluation. In Proceedings of the 2018 Annual ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), Nov 2018. [pdf]
The artifact for the OOPSLA 2018 paper is available here.