Static Analysis of Imperative Languages

Last year, I got the assignment to work through The Calculus of Computation by Bradley & Manna. The result is — in my humble opinion — a neat introduction to static reasoning for imperative languages. If you are new to that, but know a bit about predicate logic, then it might be a short and hopefully nice read to you.

Heuristics Methods for Inductive Invariant Generation in Pi explains the basics such as weakest precondition and strongest postcondition, why it is important to have inductive assertions for loops, why they are hard to find (hard as in undecidably-hard), and further what heuristics we could apply to simple standard cases to generate inductive assertions automatically.

If you enjoy it (or hate it), leave me a comment. Now, I finally found the blogger.com option to notify me, when new comments come in, so that I have a chance to reply.

Patching for broken SD card readers

I had the pleasure to buy a broken SD card reader. It reports 2GB cards as 1GB cards. Here is a fix that allows you to force capacities onto the scsi disk kernel subsystem of the Linux kernel: scsi-capacity-setter.patch. The respective user space program is here capacity.c. You might want to use it in conjunction with some udev rules.

Liskell standalone

Some time has passed since I last blogged about Liskell. It is not dead nor have I changed my mind that Haskell needs a proper meta-programming facility not to mention a better syntax.

Liskell was a branch of GHC once. Now it sits on top of the GHC API, or I should rather say sneaks behind its back as it creates its own API as the original one is not suitable for the stunts I'm interested in. If Liskell sticks with GHC as its soil, I will definitely send patches upstream to refine the GHC API in the areas where it needs more flexibility for Liskell. However for the moment, my main target was to get something out that compiles with a stable version of GHC.

You can grab it with the usual

darcs get http://code.haskell.org/liskell/

This version has been tested with ghc 6.10.1 and should install like

./Setup.lhs configure
./Setup.lhs build
./Setup.lhs install
cd LskPrelude
make install-inplace

Optionally you can run make tests in the testsuite subdirectory. Thanks to community.haskell.org for darcs hosting!

LUKS on-disk-format revision 1.1.1

Today, I published a new minor revision of the LUKS on-disk-format specification. It contains clarifications with respect to IV/tweak reference points. Thanks to Michael Gorven for the suggestion.

It is available at new home of cryptsetup/LUKS at Google Code http://code.google.com/p/cryptsetup/wiki/Specification.

XMonad GridSelect

Personally, I not just need a window manager, I need a focus manager. I tend to think of windows as TODO items, and as there are many TODOs in life there are many windows on my workspaces. Usually a fraction of that can't be closed or worked on immediately, so they linger around on my desktop, cluttering my workspace.

I used to use the Tabbed layout. But Tabbed isn't the answer when you are a guy who reports bugs such as "XMonad 0.6 with Tabbed dies when firefox-session-restore slams 40 windows at once on the desktop". In other words, I use a lot of windows. The workspaces concept isn't particularly useful to me either. My mind just doesn't work with mental boxes. So the result is, that I have too few workspaces with too much windows on them, so that Tabbed has trouble displaying useful window titles, and navigating through them is slow and cumbersome (mostly because tab switching generates a lot of useless X Expose events).

GridSelect is my answer to that. It brings up a 2D grid of windows in the center of the screen, and I can select a window with cursors keys. The window is delivered back to the caller of GridSelect, and for the moment the most useful thing it does for me is to raise and focus the selected window. The advantage over the presentation of Tabbed is that there is much more space for window titles, that are now not forced into a single row at the top of the screen, but can occupy multiple rows. Also navigating a 2D grid is also much faster than navigating a linear 1D structure.

GridSelect colorizes the cells according to the window class of displayed window. So, all windows with the same class get the same color, and after a while I start to remember which window class has which color. E.g., when I want my xchat window, I just have to search for light green, or if I want an emacs windows, I have to focus on dark violet.

Although GridSelect wasn't meant for inclusion into xmonad-contrib, dons was quick to merge it into the darcs repo. ATM I'm using the following key binding fragment:

((modMask, xK_f     ), (gridselect defaultGSConfig) >>= (\w -> case w of
                         Just w -> windows (bringWindow w) >> focus w >> windows W.shiftMaster
                         Nothing -> return ())

Ideas

There are a few ideas that I haven't found time to toy with. First I like the window arrangement to be more static. At the moment, the windows are sorted (by XMonad) according to its last use and GridSelect arranges them spiraling outwards in a diamond like pattern. Mentally, I can only keep track of the last two to three windows, so that I can blindly select them. For everything else, I have to read titles. It would be more helpful to give fixed spots to windows. Of course, windows get deleted and new windows pop up all the time, so probably it would be good to defragment and resort according to display time with a special key.

Substring search on window titles is another idea. As GridSelect uses cursors keys for the moment, the rest of the keyboard could be used to enter the string used in searching. GridSelect should then gray out the windows that do not contain the search term.

I guess I won't hack on these ideas immediately as GridSelect ATM does what it should do, namely lower the time that I spend searching for windows significantly.