Saturday, July 10, 2010

Rethinking Supercompilation

I have written a paper building on my Supero work that has been accepted to ICFP 2010. Various people have asked for copies of the paper, so I have put the current version online. This version will be removed in about three weeks and replaced with the final version, although the linked copy has nearly all the changes suggested by the reviewers. The abstract is:

Supercompilation is a program optimisation technique that is particularly effective at eliminating unnecessary overheads. We have designed a new supercompiler, making many novel choices, including different termination criteria and handling of let bindings. The result is a supercompiler that focuses on simplicity, compiles programs quickly and optimises programs well. We have benchmarked our supercompiler, with some programs running more than twice as fast than when compiled with GHC.

I've also uploaded a corresponding package to Hackage, but that code should be considered an early version - I intend to revise it before ICFP, to make it easier to run (currently I change the options by editing the source code) and include all the benchmarks. I don't recommend downloading or using the current version, and won't be supporting it in any way, but it's there for completeness.

In the near future I will be posting more general discussions about supercompilation, and about the work covered in this paper. In the meantime, if you find any mistakes in the paper, please mention them in the comments!

PS. Currently is down, but I have uploaded the paper there anyway. It should be present when the site recovers.


Anonymous said...

The table at page 9 is completely uninformative. It does not back up claim "the benchmarks are nearly all faster than GHC".

It would be better if Runtime column contains relative to GHC speed up.

Anonymous said...

1.1, 1st paragraph: "an entirely new" -> drop the "an" (or use "criterion", but later on you talk about multiple criteria again).

"verbatim in to" -> "verbatim into"

The frequent use of "you" (e.g., "how do do you evaluate ...") seems very informal to me. But that's up to you.

I don't see how GADTs cannot be supported by your core language. Surely it's possible to erase types and translate GHC's core into your core language, no?

"all global variables ... as first arg to App" -> do you mean "only global vars" ?

More later.

Asger Alstrup said...

How well does it optimize across applications of primitives? I.e. code that touches IO?

Let's say I have two primitives, onMouseClick, which takes a callback function to be run on every mouse click (i.e. multiple times), and a second primitive, playSound, which takes a frequency and a duration, and plays that.

Now I implement a fancy algorithm that uses a lot of temporary lists and stuff to calculate what frequency of sound to play when a mouse is clicked.

Will this code using these two primitives be able to be deforested and optimized as written, or will the "primitive barrier" stop optimizations in certain situations?

Neil Mitchell said...

thesz: "The final three columns are relative to ghc -O2 being 1.00, with a lower number being better. Runtime is how long the optimised program takes to run." So less than 1.00 is faster than GHC, and greater than 1.00 is slower.

Anon: Thanks for the comments, I'll incorporate them (I'm sending it off tomorrow so if you do have anything further please let me know!).

I don't support GADT's but they could probably be supported, I also don't support existential types. None of this is too fundamental, but I wanted to keep it simple at first.

I mean that the first argument of an app may be either local or global, but that a global var can't occur anywhere else. I'll see if I can make that more obvious (it is a bit of a wart, I'd like it to be more regular, but that complicates other bits...)

Asger: In your example all the code will end up in the same place, so will optimise perfectly. It only breaks if you have primitives that consume structure (i.e. take lists), but there aren't really any useful primitives that do that, so it isn't a problem.

Michael O'Keefe said...

For the definition of map at the end of section 2.1, for the definition of v2 in the let expression matching y:ys, shouldn't that be "v2 = map f ys" instead of "v2 = map f y"? Thank you for posting -- I'm enjoying the paper!

Neil Mitchell said...

Michael: Thanks for pointing that out. One of the referees also spotted that, and I'm happy to say it's fixed in the final version - I should post that online soon!