Michael Weber: Random Bits and Pieces

New Paper

A Multi-Core Solver for Parity Games (accepted for publication to PDMC 2008).

Abstract

We describe a parallel algorithm for solving parity games, with applications in, e.g., modal μ-calculus model checking with arbitrary alternations, and (branching) bisimulation checking. The algorithm is based on Jurdzinski's Small Progress Measures. Actually, this is a class of algorithms, depending on a selection heuristics.

Our algorithm operates lock-free, and mostly wait-free (except for infrequent termination detection), and thus allows maximum parallelism. Additionally, we conserve memory by avoiding storage of predecessor edges for the parity graph through strictly forward-looking heuristics.

We evaluate our multi-core implementation's behaviour on parity games obtained from μ-calculus model checking problems for a set of communication protocols, randomly generated problem instances, and parametric problem instances from the literature.

Lisp Logo (by Conrad Barsky)

Recently, I made good use of Michael Parker's CLAWK, a Lisp-embedded variant of AWK.

So far, I had used the real AWK, along with perl and other parts of the Unix toolbox to analyze data from experiments, and munge it into HTML and LaTeX tables. However, this time I expected the experiments to be carried out in a run–tweak–rerun fashion with several iterations, and I did not want to reparse several hundred megabytes each time, just for a change in table layout, or for adding another analysis. (Also, I had not much time for lispy things recently, so this was a good way to sneak some Lisp back into my current C++ hell...)

Enter CLAWK. The following function parses my benchmark data into Lisp objects:

(defvar *foo-table* (make-hash-table :test 'equal))

(defawk parse-foo-benchmark (&aux model)
  (#/^memtime/
   (when model
     (emit-model model *foo-table*))
   (let ((path (parse-namestring $6)))
     (setf model (make-instance 'foo-model-record :filename path))))
  (#/^Instantiator: Explored/
   (setf (get-states model) $#3
         (get-transitions model) $#6
         (get-bfs-levels model) $#9
         (completed? model) t))
  ((string= $6 "elapsed")
   (setf (get-generation-time model) $#5))
  ((string= $13 "RSS")
   (setf (get-generation-memory model) (parse-integer $15 :junk-allowed t)))
  (END
   (when model
     (emit-model model *foo-table*))
   *foo-table*))

Parsing the bulk of my data with the above function takes about 80 seconds, probably slower than it would be with AWK. However, once parsed I have all the data available at my fingertips inside the Lisp image. I can prod it with the SLIME inspector, identify outliers, and play around with it in the REPL until I am satisfied. In addition, I can selectively rerun parts of the experiments, and parse just the newly produced output to update the in-memory representation, again in no time flat. Beats the Unix everything is a byte stream way every day of the week.

Rendering the results as HTML is a breeze with CL-WHO. The same holds for reordering columns, marking interesting entries programmatically, cross-referencing with other entries (or earlier versions of the data) and refining the analyses as much as I wish, with instant feedback.

Unfortunately, CLAWK has acquired some bitrot since its release in 2002 (?). I needed to tweak it slightly to make it compile (only tested with SBCL). When I tried to contact Michael Parker, his email bounced, so I decided to put up a patched version locally until the changes are folded back into his distribution. In addition, CLAWK is now ASDF-installable (along with its dependency, REGEX), courtesy of Redshank's ASDF Defsystem skeleton.

If time permits, I will fix up the code some more to get rid of the warnings, and perhaps allow CL-PPCRE as alternative regular expression engine. However, patches from the open-source fairies are very welcome, too.

New Paper

Revisiting Resistance Speeds Up I/O-Efficient LTL Model Checking (accepted for publication to TACAS 2008).

Abstract

Revisiting resistant graph algorithms are those that can tolerate re-exploration of edges without yielding incorrect results. Revisiting resistant I/O efficient graph algorithms exhibit considerable speed-up in practice in comparison to non-revisiting resistant algorithms. In the paper we present a new revisiting resistant I/O efficient LTL model checking algorithm. We analyze its theoretical I/O complexity and we experimentally compare its performance to already existing I/O efficient LTL model checking algorithms.

MacFusion SSHFS Icon

MacFusion is a graphical user interface for MacFUSE. In a nutshell, it lets me mount remote file systems with a mouse click. The FTP protocol is supported as well (finally read/write FTP on MacOS X via the Finder!), but who wants that if SSHFS is an option?

UPDATE 2008-01-08: iTunesFS

iTunesFS Icon

While we are at it, iTunesFS is worth looking at, too.