Three papers on superoptimisation

After a recent research discussion on applications of knowledge representation and reasoning, I was reminded of my previous work in this space — in particular relating to my doctoral work on superoptimisation using answer set programming. The three papers below (in reverse date order) reflect some of the research challenges and outputs over the period 2004-2009 with colleagues at the University of Bath, bringing together work on compiler optimisations and logic programming, alongside the rapid development of improved solver tools.

1. Paper in LPNMR 2009, the 10th International Conference on Logic Programming and Nonmonotonic Reasoning (held in Potsdam, Germany):

Generating Optimal Code Using Answer Set Programming

Tom Crick, Martin Brain, Marina De Vos and John Fitch

This paper presents the Total Optimisation using Answer Set Technology (TOAST) system, which can be used to generate optimal code sequences for machine architectures via a technique known as superoptimisation. Answer set programming (ASP) is utilised as the modelling and computational framework for searching over the large, complex search spaces and for proving the functional equivalence of two code sequences. Experimental results are given showing the progress made in solver performance over the previous few years, along with an outline of future developments to the system and applications within compiler toolchains.

DOI: 10.1007/978-3-642-04238-6_57

2. Paper in ICLP 2006, the 22nd International Conference on Logic Programming (held in Seattle, USA):

TOAST: Applying Answer Set Programming to Superoptimisation

Martin Brain, Tom Crick, Marina De Vos and John Fitch

Answer set programming(ASP) is a form of declarative programming particularly suited to difficult combinatorial search problems. However, it has yet to be used for more than a handful of large-scale applications, which are needed to demonstrate the strengths of ASP and to motivate the development of tools and methodology. This paper describes such a large-scale application, the TOAST (Total Optimisation using Answer Set Technology) system, which seeks to generate optimal machine code for simple, acyclic functions using a technique known as superoptimisation. ASP is used as a scalable computational engine to handle searching over complex, non-regular search spaces, with the experimental results suggesting that this is a viable approach to the optimisation problem and demonstrates the scalability of a variety of solvers.

DOI: 10.1007/11799573_21

3. Paper in NMR’06, the 11th International Workshop on Non-Monotonic Reasoning (held in the Lake District, UK):

An Application of Answer Set Programming: Superoptimisation — A Preliminary Report

Martin Brain, Tom Crick, Marina De Vos and John Fitch

Answer set programming (ASP) is a declarative problem-solving technique that uses the computation of answer set semantics to provide solutions. Despite comprehensive implementations and a strong theoretical basis, ASP has yet to be used for more than a handful of large-scale applications. This paper describes such a large-scale application and presents some preliminary results. The TOAST (Total Optimisation using Answer Set Technology) project seeks to generate optimal machine code for simple, acyclic functions using a technique known as superoptimisation. ASP is used as a scalable computational engine for conducting searches over complex, non-regular domains. The experimental results suggest this is a viable approach to the optimisation problem and demonstrates the value of using parallel answer set solvers.

(see: full proceedings)

(also see: Publications)

1 Comment

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google+ photo

You are commenting using your Google+ account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s

This site uses Akismet to reduce spam. Learn how your comment data is processed.