Graphics Programs Reference
In-Depth Information
We assume that there is a process that initiates the concurrent execution of a
certain number of processes. This is the equivalent of the PLACED PAR
instruction in Occam. Processes can be activated by a PLACED PAR
instruction or by any PAR instruction contained in an already activated
process. In the command PAR A B ENDPAR, A and B are names of
processes and the execution of the command corresponds to instantiating
and activating a copy of each process.
Having discussed the type of languages we are interested in, we must de-
cide which features of a program we want to represent in the model. It is
important to remark that GSPNs could account for all the details of a real
concurrent program. This approach would lead to enormous nets, cluttered
with lots of details, and with huge reachability graphs. These models would
be di
cult to analyse and their results problematic to interpret. The choice
of what to model must be driven by the type of results we want to ob-
tain. Each program can be represented with different levels of abstraction,
yielding different consequences in terms of complexity and accuracy of their
analysis: in particular, it is clear that, if we want to study deadlocks, all
process synchronizations must be carefully described.
10.2.2
The translation procedure
A possible choice for the abstraction level to be used in the translation is
that of including in the model control flow, process activation and com-
single communication statement as well as each PAR, SEQ, ALT, if, and
while (repeat, for) statement that includes in its body a communication
or a process activation (i.e. an ALT, PAR, a ! or a ?). A sequence of
statements that does not include any of these instructions is represented in
the GSPN system as a timed transition whose associated delay depends on
its length.
Using this level of abstraction, concurrent programs are translated into
GSPN systems according to the following procedure.
1. From each process we obtain a process schema by coalescing into single
macro-statements all those sequences of statements that do not include
any communication or any PAR.
2. Each process schema yields a GSPN system in which processes acti-
vated by a PAR are represented by single transitions (i.e., they are
not substituted by their translation), communication statements are
represented as immediate transitions (thus disregarding the explicit
representation of the communication partner, as well as the synchro-
nization aspect of the rendez-vous), and macro-statements are substi-
tuted by timed transitions (whose associated delay is an estimate of
their execution time).
Search WWH ::
Custom Search