Events and Traces

We say that E is an EventStruct if it provides a type |E| of events, a message structure, MS $_{\mbox{\small {E}}}$, and three functions, msg $_{\mbox{\small {E}}}$, loc $_{\mbox{\small {E}}}$, and is-send $_{\mbox{\small {E}}}$. When is-send $_{\mbox{\small {E}}}$ e is true we say that event e |E| is a send event; otherwise we call it a deliver event and write is-deliver $_{\mbox{\small {E}}}$(e). The location of event e is loc $_{\mbox{\small {E}}}$ e, and its message content is msg $_{\mbox{\small {E}}}$ e which is a member of |MS $_{\mbox{\small {E}}}$|. Using these functions we define the binary relation, e$_{1}$ =msg= $_{\mbox{\small {E}}}$ e$_{2}$, that holds when events e$_{1}$ and e$_{2}$ have the same message content. For example, e$_{1}$ and e$_{2}$ might be delivery events of a message m at two different locations. We can show that this relation is an equivalence relation on events.

The formal definition of the type of event structures is

Given an event structure, E, a trace is just a list of events

A trace tr defines an ordering of the events in it. We also call the list indices of tr, the members of ||tr||, times and we say that event tr[k] occured at time k. The message in event x was delivered at time k if

If the message in event x was delivered at some location earlier than any delivery of the message in event y at that same location, then

Here is a simple lemma about this relation that we will need later.



proof: If a somewhere delivered before b then there is a time k and a location, p = (loc $_{\mbox{\small {E}}}$ tr[k]) such that the message in event a was delivered to location p at time k but no delivery of the message in event b to location p has occured before time k. If a delivery of the message in event c to location p has occured before time k, then c somewhere delivered before b. If not, then a somewhere delivered before c. This case split is decidable, so the conclusion follows