Information Technology Reference
In-Depth Information
The first line in the above model specifies the name of the process and declares
the associated process parameters. In this case the buffer has two parameters.
The first process parameter represents the identity of an output buffer. The
second process parameter captures the contents of the queue as a list of packets.
As already described, an arbitrary packet can be received as long as the buffer
is not yet full (#
c
denotes the number of elements in the list
c
). So the first
summand, specifies that when a packet is received, it is appended to the buffer.
Appending a packet
p
to a buffer contents
c
is denoted by
p
c
. The second
summand describes that the packet (if any) that has been inserted into the queue
(so the buffer is not empty,
c
[]) first (
rhead
(
c
) denotes this element), it exits
the switch by means of the
leave
action and is removed from the queue (
rtail
(
c
)).
Note that modeling the buffer in this way, the specification of the output buffer
does not rely in any way on the fact that only packets with a specific first bit
will be send to it, e.g. it accepts packets regardless of their content.
For both the output buffer as described in this subsection and the input buffer
described in the following subsection we have chosen to allow it to perform at
most one action at the same time.
≈
3.5
The Input Buffers with Capacity
cap
The main challenges of this modeling exercise are to deal appropriately with the
priority of input buffer 0 over input buffer 1 in case both buffers want to transfer
a packet to the same destination; and to deal with the required simultaneous
packet transfer in case both buffers want to transfer packets to different destina-
tions. In this section we gradually shape the model, by defining the interaction
between the different processes, as well as specifying the input buffer such that
it eventually complies to the settled design intent.
We start by modeling the behavior of the input buffer analogously to the
output buffer:
proc
Input
(
i
:
,c
:
List
(
Packet
)) =
#
c<
cap
N
→
enter
(
i, p
)
·
Input
(
i, p
c
)
p
:
Packet
+
c ≈
[]
→
send
(
i,
dest
(
rhead
(
c
))
,
rhead
(
c
))
·
Input
(
i,
rtail
(
c
));
Next, we setup the basic communication between input buffers and output
buffers. We first specify that the four buffers require to run in parallel. Fur-
thermore, we specify that a successful synchronization of
send
and
recv
actions,
results in a
comm
action. This is expressed by means of the subscript parameter
send
comm
in the communication operator
Γ
. We only allow successful
communications, therefore we encapsulate all
send
and
recv
actions that do not
result in a successful synchronization. This way, insertion or removal of a packet
can be done simultaneously, while other buffers transfer packets. Combining the
instantiated process definitions with the communication and encapsulated oper-
ators, leads to the following initialization:
|
recv
→
