Equivalence of the two semantics of the Close-operator

To prove $\mbox{\tt {SemL}$($}S\mbox{$)$} = \mbox{\tt {SemG}$($}S\mbox{$)$}$, for any non-nested Splice program $S$, first observe that it is rather straightforward to prove that if $\mbox{\it lsp}\in \mbox{\tt {SemG}$($}S\mbox{$)$} (s)$ then $\mbox{\it lsp}\in \mbox{\tt {SemL}$($}S\mbox{$)$} (s)$. The proof proceeds by induction on the structure of $S$, which is possible in PVS because we have defined programs as an abstract data type. Most cases are trivial, only for the ${\tt Close}$ statement one has to observe that given a strict total order on the events, this order can be used as the required order on the read events and also as the local order for each process identity.

The proof that $\mbox{\it lsp}\in \mbox{\tt {SemL}$($}S\mbox{$)$} (s)$ implies $\mbox{\it lsp}\in \mbox{\tt {SemG}$($}S\mbox{$)$} (s)$ also proceeds by induction on $S$. The main issue here is again the proof for the ${\tt Close}$ statement; given a strict total order on all read events ($\prec _1$) and for each process identifier a total order on all events ($\prec _2$--see the definition of $\mbox{\tt {SemL}$($}{\tt Close}(S)\mbox{$)$}(s)$), we have to construct a global strict total order on all events.

To do this, we introduced in PVS an axiom stating that there exists some total order $\prec _{\mbox{events}}$ on the set of all events $\mbox{\tt Events}$. This order is used to construct a so-called minimal extension $\prec _{me}$ of the order $\prec _1$ on the read events:

$$\begin{eqnarray*} & & \mbox{}\hspace{-0.5cm} E_1 \prec _{me}E_2~\iff~\rule{10cm... ...all E_3 \big[ E_3 \prec _1 E_1 \iff E_3 \prec _1 E_2 \big]\big). \end{eqnarray*}$$

The idea is that write events are ordered as early as possible in the sense that any read event that does not preceed a write event $E$ in $\mbox{\it ord}$ is ordered after $E$ by $\prec _{me}$. Hence this minimal extension orders all write events not later than any of the local orders. We have proved that this minimal extension satisfies the condition on the read events in the definition of the global semantics $\mbox{\tt {SemG}$($}{\tt Close}(S)\mbox{$)$}(s)$ (which is equal to the one in the definition of $\mbox{$[\![\:$}{\tt Close}(S)\mbox{$\:]\!]$}(s)$), because this condition is invariant under the operation of ordering write events earlier.