Varia: Optimization by Logic Programming

Abstract

We have designed a prototype compiler optimization infrastructure called Varia and demonstrated its potential to explore the space of optimizations. In Varia everything is represented as logic: instructions and blocks are axioms, analyses and transformations are inference rules, and optimization proceeds by forward-chaining deduction. Varia makes adding and combining optimizations simple—every rule may be eligible to fire at each step, so optimizations are automatically combined. We have coded five optimizations in our system and demonstrate that Varia can combine them. We describe how to translate normal iterative data-flow analyses into Varia, briefly discuss the performance of the rules engine, and finally, propose changes in the engine to make it more suitable for optimization. Things we need to edit: Massage an example so we can fully demonstrate how hypothetical facts allow the combination of two analyses/optimizations. Ie. How the hypothetical fact allows us to trigger an optimization, which then discharges the hypothesis, thus reaching a fixed point. I would really be happy if we could find some strong relation to logical axioms for this. I need to read all my modal logic books.