Superoptimisation: provably optimal code generation using answer set programming

Abstract

Code optimisation in modern compilers is an accepted misnomer for performance improvement some of the time. The code that compilers generate is often significantly improved, but it is unlikely to produce optimal sequences of instructions; and if it does, it will not be possible to determine that they are indeed optimal. None of the existing approaches, or techniques for creating new optimisations, is likely to change this state of play.

Superoptimisation is a radical approach to generating provably optimal code, that performs searches over the space of all possible instructions. Rather than starting with naively generated code and improving it, a superoptimiser starts with the specification of a function and performs a directed search for an optimal sequence of instructions that fulfils this specification.

In this thesis, we present TOAST, the Total Optimisation using Answer Set Technology system, a provably optimal code generation system that applies superoptimising techniques to optimise acyclic integer-based code for modern microprocessor architectures. TOAST utilises Answer Set Programming (ASP), a declarative logic programming language, as an expressive modelling and efficient computational framework to solve the optimal code generation problem.

We demonstrate the validity of the approach of superoptimisation using Answer Set Programming by optimising code sequences for two 32-bit RISC architectures, the MIPS R2000 and the SPARC V8. We also present an application of the TOAST system as a peephole optimiser, by generating libraries of equivalence classes of all optimal instruction sequences of a given length for a specific microprocessor architecture. While this is a computationally expensive process, it only ever needs to be performed once per architecture. We also provide significant benchmarks for the performance of state of the art domain solver tools, further demonstrating the applicability of Answer Set Programming in modelling complex real-world problems.

Date of Award	1 Aug 2009
Original language	English
Awarding Institution	University of Bath
Supervisor	John Fitch (Supervisor) & Marina De Vos (Supervisor)