Parallel State Space Construction for Model-Checking

Hubert Garavel, Radu Mateescu, and Irina Smarandache

Proceedings of the 8th International SPIN Workshop on Model Checking of Software SPIN'2001 (Toronto, Canada), May 2001

Revised version available as INRIA Research Report RR-4341 (December 2001), which supersedes an earlier version formerly available as INRIA Research Report RR-4145 (March 2001).

Abstract:

The verification of concurrent finite-state systems by model-checking often requires to generate (a large part of) the state space of the system under analysis. Because of the state explosion problem, this may be a resource-consuming operation, both in terms of memory and CPU time. In this report, we aim at improving the performances of state space construction by using parallelization techniques. We present parallel algorithms for constructing state spaces (or Labeled Transition Systems) on a network or a cluster of workstations. Each node in the network builds a part of the state space, all parts being merged to form the whole state space upon termination of the parallel computation. These algorithms have been implemented within the CADP verification tool set and experimented on various concurrent applications specified in LOTOS. The results obtained show linear speedups and a good load balancing between network nodes.

20 pages

PDF

PostScript

Slides of H. Garavel's lecture at SPIN'01

PDF

See also a more recent publication about the DISTRIBUTOR and BCG_MERGE tools.

ERRATA [May 14, 2003]

• The former version of this paper (i.e., the version published at SPIN 2001 and formerly available as INRIA Research Report RR-4145 dated March 2001) is no longer available. It is superseded by a revised version (INRIA Research report RR-4341 dated December 2001), which brings several improvements, including:
  • A refined definition of partitioned LTS based on a precise distinction between the notions of state vector and state number,

  • An improved algorithm for termination detection in the DISTRIBUTOR procedure, and

  • A more elegant algorithm for the BCG_MERGE procedure, the former definition of which contained a duplicated line of code.

• Yet, in the revised version itself, Nicolas Descoubes reported a minor error in the DISTRIBUTOR procedure defined on page 7. This error creates a "hole" in the numbering of states. More precisely, the first state processed by each node (except the initiator node) receives a number than is higher that it should be. This error can be corrected using the two following modifications:
  • The 4^th line of the DISTRIBUTOR procedure:
    n_i (s₀) := c_i ;     V_i := { s₀ } ;     S_i := { n_i (s₀) }
    should be replaced by:
    n_i (s₀) := c_i ;     c_i := c_i + N ;     V_i := { s₀ } ;     S_i := { n_i (s₀) }

  • On the 22^th line of the DISTRIBUTOR procedure, the two first instructions:
    c_i := c_i + N;     n_i (s) := c_i ;     ...
    should be permuted, so as to obtain:
    n_i (s) := c_i ;     c_i := c_i + N ;     ...