Information Technology Reference
In-Depth Information
We may only transfer packets simultaneously if they have different destina-
tions and at most one packet is interesting. This is expressed in the second
summand below.
In case both input buffers contain an interesting packet and these packets
have different destinations, priority is granted to any input buffer with lower
identity. See the fifth summand below.
We are required to grant priority to both interesting and non-interesting pack-
ets if the local packet is non-interesting. For that reason, the last summand is
adapted as well.
proc
Input
(
i
:
,c
:
List
(
Packet
)) =
#
c<cap
N
→
enter
(
i, p
)
·
Input
(
i, p
c
)
p
:
Packet
+
c
≈
[]
→
dest
(
p
)
≈
dest
(
rhead
(
c
))
∧
(
¬
int
(
p
)
∨¬
int
(
rhead
(
c
)))
→
p
:
Packet
n
:
N
n
≈
i
→
send
(
i,
dest
(
rhead
(
c
))
,
rhead
(
c
))
|
free
(
n,
dest
(
p
)
,p
)
·
Input
(
i,
rtail
(
c
))
+
c
≈
[]
→
send
(
i,
dest
(
rhead
(
c
))
,
rhead
(
c
))
·
Input
(
i,
rtail
(
c
))
→
n,m
:
N
+
c
≈
[]
grant
(
n, m, p
)
·
Input
(
i, c
)
p
:
Packet
dest
(
p
)
≈
dest
(
rhead
(
c
))
∨
int
(
p
)
→
+
c
≈
[]
∧
int
(
rhead
(
c
))
→
p
:
Packet
n
:
N
n<i
→
grant
(
n,
dest
(
p
)
,p
)
·
Input
(
i, c
)
+
c
≈
∧¬
int
(
rhead
(
c
))
→
[]
b
1
(
p
)
≈
b
1
(
rhead
(
c
))
→
p
:
Packet
n
:
N
n<i
→
grant
(
n,
dest
(
rhead
(
c
))
,p
)
·
Input
(
i, c
);
5 Specification of the Modified 2
×
2Switch
×
The modified 2
2 switch alters the way the priority is handled amongst collid-
ing transfers in the case that the packets are both interesting and have a different
destination. We have defined two conditions, namely both head packets have the
same destination (C1) and both head packets are interesting (C2). If either one
of these conditions holds, priority is given to the transferral of the packet from
input buffer 0.
Now, in the Modified Switch, we keep that if C1 holds, the first input buffer
will be given priority over the second buffer. However if C1 does not hold, while
C2 holds, priority is given to transferral of the packet from input buffer 1.
This only requires the adaptation of the model of the input buffers. In the
relevant case this time priority is granted to the input buffer with the higher
identity. The last but one summand of the specification of the input buffer of
the Original Switch is split in these two cases.
