ICFP is next week, and as usual, Galois will be involved, sponsoring workshops, chairing sessions, presenting papers, and generally talking to people about functional programming and the future. We’re particularly excited about the expanded Haskell Symposium, the line-up for the Commercial Users of Functional Programming, and the all-new DEFUN developer tracks on functional programming (watch Oleg hack live!).If you want to catch up, keep an eye out for Andy, Don, Eric, Iavor, Joe, Joel, John, Levent, Magnus and Trevor, or follow us on Twitter. Happy hacking!

At Galois, Aaron Tomb has been experimenting with the new Haskell Language.C libraries recently (a Summer of Code project by Benedikt Huber, mentored by a Galois engineer, Iavor Diatchki), and he’s been impressed by what it can do. Here are his thoughts on parsing the Linux kernel with Haskell, with an eye to future static analysis work:My interest in the library is for use in static analysis of very large bodies of legacy C code, which means two issues matter a lot to me: 1) rock-solid support for all of GCC’s numerous extensions, and 2) speed. I have used CIL, and tools based on CIL in the past, but have been disappointed with its speed.As a simple scalability and robustness experiment, I decided to see how well Language.C would do on the Linux source tree. It doesn’t yet have an integrated preprocessor (depending on GCC’s for now), but I happened to have an already-preprocessed set of sources for Linux 2.6.24.3 sitting around (configured with defconfig).Could Language.C handle the Linux kernel?I wrote a little wrapper around the C parser to essentially just syntax-check all of the code.

import Language.Cimport Language.C.System.GCCimport System.Environmentprocess :: String -> IO ()process file = do putStr filestream <- readInputStream fileputStr (take (20 - length file) $ repeat ' ')either print(const $ putStrLn "Pass")(parseC stream nopos)main :: IO ()main = dofiles <- getArgsmapM_ process files

It prints the filename followed by “Pass” if the parse succeeds, or details about a syntax error if the parse fails. When I ran this on the Linux code mentioned above, I was amazed to find that it processed it all successfully! All 18 million lines of pre-processed source without a hitch.Since I also care about speed, I wanted to compare it with GCC. GCC has a handy flag, -fsyntax-only, which tells it to just check the syntax of the input file and quit. I ran both the Language.C wrapper(compiled with GHC 6.8.3 and the -O2 option) and GCC on all that code, on a 2.2GHz/4GB MacBook Pro. The result: Language.C parsed all of the code in about 6 minutes, while GCC managed it in a little over 2. GCC is still faster, but I’m happy to take a 3x speed hit for the benefit of being able to write all the subsequent analysis in Haskell.The following table shows the precise time and memory statistics for Langugage.C and GCC, both on the entire source collection and on the single largest file in the tree, bnx2.i, the driver for the Broadcom NetXtreme II network adapter. For the Language.C tests, I compared the performance when the garbage collector used 2 generations (the default) to 4 generations (specified with the +RTS -G4 option). Increasing the number of generations helped slightly.

The Bike Commute Challenge is a wonderful Oregon tradition that Galois has participated in for the past 3 years. This year was a bit disruptive for Galois commuters, because we moved offices from Beaverton to downtown Portland. I think quite a few West-siders haven’t yet figured out the best way to get downtown by bike. Nevertheless, we’re holding steady at an overall 15% commute rate, with a few folks standing out from the crowd: Sigbjorn Finne at 360 miles and Paul Heinlein at 250 miles.The challenge web site has had a few ups and downs (er, mostly downs), but it seems to be back on-line, so I’m hoping folks are able to log their trips without troubles. One weird thing is I think they’re miscomputing the commute rate – it says Paul and Sigbjorn are around 80%, but I’m pretty sure they’re both at 100%, so perhaps there are still a few kinks left to work out. (and once they are worked out, I suspect our overall rate will be well-above 15%)Anyone reading this, please commend any of your bike-commuting colleagues, and I’ll take this opportunity to thank everyone for participating (Galwegians and everyone else!)

Formal Methods in Computer Aided Design (FMCAD’08) is the preeminent conference in formal methods for hardware and systems, and this year, it’ll be held in downtown Portland, November 17-20. The advance program has been announced, and the lineup of technical papers, invited tutorials, invited speakers, and panel discussion looks awesome.Registration is open, so be sure to get your spot soon!Galois is sponsoring this year’s conference, along with Cadence, IBM, Intel, NEC, and Synopsis.  If you attend, stop by Galois; we’re only a few blocks from the conference hotel.

