1 Packet Delivery Systems

Let M be a set of message types. For any m ∈ M the event m^{O} represents output of a message of type m, and m^{I} represents input of such a message. M^{O} denotes {m^{O} | m ∈ M} and M^{I} denotes {m^{I} | m ∈ M}. The process

T(b) =  (_{m∈M} m^{O} → T(b ⊕ {m ↦ b(m) + 1}))

( ⊓_{m∈M∧b(m)≠0} m^{I} → T(b ⊕ {m ↦ b(m) − 1}))

represents a packet delivery system. b is a bag of items from M, and ⊕ is the overriding operator (in Z style). The alphabet of T is M^{O} ∪ M^{I}.

Define the set-valued functions

pending-ins (b, tr) = {m^{I} | m ∈ M ∧ (b(m) + tr ↓ {m^{O}}) > tr ↓ {m^{I}}}
pending-outs (b, tr) = {m^{I} | m ∈ M ∧ (b(m) + tr ↓ {m^{O}}) < tr ↓ {m^{I}}}

on traces.

Theorem:

T(b) sat S(b)(tr, ref)

where

S(b)(tr, ref) = (M^{O} ∩ ref) = ∅ ∧

((pending-ins (b, tr) ≠ ∅) ⇒ (pending-ins (b, tr) ⊄ ref)) ∧ pending-outs (b, tr) = ∅

Proof:

Write

