=Paper=
{{Paper
|id=Vol-1525/paper-07
|storemode=property
|title=A state space tool for concurrent system models expressed in C++
|pdfUrl=https://ceur-ws.org/Vol-1525/paper-07.pdf
|volume=Vol-1525
|dblpUrl=https://dblp.org/rec/conf/splst/Valmari15
}}
==A state space tool for concurrent system models expressed in C++==
https://ceur-ws.org/Vol-1525/paper-07.pdf
SPLST'15
A State Space Tool for Concurrent System
Models Expressed In C++
Antti Valmari
Department of Mathematics
Tampere University of Technology
P.O. Box 553, FI–33101 Tampere, FINLAND
Antti.Valmari@tut.fi
Abstract. This publication introduces a state space exploration tool
that is based on representing the model under verification as a piece
of C++ code that obeys certain conventions. This approach facilitates
experimenting with many kinds of modelling ideas. On the other hand,
the use of stubborn sets and symmetries requires that either the mod-
eller or a preprocessor tool analyses the model at a syntactic level and
expresses stubborn set obligation rules and the symmetry mapping as
suitable C++ functions. The tool supports the detection of illegal dead-
locks, safety errors, and may progress errors. It also partially supports
the detection of must progress errors.
Keywords: model checking; stubborn sets; symmetries; safety; progress
1 Introduction
This publication discusses A State Space Exploration Tool called ASSET. It
started in autumn 2014 as a simple quickly written tool that could be used
to illustrate deadlocks, livelocks, the effect of the level of atomicity, and other
concurrency-related issues to advanced programming students. The students had
programmed in C++. An important goal was that starting to use the tool would
not require complicated installation or learning a new language. Indeed, to install
ASSET, it suffices to download one C++ file called asset.cc. (However, the
need to learn concurrency-oriented concepts such as local state, global state and
transition cannot, of course, be avoided.)
At the same time, the need arose to test a new method [10] of alleviating the
state explosion problem. ASSET proved very suitable for that purpose.
ASSET is written in C++. From the point of view of its users, the key differ-
ence to other state space tools is that ASSET does not have an input language
of its own, such as the Promela language of the SPIN tool [4] or the textual
CSP language of the FDR tool [7]. Instead, the user represents the model under
verification as a piece of C++ code that uses the pre-defined type state var
provided by ASSET and implements certain functions such as fire transition,
print state, and check state. The model is checked by copying it to the file
91
SPLST'15
asset.model and then compiling and executing the file asset.cc. The latter
#includes the former.
The advantage is that the user can use most C++ features and his/her earlier
programming knowledge very flexibly when writing models of concurrent systems
and verification questions. The examples in this publication give an idea of what
can be achieved. The disadvantage is that although the modelling of individual
transitions is simple and natural, the part of code that directs execution to the
right transition is often an ugly collection of if- and switch-statements.
This approach leads to very fast execution of the transitions of the model,
because the model is compiled into machine code instead of being simulated by
ASSET. This idea is not new. For instance, SPIN uses it.
Another drawback is that ASSET cannot perform any syntactic analysis on
the model, because it is not read by ASSET but by the C++ compiler. This is
not a big problem for plain state space exploration. On the other hand, some
advanced methods such as the symmetry method [2, 3, 5] require such analysis.
The symmetry method relies on a function that, in a certain sense, represents
the symmetry that is exploited. The typical approach is that the input language
supports modelling the system in a way that makes the symmetry obvious, so
that the tool can easily pick it and construct the necessary function. This means
that also the modeller knows the symmetry. Designing the function only requires
basic understanding of the symmetry method, and representing it in C++ is just
a programming problem. ASSET is used in this way in Section 6. Although this
is of course less convenient than the typical approach, it is realistic, especially
when ASSET is used for teaching or for scientific experiments.
The advanced method known as stubborn sets [8–10] requires so complicated
syntactic analysis that most users cannot be expected to perform it. However,
it is reasonable to make experiments where an expert performs the analysis
and writes the result in a form that is suitable for ASSET. The results of such
experiments would tell whether it would be worth the effort to implement a
preprocessor tool that would perform the analysis, or to implement the method
in other state space exploration tools than ASSET. The experiment in [10] was
of this kind, and another is reported in Section 5.
ASSET and many models are available at http://www.cs.tut.fi/˜ava/ASSET/.
Throughout this publication, a demand-driven token ring is used as an exam-
ple. It is introduced in Section 2 and modelled for ASSET in Section 3. Section 4
discusses the features that ASSET offers for specifying correctness properties.
Sections 5 and 6 focus on the use of the stubborn set and symmetry methods
in ASSET. Results of the experiments with the example system are collected in
Table 1 towards the end of the publication. They clearly show the good time and
memory efficiency of ASSET and the benefits of stubborn sets and symmetries.
2 The Demand-Driven Token Ring
The demand-driven token ring system is a mutual exclusion system. Its overall
structure is shown in Figure 1. The system consists of n clients C0 , . . . , Cn−1
92
SPLST'15
C0 C1 C2 Cn−1
r0 g0 l0 r1 g1 l1 r2 g2 l2 rn−1 gn−1 ln−1
d0 d1 d2 d3 · · · dn−1
t0 S0 t1 S1 t2 S2 t3 · · · tn−1 Sn−1
Fig. 1. Overall structure of the demand-driven token ring.
and n servers S0 , . . . , Sn−1 . Each client has a specific piece of code called critical
section. The purpose of the system is to ensure that two or more clients are never
simultaneously in their critical sections. This property is called mutual exclusion.
The system must also guarantee eventual access, that is, always when a client
has requested for access to its critical section, it eventually gets the permission
to go there. The servers receive requests from the clients, grant permissions to
enter the critical sections, and receive notices that the clients have left the critical
sections. In Figure 1, these are denoted with arrows labelled with ri , gi , and li .
To guarantee mutual exclusion, precisely one token circulates in the ring.
Only the server that has the token may grant permission to its client. To avoid
unnecessary activity, the token is circulated only when there is a pending request.
When a server Si that does not have the token gets a request from its client,
it demands the token from the previous server via di . The demand propagates
in the ring until it reaches the server Sj that has the token. If Cj has made a
request or is in its critical section, then Sj grants permission if it has not yet
done that, and waits until Cj has left its critical section, after which Sj gives the
token to Sj⊕1 . By x ⊕ y we mean (x + y) modulo n. Otherwise Sj just gives the
token to Sj⊕1 . The server Sj⊕1 first serves its own client if it has made a request,
and then gives the token to Sj⊕2 . In this way the token eventually propagates
to Si which can then grant permission to its server.
The clients are shown in state machine form in Figure 2 left. The critical
section consists of state 2. In addition to the ri -gi -li cycle that models requesting
for access and then entering and leaving the critical section, there is a transition
from state 0 to state 3. It models the unforced request property, that is, that
the client may choose to not request for access. This is important for catching
certain kinds of errors.
To see this, assume that the servers are modified such that after getting the
token, each server always waits until its client makes a request and then serves
its client before giving the token to the next server. This is incorrect, because if
the client never makes the request, then the token is blocked at that server, and
the requests by other clients remain unsatisfied forever.
However, in the absence of the transition from state 0 to state 3, this error
would not be caught. This is because most if not all formalisms for concurrency
make implicitly or explicitly the assumption that if something can happen, then
something will happen. (Without this assumption, systems could deadlock at
any time without a reason, which of course would be an inappropriate model
93
SPLST'15
0: wait until ri or di⊕1 has occurred
if ti has not occurred then di
li goto 1
0 2
1: wait until ti has occurred
ri gi
if ri has occurred then gi ; goto 2
3 1 else ti⊕1 ; goto 0
2: wait until li has occurred
ti⊕1 ; goto 0
Fig. 2. The clients and servers.
of reality.) With the assumption, with the modified servers, and without the
transition from state 0 to state 3, consider the situation where every client has
made the request except the one whose server has the token, and all demands
have propagated to that server. Then the only thing that can happen is that
this client makes a request. The assumption forces it to happen. So the client is
forced to make the request even if it does not want to. The client behaviour that
would reveal that the servers are incorrect is thus left out from the analysis.
Another way to look at this is that there is a fundamental difference between
the transitions from state 2 to state 0 and from state 0 to state 1. If the client
chooses to stay in its critical section — that is, state 2 — forever, then requests
by other clients cannot be satisfied without violating mutual exclusion. On the
other hand, not satisfying them violates eventual access. Because of this, every
reasonable analysis of eventual access assumes that if a client is in its critical
section, it eventually leaves it. On the other hand, we just argued that we must
not assume that if a client is in its initial state, it eventually makes a request.
This is a fundamental difference.
Often this difference is represented with so-called idling transitions and fair-
ness assumptions, as explained in [6]. Another mainstream method is to exploit
some variant of so-called failures [1, 7]. We do so by adding the transition from
state 0 to state 3. The client is not forced to take the transition from state 0 to
state 1, because it can take the transition from state 0 to state 3 instead.
That this model is appropriate has been argued in [10,11], based on the theory
of (stable) failures. We do not present full details here, but do briefly discuss
one issue that has caused confusion. Because the client cannot come back from
state 3 to state 0, this model might seem inappropriate in the situation where
the client does not want to make a request now but wants to make it some
later time. However, this situation is represented by the possibility of the client
staying at state 0 until it wants to make a request again. Moving to state 3 only
represents the possibility of making a request never again.
The behaviour of the servers is too tricky to be shown here as a state machine.
Instead, it is represented in pseudocode in Figure 2 right. A precise ASSET model
will be shown in Figure 4.
The server stays in state 0 as long as it has no request or demand to serve.
While in this state, it may have the token. A request or demand makes it to move
to state 1. When going there, it demands the token, if it does not yet have it. It
94
SPLST'15
#ifdef size_par // n is the number of clients and servers
const unsigned n = size_par; // n comes from the compilation command
#else
const unsigned n = 6; // default value of n
#endif
state_var
C[n] = 2, // state of client i:
// 0 = idle, 1 = requested, 2 = critical, 3 = terminated
S[n] = 2, // state of server i:
// 0 = idle, 1 = waiting for token, 2 = waiting for client
T[n] = 1; // true <==> server i has token
#ifdef symm_must // a trick used with the symmetry method
state_var c0now; // the current index of the original client 0
#else
unsigned const c0now = 0;
#endif
const char Cchr[] = { ’-’, ’R’, ’C’, ’ ’ }, Schr[] = { ’i’, ’w’, ’t’ };
void print_state(){
for( unsigned i = 0; i < n; ++i ){
std::cout << Cchr[C[i]] << Schr[S[i]];
if( T[i] ){ std::cout << ’*’; }else{ std::cout << ’ ’; }
}
std::cout << ’\n’;
}
Fig. 3. Model of the demand-driven token ring, part 1.
stays in state 1 until it has the token. If it does not have a pending request by
its client, it gives the token to the next server and returns to the initial state 0.
Otherwise it grants the permission to its client and goes to state 2. It waits there
until its client leaves the critical section, after which it gives the token to the
next server and returns to the initial state.
When going from state 2 to state 0, the server gives the token to the next
server even in the absence of a demand. The purpose of this is to ensure that if
its own client makes immediately a new request, it is not served before the other
clients have had the chance to go to the critical section.
3 ASSET Model of the System
Figures 3 and 4 show the model of the example system.
The #ifdef size par structure makes it possible to specify the number of
clients and servers via an option that is given to the C++ compiler. Also many
features of ASSET can be controlled in a similar way. For instance, with the Gnu
95
SPLST'15
C++ compiler, the options -Dstubborn -Dsize par=13 -Dstop cnt=100000000
command ASSET to use stubborn sets, set n = 13, and stop the construction of
the state space when 108 states are exceeded.
The initialization C[n] = 2 does not specify that the initial local state of each
client is 2 (the critical section) but that two bits are used for representing the
local state of each client. The value of each state variable is an unsigned integer
in the range 0, . . . , 2b − 1, where b is the number of bits. The default value of b
is 8. The initial value of each state variable is 0.
Internally, ASSET represents the state of the model as a sequence of unsigned
integers. To save memory, ASSET packs many state variables into the same
unsigned integer when possible. A state var object does not store the value of
the state variable, but information on in which unsigned integer and in which of
its bits the value is stored. If the most recently employed unsigned integer has
at least as many unused bits as the next state variable needs, then ASSET puts
the state variable there. This implies that the order in which the state variables
are declared may affect the amount of memory that ASSET uses per state. For
instance, assuming 16-bit unsigned integers, A x A i
state var x, A[7]=3, i(2);
consumes three unsigned integers, while Ai x A
state var x, i(2), A[7]=3;
consumes only two.
The purpose of c0now will be explained in Section 6. Until then, please
assume that c0now is 0.
When ASSET has detected an error, it prints a counterexample in the form
of a sequence of states. For this purpose, it needs a print state function. To
improve the readability of the counterexamples, the function in Figure 3 uses
character encodings for local states. The use of C++ facilitates this and other
methods for making the printout look natural for the model. This has been
widely exploited in the models on the web page of ASSET.
The function nr transitions in Figure 4 tells ASSET how many transitions
the model contains. The most common case is that a transition models one or
more atomic operations of the system. Transitions in ASSET are deterministic.
This implies that nondeterministic operations such as tossing a coin must be
modelled by more than one transition. Other than that, ASSET does not restrict
the grouping of atomic operations to transitions.
In its initial state, a client of the example system makes a nondeterministic
choice between requesting access and terminating for good. For this reason, two
transitions are used to model each client. Each server has one transition.
The function nr transitions may also be used for implementing whatever
operations are necessary before starting the construction of the state space. In
Figure 4, it is used for giving the token to client 1. Client 1 was chosen here,
because eventual access will be tested for client 0, so we wanted it to lack the
token initially.
96
SPLST'15
unsigned nr_transitions(){ T[1] = true; return 3*n; }
inline unsigned next( unsigned i ){ return (i+1) % n; }
inline unsigned prev( unsigned i ){ return (i+n-1) % n; }
bool fire_transition( unsigned i ){
/* Servers */
if( i >= 2*n ){
i -= 2*n;
#define goto(x){ S[i] = x; return true; }
switch( S[i] ){
case 0:
if( C[i] == 1 || ( S[next(i)] == 1 && !T[next(i)] ) ){ goto(1) }
return false;
case 1:
if( !T[i] ){ return false; }
if( C[i] == 1 ){ C[i] = 2; goto(2) }
if( S[next(i)] == 1 ){ T[i] = false; T[next(i)] = true; goto(0) }
return false;
case 2:
if( C[i] == 2 ){ return false; }
T[i] = false; T[next(i)] = true; goto(0)
default: err_msg = "Illegal local state"; return false;
}
#undef goto
}
/* Clients */
#define goto(x){ C[i] = x; return true; }
if( i >= n ){ // termination transition
i -= n;
if( C[i] == 0 ){ goto(3) }else{ return false; }
}
if( C[i] == 0 ){ goto(1) } // request access
if( C[i] == 2 ){ goto(0) } // leave critical
return false;
}
Fig. 4. Model of the demand-driven token ring, part 2.
97
SPLST'15
The transitions of the model are numbered starting from 0. The function
fire transition(t) returns true or false to indicate whether transition num-
ber t is enabled. If t is enabled, then fire transition modifies the state ac-
cording to the occurrence of t. If t is disabled, then fire transition must not
modify the state. This rule makes it possible for ASSET to try the next transition
without having to upload the state again.
To improve readability, Figure 4 introduces two versions of a goto(x) macro.
They model the server and the client going to local state x and indicate that the
transition was enabled.
If 0 ≤ t < n, transition t models client t going either from local state 0 to
local state 1 (that is, requesting access) or from local state 2 to local state 0
(leaving the critical section). If n ≤ t < 2n, transition t models client t − n going
from local state 0 to local state 3 (that is, terminating).
Finally, the transitions 2n ≤ t < 3n model server t − 2n. It waits in local
state 0 until its client requests access or the next server needs the token. For the
reason discussed in Section 5, it tests that the next server does not already have
the token.
Then it waits in local state 1 until it has the token. If its client has requested
access, it moves the client to the critical section and goes to local state 2. Oth-
erwise, if the next server needs the token, server t − 2n gives it to it. Otherwise,
server t − 2n continues waiting.
In local state 2, server t − 2n waits until its client has left the critical section.
Then it gives the token to the next server and returns to the idle state. As a
consequence, its client cannot get access again before the token has circulated
through the ring and the other clients have had the chance to get access.
The default branch is explained in Section 4.
4 The Checking Features
Figure 5 shows the checking functions used in the experiments of this publication.
Each of them can be switched off by commenting out the corresponding #define,
without having to comment out the function as a whole. This is handy for
experimenting. (It would have been nice to use the same word in the #define
and as the name of the function, but C++ does not allow that.) More flexibility
comes from the fact that if xxx has not been switched on in the model with
#define xxx, then it can be switched on at compile time with a compiler option.
ASSET operates in stages. In the first stage, it checks for safety errors and
illegal deadlocks (if the checking of them has been switched on). It constructs
the state space in breadth-first order, to minimize the length of counterexam-
ples. ASSET calls check state each time when it has constructed a new state,
and check deadlock when it has tried to fire transitions in a state but none
was enabled. If the state is not good, the function returns a character string.
ASSET prints an error message containing it and terminates. That is, ASSET
implements on-the-fly detection of safety and illegal deadlock errors. That the
state is good is indicated by returning the null pointer 0.
98
SPLST'15
/* Check that at most one client is in critical section at any time. */
#define chk_state
const char *check_state(){
unsigned cnt = 0;
for( unsigned i = 0; i < n; ++i ){ if( C[i] == 2 ){ ++cnt; } }
if( cnt >= 2 ){ return "Mutual exclusion violated"; }
return 0;
}
/* Check that every client has stopped. */
#define chk_deadlock
const char *check_deadlock(){
for( unsigned i = 0; i < n; ++i ){
if( C[i] != 3 ){ return "Client not terminated"; }
}
return 0;
}
/* Check that the original client 0 eventually gets access
if it wants to. */
//#define chk_must_progress
bool is_must_progress(){ return C[c0now] != 1; }
Fig. 5. The check functions of the model of the demand-driven token ring.
By using a global or static C++ variable, check deadlock (or check state)
can be made to count the number of deadlocks that it has detected, and only give
the error message for, say, the tenth. Thus, although ASSET does not provide a
mechanism for investigating each deadlock in turn, C++ makes it possible.
If ASSET did not detect any errors and if it has further checks to perform,
it constructs a data structure that contains the edges of the state space in the
reverse direction. To do that, it goes through all states that it has found and
fires the transitions again in them. (In the case of stubborn sets, it fires the same
subsets of transitions.) In this way, only one unsigned integer per edge is needed.
Storing the edges during the first stage and sorting them afterwards would have
used two unsigned integers per edge.
Then, if chk may progress is on, ASSET checks the state space for may
progress errors by performing a linear-time search along the reversed edges. A
may progress error is a reachable state from which no terminal state and no state
accepted by is may progress is reachable. May progress can be thought of as
a less stringent alternative to linear-time liveness that does not need fairness
assumptions. This feature has been discussed extensively in [10] and is not used
in the experiments of the present publication, so it will not be discussed further
here.
Next ASSET checks the state space for must progress errors, if it has been
commanded to do so and it has not yet terminated because of another error. A
99
SPLST'15
must progress error is a cycle in the state space that does not contain any state
accepted by is must progress. This is a restricted form of checking linear-time
liveness. For reasons discussed in the next two sections, the simultaneous use of
this feature with stubborn sets and symmetries is limited. Therefore, it has been
switched off in Table 1.
Outside Table 1, the is must progress function in Figure 5 was switched
on in some experiments. ASSET found no errors in the model in Figures 3
and 4. Also a modified model was used where, when leaving local state 2, instead
of giving the token to the next server and going to local state 0, the server
goes to local state 1. ASSET reported that this model has a cycle where a
requesting client does not get access. In it, another client leaves the critical
section, requests for access again, and gets access again. The output of ASSET
is shown below with explanatory comments. (ASSET does not minimize the
length of counterexamples that contain a cycle.)
-i -i* initial state
========== after this line, must progress fails for a pending request
Ri -i* client 0 requests
Rw -i* server 0 waits for token
---------- after the last line, the counterexample jumps back here
Rw -w* the demand reaches server 1
Rw Rw* client 1 requests
Rw Ct* client 1 gets permission
Rw -t* client 1 leaves the critical section
!!! Must-type non-progress error
46 states, 66 edges
Finally, if the stubborn set method is used, safety or progress was checked,
and ASSET has not yet found any error, it checks that the state space is always
may-terminating in the sense discussed in the next section.
The model may at any time assign a character string to err msg. It causes
ASSET to terminate and print an error message containing the string. This
feature is not intended for specifying correctness properties, but for catching
inconsistent situations within the model. In Figure 4 it is used in the default
branch of the switch statement, to indicate that the modeller believes that the
branch is never entered.
In addition to the memory needed for the state itself, ASSET uses two or five
unsigned integers per state, depending on whether the verification task involves
graph search operations in the state space. To quickly detect whether a state is
new or has been constructed also earlier, there is a hash table whose base table
uses 2h unsigned integers, where h is 23 by default but can be changed. The
stubborn set method consumes an additional 5t unsigned integers, where t is the
number returned by nr transitions.
Therefore, in theory, ASSET uses approximately ((2 + s)n + 2h )u bytes for
the easier and ((5 + s)n + m + 2h )u or ((5 + s)n + m + 2h + 5t)u bytes for the
more difficult verification tasks, where n is the number of constructed states,
100
SPLST'15
void next_stubborn( unsigned i ){
if( i >= 2*n ){
i -= 2*n;
switch( S[i] ){
case 0: if(
C[i] == 1 || ( S[next(i)] == 1 && !T[next(i)] )
){ return; }
stb(i, next(i)+2*n); return;
case 1: if( !T[i] ){ stb(prev(i)+2*n); return; }
if( C[i] == 1 ){ return; }
if( S[next(i)] == 1 ){ stb(i); return; }
stb(i, next(i)+2*n); return;
case 2: if( C[i] == 2 ){ stb(i); }
return;
default: return;
}
}
if( i >= n ){ stb(i-n); return; }
switch( C[i] ){
case 0: stb(i+n, i+2*n); return;
case 1: stb(i+2*n); return;
case 2: stb_all(); return;
default: return;
}
}
Fig. 6. The stubborn set obligation rules of the demand-driven token ring.
m is the number of constructed edges, s is the number of unsigned integers
used for representing a state, and u is the number of bytes in an unsigned
integer (usually u = 4 or u = 8). These formulae correctly predict the numeric
and “–” entries in Table 1. However, because of how the dynamically growing
arrays of C++ work, the real memory consumption may add almost (2 + s)nu
or (5 + s)nu bytes to this. With 13 servers and clients, the stubborn set method
yields 13·3 777 949 = 49 113 337 states. This would otherwise fit the memory, but
the doubling of the arrays at 225 = 33 554 432 states causes a memory overflow,
explaining the “..” entries in Table 1.
5 The Stubborn Set Method in ASSET
The implementation of the stubborn set method in ASSET is discussed exten-
sively in [10]. Therefore, it is discussed here only briefly.
Only the basic strong stubborn set method that preserves the deadlocks is
implemented. However, theorems in [10] tell that if the model is always may-
101
SPLST'15
terminating — that is, if from every reachable state, a terminal state is reachable,
then the basic strong stubborn set method preserves also safety and certain
progress properties. Furthermore, whether the model is always may-terminating
can be checked from the reduced state space.
To use the method, the function next stubborn must be provided. It rep-
resents state-dependent rules of the form “if this transition is in the stubborn
set, then also these transitions must be”. Figure 6 shows the rules used in the
experiments reported in Table 1.
The present author did not at first realize the necessity of the part &&
!T[next(i)] in case 0 in Figure 4. When it was lacking, the plain and sym-
metry methods did not give any error messages. Indeed, mutual exclusion and
eventual access are not violated. However, thanks to the check that the model
is always may-terminating, the stubborn set method gave the following when
n = 2.
-i -i*
-i i*
==========
Ri i*
Rw i*
Rw w*
Rw* i
Rw* w
Ct* w
-t* w
-i w*
----------
i w*
w w*
w* i
w* w
!!! State was reached from which termination is unreachable
67 states, 93 edges
In it, client 0 visits the critical section and both clients terminate. Because
waiting information may be propagated from server i ⊕ 1 to server i even if the
former has the token, unnecessary waiting information enters the ring. Eventu-
ally the model runs in a cycle where unnecessary waiting information circulates
in one direction and, driven by it, the token circulates in the opposite direction.
The cycle consists of the states below the “----------” mark. Reaching a ter-
minal state is impossible after the “==========” mark. So the first erroneous
state is Ri i*.
The stubborn set implementation in ASSET does not guarantee that must
progress errors are found. If must progress is used with stubborn sets and ASSET
finds no errors, then it gives a warning that the pass verdict is unreliable. With
the modified model discussed in Section 4, ASSET did find the error with stub-
born sets switched on. With n = 8, there were 2 472 336 states and 17 539 200
edges without and 163 264 states and 293 984 edges with stubborn sets.
102
SPLST'15
void symmetry_representative(){
unsigned i = 0;
while( !T[i] ){ ++i; } // find the server with the token
i = prev(i);
if( !i ){ return; } // terminate, if the state maps to itself
unsigned A[n], j;
for( j = 0; j < n; ++j ){ A[j] = C[(i+j) % n]; }
for( j = 0; j < n; ++j ){ C[j] = A[j]; }
for( j = 0; j < n; ++j ){ A[j] = S[(i+j) % n]; }
for( j = 0; j < n; ++j ){ S[j] = A[j]; }
for( j = 0; j < n; ++j ){ A[j] = T[(i+j) % n]; }
for( j = 0; j < n; ++j ){ T[j] = A[j]; }
#ifdef symm_must
c0now = (c0now + n-i) % n;
#endif
}
Fig. 7. The symmetry representative function of the demand-driven token ring.
6 The Symmetry Method in ASSET
Many systems contain similar components organized in a symmetric fashion.
Several authors have suggested exploiting the symmetry for reducing the size of
the state space, including [2, 3, 5].
The implementation of the symmetry method in ASSET is very simple. Un-
fortunately, as we will see, it leaves a lot of responsibility to the modeller or
preprocessor tool.
Most importantly, the modeller or preprocessor must provide a function
symmetry representative that maps each state to a symmetric state. The more
states are mapped to the same state, the better are the reduction results. Ide-
ally, all states that are symmetric to each other are mapped to the same state.
However, the method remains correct even if the function is not ideal in this
respect.
If the symmetry method has been switched on, ASSET calls the function
symmetry representative on the initial state and on each result of a successful
firing of a transition. As a consequence, paths in the reduced state space may
contain symmetry hops, that is, the head state of an edge is not necessarily the
real result of firing the transition in question in the tail state of the edge. Instead,
it may be another state that is symmetric to the real result.
Figure 7 shows the symmetry mapping used in the experiments of this pub-
lication. It first finds the server that has the token, and then rotates the ring so
that the found server becomes server 1.
The modeller or preprocessor must take the symmetry mapping into account
when formulating the checked properties. Because each of check state and
check deadlock analyses a single state, it is not difficult to make them give the
same reply on symmetric states. The versions in Figure 5 do so.
103
SPLST'15
It is more difficult with progress properties. For instance, consider the even-
tual access property “if client 0 wants to go to the critical section, it eventually
gets there”. When symm must is off, the is must progress function in Figure 5
formulates the property in a manner that is appropriate only when the sym-
metry method is not used. Because the symmetry mapping in Figure 7 always
rotates the system such that server 1 has the token, only client 1 ever gets to the
critical section in the symmetry-reduced state space. However, the rotation does
not prevent client 0 from trying to go to the critical section. What happens is
that just when client 0 is about to get to the critical section, it becomes client 1.
So ASSET incorrectly reports that client 0 tried to go to the critical section but
never got there.
To solve this problem, the state variable c0now was added to the model. It
keeps track of the current number of the original client 0. The verification results
became correct, but the reduction in the size of the state space was lost entirely.
This is a problem of not just ASSET, but the symmetry method in general.
The counterexamples printed by ASSET may contain symmetry hops. How-
ever, in the experience of the present author, they have not harmed the interpre-
tation of counterexamples. They may even be helpful. When a counterexample
contains many symmetric copies of the same theme, symmetry hops may reduce
them to a single copy.
Acknowledgement. I thank the anonymous reviewers for helpful comments.
References
1. Brookes, S. D. & Hoare, C. A. R. & Roscoe, A. W.: A Theory of Communicating
Sequential Processes. Journal of the ACM 31, 3 (1984) 560–599
2. Clarke, E. M. & Filkorn, T. & Jha, S.: Exploiting Symmetry in Temporal Logic
Model Checking. In: Courcoubetis, C. (ed.) Computer-Aided Verification ’93, Lec-
ture Notes in Computer Science 697 (1993) 450–462
3. Emerson, E. A. & Sistla, A. P.: Symmetry and Model Checking. In: Courcoubetis,
C. (ed.) Computer-Aided Verification ’93, Lecture Notes in Computer Science 697
(1993) 463–477
4. Holzmann, G. J.: The SPIN Model Checker: Primer and Reference Manual.
Addison-Wesley (2003) 596 p
5. Jensen, K.: Coloured Petri Nets, Volume 2, Analysis Methods. Monographs in The-
oretical Computer Science, Springer (1995) 174 p
6. Manna, Z. & Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems
– Specification. Springer-Verlag (1992) 427 p
7. Roscoe, A. W.: Understanding Concurrent Systems. Springer, Heidelberg, Germany
(2010) 533 p
8. Valmari, A.: Error Detection by Reduced Reachability Graph Generation. In: Pro-
ceedings of the 9th European Workshop on Application and Theory of Petri Nets
(1988) 95–122
9. Valmari, A.: The State Explosion Problem. In: Reisig, W. & Rozenberg, G. (eds.)
Lectures on Petri Nets I: Basic Models, Lecture Notes in Computer Science 1491
(1998) 429–528
104
SPLST'15
10. Valmari, A.: Stop It, and Be Stubborn! In: Haar, S. & Meyer, R. (eds.) 15th In-
ternational Conference on Application of Concurrency to System Design, IEEE
Computer Society (2015) 10–19, DOI 10.1109/ACSD.2015.14
11. Valmari, A. & Setälä, M.: Visual Verification of Safety and Liveness. In: Gaudel,
M.-C. & Woodcock, J. (eds.) Formal Methods Europe ’96: Industrial Benefit and
Advances in Formal Methods, Lecture Notes in Computer Science 1051 (1996) 228–
247
n states edges time states edges time
2 P 68 140 0.0 S 44 60 0.0
Y 34 70 0.0 B 22 30 0.0
3 P 468 1 350 0.0 S 219 327 0.0
Y 156 450 0.0 B 73 109 0.0
4 P 2 928 10 880 0.0 S 920 1 432 0.0
Y 732 2 720 0.0 B 230 358 0.0
5 P 17 280 78 600 0.1 S 3 505 5 625 0.0
Y 3 456 15 720 0.0 B 701 1 125 0.0
6 P 98 064 527 760 0.2 S 12 540 20 772 0.1
Y 16 344 87 960 0.1 B 2 090 3 462 0.0
7 P 541 296 3 364 200 0.8 S 43 015 73 899 0.2
Y 77 328 480 600 0.4 B 6 145 10 557 0.1
8 P 2 927 232 20 632 320 4.5 S 143 408 256 880 0.4
Y 365 904 2 579 040 1.6 B 17 926 32 110 0.2
9 P 15 583 104 122 821 920 30.0 S 469 053 879 885 1.4
Y 1 731 456 13 646 880 10.0 B 52 117 97 765 0.3
10 P 81 933 120 714 052 800 262 S 1 514 900 2 984 860 4.6
Y 8 193 312 71 405 280 59.5 B 151 490 298 486 0.9
11 P – – 341 S 4 852 771 10 057 839 16.3
Y 38 771 136 370 202 400 339 B 441 161 914 349 2.6
12 P S 15 464 040 33 719 400 60.1
Y – – 1039 B 1 288 670 2 809 950 9.1
13 P S .. .. 65.0
Y B 3 777 949 8 659 221 30.0
14 P S
Y B 11 116 762 26 741 542 96.1
15 P S
Y B 32 826 001 82 708 765 353
16 P S
Y B .. .. 131
Table 1. Results on the demand-driven token ring. “P” = plain, “S” = stubborn sets,
“Y” = symmetries, and “B” = both. “–” denotes that 108 states was exceeded. “..” in-
dicates memory overflow. The times are in seconds and do not include the compilation.
The experiments were run on a year 2009 laptop with a 1.6 GHz dual core processor
and 1.954 GiB (that is, 2.098 GB) of RAM.
105