This summer I attended the International Joint Conference on Automated Reasoning (IJCAR 2008) in cold, cold Sydney, to give a tutorial on Formal Methods in Use at Galois. The overview slides of the tutorial are available for download, for people interested in seeing some industrial applications of formal methods. Incidentally, while I was at the conference, I entered the automatic theorem prover competition with my ML prover Metis, and finished respectably mid-table.

Don will be giving a talk SC’08 in Austin, Texas on Monday 17th November, as part of the Bridging Multicore’s Programmability Gap workshop (see the schedule here), talking about programming mainstream multicore systems with Haskell, now. Here’s the abstract,

Haskell is a general purpose, purely functional programming language. If you want to program a parallel machine, a purely functional language such as Haskell is a good choice: purity ensures the language is by-default safe for parallel execution, (whilst traditional imperative languages are by-default unsafe).This foundation has enabled Haskell to become something of a melting pot for high level approaches to concurrent and parallel programming, all available with an industrial strength compiler and language toolchain, available now for mainstream multicore programming.In this talk I will introduce the features Haskell provides for writing high level parallel and concurrent programs. In particular we’ll focus on lightweight semi-explicit parallelism using annotations to express parallelism opportunities. We’ll then describe mechanisms for explicitly parallel programs focusing on software transactional memory (STM) for shared memory communication. Finally, we’ll look at how Haskell’s nested data parallelism allows programmers to use rich data types in data parallel programs which are automatically transformed into flat data parallel versions for efficient execution on multi-core processors.

See Simon Peyton-Jones and Satnam Singh’s recent tutorial for more background on multicore Haskell, on which this talk is based.

NASA has awarded Galois, Inc. together with the National Institute of Aerospace (NIA), a research contract to investigate monitor synthesis for software health management (here is NASA’s press release). The research team includes myself, Lee Pike as the Principal Investigator,  Cesar Munoz as the Co-PI (NIA), and Alwyn Goodloe as a Research Scientist (NIA). The award runs through the end of 2011, and we are investigating the formal synthesis of online monitors from requirements specifications. The research will focus on safety properties and real-time properties of distributed systems. Here are some slides I gave as part of an invited panel kicking off the project, and here’s the press release from Reuters. If you’re interested in finding out more about the research or are interested in collaborating, don’t hesitate to contact me, or leave a comment!

Here’s a nice interview with Simon Peyton-Jones in the Australian version of Computerworld. It’s got some nice history, interesting insights (I enjoyed hearing how eye-opening Conal Elliot’s Functional Reactive Animation work was), and Simon’s usual wit and wisdom.

With only a week to go in the 2008 Bike Commute Challenge, it’s looking as if Galois will pass its 2007 results. Last year (PDF), 17.1% of our September commmutes were by bicycle. This year, our commute-by-bike rate is 19.1%.N.B. If last year’s statistics (PDF) hold true for this year, Galois employee Sigbjorn Finne will finish in the Top 10 Riders By Distance category, and most likely in the top five.Friday, Sept. 26 update: Folks must have caught up on their riding logs, because the Galois commute rate has risen to 21.6%!

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.

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