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

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:

• The naive specification is obtained by a two-step translation, first from Erlang to mcrl, then from mcrl to LOTOS. The second step is a crude translation that only targets the "mcrl-like" subset of LOTOS and does not take advantage of the value-passing facility associated to the LOTOS sequential composition operators ("exit" and ">>").
• The untyped specification is obtained by a direct translation from Erlang to LOTOS. The generated LOTOS specification is identical to the naive one, except that it uses the higher-level sequential composition operators ("exit" and ">>") that exist in LOTOS but not in mcrl.
• The typed specification is obtained from the untyped one by defining distinct data types while the mcrl specification defined only one "universal" data type; this does not change the state space but makes its generation a bit faster.

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:

• On comparable specifications ("mcrl" vs "untyped"), mcrl generates larger state spaces (about 33% larger) than Caesar 7.0.

• Additionally, mcrl appears to be slower than Caesar 7.0 by an order of magnitude (13 times slower for "untyped" specifications and 23 times slower for "typed" ones).

Benchmark	Program		States	Transitions	Time
5 exclusive clients	caesar 6.2	naive	142,981	235,425	59 sec
		untyped	91,431	174,775	42 sec
		typed	91,431	174,775	13 sec
	mcrl		9,997	17,025	1 min 7 sec
	caesar 7.0	naive	11,927	20,235	9 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,285	171,801	33 sec
		untyped	66,339	124,559	24 sec
		typed	66,339	124,559	10 sec
	mcrl		6,033	10,465	47 sec
	caesar 7.0	naive	7,163	12,339	9 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,277	197,453	38 sec
		untyped	74,019	146,811	27 sec
		typed	74,019	146,811	11 sec
	mcrl		6,315	11,653	48 sec
	caesar 7.0	naive	7,417	13,511	9 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,675	565,437	1 min 41 sec
		untyped	174,129	434,359	1 min 12 sec
		typed	174,129	434,359	24 sec
	mcrl		14,215	32,643	1 min 17 sec
	caesar 7.0	naive	16,823	38,187	10 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,169	3,244,029	13 min 17 sec
		untyped	729,691	2,311,515	8 min 9 sec
		typed	729,691	2,311,515	2 min 6 sec
	mcrl		59,073	176,293	4 min 33 sec
	caesar 7.0	naive	71,963	212,919	22 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,791	15,835,335	2 h 47 min 35 sec
		typed	4,264,791	15,835,335	22 min 5 sec
	mcrl		298,437	1,100,305	20 min 56 sec
	caesar 7.0	naive	375,307	1,368,095	2 min 38 sec
		untyped	221,567	832,515	1 min 30 sec
		typed	221,567	832,515	42 sec