Preconditions on XMonad

{- ICFP referees look away now -}

I've proved that the central XMonad StackSet module is safe on several occasions, as the code keeps evolving. Each time I take the source code, run Catch on it, and send an email back to the XMonad list giving the results. So far only one other person (Spencer Janssen) has taken the time to download and install Catch and run the tests to validate my result. The reason for this is that building Catch is slightly tricky, due to the Yhc and Yhc.Core dependencies. I'm working on putting together a proper release for Hackage, expect that within a month - all the code works, its just the packaging and user interface thats lacking.

The other day dons asked me how he could "get an idea" of what Catch is doing. If you blindly accept a formal proof, its hard to get a feel of whether its correct, or if you are proving what you expect. The detailed answer is going to appear in my thesis (and hopefully as a paper beforehand), but I thought it may help to give a very light overview of what thoughts go through Catch.

In Principle

The concept behind Catch is that each function has a precondition that must hold in order for the function to execute without error. If a function f calls a function g which has a precondition, then the precondition for f must guarantee that the precondition to g holds. If you set this up so that error has the precondition False, then you have a pattern match checker.

The second concept is that given a postcondition on a function, you can transform that to a precondition on the arguments to the function. If there is a requirement that the result of f x y meets a certain condition, then this can be expressed as conditions on the variables x and y.

Before all this machinery can be put into action, it is first necessary to perform many transformations on the source code - filling in default pattern matches, doing simplifications, removing higher-order functions and abstracting some library functions. All these transformations are performed automatically, and are intended to set up the Catch machinery to do the best job it can.

In Reality

As it happens, most of the pattern matches that are checked in XMonad are relatively trivial - and do not push the power of Catch to its full potential. A few are slightly more complex, and one of these is focusLeft (XMonad code evolves very fast, so this may not be the current darcs version!):

focusLeft = modify Empty $ \c -> case c of
    Node _ _ []     [] -> c
    Node m t (l:ls) rs -> Node m l ls (t:rs)
    Node m t []     rs -> Node m x xs [t] where (x:xs) = reverse rs -- wrap

Catch identifies two separate potential pattern match errors in this statement. Firstly the lambda expression passed as the second argument to modify is potentially unsafe - as it does not mention the Empty constructor. A quick look at the modify function shows that by this stage the value must be a Node. The way Catch solves this is by transforming the code, bringing the two pices of code together. Once the case expression within modify is merged with the one in the lambda, pattern match safety is a simple transformation of elimating redundant alternatives.

The second potential error is in the where statement. If reverse rs is empty then the pattern will not match. This is a perfect example of the postconditions in action, the generated postcondition is that reverse rs must be a (:) constructed value. Using the machinery in Catch, this condition is transformed into the condition that rs must be a (:) value. Looking at the alternatives, Catch can see this is always the case, and declares the pattern safe.

In order to prove the entire module, Catch requires 23 properties, and 12 preconditions. The process takes 1.16 seconds are requires 1521.05 Kb of memory.

In Conclusion

Catch is an automated tool - no user annotations are required - which means that some people may feel excluded from its computational thoughts. If a user does wish to gain confidence in the Catch checking process, a full log is produced of all the preconditions and postconditions required, but it isn't bedtime reading. Hopefully this post will let people get an idea for how Catch works at a higher level.

I am very glad that Catch is an automated tool. XMonad is a fast changing code base, with many contributors. In a manual system, requiring proofs to remain in lockstep with the code, the pace of progress would be slowed dramatically. Hopefully Catch can give cheap verification, and therefore verification which can be of practical user to non-experts.

Does XMonad crash?

{- ICFP referees look away now. -}

Dons recently asked me to look over the StackSet.hs module of XMonad, checking for pattern-match errors, using my Catch tool. This module is the main API for XMonad, and having a proof of pattern-match safety would be a nice result. I performed an initial check of the library, including introducing the necessary infrastructure to allow Catch to execute, then sent them the required patches. After I had given them the Catch tool and the initial results, sjanssen picked up the results and went on to modify the code further - with the end result that now StackSet will never crash with a pattern-match error.

I'm not going to cover the changes that XMonad required to achieve safety - that is a story that sjanssen is much better equiped to tell. What I am going to describe is the process I followed to get to the initial results.

Step 1: Download Catch, Yhc and XMonad

Catch can be obtained from http://www-users.cs.york.ac.uk/~ndm/catch/ - however a word of warning - it is an involved installation procedure. In the next few months I hope to make Catch use Cabal, and then ordinary users will be able to easily install Catch.

Yhc can be obtained from http://www.haskell.org/haskellwiki/Yhc

XMonad can be obtained from http://www.xmonad.org/

Step 2: Make sure StackSet.hs compiles with Yhc

Initially StackSet used pattern guards, one small patch and these were removed. There was also a small issue with defaulting and Yhc, which I was able to paper over with another small patch. With these two minor changes Yhc was able to compile StackSet.

Step 3: Write a test for StackSet

The test for StackSet is based on the Catch library testing framework, and is all available at http://darcs.haskell.org/~sjanssen/xmonad/tests/Catch.hs

The basic idea is to write a main function which is all the functions under test:

--------------------------------------------------------
module Catch where
import StackSet

main = screen ||| peekStack ||| index ||| ...
--------------------------------------------------------

Catch takes care of all the remaining details. The ||| operator says to check that under all circumstances the function will not crash with a pattern-match error. The module is actually slightly more involved, but this is all detail which Catch will shortly hide into a library.

A future intention is to have a tool which automatically generates such a module from a library. This then allows the person performing the checking to simply point at a library, with no additional infrastructure.

Step 4: Test using Catch

This step is the first time we actually invoke Catch - and its as simple as a single line:

> catch Catch.hs -errors -partial

And thats it, now Catch gives you all the necessary information to start fixing your code. I emailed a summary of the results as given by Catch to the XMonad list: http://www.haskell.org/pipermail/xmonad/2007-May/000196.html

At this point I hopped on IRC, and in discussions with sjannsen talked him through installing Catch and the necessary dependencies. Once he had this installed, he was able to modify the StackSet API and implementation to guarantee that no pattern match errors are raised. After all of this, now running Catch over the test script gives success.

A lesson to take away

There were only two sticking points in running Catch over XMonad. The first was that Yhc can't always compile the code, and may require slight tweaks to be made. There are two solutions to fixing this, we can either fix Yhc, or I can make Catch use GHC Core. The GHC Core solution shouldn't be too much work, once GHC has a library for external Core.

The second sticking point is that installing Catch is a lot harder than it should be. A little bit of Cabal magic and a proper release should squash these problems easily.

So what lessons did I learn? Perhaps the thing that surprised me most is how easily someone else was able to get to grips with the Catch tool. This gives me a strong sense of hope that average users may be able to employ the Catch tool upon their programs, either in this version of a future version.