S^{n}(b)(tr, ref) = (#tr < n) ⇒ S(b)(tr, ref).

Noting S^{0}(b)(tr, ref) = true, the proof depends on showing that for any set of processes X(b)

(∀b · X(b) sat S^{n}(b)) ⇒ (∀b · F(X)(b) sat S^{n+1}(b))  (1)

where F is the function whose fixed-point defines T according to the recursive equations above. So

F(X)(b) = F^{O}(X)(b)  F^{I}(X)(b)

where

F^{O}(X)(b) = _{m∈M} F_{m}^{O}(X)(b)

F^{I}(X)(b) = ⊓_{m∈M∧b(m)≠0} F_{m}^{I}(X)(b)

and

F_{m}^{O}(X)(b) = m^{O} → X(b ⊕ {m ↦ b(m) + 1})
F_{m}^{I}(X)(b) = m^{I} → X(b ⊕ {m ↦ b(m) − 1})

Providing equation ?? obtains, the theorem follows from the proof rule for recursion (CSP, pp125), because

S(b)(tr, ref) = ∀n · S^{n}(b)(tr, ref)

Establishing equation ?? requires the following algebraic properties of the pending functions

pending-ins (b, ⟨m^{O}⟩ˆ tr) = pending-ins (b ⊕ {m ↦ b(m) + 1}, tr)  (2)
pending-outs (b, ⟨m^{O}⟩ˆ tr) = pending-outs (b ⊕ {m ↦ b(m) + 1}, tr)  (3)

and, if b(m) ≠ 0,

pending-ins (b, ⟨m^{I}⟩ˆ tr) = pending-ins (b ⊕ {m ↦ b(m) − 1}, tr)  (4)
pending-outs (b, ⟨m^{I}⟩ˆ tr) = pending-outs (b ⊕ {m ↦ b(m) − 1}, tr)  (5)

and

pending-ins (b, ⟨⟩) = {m^{I} | m ∈ M ∧ b(m) > 0}  (6)
pending-outs (b, ⟨⟩) = ∅.  (7)

Assuming the antecedent of ??, namely X(b) sat S^{n}(b),

X(b ⊕ {m ↦ b(m) + 1}) sat S^{n+1}(b)(⟨m^{O}⟩ˆ tr, ref)

follows directly from the definition of S^{n} and properties ?? and ?? above. Hence, from the proof rule for prefixing (CSP pp124)

F_{m}^{O}(X)(b) sat if tr = ⟨⟩ then m^{O} ∉ ref else S^{n+1}(b)(tr, ref).  (8)

Likewise, from properties ?? and ??, if b(m) ≠ 0

F_{m}^{I}(X)(b) sat if tr = ⟨⟩ then m^{I} ∉ ref else S^{n+1}(b)(tr, ref).  (9)

Equation ?? and the proof rule for choice imply

F^{O}(X)(b) sat if tr = ⟨⟩ then (∀m : M · m^{O} ∉ ref) else S^{n+1}(b)(tr, ref),

or simply

F^{O}(X)(b) sat if tr = ⟨⟩ then (M^{O} ∩ ref) = ∅ else S^{n+1}(b)(tr, ref). (10)

On the other hand, equation ?? and the proof rule for non-deterministic choice imply

F^{I}(X)(b) sat if tr = ⟨⟩ then
(∃m : M · b(M) > 0) ⇒ (∃m : M · b(M) > 0 ∧ m^{I} ∉ ref) else
S^{n+1}(b)(tr, ref).

Using property ?? of pending-ins this can be written as

F^{I}(X)(b) sat if tr = ⟨⟩ then

(pending-ins (b, ⟨⟩) ≠ ∅) ⇒ (pending-ins (b, ⟨⟩) ⊄ ref) else

S^{n+1}(b)(tr, ref).  (11)

A final application of the proof rule for choice, combining ?? and ?? and taking into account identity ??, establishes equation ??. This proves the theorem. □

2 Eager Readers

Simplify the definitions of the previous section to eliminate the references to b (which is internal to the implementation of the packet router):

pending-ins (tr) = {m^{I} | m ∈ M ∧ tr ↓ {m^{O}} > tr ↓ {m^{I}}}
pending-outs (tr) = {m^{O} | m ∈ M ∧ tr ↓ {m^{O}} < tr ↓ {m^{I}}}

and put T = T([[]]). So

T sat (M^{O} ∩ ref) = ∅ ∧

((pending-ins (tr) ≠ ∅) ⇒ (pending-ins (tr) ⊄ ref)) ∧ pending-outs (tr) = ∅

A process C for which αC ⊃ αT is an eager reader if

C sat ((M^{I} ∪ ref) = αC ∧ pending-outs (tr) = ∅) ⇒

(pending-ins (tr) ≠ ∅ ∧ (pending-ins (tr) ∩ ref) = ∅) .

If an eager reader can’t offer any events other than inputs there must be at least one event in pending-ins (tr), and the process must be prepared to accept any event in that set. This requirement is weakened slightly above—it need only apply if no messages have been input before being output—a restriction on traces which is imposed externally by a packet router.

Theorem:

If C is an eager reader

T ∥ C sat ref ≠ α(T ∥ C).

In other words, the combined process is deadlock-free.

Proof:

From the proof rule for parallel composition

T ∥ C sat ∃X : PαT · ∃Y : PαC · ref = X ∪ Y ∧
(M^{O} ∩ X) = ∅ ∧ ((P^{I} ≠ ∅) ⇒ (P^{I} ⊄ X)) ∧ P^{O} = ∅ ∧
(((M^{I} ∪ Y) = αC ∧ P^{O} = ∅) ⇒ (P^{I} ≠ ∅ ∧ (P^{I} ∩ Y) = ∅))

where

P^{I} = pending-ins (tr)
P^{O} = pending-outs (tr)

Suppose T ∥ C isn’t deadlock free. Then for some pair (tr, ref) we can find X and Y such that ref = X ∪ Y = αC (because α(T ∥ C) = αC). Since X ⊂ (M^{O} ∪ M^{I}) and (M^{O} ∩ X) = ∅ we have X ⊂ M^{I}, so M^{I} ∪ Y = αC. This means that the antecedent of the final clause in the specification is satisfied, so P^{I} ≠ ∅ ∧ (P^{I} ∩ Y) = ∅. The first clause here implies, with an earlier clause, that P^{I} ⊄ X, ie, there is an element of P^{I} which is not in X; but also, from the second clause, this element can’t be in Y. This contradicts the assumption that all events are in X ∪ Y. □