MODELS OF CONCURRENT ARCHITECTURES - Modelling with Generalised Stochastic Petri Nets - page 252

End of requests
from neighbours

p loc rdy

k

p ext req 1

Requests from
neighbours

t start exec

p not ext req

p ext req 2

p not exec p exec

t start req 2

t start req 1

T loc ex p req exe 1 p req exe 2

p ext acc

T end 1 T end 2

Requests to
neighbours

End of
requests

t ext acc 1

t ext acc 2

Figure 11.5: GSPN model of the behaviour of a processor in the case of
preemptive interaction and multitasking

The more elaborate GSPN models in Fig. 11.5 and 11.6 show the behaviour
of a processor taking into account multitasking and e cient use of the pro-
cessing power. Fig. 11.5 represents the case in which requests are preemp-
tive, whereas Fig. 11.6 represents the case in which requests are not preemp-
tive. It can be seen that both these models satisfy the mentioned constraints
on the scheduling policy: when a task terminates its local activity and sends
a service request to a neighbour, the processor is immediately free to serve
incoming requests or to execute another task.
In Fig. 11.5 the local computation is modelled by place p exec and transition
T loc ex with rate λ. The completion of the local computation moves a token
in p not extec , and the requests for service towards the neighbours are modelled
by the transitions t start req 1 and t start req 2 . The parametric initial marking
of place p loc rdy (k) expresses the number of tasks active on the processor
(multitasking level). A token in place p not ext req indicates that either the
processor is executing a local task or it is idle. Since the described policy is
preemptive, in both cases an external request may be immediately served.
Multiple incoming requests are not allowed to preempt each other.
The following two P-invariants can be computed with structural techniques:

M(p not ext req ) + M(p req exe 1 ) + M(p req exe 2 ) = 1