State Space Reduction for Process Algebra Specifications

Hubert Garavel and Wendelin Serwe

Proceedings of the 10th International Conference on Algebraic Methodology and Software Technology AMAST 2004 (Stirling, Scotland), July 2004

Extended version available in Theoretical Computer Science, 351(2) 131-145, February 2006.

Abstract:

Data-flow analysis to identify ``dead'' variables and reset them to an ``undefined'' value is an effective technique for fighting state explosion in the enumerative verification of concurrent systems. Although this technique is well-adapted to imperative languages, it is not directly applicable to value-passing process algebras, in which variables cannot be reset explicitly due to the single-assignment constraints of the functional programming style. This paper addresses this problem by performing data-flow analysis on an intermediate model (Petri nets extended with state variables) into which process algebra specifications can be translated automatically. It also addresses important issues, such as avoiding the introduction of useless reset operations and handling shared read-only variables that children processes inherit from their parents.

17 pages
PDF
PostScript


Slides of W. Serwe's lecture at AMAST 2004
PDF

DISCUSSION

The public presentation of this paper at AMAST 2004 gave rise to a question to which Wendelin Serwe could not answer at that time, due to the lack of specific experimental data.

Question by Jan Friso Groote: How effective is this reduction method, given that Caesar was known to generate state spaces larger than needed? Stated otherwise, how does the new Caesar 7.0 compare to similar tools, e.g., the mcrl toolset?

Answer: This question can only be answered if one finds common benchmarks on which both Caesar and the mcrl toolset can be evaluated. Concretely, one needs significant case-studies, the source code of which is available both in LOTOS and mcrl.

We know one such case-study tackled by Thomas Arts, Clara Benac Earle, and John Derrick: a resource locking protocol developed by Ericsson, specified in Erlang, and verified using both CADP and the mcrl toolset.

From this example, Clara Benac Earle extracted a suite of six Erlang benchmarks, which she translated into both LOTOS and mcrl, so as to compare the respective performance of Caesar and the mcrl toolset. We believe that these benchmarks are not biased in favour of one tool or another, as they originate from an industrial example and they have been developed by reputed `third-party' scientists.

The following table provides experimental data for the six benchmarks of Clara Benac Earle. These benchmarks correspond to all possible combinations of five client processes accessing a server process either in "exclusive" mode or in "shared" mode.

For each benchmark, we compared Caesar 6.2 (as available in CADP 2001), mcrl 2.14.8 (as available in June 2004), and Caesar 7.0 (which implements our state-space reduction method for value-passing process algebras).

For each mcrl specification, there exist three corresponding LOTOS specifications:

Note: The labelled transition systems generated from the mcrl and LOTOS specifications are branching equivalent modulo a renaming of labels (because mcrl and LOTOS do not use the same syntactic conventions for data values and labels). In particular, the mcrl and "naive" specifications produce the same labelled transition systems, apart from additional tau-transitions required by the official LOTOS semantics of the ">>" operator.

All experiments were conducted on a SunBlade 100 with 1.5 GB RAM (the same machine as used for the experiments in the AMAST 2004 paper). The execution times for the mcrl toolset are obtained by adding the execution times of mcrl (about one second in all cases) and instantiator. The mcrl tool was invoked with the options recommended on its help page, namely "-nocluster -regular2 -newstate"; calling additional tools such as stategraph and constelm provided no improvement. The execution times for Caesar 6.2 and 7.0 do not include the time necessary for calling the Caesar.adt data type compiler (half a second) since it needs to be called only once for all examples.

Finally, to answer Prof. Groote's question, our main findings are the following:


Benchmark Program States Transitions Time
5 exclusive clients caesar 6.2 naive 142,981235,42559 sec
untyped 91,431174,77542 sec
typed 91,431174,77513 sec
mcrl 9,997 17,025 1 min 7 sec
caesar 7.0 naive 11,92720,2359 sec
untyped 7,407 14,295 7 sec
typed 7,407 14,295 6 sec
4 exclusive clients
1 shared client		 caesar 6.2 naive 103,285171,80133 sec
untyped 66,339124,55924 sec
typed 66,339124,55910 sec
mcrl 6,033 10,465 47 sec
caesar 7.0 naive 7,16312,3399 sec
untyped 4,567 8,735 7 sec
typed 4,567 8,735 6 sec
3 exclusive clients
2 shared clients		 caesar 6.2 naive 113,277197,45338 sec
untyped 74,019146,81127 sec
typed 74,019146,81111 sec
mcrl 6,315 11,653 48 sec
caesar 7.0 naive 7,41713,5119 sec
untyped 4,877 9,939 7 sec
typed 4,877 9,939 6 sec
2 exclusive clients
3 shared clients		 caesar 6.2 naive 259,675565,4371 min 41 sec
untyped 174,129434,3591 min 12 sec
typed 174,129434,35924 sec
mcrl 14,215 32,643 1 min 17 sec
caesar 7.0 naive 16,82338,18710 sec
untyped 11,163 28,551 8 sec
typed 11,163 28,551 6 sec
1 exclusive client
4 shared clients		 caesar 6.2 naive 1,116,1693,244,02913 min 17 sec
untyped 729,6912,311,5158 min 9 sec
typed 729,6912,311,5152 min 6 sec
mcrl 59,073 176,293 4 min 33 sec
caesar 7.0 naive 71,963212,91922 sec
untyped 45,595 146,099 16 sec
typed 45,595 146,099 10 sec
5 shared clients caesar 6.2 naive > 5,603,037> 18,710,000> 5h
untyped 4,264,79115,835,3352 h 47 min 35 sec
typed 4,264,79115,835,33522 min 5 sec
mcrl 298,437 1,100,305 20 min 56 sec
caesar 7.0 naive 375,3071,368,0952 min 38 sec
untyped 221,567 832,515 1 min 30 sec
typed 221,567 832,515 42 sec