In the paper Accelerating Haskell Array Codes with Multicore GPUs, we describe Accelerate, embedded language for array computations in Haskell, as well as a dynamic code generator targeting NVIDIA’s CUDA GPGPU programming environment. Our CUDA code generator is based on the idea of algorithmic skeletons for parallel programming, minimises re-compilation overheads, and overlaps host-to-device data transfers, code generation, and kernel execution.
The paper outlines our embedding in Haskell, details the design and implementation of the dynamic code generator, and reports on initial benchmark results. These results indicate that we can compete with moderately optimised native CUDA code, while enabling much simpler source programs.
The second beta release of Data.Array.Accelerate (version 0.8.0.0) includes support for all array operations in the CUDA backend — except for a new stencil operation that is new in this release and currently only supported by the interpreter. The CUDA backend requires CUDA 3.x and has been tested on consumer-grade GeForce cards, TESLA high-performance GPUs, and the new Fermi cards.
If you are interested in general-purpose GPU programming in Haskell, give this release a spin — it is available on Hackage. While it is far from perfect, it should already prove useful for a considerable range of applications. Together with the other Accelerate developers, I would be very interested to hear what works for you and what doesn’t. We are also interested in suggestions for the future development of the library. Accelerate has a mailing list and a bug tracker on which we also accept feature requests.
During the first Australian Haskell Hackathon, AusHac2010, we finally managed to complete the integration of the CUDA backend, written by Sean Lee and Trevor McDonell, into the array EDSL Accelerate. It still doesn’t cover the complete functionality of the current version of the Accelerate EDSL, but already allows for interesting GPU computations. The package source (version 0.7.1.0) can be obtained from Hackage as usual. There is now also a bug tracker.
In the paper Singleton: A general-purpose dependently-typed assembly language, we introduce Singleton, a typed assembly language that embeds a variant of the calculus of inductive constructions (CiC) as an assertion language in its type system. Moreover, Singleton procedures can abstract over propositions and proof terms. Singleton’s name comes form its support for generalised singleton types that allow the values from arbitrary inductive types to be associated with the contents of registers and memory locations. Together these features allow strong statements to be made about the functional behaviour of Singleton programs.
Singleton’s development was motivated by the desire for a typed assembly language that can establish high-level properties that are not implied by type safety alone, a requirement that we encountered in the context of runtime verification. For more details on that context, see our previous papers Secure Untrusted Binaries - Provably! and On the automated synthesis of proof-carrying temporal reference monitors.
Simon Winwood, on whose PhD work the paper is based, established basic properties of Singleton’s type system, namely type safety and a type erasure property, using the Coq proof assistant: proof scripts.
The final version of the Haskell 2010 edition has been released: http://www.haskell.org/pipermail/haskell/2010-July/022189.html This completes my stewardship of the Haskell foreign function interface specification. It is now part of the language standard proper. The next language feature I personally like to see being integrated are type families, but that still requires much work.
In An LLVM Backend For GHC, we describe the design and implementation of an LLVM backend for the Glasgow Haskell Compiler (GHC). We outline the conceptual obstacles that we had to overcome and give a detailed performance analysis of the new backend compared to the existing C backend and native code generator.
When I decided to by an iPad, I had one killer application in mind: reading. I was hoping the device would also be useful otherwise, but cutting down on printing papers and the like was my main aim. As a researcher, I inevitably read a lot: research papers, books, reports, manuals, thesis drafts, the drafts of my own work-in-progress papers, and so on. I have got reading material on my desk at home, in my office, in my bag…it’s a mess. The prospect of consolidating it all into one device, which would hopefully also cover most of my note taking and sketching out of ideas, was enough to sell me on the iPad.
So, how did it work out? So far, very well — but slightly more than a week of use makes it hard to draw any final conclusions. The printed area of a paper is about the same as the size of the iPad screen, which combined with the high quality of the display makes for a good reading experience. Instead of printing a paper or other document I like to read, I now sync it to my iPad —usually using Dropbox— and read it with GoodReader for iPad. If I expect that I may want to refer to a paper at a later time, I’m adding it to my mobile library kept in Papers. If I need to annotate a document —for example, for a review— I currently use iAnnotate PDF. I like Dropbox, GoodReader, and Papers, but I’m only using iAnnotate as there doesn’t seem to be an alternative at the moment — the user interface is pretty rough.
In addition, I found over the last week that iPad is also the perfect Twitter device (I’m currently using Twitterific for iPad), and great for reading blogs and online articles, which I often file away for later reading on my iPad using Instapaper.
Simon Peyton Jones recently got stranded in Boston due to Eyjafjallajokul. He took the opportunity to give a talk about our joint Data Parallel Haskell project at Northeastern University. The Northeastern folks kindly recorded and published the talk. The talk provides a nice summary of our approach.