Wednesday
Jan202010

Tech Talk: A Scalable I/O Manager for GHC

The talk will be presented by Johan Tibell on Friday, January 29th, at 1:30pm. Slides are available (also on Slideshare and  Scribd).Abstract: The Glasgow Haskell Compiler supports extraordinarily cheap threads. These are implemented using a two-level model, with threads scheduled across a set of OS-level threads. Since the lightweight threads can't afford to block when performing I/O operations, when a Haskell program starts, it runs an I/O manager thread whose job is to notify other threads when they can safely perform I/O.The I/O manager manages its file descriptors using the select system call. While select performs well for a small number of file descriptors, it doesn't scale to a large number of concurrent clients, making GHC less attractive for use in large-scale server development.This talk will describe a new, more scalable I/O manager that's currently under development and that hopefully will replace the current I/O manager in a future release of GHC.Details:

  • Date: January 29th, 2010, Friday
  • Time: 1:30pm
  • Location: Galois Inc.,  421 SW 6th Ave. Suite 300 (3rd floor of the Commonwealth building)
Bio: Johan Tibell is a Software Engineer at Google Inc. He received a M.S. in Software Engineering from the Chalmers University of Technology, Sweden, in 2007.
Galois has been holding weekly technical seminars for several years on topics from functional programming, formal methods, compiler and language design, to cryptography, and operating system construction, with talks by many figures from the programming language and formal methods communities. The talks are open and free. An RSVP is not required, but feel free to contact the organizer with questions and comments.

Click to read more ...

Wednesday
Jan202010

PADL/PEPM 2010, Day 2

