Fusion of Trace Properties

If the protocol associated with each label is guaranteeing some trace property P, and tr is a trace, then we will have m:Label. (P tr$\mid$). A switch protocol must guarantee some additional property I that is strong enough to guarantee that property P holds of the whole trace tr. If this is the case for I and P then we say that I is a fusion condition for P, and we define

We will be looking for properties I that are fusion conditions for whole classes of trace properties P. We will show that certain properties are fusion conditions for all properties P that satisfy certain meta-properties. We start this investigation with some simple lemmas about fusion.











The proofs of these lemmas are straightforward. We will also need a few lemmas about fusion conditions for the properties Causal $_{\mbox{\small {E}}}$ and No-dup-deliver $_{\mbox{\small {E}}}$.



proof: This lemma says that if m:Label. (Causal $_{\mbox{\small {E}}}$ tr$\mid$) then Causal $_{\mbox{\small {E}}}$ tr. To show this, let tr[j] be a member of tr. We must show that there is an i j such that tr[i] is the send event for tr[j]. Event tr[j] has some tag m and using the causal property on tr$\mid$, we find a send event x for tr[j] in tr$\mid$. Since tr$\mid$ is a sublist of tr, event x also precedes j in the trace tr.



proof: If trace tr has a duplicate delivery of the message in event x, then trace tr$\mid$, where m = (tag $_{\mbox{\small {E}}}$ x), also has a duplicate delivery because, if tr has the Tag-by-msg $_{\mbox{\small {E}}}$ property, all the relevant events have the same tag, m.



proof: If x is an event in tr, it has tag m = (tag $_{\mbox{\small {E}}}$ x) and since tr$\mid$ is causal, there is a send event for x with tag m. So any event x has a send event with the same tag. If tr has the No-dup-send $_{\mbox{\small {E}}}$ property, then any two events with the same message must have the same send event and therefore the same tag.



proof: This follows easily from lemma 5.0.6.



proof: By lemma 5.0.7, it is enough to show that (I No-dup-send $_{\mbox{\small {E}}}$ Tag-by-msg $_{\mbox{\small {E}}}$) fuses P. Then using the fusion simplification lemma 5.0.3 with J = (Causal $_{\mbox{\small {E}}}$ No-dup-deliver $_{\mbox{\small {E}}}$), it is enough to show that

This follows from lemma 5.0.1, lemma 5.0.2, lemma 5.0.4, and lemma 5.0.5.