QF_IDL: A Core Optimization Problem in Automated System Design
Matthew Walter Moskewicz and Kurt Keutzer
Gigascale Systems Research Center
VLIW and DSP style instruction sets somewhat reduce the semantic gap between the microprocessors and their instruction sets, compared to complex and power hungry superscalar type designs. They expose more of the pipeline-level behavior of the processor to the compiler, and the simpler control mechanisms ease processor design and verification. By analogy, we can also consider the more general semantic gap between the hardware level description of a programmable component and the exported semantics of the same component. Even more generally, we can expand our scope to the gap between system and application semantics. Various approaches to close these gaps using tools have been implemented.
For example, Andrew Mihal's work used models of computation and model transforms to attack the problem of efficiently and correctly mapping high level concurrent applications in various particular domains to (typically lower level) computation and communication primitives. Scott Weber's Tipi work focused on the formal modeling of micro architectures with automatic generation of tools such as fast simulators. My (Matthew Moskewicz's) initial work focused on providing an automated, robust, and efficient compilation system that takes input from higher level languages/models, and targets an interesting subset of Tipi processing elements (or PEs). In my approach, the key problem in code generation was formulated as SAT, with a few additional integer (cardinality) constraints.
Additional work in this research group has led to more optimization (mapping and scheduling) problems arising from automation of higher levels of the mapping process. These problems are also formulated as SAT with additional integer constraints. Specifically, these problems are best described as QF_IDL, and are currently solved using an enhanced SAT solver. QF_IDL is an SMT that consists of a SAT formula with some boolean variables constrained by the inequalities of the form (A < B + Z), where A,B are integer variables and C is an integer constant.
There has been a recent increase in off-the-shelf solvers that can handle various SMTs including QF_IDL, and a corresponding increase in the usage of such solvers, which are often competitive with or superior to custom solvers; see the smtlib website for more details. As with SAT, over time the use of QF_IDL solvers as an abstraction layer may yield great improvements in both solver performance, and in the types of applications that may be implemented without the development of custom solvers.
Given that increased performance and scalability are clearly beneficial for both of the previous applications, as well as many other practical problems, research toward developing both more robust solvers for these types of applications (those beyond pure SAT, but within various SMTs, initially QF_IDL) seems useful. The approach is to combine solid benchmarking of existing solvers and applications with attempts to improve existing formulations and implementations. Initial work will draw together the new applications that have been developed within the group to form benchmark sets that can be added to smtlib. Existing solvers will be benchmarked, and new approaches to both problem formulation and solver implementation will be explored. Most existing QF_IDL solvers appear to build heavily upon existing (open source) developments in SAT, but few contribute their work back to the field in a useful manner. This research will strive to create a state-of-the art open QF_IDL solver, combining existing research with novel improvements.