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.
The paper Regular, shape-polymorphic, parallel arrays in Haskell describes a new Haskell library, named Repa, for multi-dimensional, regular arrays based on our work on Data Parallel Haskell and a delayed array representation avoiding unnecessary data structures. As the following table shows, the sequential performance already gets close to the performance of C programs. More importantly, the Haskell code transparently makes use of multicore hardware — something that is much more difficult in C.
The Haskell code is purely functional, using collective array operations. Here is matrix-matrix multiplication:
mmMult :: (Num e, Elt e)
=> Array DIM2 e -> Array DIM2 e -> Array DIM2 e
mmMult arr brr = sum (zipWith (*) arrRepl brrRepl)
trr = force (transpose2D brr)
arrRepl = replicate (Z :.All :.colsB :.All) arr
brrRepl = replicate (Z :.All :.All :.rowsA) trr
(Z:. colsA:. rowsA) = extent arr
(Z:. colsB:. rowsB) = extent brr
In addition to good performance, the library facilitates reuse through the use of shape polymorphism.
GHC’s new LLVM backend, developed by David Terei as part of his Honours thesis at PLS, is being made ready for inclusion into the main GHC repository. The backend requires a new calling convention to be added to LLVM. David got a patch including the new calling convention accepted into the main LLVM distribution, just in time to become part of the forthcoming LLVM 2.7 release — the inclusion into 2.7 has been confirmed.
The next step is to incorporate a number of suggestions by Simon Marlow on how to improve the LLVM backend code. After that, the patch should be ready to go into the tree!
David will be on an internship at GHC HQ at Microsoft Research Cambridge in the second quarter of this year, specifically to work on the GHC LLVM backend.