Johan Tibell, from Google, visited Galois on Monday 15th September, and gave a tech talk about efficient IO in Haskell, based on left-fold enumerators, along with a demo of his high perf. Haskell webserver, Hyena, based on left-fold IO. (.pdf slides).For more on left-fold, resource-managing IO subsystems, see Oleg Kiselyov’s work on the best collection traversal interface, From enumerators to cursors: turning the left fold inside out and Peng Li’s work on massively threaded Haskell web servers based on epoll. This stuff is quite hot, with Oleg coincidentally talking about left folds for web servers next week, at DEFUN.

Abstract

I will describe a programming style for I/O operations that is based on left-fold enumerators. This style of programming is more expressive than imperative style I/O represented by the Unix functions read and write, and safer than lazy I/O using streams. Left-fold enumerators offers both high-performance using block based I/O and safety in terms of error handling and resource usage. I will demonstrate Hyena, a web server prototype written in Haskell, as an example of left-fold enumerator style of programming.This talk is intended as a starting point for further discussions on what would be a good interface for I/O rather than a presentation of finished research.

The talk was held at 1pm, on Monday 15th September, at Galois, in Portland.

This Galois Tech Talk was held on Tuesday September 16th, 10.30am, with John Harrison, Principal Engineer at Intel, talking about theorem proving for formal verification. (You can also check out his Handbook of Practical Logic and Automated Reasoning). (.pdf slides, proof demo)

Abstract

The theorem proving approach to verification involves modelling a system in a rich formalism such as higher-order logic or set theory, then performing a human-driven interactive correctness proof using a proof assistant. In a striking contrast, techniques like model checking, by limiting the user to a less expressive formalism (propositional logic, CTL etc.), can offer completely automated decision methods, making them substantially easier to use and often more productive. With this in mind, why should one be interested in the theorem proving approach? In this tutorial I will explain some of the advantages of theorem proving, showing situations where the generality of theorem proving is beneficial, allowing us to tackle domains that are beyond the scope of automated methods or providing other important advantages. I will talk about the state of the art in theorem proving systems and and give a little demonstration to give an impression of what it’s like to work with such a system.

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.

The next Galois Tech Talk will be Tuesday September 9th, 10.30am, with Lee Pike, talking about how to visually present proofs and formal notation.(.pdf slides):Abstract

To the typical engineer or evaluator, mathematics can be scary, logic can be scarier, and really long specifications can simply be overwhelming. This talk is about the problem of the visual presentation of formal specifications clearly and concisely. We take as our initial inspiration Leslie Lamport’s brief papers, “How to Write a Long Formula” and “How to Write a Proof” in which he proposes methods for writing the long and tedious formulas and proofs that appear in formal specification and verification.I will describe the problem and present one particular solution, as implemented in a simple pretty-printer I’ve written (in Haskell), that uses indentation and labels to more easily visually parse long formulas. Ultimately, I propose a “HOL Normal Form” for presenting specifications, much like BNF is used for presenting language definitions.

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.

Please join us for an open house to celebrate our new office space in downtown Portland’s historic Commonwealth Building. Located on SW 6th Avenue between Stark and Washington streets, we’re easily accessible via MAX or TriMet buses. We’re up on the third floor.Parking will also be available in the Alder Street Star Park parking garage located at 615 SW Alder, just one block from our building; validation will be provided at the event.

RSVP: Anne Marie @ ph. 503.626.6616, x153 or email anne at galois.com

This Galois tech talk was held on Tuesday, September 2nd, 10.30am. Sean Lee from UNSW, Sydney, talked about programming GPUs from Haskell. Here’ s the abstract  (.pdf slides):GpuGen: Bringing the Power of GPUs into the Haskell WorldAbstract

For the last decade, the performance of GPUs has out-grown CPUs, and their programmability has also improved to the level where they can be used for general-purpose computations. Nonetheless, GPU programming is still limited only to those who understand the hardware architecture and the parallel processing. This is because the current GPU programming systems are based on the specialized parallel processing model, and require low-level attention in many aspects such as thread launching and synchronization.The need for a programming system which provides a high-level abstraction layer on top of the GPU programming systems without losing the performance gain arises to facilitate the use of GPUs. Instead of writing a programming system from the scratch, the development of a Haskell extension has been chosen as the ideal approach, since the Haskell community has already accumulated a significant amount of research and resources for Nested Data Parallelism, which could be adopted to provide a high-level abstraction on GPU programming and even to broaden the applicability of GPU programming. In addition, the Foreign Function Interface of Haskell is sufficient to be the communication medium to the GPU.GpuGen is what connects these two dots: GPUs and Haskell. It compiles the collective data operations such as scan, fold, map, etc, which incur most computation cost, to the GPU. The design of the system, the structure of the GpuGen compiler, and the current development status are to be discussed in the talk.

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. If you’re planning to attend, dropping a note to dons at galois.com is appreciated, but not required. If you’re interested in giving a talk, we’re always looking for new speakers.