PhD: five years on

Today marks the fifth anniversary of the submission of my PhD — entitled “Superoptimisation: Provably Optimal Code Generation using Answer Set Programming” — that I completed in the Department of Computer Science at the University of Bath, under the supervision of Dr Marina De Vos and Professor John Fitch.

With my first doctoral student shortly to submit his thesis, it feels odd reflecting on my own doctoral study — from the initial transition from undergrad to being a research student, the “second year blues”, the first few publications, emerging clarity about the end product, mad rush to submission, viva/minor corrections/graduation, post-doctoral research and eventually my first permanent academic post. For what has probably not been a straightforward PhD journey, I hope that I am able to use this experience to be an effective and understanding supervisor, supporting my students academically as well as pastorally.

As you can see in the abstract below, my thesis brings together two interesting* areas in computer science: compiler optimisations and logic programming. Instead of attempting to improve sequences of code through the various stages of the compilation process, we aim for optimality from the outset — and thus, superoptimisation. By modelling this as declarative search problem, we are able to use answer set programming (ASP), a form of declarative programming oriented towards difficult (primarily NP-hard) search problems based on the stable model (answer set) semantics of logic programming. A major outcome of this work — the development of TOAST, the Total Optimisation using Answer Set Technology system — provided a tractable modelling and computational framework in an attempt to solve the optimal code generation problem.

You can read the full thesis online; it seems other people sometimes do too!

Superoptimisation: Provably Optimal Code Generation using Answer Set Programming

Tom Crick
Department of Computer Science, University of Bath

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.

Repository: http://opus.bath.ac.uk/20352/

*IMHO, obviously.