Again, here are a few talks that caught my attention and I thought I would share my impressions. Enjoy!An Ode to Arrows, Hai Liu & Paul Hudak (PADL 2010)Representing the infinite tower of derivatives of a function as a lazy list has become popular in the Haskell world, the most recent example being Conal Elliott's paper on Beautiful Differentiation at ICFP 2009. This work explores taking the same ideas and using them to express systems of Ordinary Differential Equations.A natural translation of these ideas into Haskell requires recasting the ODEs in an integral form, rather than a purely differential form, leading to a shallow embedding of the equations as recursive equations in Haskell. Unfortunately, this simple translation leads to quadratic computational complexity, in both time and space. Memoization can address this moderately well, except that one is left with the problems of managing (and freeing) the memo-tables.Moving to arrows leads to a better solution. The recursion is expressed using Paterson's 'loop' construct, which puts it in the control of the programmer. When combined with Causal Commutative Arrows (http://lambda-the-ultimate.org/node/3659) the circuits can be optimized into tight iterative loops, with dramatic improvements in performance.A DSL Approach to Protocol Stack Implementation, Yan Wang & Veronica Gaspes (PADL 2010)Implementations of network code are very hard to connect with the specifications, leading to major challenges for maintenance. This is significant for embedded devices which need implementations that appropriately trade off power, speed, and memory usage. To that end, IPS is a DSL for generating network code. It allows packet formats to be defined using dependencies between fields, handles the interaction of protocol and packet, and provides a framework for constructing the protocol stacks.In a comparison exercise, IPS was used to generate code for the Rime protocol stack. Compared with the published hand-written version in C, the IPS code was 1/4 of the size of the C, but produced an executable 25% larger. The performance on sending packets was 10% worse in the IPS version, but both versions were equivalent for receiving packets.No measurements were given for ease of maintenance or design exploration between the two versions, but I know which one I would prefer to have to work with…I/O Guided Detection of List Catamorphisms, Martin Hofmann & Emanuel Kitzelmann (PEPM 2010)Having the computer write its own programs has always been appealing. You provide some input/output pairs and the machine comes up with a generalization expressed as a program that has the same behavior. Broadly, there are two ways to do this: analytical (where the structure of the data is examined to build the program), and generate & test (where many programs are produced, and their behavior improved, perhaps by evolutionary combinations).This work uses the idea of catamorphisms (also known an fold or reduce functions) as a template to explore, when the i/o pairs comes from a recursive data type (just lists at the moment, I think). Using the fact that if a function g satisfies 'g [] = v' and 'g (x:xs) = f x (g xs)' for some 'f' and 'v', then 'g = fold f v', the system figures out what the i/o pairs for the sub-functions would be, and then tries to deduce the definitions. It includes specific smarts that notice when the form of the function corresponds to a 'map' or 'filter'.Bridging the Gap Between Symbolic and Efficient AES Implementation, Andrew Moss & Dan Page (PEPM 2010)Different implementations of AES, the standard for block encryption, run at very different speeds. The original reference implementation takes about 840 cycles per round, the Open SSL implementation takes 30, and a top performing assembly code version takes 21.6 cycles per round. The CAO DSL and compiler described in this paper takes a high-level spec and compiles it, producing code that takes 23 cycles per round. Impressive.CAO is a sequential language, designed to be easily related to the pseudo code that crypto specifications often use. A significant amount of effort in the compiler then goes into deducing what parallelism is possible and how best to balance the work. CAO has matrices as first class objects, to allow the compiler opportunity to deduce good representations. There are also optimizations to convert references from the matrices in their entirety to references to the appropriate sub-portions, so as to eliminate unnecessary additional sequential dependencies. The compiler also has some optimizations that are specific to AES.Clone Detection and Elimination for Haskell, Christopher Brown & Simon Thompson (PEPM 2010)I liked this talk partly because it reminded me to go and play with HaRe (https://www.cs.kent.ac.uk/projects/refactor-fp/hare.html). The Haskell Refactorer is an Emacs and Vim tool for manipulating Haskell 98 programs, providing structural transformation (like fold/unfold), altering data types (like adding or eliminating arguments), slicing, and now, clone elimination (cue Star Wars music).The clone eliminator finds repeated code forms above a threshold size, and deduces the least-general generalization of the code to invent new functions if necessary. Clone detection is entirely automatic, but it is up to the programmer to decide which ones to act upon -- sometimes adding abstraction helps the structure of a program, and sometimes it obscures it. It works within monadic code too.HaRe works mostly at the AST level, though it does use the raw token stream for some of its discovery. It also works across modules.Making "Stricterness" More Relevant, Stefan Holdermans & Jurriaan Hage (PEPM 2010)The old approaches to strictness were all denotational, but to actually use strictness within the compiler it is better to have a syntax-driven formulation, i.e. in logic. There is a nice approach which uses the concept of 'relevance', where 'x' is relevant to 'e' if every evaluation of 'e' demands 'x'. Clearly, relevance is equivalent to strictness.But actually it doesn't work so well in the presence of 'seq'. The original formulation of relevance assumed that the only time a function would be evaluated was at its point of application. Then there is no way to distinguish 'undefined' from '\x->undefined'. 'Seq' changes all that. The paper shows how to fix relevance by tracking which lambdas are used applicatively (i.e. applied somewhere in the program in a place that will be evaluated). The definition is circular, but the least solution is the one intended.

Click to read more ...

Tuesday
Jan192010

PADL/PEPM 2010, Day 1

Here are some papers which caught my imagination at this year's PADL and PEPM conferences in Madrid.O Partial Evaluator, Where art thou? Lennart Augustsson (PEPM 2010)In this invited talk, Lennart walked us through his personal engagement with PE-like code transformations that he has confronted directly in his career, which has consisted of Haskell programming in a wide variety of commercial and industrial settings. The examples included optimizing airline scheduling code for Lufthansa, eliminating unnecessary hardware elements in Bluespec compilation, and generating efficient Monte-Carlo computations in investment banking.In Bluespec, Lennart needed to introduce a 'tabulate' function which produces a table-driven implementation of its function argument. It is a powerful idea, but it requires a sufficiently powerful set of transformations for its boilerplate to get simplified away. In this case, Lennart needed to introduce a term '_' which means "don't care", i.e. any convenient result can be returned. During unfolding and partial evaluation, '_' could be replaced with any term that would help the partial evaluator make good progress on simplification. Semantically, this is a form of refinement of non-determinism performed during code transformation (in fact, I'm still not sure what the correct denotational approach to its semantics would be). Lennart then explored using 'tabulate' directly in Haskell, but found it next to impossible to get the GHC simplifier to do enough transformation.The Paradise ESDL is like Bluespec in that it uses the Haskell framework to bolt together primitive elements from a lower level language. In this case, the efficiency opportunities arise from, say, 18-argument functions being called repeatedly with 15 known arguments. Lennart introduced a 'compile' function which is semantically the identity function, but which invokes a run-time compilation. Yet again, Lennart found himself writing essentially the same kind of code he had previously written in a different setting. Each time it is fairly simple partial evaluation.Where oh where is the partial evaluator for Haskell? And don't worry about self-application or anything fancy like that. Just something that is solid and reliable.Explicitly Typed Exceptions for Haskell, Jose Iborra (PADL 2010)Java gives you safe exceptions, in that if you don't handle an exception that could be raised, the compiler will complain. Currently Haskell does not. This paper builds on Simon Marlow's work of providing an exception library with existentially-quantified exceptions, that provide access to the exception through class methods. Marlow's exceptions work very nicely with the type system, allowing exception and non-exception code to be intermingled. If only there was a way still to know which particular exceptions could be raised ...Iborra to the rescue! He adapts Marlow's exceptions with additional class constraints that track exactly which exception could be raised, fulfilling those constraints when a handler for the exception is provided. Unhandled exceptions show up as missing instances (of handlers), pinpointing the code that is at fault. It all works very beautifully. The downside? He needs to use overlapping instances to be able to 'subtract' that constraints. Hmmm. Normally I'm very down on overlapping instances: it seems really fragile to rely on details of the type-inference engine to select what code should run. But this is a particularly benign case: here the overlapping instances are over phantom type variables, so the same code will run in either case. Maybe Haskell should allow that in general; overlapping instances are fine if the same run-time code is produced however the instances are resolved.Conversion by Evaluation, Mathieu Boespflug (PADL 2010)Proof tactics in theorem provers often require large lambda terms to be normalized. For example some Coq tactics perform reflective computation over other Coq terms. This reduction can be quite inefficient when done explicitly, because of the interpretive overhead, yet the result of evaluation needs to be in a form where the final lambda term can be examined.This paper shows the how to interpret explicit lambda terms efficiently by mapping them into a underlying evaluation mechanism of the host language (e.g. Haskell). The approach is deceptively simple and consists of a set of straightforward optimizations (higher-order abstract syntax, currying, de Bruijn indices etc). Astonishingly, the result is that the evaluation incurs only a 10-30% overhead compared with using the underlying evaluator directly! A must-read for anyone interested in reflective evaluation.Optimizing Generics Is Easy! Jose Pedro Magalhaes et al (PEPM 2010)Generic programming is a way to provide a programmable version of the deriving concept that arises in Haskell. The problem is that the current libraries for implementing generics introduce performance overheads from 50% to 16x compared with writing the original by hand. This paper presents a framework for doing generics using type families to represent the components of algebraic datatypes, together with overloaded operators for mapping between the generic datatype and any user datatype.GHC does a good job of rewriting much of the overhead away, but needs to be encouraged to do the best it can. There are GHC flags to control decision thresholds for inlining etc that turn out to enable GHC to completely remove the overhead of the generic code, producing in some cases exactly the code that would get written by hand. The open problem is that increasing the threshold over the whole program might have negative effects elsewhere in the compilation, so a mechanism for localizing the effect of increased thresholds would be valuable.

Click to read more ...

Wednesday
Jan062010

GHC Nominated for Programming Language Award

ACM SIGPLAN recently announced a new award:

The SIGPLAN Programming Languages Software Award is awarded to an institution or individual(s) to recognize the development a software system that has had a significant impact on programming language research, implementations, and tools. The impact may be reflected in the wide-spread adoption of the system or its underlying concepts by the wider programming language community either in research projects, in the open-source community, or commercially. The award includes a prize of $2,500.
I think that GHC (Glasgow Haskell Compiler) and the two Simons (Peyton Jones and Marlow) are prime candidates for this. So, being careful to stay within the 500 word limit, I submitted a nomination statement for GHC as follows:
For the last decade, Haskell has been at the center of the most exciting innovations within programming languages, with work on software transactional memory, generalized algebraic data types, rank-N polymorphism, monads, multi-parameter type classes, embedded domain-specific languages, property-based testing, data parallelism, thread-profiling, and so on, generating hundreds of research papers from many diverse research groups.GHC, the Glasgow Haskell Compiler, is the vehicle that made this research possible.It is hard to explore radical ideas on real systems, yet the GHC team created a flexible platform that allows other researchers to explore the implications of their ideas and to test whether they really work in the large. From the first beta release in 1991, GHC emphasized collaboration and open “bazaar” style development, as opposed to the “cathedral” development of most of its contemporaries. GHC was open source even before Linux made open source cool. GHC has continued in the same vein, now listing over 60 contributors to the codebase.In those early days, efficient compilation of a higher-order, allocation-rich, lazy functional language seemed to be a pipe dream. Yet GHC has risen to be a top-flight performer in the online language performance shootout (shootout.alioth.debian.org), comparable with Java Server-6, and approaching native C in performance overall. This is a tribute to the incredible amount of profound optimization built into the compiler, with techniques like cross-module code migration, unboxed data types, and automated removal of intermediate data structures, all done through correctness-preserving transformations that exploit the algebraic simplicity of Haskell terms, even in the presence of monadic effects.The impact GHC has had on programming language research would be sufficient to merit an award by itself, but GHC is having a corresponding influence in industry. By showing the feasibility of purely functional, statically-typed programming in the large, GHC Haskell has also had clear influence on many of the newest generation of languages, such as C#, F#, Java Generics, LINQ, Perl 6, Python, and Visual Basic 9.0. As Soma Somasegar, Microsoft Developer Division Chief, said in 2007, “One of the important themes in programming languages over recent years has been a move to embrace ideas from functional programming, [which] are helping us address some of the biggest challenges facing the industry today, from the impedance mismatch between data and objects to the challenges of the multi-core and parallel computing space.”GHC now supports a burgeoning professional Haskell world. The O’Reilly book Real World Haskell, targeted to professional programmers and oriented to GHC, was published in 2008. It went on to win the Jolt Award for best technical book of the year. In 2009 there were 3500+ Haskell package updates, with more than 100,000 package downloads in November alone. GHC is now used across the financial sector in institutions like Credit Suisse and Standard Chartered Bank, and for high assurance software in companies like Amgen, Eaton, and Galois. Some of these companies came together in 2009 to create the Industrial Haskell Group, whose purpose is to ensure the health and longevity of GHC.
499 words. Whew! There is so much that could be said, but let's hope this is enough. I think the case is very strong, and both Simon's deserve honor and accolade for their work. Thank you both so much!

Click to read more ...

Wednesday
Dec302009

Tech Talk: Ground Interpolation for Combined Theories

The next Galois Tech Talk will be delivered by Amit Goel.  Come kick off 2010 with us!Title: Ground Interpolation for Combined Theories Abstract: We give a method for modular generation of ground interpolants in modern SMT solvers supporting multiple theories. Our method uses a novel algorithm to modify the proof tree obtained from an unsatifiability run of the solver into a proof tree without occurrences of troublesome “uncolorable” literals. An interpolant can then be readily generated using existing procedures. The principal advantage of our method is that it places few restrictions (none for convex theories) on the search strategy of the solver. Consequently, it is straightforward to implement and enables more efficient interpolating SMT solvers. In the presence of non-convex theories our method is incomplete, but still more general than previous methods.

  • Date: Tuesday, 10:30am, 05 Jan 2010
  • Time: 10:30am – 11:30am
  • Location: Galois, Inc.421 SW 6th Ave. Suite 300(3rd floor of the Commonwealth Building)Portland, OR 97204
Bio: Amit Goel is a member of Intel's Strategic CAD Labs.
Galois has been holding weekly technical seminars for several years on topics from functional programming, formal methods, compiler and language design, to cryptography, and operating system construction, with talks by many figures from the programming language and formal methods communities. The talks are open and free. An RSVP is not required, but feel free to contact the organizer with questions and comments.

Click to read more ...