Graphics Programs Reference
In-Depth Information
+ while
2
), (infor
1
+ whileSpAlt + infor
2
). As we have already mentioned
in Section
10.1,
deadlock states detected by the static analysis do not nec-
essarily mean deadlocks of the program, and this must be carefully verified
case by case.
As an example let us check the state with places while
1
,while
2
and infor
1
Sp
marked. Processes P
1
and P
2
are in places while
1
and while
2
waiting to
put a communication on channels Chan
1
and Chan
2
, respectively; Spooler is
waiting for an input from P
1
Sp. This is clearly a deadlock since all processes
are blocked. We can observe that the model can reach this state starting
from a marking with process P
1
in place for
1
and Spooler in place for
1
Sp.
Indeed, since the number of iterations of the for is modelled probabilistically
and since there is no relation in the net among the two for's, process P
1
may decide to exit the for, while process Spooler may decide to do one
more loop! These decisions are perfectly legal in the GSPN system, but
do not correspond to a possible action of the program: the two fors will
indeed execute the same number of loops since they are controlled by two
variables whose values have been set equal prior to the beginning of the
communication. This feature of the real program is not captured by the
model that can thus enter an “illegal” situation.
In this simple case it is not too di
cult to understand that the deadlock
detected by the static analysis is a nonfault. This is not always the case, as
it may be necessary to trace the model execution from the deadlock state
back to the initial state: this may lead to many execution paths whose
testing can be very tedious and error prone even in the presence of proper
supporting tools.
10.4
Modelling Control Variables to Reduce Non-
faults
As we remarked at the beginning of this chapter, Petri nets have the capabil-
ity of modelling a program in great detail. In this section we shall partially
profit from this ability by including control variables into the model: we
call control variables those that appear in a test explicitly included in the
model. The goal is that of decreasing the number of anomalies detected by
the analysis which are actually nonfaults.
There is a standard way to represent a variable in a Petri net model: a place
is inserted in the net for each possible value of the variable; at most one of
these places can be marked in a state, representing the value of the variable.
Testing and assigning values to the variables is relatively simple, but the
net becomes cluttered with arcs and places when the range of the variable
is large.
Another possible solution is that of introducing one place per variable: the
number of tokens in the place indicates the value of the variable. We may
Search WWH ::
Custom Search