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.

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.

A Database Approach to Distributed State Space Generation (accepted for publication to PDMC 2007).

Abstract

We study distributed state space generation on a cluster of workstations. It is explained why state space partitioning by a global hash function is problematic when states contain variables from unbounded domains, such as lists or other recursive datatypes. Our solution is to introduce a database which maintains a global numbering of state values. We also describe tree-compression, a technique of recursive state folding, and show that it is superior to manipulating plain state vectors.

This solution is implemented and linked to the μCRL toolset, where state values are implemented as maximally shared terms (ATerms). However, it is applicable to other models as well, e.g., PROMELA models via the NIPS virtual machine. Our experiments show the trade-offs between keeping the database global, replicated, or local, depending on the available network bandwidth and latency.

The work described here has been in successful production use for some time. Still, during the measurements of the paper, we got a truckload of ideas for improvements. Watch this space...

Fun war story: when measuring, we found that 2% of the zillion queries between the cluster nodes and the database were unproportionally slow: They took a whopping 200 milliseconds round-trip! With some analyzer gear plugged into the switch and the help of our networking guys, we were able to predict when one of the slow messages would appear (confirmed by program instrumentation). In the end we traced it down to a driver problem. Switching to a different brand of network cards made the problem go away.

An Embeddable Virtual Machine for State Space Generation (accepted for publication to SPIN 2007).

Abstract

The semantics of modelling languages are not always specified in a precise and formal way, and their rather complex underlying models make it a non-trivial exercise to reuse them in newly developed tools. We report on experiments with a virtual machine-based approach for state space generation. The virtual machine's (VM) byte-code language is straightforwardly implementable, facilitates reuse and makes it an adequate target for translation of higher-level languages like the SPIN model checker's PROMELA, or even C. As added value, it provides efficiently executable operational semantics for modelling languages. Several tools have been built on top of the VM implementation we developed, to evaluate the benefits of the proposed approach.

This is one pixel in a bigger picture.

Together with Moritz Hammer, I wrote a paper on how to explore very large state spaces: To Store or Not to Store Reloaded: Reclaiming Memory on Demand (accepted for publication to FMICS 2006).

Abstract

Behrmann et al. posed the question whether "To Store or Not To Store" states during reachability analysis, in order to counter the effects of the well-known state space explosion problem in explicit-state model checking. Their answer was to store not all but only some strategical states. They pay in run-time if the answer too often is "Not To Store". We propose a different strategy to adaptively trade time for space: "To Store" as many states as memory limits permit. If memory runs full, we gradually swap states out to secondary storage. We are careful to minimize revisits, and I/O overhead, and also stay sound, i.e. on termination it is guaranteed that the full state space has been explored. It is also available for counterexample reconstruction. In our experiments we tackled state spaces of industrial-sized models with more than 10⁹ explicit states with still modest storage requirements.

We actually have a practical application for this: automatically finding subtle bugs in Embedded Systems software.