John Launchbury presented a Galois Developer Symposium lunch on March 4th, 2010, where he presented the semantics for asynchronous exceptions in Haskell. In particular, discussion concentrated on the interactions between Concurrent Haskell, laziness and exceptions.Follow the talk online, or download the pdf.
The talk will be presented by Iavor Diatchki on Tuesday, February 16th, at 10:30am.(slides)Abstract: The Grammatical Framework (created by Aarne Ranta) is a programming language for multilingual grammar applications. It may be seen in a number of different ways:
This talk is an introduction to GF’s basic concepts by example. We will look at how to define the meaning and syntax of a language, perform simple translations, define semantic properties, and how to use GF together with another language such as Haskell.Bio: Iavor Diatchki is a R&D Engineer at Galois, Inc. with a Ph.D. from the Oregon Graduate Institute.Details:
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.
The talk will be presented by Joe Hendrix on Tuesday, February 2nd, at 10:30am. (slides)Abstract: There is a great deal of interest today in developing multi-purpose environments that combine declarative programming, with specification languages and useful automated analysis techniques. In this talk, I will survey one such an environment: the Maude system. I will start by describing how to program in Maude with a focus on its support for rewriting modulo axioms. After some examples, I will also survey some of the different analysis tools developed on top of the Maude system —- including the model checker, inductive theorem prover, and an extension to the core language for modeling systems that operate in real-time.Details:
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.
Here are some talks that caught my attention on the opening day of POPL 2010.Reconfigurable Asynchronous Logic Automata, Neil GershenfeldIn this invited talk, Neil proposed that we throw out the sequential model of computation from Turing and Von Neumann, and re-imagine computing from the ground up, more along the line of physics as it is manifested in the world. This might be the way forward given the huge power demands that will arise from traditional architectures as they become more and more powerful. Rather than imposing a top-down structure on the machine, Neil propose we consider systems built up from cellular automata. In ALA each cell is able to do a basic logic operation or, in RALA, reconfigure other cells. Built around 2D grids, and computing in parallel without any global clock, the automata are able to compute many basic functions in linear time, including multiplication and sorting (of course, they also take a linear number of cells to do so).What I liked about this talk is that it called on me to think more broadly about the nature of computation. I don’t think I buy the line that how we do computing today is wrong. But I do believe that computing and information theory is going to become more and more important in the development of many other subjects, including physics and biology. I also believe that we will need to harness many more structures to do computing rather than simply relying on gates burned in silicon. Coincidentally, at lunch today Luca Cardelli was telling me about his explorations in computing with DNA. Fascinating stuff!At the lowest levels, the primitive components of computation reflect the computational substrate, so they are very different from one instantiation to another. As primitive computational elements become combined, however, the different descriptions become more abstract, and start to look more and more alike. The same mathematical operations may arise in each form, for example. That makes me wonder what the space of truly computationally-neutral specifications looks like: how might we program in such a way that we really don’t have a preference for what substrate we map the computation onto. We already consider FPGAs, GPUs and CPUs as standard targets for languages like Cryptol. Let’s conceptually add DNA and RALA to the list, and see if that would have us change anything.A Simple, Verified Validator for Software Pipelining, Jean-Baptiste Tristan & Xavier LeroySoftware pipelining is a compiler transformation that reorders loop code to make more efficient use of the CPU and memory accesses. Code from many different iterations of the loop might be drawn together and overlapped to execute out of order, and perhaps in parallel. The question is how to verify that the pipelining has been done correctly.The paper proposes using symbolic evaluation. It describes an equivalence principle which requires proving two separate commutativity properties. These may both be shown by symbolic evaluation of the instruction code, being careful to handle the small differences (such as different temporary variables in the two paths). Overall the process is simple enough that it could be a standard component of any compiler, even if the compiler is non-verifying overall.A Verified Compiler for an Impure Functional Language, Adam ChlipalaHandling object-level variables in proofs is a real pain, one that is hard to eliminate. This paper has an interesting way of dealing with them. It describes a Coq verification of a compiler for Untyped Mini-ML with references and exceptions, compiling to an idealized assembly code.Now, using explicit object variables leads to lots of lemmas about substitution. On the other hand, full higher-order abstract syntax (HOAS) would lead quickly to non-termination, and hence unsoundness. So instead, the paper introduces a closure semantics in which variables are just numbers pointing into a heap. Many operations that would reorder substitutions (and hence require big proofs) don’t affect the closure heap, so the proofs go through easily.The paper also uses a high degree of proof automation: it has a generic proof script that looks at the hypotheses and goals, and decides what approaches to try. The proof script is a bit slow because the evaluation mechanism of Coq wasn’t designed for this particularly (but see my blog post from PADL about accelerating normalization). However, because the proof is highly automatic, it is not hard to evolve the compiler and proof simultaneously. In fact, the compiler and proof were developed incrementally in exactly this way.Verified Just-in-Time Compiler on x86, Magnus MyreenJIT compiling has become standard for accelerating web pages, amongst other things. Good JIT compilers can take into account the input to the program as well as the program itself. But it is hard to get them right, as witnessed apparently by a recent Firefox bug.An aspect that makes verification tricky is that code and data are mixed: a JIT compiler essentially produces self-modifying code. The paper provides a programming logic for self-modifying code by adapting Hoare triples so that there is both “before” and “after” code. Some practical issues also need to be handled: for example, the frame-property has subtleties regarding the instruction cache, and code-updates can sometime happen too recently to show up in the current instruction stream. The x86 documentation is a little vague about how soon code-modifications can be relied on to be present.The end result is a verified JIT compiler from a toy input byte-code language, but mapping to a realistic semantics for x86. The compiler produces comparable code quality to C for a GCD example.
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:
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.
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.
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.
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!
The December 15th Galois Tech Talk will be delivered by John Launchbury. He will present Conal Elliott’s 2009 ICFP paper entitled Beautiful Differentiation for those of us who were not able to attend this wonderful talk in-person.
Abstract: Automatic differentiation (AD) is a precise, efficient, and convenient method for computing derivatives of functions. Its forward-mode implementation can be quite simple even when extended to compute all of the higher-order derivatives as well. The higher-dimensional case has also been tackled, though with extra complexity. This paper develops an implementation of higher-dimensional, higher-order, forward-mode AD in the extremely general and elegant setting of calculus on manifolds and derives that implementation from a simple and precise specification.In order to motivate and discover the implementation, the paper poses the question, “What does AD mean, independently of implementation?‚” An answer arises in the form of naturality of sampling a function and its derivative. Automatic differentiation flows out of this naturality condition, together with the chain rule. Graduating from first-order to higher-order AD corresponds to sampling all derivatives instead of just one. Next, the setting is expanded to arbitrary vector spaces, in which derivative values are linear maps. The specification of AD adapts to this elegant and very general setting, which even simplifies the development.Bio: John Launchbury is the founder and Chief Scientist of Galois, Inc.
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.
The November 3rd Galois Tech Talk will be delivered by Ki Yung Ahn, titled “Testing First-Order-Logic Axioms in AutoCert.”
Abstract: AutoCert is a formal verification tool for machine generated code in safety critical domains, such as aerospace control code generated from MathWorks Real-Time Workshop. AutoCert uses Automated Theorem Proving (ATP) systems based on First-Order-Logic (FOL) to formally verify safety and functional correctness properties of the code. These ATP systems try to build proofs based on user provided domain-specific axioms, which can be arbitrary First-Order-Formulas (FOFs). That is, these axioms are the crucial trusted base in AutoCert. However, formulating axioms correctly (i.e. precisely as the user had really intended) is non-trivial in practice, and speculating validity of the axioms from the ATP systems is very hard since theorem provers do not give examples or counter-examples in general.We adopt the idea of model-based testing to aid axiom authors to discover errors in axiomatization. To test the validity of axioms, users can define a computational model of the axiomatized logic by giving interpretations to each of the function symbols and constants as computable functions and data constants in a simple declarative programming language. Then, users can test axioms against the computational model with widely used software testing frameworks. The advantage of this approach is that the users have a concrete intuitive model with which to test validity of the axioms, and can observe counterexamples when the model does not satisfy the axioms. We have implemented a proof of concept tool using Template Haskell, QuickCheck, and Yices.(This is a joint work with Ewen Denney at SGT/ NASA Ames Research Center, going to be presented in the poster session at Asian Symposium on Programming Languages and Systems this December.)Bio: Ki Yung Ahn is a Ph.D student at Portland State University working with Tim Sheard and other members of the TRELLYS project, designing and implementing a dependently typed programming language that is general purpose programming friendly. He received a BS in Computer Science from KAIST in 2002, worked as online storage service server programmer at Gretech before joining graduate program at Portland State University in 2005. He has been working on Shared Subtypes, Korean translation of “Programming in Haskell” by Graham Hutton, and enjoying other small funs of Haskell hacking.
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.
We take pride in personally connecting with all interested partners, collaborators and potential clients. Please email us with a brief description of how you would like to be connected with Galois and we will do our best to respond within one business day.