Let the context of our discussion in this chapter be fixed with a vocabulary $\vocab = (\myprocedure, \var, \globvar, \locvar)$, a domain $\dom$ and a \minimp{} model $\model$. Given a procedure $f \in \myprocedure$, we use \textsf{body}($f$) to denote the body statement of $f$. The partial correctness of a MiniMP program can be specified as a collective triple $\cotriplearg{\textsf{body}(\texttt{main})}$. To prove the validity of this triple in a composite and modular way, we introduce an inference system, denoted $\corule$, in this chapter. By applying $\corule$ to $\cotriplearg{\textsf{body}(\texttt{main})}$, the validity of the triple can be proved by proving a set of collective triples, each of which specifies a smaller statement than $\textsf{body}(\texttt{main})$. The inference system $\corule$ is defined with a set of rules in \S\ref{sec:minimp:spec:rule}. \S\ref{sec:minimp:spec:rule:adaptation} discusses about the \emph{adaptation problem} arising in practice of the rules. We show a derivation example of $\corule$ in \S\ref{sec:rules:example}. Finally, we define notations in \S\ref{sec:extended:enter:exit}, which are used in the soundness proof of $\corule$ in \S\ref{sec:rules:soundness}. \section{Rules for Decomposing Collective Triples} \label{sec:minimp:spec:rule} In this section, we introduce an inference system for composite and modular verification of \minimp{} programs. We use $\corule$ to denote this inference system. $\corule$ consists of four rules for reasoning about collective triples. With $\corule$, one is able to decompose a collective triple $\cotriplenoloc{}$ into a set of collective triples $\Tri$ such that $\model \models \cotriplenoloc{}$, if $\forall{\tri \in \Tri}.\, \model \models \tri$. Normally, proving the validity of a $\tri \in \Tri$ is a much smaller problem than proving the validity of the original triple. The rules in $\corule$ involve assertions that will be explained below. These assertions, as well as the rules, constraint path-requirements or guarantees. As aforementioned, path-requirements and guarantees can be represented by conjuncting over set comprehensions of absence assertions. Therefore, we define a few operations that are similar to set operations for expressing those assertions. These operations shall be interpreted under a certain context---a path, where there is exact one state for evaluating an absence assertion involved in an operation. \begin{defn} A \emph{partial evaluation} $\mypevaltitle\colon{} \sabsentv{_\vocab} \times \mystates{} \times \nprocs{n} \rightarrow \sabsentv{_\vocab}$ is a function that maps an absence assertion to another absence assertion at a state for a process. Given an absence assertion $\lambda$, a state $s$ and a process $p$, $\mypeval{\lambda}{s}{p}$ is defined by \begin{align} \mypeval{\lambda}{s}{p} =~ & \text{let } p = \myeval{e_0}(s, p) \text{ in} \nonumber \\ & \text{let } q = \myeval{e_1}(s, p) \text{ in} \nonumber \\ & \text{let } r = \myeval{e_2}(s, p) \text{ in} \nonumber \\ & \texttt{\acslabsent{\acslsend($p$, $q$)}{\acslexit($p$)} {\acslexit($r$)}}, \nonumber \\ & \text{if } \lambda = \texttt{\acslabsent{\acslsend($e_0$, $e_1$)}{\acslexit($e_0$)}{\acslexit($e_2$)}} \nonumber \\ & \ldots{} \nonumber \end{align} For brevity, we do not show the full definition. The omitted definition should be obvious to readers. $\qed$ \end{defn} \begin{defn} Let $\lambda$ be an absence assertion. Let $\lambda^0_a, \lambda^1_a, \ldots{}$ and $\lambda^0_b, \lambda^1_b, \ldots{}$ be absence assertions. Let $e_a, e_b \in \sexprv_{\vocab}$. Let $m_a, m_b$ be two positive integers. $\Lambda_a, \Lambda_b$ are two expressions of the forms: \begin{align} \Lambda_a =~~ e_a \texttt{ ==> } \lambda^0_a \texttt{ \&\& } \ldots{} \texttt{ \&\& } \lambda^{m_a-1}_a, \nonumber \\ \Lambda_b =~~ e_b \texttt{ ==> } \lambda^0_b \texttt{ \&\& } \ldots{} \texttt{ \&\& } \lambda^{m_b-1}_b. \nonumber \end{align} Let $\rho$ be a path. Let $s, s_a, s_b$ $\in \mypathstates(\rho)$ be the only states, where $\lambda$, $\Lambda_a$ and $\Lambda_b$ shall be evaluated, respectively. We define \begin{align} \lambda \in_{\rho} \Lambda_a & \text{ iff } \exists{p \in \nprocs{n}}.\,\myseval{e_a}(s_a, p) = \textbf{T} \wedge{} \exists{m \in \nprocs{m_a}}.\, \lambda = \mypeval{\lambda^m_a}{s_a}{p} \nonumber \\ %%% \Lambda_a \subseteq{_{\rho}} \Lambda_b &\text{ iff } \forall{i \in \nprocs{m_a}}.\forall{p \in \nprocs{n}}.\, \myseval{e_a}(s_a, p) = \textbf{T} \Rightarrow{} \mypeval{\lambda^i_a}{s_a}{p}\in_\rho \Lambda_b \qed\nonumber \end{align} \end{defn} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%% DEFINE HELPER ASSERTIONS %%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Now we describe the assertions. Let Def.\ \ref{defn:guarantee:assertion}, Def.\ \ref{defn:nosend:subset}, Def.\ \ref{defn:infer:togather} and Def.\ \ref{defn:nocancel} be under the context described by the following. Let $C_0$ and $C_1$ be two \minimp{} substatements. Suppose there are three triples: $\cotriplearg{C_0C_1}$, $\mycosubtriple{0}{\psi_0}{\phi_0}{C_0}$ and $\mycosubtriple{1}{\psi_1}{\phi_1}{C_1}$. Let $\rho = \pi_0 \circ{} \rho_1$ be a path such that $\pi_0$ is an execution of $C_0$ and $\rho_1$ is a prefix of an execution of $C_1$. Obviously, according to the semantics of collective triples defined in Def.\ \ref{defn:semantics:collective:triple}, $\Gamma, \Upsilon, \Gamma_0, \Upsilon_0$ shall be partially evaluated at $\mysrc(\myhead(\rho))$, and $\Gamma_1, \Upsilon_1$ shall be partially evaluated at $\mysrc(\myhead(\rho_1))$. \begin{defn} The assertion \[\Upsilon_1~\ruleguarantee{_{\rho}}~\Gamma_0\] is true iff for every \[ \texttt{\acslgamma{$p$}{$q$}{$r$}} \in_{\rho} \Gamma_0, \] there is \[ \texttt{\acslguarantee{$p$}{$q$}{$r$}} \in_{\rho} \Upsilon_1. \qed \] \label{defn:guarantee:assertion} \end{defn} \begin{defn} Let $i, j$ be two positive integers. Let $e\in\sexprv_{\vocab}$. Let $\lambda_0, \lambda_1,\ldots{}$ and $\lambda'_0, \lambda'_1, \ldots$ be absence assertions. If $\Upsilon$ has such a form $e \texttt{ ==> } \lambda_0 \texttt{ \&\& } \ldots{} \texttt{ \&\& } \lambda_{i-1}$, $\nosendsubset$$(\Upsilon)$ denotes an expression of such a form:$ e \texttt{ ==> } \lambda'_0 \texttt{ \&\& } \ldots{} \texttt{ \&\& } \lambda'_{j-1}$ that \begin{enumerate} \item $\forall{x, y \in \nprocs{j}}.\, x \not= y \Rightarrow{} \lambda'_x \not= \lambda'_y$ \item $\forall{y \in \nprocs{j}}.\exists{x \in \nprocs{i}}. \lambda'_y = \lambda_x$, \item every $\lambda'_k$ for $k \geq 0$ is of the form: \[ \texttt{\acslguarantee{$p$}{$q$}{$r$}}.\] \item there is no such integer $h$ that $h > j$ and $ e \texttt{ ==> } \lambda'_0 \texttt{ \&\& } \ldots{} \texttt{ \&\& } \lambda'_{h-1}$ satisfies the three conditions above. $\qed$ \end{enumerate} \label{defn:nosend:subset} \end{defn} In other words, if taking $\Upsilon$ as a set comprehension of absence assertions, $\nosendsubset(\Upsilon)$ is the maximal subset of $\Upsilon$ containing elements of the specific kind of absence assertions. \begin{defn} The assertion \[\myruleinfer{\Upsilon_0}{\Upsilon_1}{\nosendsubset(\Upsilon)}{\rho}\] is true iff for every \[ \upsilon~=~\texttt{\acslguarantee{$p$}{$q$}{$r$}} \in_{\rho} \nosendsubset(\Upsilon), \] we have $\upsilon \in_{\rho} \Upsilon_0$, and \begin{itemize} \item \texttt{\acslwaitsfor{$p$}{$r$}} $\in_{\rho} \Upsilon_0$, or \item $\upsilon[x / r] \in_{\rho} \Upsilon_1$, if there is such $x\in\nprocs{n}$ that\\ \texttt{\acslwaitsfor{$x$}{$r$}} $\in_\rho \Upsilon_0$, or \item $\upsilon \in_{\rho} \Upsilon_1~\vee{}~\upsilon[q / r] \in_\rho \Upsilon_1$. $\qed$ \end{itemize} \label{defn:infer:togather} \end{defn} We explain Def.\ \ref{defn:infer:togather}. An element $\upsilon \in_\rho \nosendsubset(\Upsilon)$ asserts that process $p$ shall not send a message to process $q$ during in $C_0C_1$ before process $r$ entering $C_0C_1$. We have $\Upsilon_0$ and $\Upsilon_1$ of $C_0$ and $C_1$, respectively, infer $\upsilon$, if \begin{itemize} \item[1] $\Upsilon_0$ also contains $\upsilon$. If so, $p$ cannot send a message to $q$ during in $C_0$ before $r$ entering $C_0$. \item[2] Moreover, $p$ shall also not send a message to $q$ during in $C_1$ before $r$ entering $C_0$. Hence, one of the following conditions must hold. \begin{itemize} \item[2.1] $C_0$ guarantees that the sender $p$ will not enter the following $C_1$ until $r$ enters itself; \item[2.2] If $C_0$ guarantees that some process $x$ will not enter the following $C_1$ until $r$ enters itself, $C_1$ shall guarantee that $p$ will not send a message to $q$ until $x$ enters itself. \item[2.3] $C_1$ guarantees that process $p$ will not send a message to $q$ until process $q$ or $r$ enters itself. \end{itemize} \end{itemize} \begin{defn} Let \[ \gamma = \texttt{\acslgamma{$p$}{$q$}{$r$}} \in_{\rho} \Gamma_0, \] we say $\Upsilon_1~\rulecancels{_{\rho}}~\gamma$ iff \[ \texttt{\acslwaitsfor{$p$}{$r'$}} \in_{\rho} \Upsilon_1, \] where $r' = r \vee r' = q$. $\qed$ \label{defn:nocancel} \end{defn} The intuitive meaning for Def.\ \ref{defn:nocancel} is that for a $\gamma \in_\rho \Gamma_0$, if $\Upsilon_1~\rulecancels{_\rho}~\gamma$, $C_0C_1$ no longer requires $\gamma$. Rules in Hoare logic is defined with respect to kinds of program statements, such as branch or loop. Here we define a premise of a rule in $\corule$ that depends on the semantics instead of the structure of \minimp{} programs. We call this premise the ``elaboration condition'', because the complexity of proving this premise for a substatement $C$ will be no less than elaborating all executions in state space graphs of $C$. \begin{defn} Let $\rho_0$ and $\rho_1$ be two paths. Let $\xi_0$ and $\xi_1$ be two transition sequences that are the projections of $\rho_0$ and $\rho_1$, respectively, onto transitions associated with non-\myskipstmt{} actions. We say $\rho_0$ and $\rho_1$ are \emph{equivalent} if $\xi_0 = \xi_1$. $\qed$ \label{defn:path:equivalence} \end{defn} \begin{defn} Let $C$ and $C'$ be two substatements. We say $C'$ \emph{contains behaviors of} $C$ \emph{under} $\psi$, denoted $\cocond{\psi, \emptyset}~\overrightarrow{C} \subseteq{} \overrightarrow{C'}$, if for every extended execution $\zeta$ of $C$ such that $\psi$ holds on $\mysrc(\myhead(\zeta))$ for all processes, there is an \emph{equivalent} extended execution $\zeta'$ of $C'$. $\qed$ \end{defn} Now we define the rules in $\corule$. \begin{defn} The \emph{inference system} $\corule$ for collective triples is defined in Fig.\ \ref{fig:triple:rules}. $\qed$ \end{defn} \begin{figure}[t] \centering \fbox{ \parbox{0.9\textwidth}{ \begin{align} & \frac{ \mycosubtriple{0}{\psi}{\mu}{C_0},\,\, \mycosubtriple{1}{\mu}{\phi}{{C_1}} } { \cotriplearg{C_0C_1} } ~~~\textit{(sequence)}\nonumber \\ \text{if } & \text{for every execution } \pi_0 \circ{} \pi_1 \text{ of } C_0C_1 \text{ s.t.\ } \nonumber \\ \pi_0 &\text{ is an execution of } C_0 \text{ and } \pi_1 \text{ is an execution of } C_1, \nonumber \\ \text{1. }& \Upsilon_1~\ruleguarantee_{\pi_0 \circ{} \pi_1}~\Gamma_0, \nonumber \\ % \text{and 2. }& \nosendsubset(\Upsilon) \subseteq \Upsilon_0,\nonumber\\ \text{2. }& \myruleinfer{\Upsilon_0}{\Upsilon_1}{\nosendsubset(\Upsilon)}{\pi_0 \circ{} \pi_1}, \nonumber \\ \text{3. }& \Upsilon \subseteq_{\pi_0 \circ{} \pi_1} \Upsilon_0 \cup{} \Upsilon_1, \text{ and}\nonumber \\ \text{4. }& \{\gamma \in \Gamma_0 \mid \neg{}(\Upsilon_1~\rulecancels_{\pi_0 \circ{} \pi_1}~\gamma)\} \cup \Gamma_1~\subseteq_{\pi_0 \circ{} \pi_1}~\Gamma. \nonumber \end{align} \begin{align} &\frac{ \cocond{\psi', \Gamma'}~C~\cocond{\phi', \Upsilon'} } { \cocond{\psi, \Gamma}~C~\cocond{\phi, \Upsilon} } ~~~ \textit{(consequence)} \nonumber \\ \text{if for every } & \text{execution } \pi \text{ of } C,~ %\nonumber \\ \Gamma' \subseteq_{\pi} \Gamma~\wedge{}~\Upsilon \subseteq_\pi \Upsilon' ~\wedge{}~\psi{} \Rightarrow \psi' ~\wedge{}~\phi' \Rightarrow \phi \nonumber \end{align} \begin{align} & \frac{ \cocond{\mymath{inv} \wedge{} c,\, \Gamma}~C~ \cocond{\mymath{inv},\, \Upsilon} }{ \cocond{\mymath{inv},\,\Gamma{}}~ \texttt{while(}c\texttt{)} ~C ~\cocond{\neg{}c \wedge{} \mymath{inv},\, \Upsilon{}} } ~~~ \textit{(collective loop)} \nonumber \\ & \text{if for every execution } \pi \text{ of } C, \Upsilon{}~\ruleguarantee_\pi~\Gamma \nonumber \end{align} \begin{align} \frac{ \cocond{\psi{},\, \emptyset}~ \overrightarrow{C} \subseteq{} \overrightarrow{C_0C_1}~ ,\,\, \cocond{\psi{},\, \Gamma}~ C_0C_1~ \cocond{\phi{},\, \Upsilon} }{ \cocond{\psi{},\, \Gamma}~ C~ \cocond{\phi{},\, \Upsilon} }~~~\textit{(elaboration)} \nonumber \end{align} } } \caption{Rules for decomposing collective triples} \label{fig:triple:rules} \end{figure} The \textit{sequence}, \textit{consequence} and \textit{collective loop} rules in $\corule$ were inspired by the \textit{sequence}, \textit{consequence} and \textit{loop} rules in Hoare logic. Rules in $\corule{}$ over state-requirements and -guarantees are similar to pre- and post-conditions in Hoare logic. Rules over path-requirements and -guarantees are explained by the follows. The \textit{sequence} rule is the basis of the decomposition. For a a sequence of two substatements $C_0C_1$, in order to prove $\model \models \cotriplearg{C_0C_1}$, one proves $\model \models \mycosubtriple{0}{\psi}{\mu}{C_0}$ and $\model \models \mycosubtriple{1}{\mu}{\phi}{C_1}$ separately instead. The decomposition is feasible if all the side conditions are satisfied. Side Condition 1 enforces that $C_0$ will never be interfered by $C_1$. The meaning of Side Condition 2 has been explained with the ``$\ruleinfer{\ldots}{\ldots}{\ldots}$'' assertion above. Side Condition 3 expresses that the path-guarantees of $C_0$ and $C_1$ together shall be no weaker than the one of $C_0C_1$. Stated by Side Condition 4, since $\Upsilon_1$ may $\rulecancels$ some elements in $\Gamma_0$, the path-requirement of $C_0$ and $C_1$ together may be weaker but shall not be stronger than the one of $C_0C_1$. The \textit{consequence} rule is more obvious: if a collective triple is valid, it is still valid after strengthening its state- or path-requirement, and it is still valid after weakening its state- or path-guarantee. The \textit{collective loop} rule requires the user to provide a loop invariant $\mymath{inv}$. This rule can only be applied to the loops whose body $C$ can be specified by a collective triple $\cotriplenoloc{}$. In other words, the loop body must be collective style. This rule can be seen as a sequence of applications of the \textit{sequence} rule to the unrolled loop body $CC\ldots{}$. The \textit{elaboration} rule is designed for the cases where a collective triple cannot be decomposed by the three rules above due to the existence of branches, such as the following statement $C$ (at line 3--6): \begin{center} \begin{program} \ccode{var} dat;\\ ...\ \\ \ccode{if} (PID == 0) \\ \lb{}bcast(dat, 0); gather(dat, 0);\rb{} \\ \ccode{else} \\ \lb{}bcast(dat, 0); gather(dat, 0);\rb{} \end{program} \end{center} where \texttt{bcast} and \texttt{gather} are procedures defined in Fig.\ \ref{fig:minimp:example:bcast} and \ref{fig:minimp:example:gather}, respectively. One can tell that the code above is equivalent to such a sequence of calls \begin{center} \texttt{bcast(dat, PID); gather(dat, PID);}. \end{center} However, the sequence rule is not suitable for the original branch. With the elaboration rule, if one can prove the ``elaboration condition'', \begin{center} $\cocond{\psi, \emptyset{}}~\overrightarrow{C} \subseteq \overrightarrow{\texttt{bcast(dat, PID);gather(dat, PID);}}$ \end{center} for some condition $\psi$, is valid, one can infer a collective triple of the original branch from a triple of the sequence of calls. The latter triple can be further decomposed by an application of the sequence rule. Proving the elaboration condition requires some other techniques, such as model checking. It is out of the scope of this chapter. Concluding this section, $\corule$ is incomplete. It means that it is not always the case that a collective triple can be derived by $\corule$. As we argued in Chapter \ref{chp:intro}, the effectiveness of $\corule$ relies on the collective programming style, which dominates the message-passing HPC programming. %%%%%%%%%%%%%%%%%% ADAPTATION %%%%%%%%%%%%%%%%%% \section{The Adaptation Problem} \label{sec:minimp:spec:rule:adaptation} There is an \emph{adaptation problem} that arises from re-using verified collective triples. Example \ref{exam:minimp:rule:adaptation} shows such a problem. \begin{exmp} Let $C$ be the left and $C'$ be the right statements below: \begin{minipage}[t]{.45\textwidth} \begin{program} \ccode{if} (PID == 0) \lb{} \\ \ \ send(x, y); \\ \rb{} \ccode{else if} (PID == 1) \lb{} \\ \ \ recv(x, 0); \\ \rb{} \\ \end{program} \\ \end{minipage} \begin{minipage}[t]{.45\textwidth} \begin{program} \ccode{if} (PID == 0) \lb{} \\ \ \ send(x, z); \\ \rb{} \ccode{else if} (PID == 1) \lb{} \\ \ \ recv(x, 0); \\ \rb{} \\ \end{program} \\ \end{minipage}\\ The only difference between $C$ and $C'$ is that variable \texttt{y} in $C$ is replaced by \texttt{z} in $C'$. Now suppose that we have verified a collective triple of $C$, $\cocond{\texttt{y} = 1, \Gamma}~C~\cocond{\phi, \Upsilon}$, and is going to verify a collective triple of $C'$, $\cocond{\texttt{z} = 1, \Gamma}~C'~\cocond{\phi, \Upsilon}$. Intuitively, the validity of the triple of $C'$ can be concluded from the former one. However, no rule in $\corule$ can be applied here to re-use the verified triple of $C$ without a variable name substitution from \texttt{y} to \texttt{z} happens first. $\qed$ \label{exam:minimp:rule:adaptation} \end{exmp} To generalize the solution to the problem of Example \ref{exam:minimp:rule:adaptation}, one shall allow free substitution from existing variable names to fresh new variable names over collective triples. Such substitutions are common transformations in first order logic that cannot affect the validity of collective triples. In this dissertation, we will not discuss about details in solving adaptation problem for two reasons. First, the adaptation problem has been well studied and tackled by earlier works \cite{hoare:1969:axiomatic, Kleymann:1999:HLA:2769784.2769811}. There is nothing new in this problem for our unique inference system for \minimp{}. More importantly, in later chapters, we will focus on applying collective triples to procedures only. This is one of the typical ways to implement a contract based verification system. For \minimp{} procedures, the adaptation problem is naturally solved. Recall the semantics of \minimp{} in \S\ref{sec:minimp:semantics}, a mapping from actual parameters to formal parameters happens automatically. In addition, global variables are visible everywhere in a program. No substitution is ever needed for global variables. %%%%%%%%%%%%%%%%%% EXAMPLES %%%%%%%%%%%%%%%%%% \section{An Derivation Example} \label{sec:rules:example} We now show an example of the application of $\corule$. Figure \ref{fig:minimp:corule:example:1} shows a contract for the sequential combination $C=C_0C_1$ of two substatements. $C_0$ and its contract are given by Fig.\ \ref{fig:minimp:spec:bcast}. $C_1$ and its contract are given by Fig.\ \ref{fig:minimp:spec:gather}. Recall that we have explained in \S\ref{sec:minimp:spec:triple} that the contract of $C_1$ misses a path-requirement. Figure \ref{fig:minimp:corule:apply:1} shows a $\corule$ derivation of the collective triple representing $C$ and its contract. In the derivation, we write $\textsf{id}$ for the value of \texttt{PID}, $n$ for the value of \texttt{NPROCS}, $v$ for the value of \texttt{val}, and $r$ for the value of \texttt{root}. We write $x_p$ for a variable or value $x$ on process $p$. Let $X_p, Y_p, Z_p \in \dom$ be values of \texttt{dat} on a process $p \in \nprocs{n}$ at different states. In this derivation, irrelevant conditions are simplified, e.g., we ignored the values of variables \texttt{root} and \texttt{val} in the state-guarantee of Triple 1. At a generic pre-state of $C$, variable \texttt{dat} on process $i$ holds value $X_i$. We simplified the condition that all processes have an agreement on their values of \texttt{root} by letting all processes have the same value $r$ for \texttt{root}. Note the state-guarantee in Triple 1 involves the use of the \texttt{\acslold{}} construct to refer the value $X_i$ of \texttt{dat} at the pre-state on process $i$. Triple 1 represents $C$ and its contract. It can be proved valid if Triple 1.1 and 1.2 are valid, according to the sequence rule. Triple 1.1 relates to the contract of $C_0$. Note we added the path-requirement here that was missing in Fig.\ \ref{fig:minimp:spec:gather}. Besides, since \texttt{dat} is modified by $C_0$, the value of \texttt{dat} at the post-state of $C_0$ needs to be represented by a different symbol $Y$. According to the contract of $C_0$, elements in \texttt{dat} on process \texttt{root} are ``gathered'' from other processes, i.e., \[ \forall{t \in \nprocs{n}}.\, Y_r = X_t[t]. \] Triple 1.2 relates to the contract of $C_1$. In addition to the contract showed in Fig.\ \ref{fig:minimp:spec:bcast}, we added an extra path guarantee \begin{center} \texttt{\acslguarantee{\textsf{id}}{\texttt{root}}{\texttt{root}}}. \end{center} Adding such a path guarantee strengthens the guarantee of the original contract. It is not hard for the reader to find out that $C_1$ still satisfies the strengthened contract. By the consequence rule, if the strengthened the triple is valid, the original triple of $C_1$ is also valid. This extra path guarantee is required in meeting Side Condition 1 of the sequence rule. The rest of the side conditions are valid with obviousness. At the post-state of $C_1$, the values of \texttt{dat} are represented with the symbol $Z$ for the aforementioned reason. The state-guarantee can be further simplified to be exact the same as the state-guarantee in Triple 1. \begin{figure} \begin{center} \begin{program} \ccode{var} dat, val, root, i, y;\\ ...\ \\ \mycomment{// contract:}\\ \ccode{requires} \acslforall{} t; \acslon{}(root, t) == root;\\ \ccode{requires} 0 <= root \&\& root < NPROCS \&\& val == dat[PID]; \\ \ccode{assigns} dat, i, y;\\ \ccode{ensures} \acslforall{} t; 0 <= t \&\& t < NPROCS ==>\\ \ \ \ \ \ \ \ \ \ \ dat[t] == \acslold(\acslon(dat[t], t)); \\ \ccode{ensures} \acslabsent{\acslexit(PID)}{\acslenter(PID)}{\acslenter(root)};\\ \end{program} \end{center} \caption{A contract for the sequential combination of the two branch statements given by Fig.\ \ref{fig:minimp:spec:gather} and \ref{fig:minimp:spec:bcast}.} \label{fig:minimp:corule:example:1} \end{figure} \begin{figure}[t] \centering \fbox{ \parbox{.97\textwidth}{ \[ \begin{array}{l l l} 1. & \lco{}~\textsf{dat}_{\textsf{id}} = X_{\textsf{id}} \wedge{} \texttt{root}_{\textsf{id}} = r \wedge{} \texttt{val}_{\textsf{id}} = v_{\textsf{id}} \wedge{} & \hspace{-3cm}\text{(seq 1.1, 1.2)} \\[\myskip] &~~X_{\textsf{id}}[\textsf{id}] = v_{\textsf{id}} \wedge{} 0 \leq r < n,\, \emptyset & \\ &~\rco{} & \\[\myskip] &~C_0C_1 & \\[\myskip] & \lco{}~ \forall{t \in \nprocs{n}}.\, Z_{\textsf{id}}[t] = X_t[t]~\wedge{}~\textsf{dat}_{\textsf{id}} = Z_{\textsf{id}}, & \\ &~~\{\texttt{\acslwaitsfor{\textsf{id}}{$r$}}\} & \\ & \rco{} & \\[\myskip] 1.1. & \lco{}~\textsf{dat}_{\textsf{id}} = X_{\textsf{id}} \wedge{} \texttt{root}_{\textsf{id}} = r \wedge{} \texttt{val}_{\textsf{id}} = v_{\textsf{id}} \wedge{} X_{\textsf{id}}[\textsf{id}] = v_{\textsf{id}} \wedge{} 0 \leq r < n, & \\[\myskip] &~\{\texttt{\acslgamma{\textsf{id}}{$r$}{$r$}}\}~ & \\ [\myskip] & \rco{} &\\ & ~C_0 & \\ [\myskip] & \lco{}~(\forall{t \in \nprocs{n}}.\, Y_r[t] = X_t[t]) \wedge{} \textsf{dat}_{\textsf{id}} = Y_{\textsf{id}} \wedge{} \texttt{root}_{\textsf{id}} = r \wedge{} 0 \leq{} r < n,\, \emptyset{}~\rco{}~ \\ [\myskip] 1.2. & \cocond{~(\forall{t \in \nprocs{n}}.\, Y_r[t] = X_t[t]) \wedge{} \textsf{dat}_{\textsf{id}} = Y_{\textsf{id}} \wedge{} \texttt{root}_{\textsf{id}} = r \wedge{} 0 \leq{} r < n,\, \emptyset{}~} & \\ [\myskip] & ~C_1 & \\ [\myskip] & \lco{}~(\forall{t \in \nprocs{n}}.\, Y_r[t] = X_t[t])~\wedge{}~\textsf{dat}_{\textsf{id}} = Z_{\textsf{id}}~\wedge{}~Z_{\textsf{id}} = Z_r~\wedge{}~Z_r = Y_r, & \\ & \texttt{\ \ $\{$\acslguarantee{\textsf{id}}{$r$}{$r$}}, & \\ & \texttt{\ \ \ \acslwaitsfor{\textsf{id}}{$r$}} \} &\\ &\rco{}& \end{array} \] }} \caption{A $\corule$ derivation of a collective triple that specifies a sequential combination of two collective style \minimp{} statements. } \label{fig:minimp:corule:apply:1} \end{figure} %%%%%%%%%%%%%%%%%% SOUNDESS %%%%%%%%%%%%%%%%%% \section{Extending the Entering/Exiting Notation} \label{sec:extended:enter:exit} In \S\ref{sec:minimp:spec:progseg}, we defined two notations $\myenter^C_{p, \rho}$ and $\myexit^C_{p, \rho}$ for marking the first entering and the corresponding exiting of a substatement $C$ by a process $p$ on a path $\rho$. Here we extend such notations for a sequence of statements $C_0C_1\ldots{}C_{m-1}$. \begin{defn} Let $\progsegs{l_0}{C_0}{l_1}{C_1}{l_2}\ldots{}\progseg{l_{m-1}}{C_{m-1}}{l_m}$ be a program segment of the statement $C = C_0C_1\ldots{}C_{m-1}$. Let $\rho$ be a path. Let $t \in \mypathtrans(\rho)$ be a global transition of the path $\rho$. We define $\myenter^{C_i}_{p, \rho}$ and $\myexit^{C_i}_{p, \rho}$ for $0 \leq{} i < m$ by \begin{itemize} \item $\myenter^{C_0}_{p, \rho} = \myenter^C_{p, \rho}$, \item $t = \myenter^{C_i}_{p, \rho}$, for $i > 0$, if $t$ is the first such transition appearing after $\myexit^{C_{i-1}}_{p, \rho}$ on $\rho$ that \[ \mytoploc(\mysrc(t), p) = l_i~\wedge{}~\myproc(t) = p \] \item $t = \myexit^{C_i}_{p, \rho}$, for $i \geq{} 0$, if $t$ is the first such transition appearing after $\myenter^{C_i}_{p, \rho}$ on $\rho$ that \[ \mytoploc(\mydest(t), p) = l_{i+1}~\wedge{}~\myproc(t) = p~\wedge{}~|\mystack(\mydest(t), p)| = |\mystack(\mysrc(\myenter^{C_i}_{p, \rho}), p)| \] \end{itemize} $\qed$ \end{defn} Intuitively, $\myenter^{C_i}_{p, \rho}$ and $\myexit^{C_i}_{p, \rho}$ represent the entering and exiting, respectively, of each substatement $C_i$ of $C$ by the process $p$ on $\rho$. Again, when $\rho$ is clear in the context, we may simplify the notations to $\myenter^{C_i}_p$ and $\myexit^{C_i}_p$. Remark that, for an execution or an extended execution with $n$ processes of $C_0C_1\ldots{}C_{m-1}$, there is a unique $\myenter^{C_i}_p$, or $\myexit^{C_i}_p$, for $p \in \nprocs{n}, 0 \leq{} i < m$. %% does the event interpretation and absence assertion evaluation need %% to be extended ??? %%%% For The interpretation of events $I^{\textsf{event}}_{C, \rho}$ %%%% has to be generalized accordingly. %%With the generalized event interpretation, the absence assertion %%interpretation $\myaeval{~}$ is generalized naturally. \section{Soundness} \label{sec:rules:soundness} This section presents a proof for the soundness of $\corule$. \begin{defn} Let $t \circ{} t'$ be a path. Let $\myact(t) = p \wedge{} \myact(t') = q$ such that $p \not= q$. The actions of $t$ and $t'$ are said to be \emph{swappable} if it is not the case that \[ \myact(t) = \myactsend{$v$}{$q$}~\wedge{}~\myact(t') = \myactrecv{$v'$}{$p$}~\wedge{}~\mychan(\mysrc(t))(p, q) = \epsilon \qed\] \end{defn} For convenience, we also say two global transitions $t$ and $t'$ are swappable if their actions are swappable. Intuitively, $t$ and $t'$ are swappable if they are associated with different processes and they are independent, i.e., $\myproc(t)$ can execute $\myact(t)$ regardless of $t'$ being executed first or not, and vice versa; $t$ and $t'$ cannot access the process state of a same process or the same message in a message channel. \begin{lema} Let $s \xrightarrow[p]{a} s'$ represent a global transition $t = (s, p, \alpha, s')$ such that $\myact(t) = a$. A path then can be written as $\ldots{} s_0 \xrightarrow[p]{a} s_1 \xrightarrow[q]{b} s_2 \ldots{}$. For $s_0 \xrightarrow[p]{a} s_1 \xrightarrow[q]{b} s_2$, if the two global transitions are swappable, we have \begin{center} $s_0 \xrightarrow[q]{b} s_1' \xrightarrow[p]{a} s_2$ \end{center} \label{lema:base} \end{lema} \noindent{} \textbf{Proof} A proof can be constructed by induction on atomic actions of the two global transitions. We omit this proof for two reasons (1) it is in fact a more specific case of the general \emph{reduction} approach proposed by Lipton in \cite{lipton:reduction}; and (2) the lemma is intuitive and is well-known in the field of verification of message-passing programs. $\qed$ Given a path $\rho\colon{} s_0 \xrightarrow[p]{a} s_1 \xrightarrow[q]{b} s_2$ with two swappable transitions, the path $s_0 \xrightarrow[q]{b} s_1' \xrightarrow[p]{a} s_2$ is said to be obtained via \emph{swapping transitions} of $\rho$. And, by Lemma \ref{lema:base}, we know these two paths share their initial and the final states. %%%% SUFFICIENT NON-INTERFERENCE LEMMA \begin{lema} Let $\rho$ be a path in the state space graph of $C_0C_1$ with $n$ processes. If $C_1$ does not interfere $C_0$, then for every sub-path $t \circ{} t'$ of $\rho$ such that (1) $\myproc(t) \not= \myproc(t')$, and (2) $t$ appears before $\myexit^{C_0}_{\myproc(t), \rho}$ and $t'$ appears after $\myexit^{C_0}_{\myproc(t'), \rho}$ on $\rho$, formally, \begin{align} \exists{i, j, x, y \in \mathbb{Z}}.\,\, & i < j~\wedge{}~x < y~\wedge{}~t = \rho[i]~\wedge{}~t' = \rho[y]~\wedge{} \nonumber \\ &\myexit^{C_0}_{\myproc(t), \rho} = \rho[j] \wedge{} \myexit^{C_0}_{\myproc(t'), \rho} = \rho[x], \nonumber \end{align} then $t$ and $t'$ are swappable. \label{lema:gen:non-interfere-sufficient} \end{lema} \noindent\textbf{Proof} We prove by contradiction. Suppose that there is a sub-path $t \circ{} t'$ of $\rho$ satisfying Condition 1 and 2 given in the lemma above, but $t, t'$ are not swappable. Let $\myproc(t) = p$, $\myproc(t') = q$, and $\rho_p$, $\rho_q$ be two prefixes of $\rho$ such that $\rho_p$ ends with $\myexit^{C_0}_p$ and $\rho_q$ ends with $\myexit^{C_0}_q$, respectively. Since $C_0$ is not interfered by $C_1$ on $\rho$, \begin{equation} \mynsends{\rho_p}{p}{q} = \mynrecvs{\rho_q}{p}{q}~\wedge{}~ \mynsends{\rho_q}{q}{p} = \mynrecvs{\rho_p}{q}{p} \tag{3} \end{equation} Since $t$ and $t'$ are not swappable, $\mychan(\mysrc(t))(p, q) = \epsilon$. Let $\rho_t$ be the prefix of $\rho_p$ that ends with $t$. We have \begin{equation} \mynrecvs{\rho_{t}}{p}{q} = \mynsends{\rho_{t}}{p}{q}. \tag{4} \end{equation} Since $\myact(t) = \myactsend{p}{q}$, \begin{equation} \mynsends{\rho_p}{p}{q} > \mynsends{\rho_{t}}{p}{q}. \tag{5} \end{equation} Simplifying $(3), (4), (5)$ to \begin{equation} \mynrecvs{\rho_q}{p}{q} > \mynrecvs{\rho_{t}}{p}{q}. \tag{6} \end{equation} However, by our assumption, $t \circ{} t'$ appears after $\myexit^{C_0}_q$ on $\rho$, we have \begin{equation} \mynrecvs{\rho_q}{p}{q} \leq \mynrecvs{\rho_{t}}{p}{q}. \tag{7} \end{equation} There is a contradiction between $(6)$ and $(7)$. $\qed{}$ \begin{coro} Let $\pi$ be an execution in a state space graph of $C_0C_1$ that ends with the termination of all processes. If $C_1$ cannot interfere $C_0$, Lemma \ref{lema:gen:non-interfere-sufficient} allows one to keep swapping swappable transitions on $\pi$ to produce an alternative path $\pi'$ in the same state space graph such that \begin{enumerate} \item $\pi$ and $\pi'$ share their initial and the final states. \item $\pi' = \pi_0 \circ{} \pi_1$, where $\pi_0$ is an execution of $C_0$ and $\pi_1$ is an execution of $C_1$. $\qed$ \end{enumerate} \label{coro:pre:post:alternative} \end{coro} %%%% REPRODUCE LEMMA \begin{lema} Let $\zeta$ be an extended execution of $C_0C_1$ with $n$ processes. Let $P$ be a set of processes such that \[ p \in P \text{ iff } \myexit^{C_0}_{p, \zeta} \in \mypathtrans(\zeta). \] Now if \[ \forall{q \in \nprocs{n}}.\,\forall{p \in P}.\,\, \mychan(\mydest(\myexit^{C_0}_{p, \zeta}))(q, p) = \epsilon, \] then there is another extended execution $\zeta'$ of $C_0C_1$ with $n$ processes such that $\zeta' = \pi_0' \circ{} \zeta_1'$, where \begin{enumerate} \item $\pi_0'$ is an execution of $C_0$ with $n$ processes, \item $\zeta_1'$ is an extended execution of $C_1$ with $n$ processes, \item $\forall{t \in \mypathtrans(\zeta_1')}.\, \myproc(t) \in P$, and \item every global transition $t \in \mypathtrans(\zeta_1')$ corresponds to a unique one appearing after $\myexit^{C_0}_{\myproc(t), \zeta}$ on $\zeta$, formally, \begin{align} & \text{let } N = \{i \in \mathbb{Z} \mid 0 \leq{} i < |\zeta|\} \text{ in} \nonumber \\ & \forall{t' \in \mypathtrans(\zeta_1')}.\, \exists{t \in \mypathtrans(\zeta)}.\,\exists{i, j \in N}.\,\, i < j~\wedge{}~ \zeta[i] = \myexit^{C_0}_{\myproc(t)}~\wedge{} \nonumber \\ &~~~~~~~~~~~~~~~~\zeta[j] = t~\wedge{}~\myact(t) = \myact(t')~\wedge{}~\myproc(t) = \myproc(t'). \nonumber \end{align} \end{enumerate} \label{lema:seq:reproduce} \end{lema} \noindent\textbf{Proof} Considering the same path $\zeta$ and process set $P$ in this lemma. By Lemma \ref{lema:base} and \ref{lema:gen:non-interfere-sufficient}, we have an alternative path $\rho$ to $\zeta$ with $n$ processes such that \begin{enumerate} \item $\rho$ shares the initial state with $\zeta$ \item $\rho = \rho_0 \circ{} \rho_1$ such that \[ p \in P \text{ iff } \myexit^{C_0}_{p, \rho} \in \mypathtrans(\rho_0) ~\text{ and }~ p \in P \text{ iff } \myenter^{C_1}_{p, \rho} \in \mypathtrans(\rho_1) \tag{2.1} \] \end{enumerate} Condition 2.1 above implies that (1) all processes in $P$ are at the exit of $C_0$ (or entry of $C_1$) at the final state of $\rho_0$ while other processes are still in $C_0$, and (2) $\rho_1$ contains no transition associated with processes not in $P$. Furthermore, according to the assumption over message channels, we have \[ \forall{q \in \nprocs{n}}.\,\forall{p \in P}.\,\mychan(\mysrc(\myhead(\rho_1)))(q, p) = \epsilon. \] Therefore, no transition in $\rho_1$ depends on any process in $\nprocs{n}\BSL{}P$ or the message channels from $\nprocs{n}\BSL{}P$ to $P$ at the initial state of $\rho_1$. Now we first construct the execution $\pi_0'$ of $C_0$ to $\pi_0' = \rho_0 \circ{} \rho_0'$ via letting all processes in $\nprocs{n} \BSL{} P$ continue to execute from $\mydest(\mytail(\rho_0))$ until they are all at the exit of $C_0$. Process states of processes in $P$ stay the same along $\rho_0'$ because none of them ever executes. Note we are not interested in non-termination problem here. Second, we construct the $\zeta'$ to $\zeta' = \pi_0' \circ{} \zeta_1'$ via making $|\rho_1| = |\zeta_1'|$ and \[ \forall{i\in\mathbb{Z}}.\, 0 \leq{} i < |\rho_1| \Rightarrow{} \myproc(\rho_1[i]) = \myproc(\zeta_1'[i])~\wedge{}~ \myact(\rho_1[i]) = \myact(\zeta_1'[i]). \] Although there is no guarantee that $\mychan(\mydest(\mytail(\pi_0'))(q, p) = \epsilon$ for some $q \in \nprocs{n}$ and $ p \in P$, transitions in $\rho_1$ only depend on the process states of processes in $P$. So the construction is feasible. Remark that transitions in $\rho_1$ are obtained by swapping transitions in $\zeta$, so Condition 4 in this lemma is naturally implied. $\qed$ \begin{teom}[soundness of the sequence rule] Assuming all the side conditions of the sequence rule hold, \begin{center} $\model \models \cotriplearg{C_0C_1}$, if \\ $\model \models \mycosubtriple{0}{\psi}{\mu}{C_0}$ and $\model \models \mycosubtriple{1}{\mu}{\phi}{C_1}$. \end{center} \label{lema:seq} \end{teom} \noindent\textbf{Proof} The proof of Theorem \ref{lema:seq} is carried out by Lemma \ref{lema:seq:zero}, \ref{lema:seq:one}, \ref{lema:seq:two} and \ref{lema:seq:three}. $\qed$ %%%% LEMMA ZERO \begin{lema} Under the assumption made in Theorem \ref{lema:seq}, for an execution $\pi$ in the state space graph of $C_0C_1$ with $n$ processes, if $\psi$ and $\myallemptyguard{}$ hold on the initial state for all processes, $C_1$ does not interfere $C_0$ on $\pi$. \label{lema:seq:zero} \end{lema} \noindent\textbf{Proof} We prove by contradiction. Assuming $\myinterfere{\pi}{C_0}(p, q)$ for an ordered pair of unique processes $p, q \in \nprocs{n}$. Without loss of generality, we also assume that \begin{enumerate} \item[(a)] $(p, q)$ is the only such ordered pair of processes that $\myinterfere{\pi}{C_0}(p, q)$, and \item[(b)] let $\rho_p$ and $\rho_q$ be the prefixes of $\pi$ that end with $\myexit^{C_0}_{p, \pi}$ and $\myexit^{C_0}_{q, \pi}$, respectively, $\mynsends{\rho_p}{p}{q} + 1 = \mynrecvs{\rho_q}{p}{q}$. \end{enumerate} Then $\pi$ must have such a form: $\ldots{} \circ{} t_p \circ{}\ \ldots{} \circ{} t_q \circ{} \ldots{} $, where \begin{enumerate} \item $\myproc(t_p) = p$, $\myact(t_p) = $ \myactsend{$v$}{$q$}, $\myproc(t_q) = q$ and $\myact(t_q) = $ \myactrecv{$v'$}{$p$}, for some $v$ and $v'$, and \item $\mychan(\mysrc(t_p))(p, q) = \epsilon{}$, and \item $t_p$ appears after $\myexit^{C_0}_{p,\pi}$ and $t_q$ appears before $\myexit^{C_0}_{q,\pi}$ on $\pi$. \end{enumerate} Since $C_0$ is interfered by $C_1$ as above, and $\model \models \mycosubtriple{0}{\psi}{\mu}{C_0}$, it must be the case that \begin{align} \texttt{\acslgamma{$p$}{$q$}{$r$}} \in_\pi \Gamma_0, \nonumber \end{align} for some processes $r \in \nprocs{n}$. Considering the prefix $\rho$ of $\pi$ that ends with $t_p$. Let $P$ be the set of processes such that $x \in P$ iff $\myexit^{C_0}_x$ is in $\mypathtrans(\rho)$. Obviously $p \in P$ and $q, r \not\in P$. By the assumption (a) above, we have \[ \forall{y \in \nprocs{n}}\forall{x \in P}.\, \mychan(\mysrc(\myhead(\myexit^{C_0}_x)))(y, x) = \epsilon{}. \] So we can apply Lemma \ref{lema:seq:reproduce}. It results in the existence of an extended execution $\zeta = \pi_0 \circ{} \rho_1$ of $C_0$ such that \begin{itemize} \item the execution $\pi_0$ of $C_0$ shares the initial state with $\pi$, \item $\rho_1$ is a prefix of an execution of $C_1$, and \item $\forall{t \in \mypathtrans(\rho_1)}.\,\, \myproc(t) \in P$ and $\exists{t \in \mypathtrans(\rho_1)}.\,\, \myact(t) = $ \myactsend{$v$}{$q$} for some $v$. \end{itemize} Note $\zeta$ is also in the same state space graph as where $\pi$ is in. Since $\pi_0$ is an execution of $C_0$, which shares the initial state with $\pi$, and the triple of $C_0$ is valid, we have $\mu$ and \myallemptyguard{} hold at the final state $\mydest(\mytail(\pi'))$ (equal to $\mysrc(\myhead(\rho'))$) for all processes. Since $\model \models \mycosubtriple{1}{\mu}{\phi}{C_1}$, considering the $\rho_1$, there is no \begin{align} \texttt{\acslguarantee{$p$}{$q$}{$r'$}} \in_{\rho_1} \Upsilon_1 \nonumber \end{align} such that $r' = r \vee r' = q$. Thus, for $\zeta$, the assertion $\Upsilon_1~\ruleguarantee{_\zeta}~\Gamma_0$ fails to hold. It contradicts the assumption that Side Condition 1 is satisfied. $\qed$ %%%%%%%%%%%%%% LEMMA ONE %%%%%%%%%%%%%%%%%%% \begin{lema} Under the assumption made in Theorem \ref{lema:seq}, if an execution $\pi$ of $C_0C_1$ emanates from a pre-state of $C_0$ where $\psi$ and $\myallemptyguard{}$ hold for all processes, and $\pi$ ends with a post-state of $C_1$, then $\phi$ and $\myallemptyguard{}$ hold on the post-state for all processes. \label{lema:seq:one} \end{lema} \noindent\textbf{Proof} According to Lemma \ref{lema:seq:zero}, $C_0$ cannot be interfered by $C_1$ on $\pi$. Then we can apply Corollary \ref{coro:pre:post:alternative}. It results in an alternative $\pi'$ to $\pi$ in the same state space graph such that \begin{enumerate} \item $\pi$ and $\pi'$ share the initial and the final states, and \item $\pi' = \pi_0 \circ{} \pi_1$ such that $\pi_0$ is an execution of $C_0$ and $\pi_1$ is an execution of $C_1$. \end{enumerate} Because of $\model \models \mycosubtriple{0}{\psi}{\mu}{C_0}$ and $\model \models \mycosubtriple{1}{\mu}{\phi}{C_1}$, we have $\phi$ and $\myallemptyguard$ hold on $\mydest(\mytail(\pi'))$. Thus, $\phi$ and $\myallemptyguard$ also hold on $\mydest(\mytail(\pi))$. $\qed$ %%%%%%%%%%%%%%%% LEMMA TWO %%%%%%%%%%%%%%%%%% \begin{lema} Under the assumption made in Theorem \ref{lema:seq}, for an execution $\pi$ with $n$ processes of $C_0C_1$ that emanates from a pre-state $s$ of $C_0$, where $\psi$ and $\myallemptyguard{}$ hold for all processes, $\forall{p \in \nprocs{n}}. \pi \vdash{} \myaeval{\textup{$\Upsilon$}}_{C_0C_1}(s, p)$. \label{lema:seq:two} \end{lema} \noindent\textbf{Proof} By Lemma \ref{lema:seq:zero}, $C_1$ cannot interfere $C_0$. We prove this lemma by contradiction. Let $p, q, r, x \in \nprocs{n}$ be some processes. Let $s = \mysrc(\myhead(\pi))$. Suppose that there is an absence assertion $\upsilon \in_\pi \Upsilon$ such that \begin{equation} \pi \vdash{} \neg\myaeval{\upsilon}_{C_0C_1}(s, k), \tag{a} \label{lema:seq:two:proof:a} \end{equation} for any $k \in \nprocs{n}$. There are two cases according to the possible forms of $\upsilon$. Case 1, we have \begin{equation} \upsilon = \texttt{\acslwaitsfor{$p$}{$q$}}. \tag{b} \label{lema:seq:two:proof:caseone:b} \end{equation} By Side Condition 3 of the sequence rule, there are two sub-cases. \begin{enumerate} \item[(1.1)] $\upsilon \in_\pi \Upsilon_0$. By Corollary \ref{coro:pre:post:alternative}, there is an alternative execution $\pi'$ to $\pi$ such that $\pi' = \pi_0 \circ{} \pi_1$, where \begin{itemize} \item $\pi$ and $\pi_0$ share the initial state $s$, \item $\pi_0$ is an execution of $C_0$, and \item $\pi_1$ is an execution of $C_1$. \end{itemize} The transition swapping performed on $\pi$ for obtaining $\pi'$ preserves the order that $\myexit^{C_0}_{p, \pi}$ appears before $\myenter^{C_0}_{q, \pi}$ on $\pi$ (by Assumption \ref{lema:seq:two:proof:a}). So $\pi_0 \vdash \neg\myaeval{\upsilon}_{C_0}(s, k)$ as long as $\pi \vdash{} \neg\myaeval{\upsilon}_{C_0C_1}(s, k)$. It contradicts the assumption that the triple of $C_0$ is valid. \item[(1.2)] Since $C_0$ cannot be interfered by $C_1$, we can apply Lemma \ref{lema:seq:reproduce} to a prefix of $\pi$ that ends with $\myexit^{C_1}_{p, \pi}$. It results in an extended execution $\zeta$ of $C_0$ such that $\zeta = \pi_0 \circ{} \xi_1$, where \begin{itemize} \item $\pi_0$ is an execution of $C_0$, \item $\xi_1$ is a prefix of an execution of $C_1$, and $\mu$ and $\myallemptyguard$ hold for all processes on $\mysrc(\myhead(\xi_1))$, according to Lemma \ref{lema:seq:one}, and \item $\upsilon \in_{\xi_1} \Upsilon_1$. \end{itemize} We show a contradiction to the validity of the triple of $C_1$ by showing that $\upsilon$ is violated by $\xi_1$. By Assumption \ref{lema:seq:two:proof:a}, process $q$ has not entered $C_0$ while process $p$ exits $C_1$, i.e., $\myenter^{C_0}_{q, \pi}$ appears after $\myexit^{C_1}_{p, \pi}$ on $\pi$. And by fact, $\myenter^{C_1}_{q, \pi}$ has to appear after $\myenter^{C_0}_{q, \pi}$ on $\pi$. Thus, no $\myenter^{C_1}_{q, \zeta}$ in $\xi_1$, while by Lemma \ref{lema:seq:reproduce}, $\xi_1$ includes $\myexit^{C_1}_{p, \zeta}$. \end{enumerate} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Now considering Case 2. We have \begin{equation} \upsilon = \texttt{\acslguarantee{$p$}{$q$}{$r$}}. \tag{c} \label{lema:seq:two:casetwo:c} \end{equation} By the $\nosendsubset(\Upsilon) \subseteq_\pi \Upsilon_0$ part of Side Condition 2 of the sequence rule, we have $\upsilon \in_\pi \Upsilon_0$. We now have two sub-cases regarding to the order of $\myexit^{C_0}_{p, \pi}$ and a transition $t_p$ on $\pi$, where $\myproc(t_p) = p$ and $\myact(t_p) = $ \myactsend{$v$}{$q$} for some $v$. Note such $t_p$ must exist on $\pi$ because $\upsilon$ is assumed to be violated on $\pi$. \begin{itemize} \item[2.1] \begin{equation} t_p \text{ appears before } \myenter^{C_0}_{r, \pi} \text{ and } \myexit^{C_0}_{p, \pi} \text{ on } \pi \tag{d} \label{lema:seq:two:casetwoone:d} \end{equation} Let us continue to consider the execution $\pi' = \pi_0 \circ{} \pi_1$ mentioned in Case 1.1. Again, the transition swapping performed on $\pi$ to obtain $\pi'$ preserve the order that $t_p$ appears before $\myenter^{C_0}_{r, \pi}$ on $\pi$ (by Condition \ref{lema:seq:two:casetwoone:d}). We have $\pi_0 \vdash{} \neg\myaeval{\upsilon}_{C_0}(s, k)$ as long as $\pi \vdash{} \neg\myaeval{\upsilon}_{C_0C_1}(s, k)$ (Assumption \ref{lema:seq:two:proof:a}). Contradicting the validity of the triple of $C_0$. \item[2.2] \begin{equation} t_p \text{ appears before } \myenter^{C_0}_{r, \pi} \text{ and after } \myexit^{C_0}_{p, \pi} \text{ on } \pi \tag{e} \label{lema:seq:two:casetwotwo:e} \end{equation} There are three further sub-cases according to Side Condition 2 of the sequence rule. \item[2.2.1] There is \begin{align} \texttt{\acslwaitsfor{$p$}{$r$}} \in_\pi \Upsilon_0 \nonumber \end{align} This case can be proved contradicting to Assumption \ref{lema:seq:two:casetwotwo:e} with the same idea as how was Case 2.1 proved. \item[2.2.2] Considering the alternative $\pi' = \pi_0 \circ{} \pi_1$ mentioned in Case 1.1. There is \begin{align} \texttt{\acslwaitsfor{$x$}{$r$}} \in_\pi \Upsilon_0 \nonumber \end{align} and there is \begin{align} \texttt{\acslguarantee{$p$}{$q$}{$x$}} \in_{\pi_1} \Upsilon_1 \nonumber \end{align} Since both the triples of $C_0$ and $C_1$ are valid, we have \begin{align} &\myenter^{C_0}_{r, \pi_0} \text{ appears before } \myexit^{C_0}_{x, \pi_0} \text{ on } \pi_0, \tag{f} \label{lema:seq:two:casetwotwotwo:f} \\ &\myenter^{C_1}_{x, \pi_1} \text{ appears before every such } t_p' \text{ on } \pi_1 \text{ that } \myproc(t_p') = p\wedge{}\myact(t_p') = \myact(t_p)\tag{g} \label{lema:seq:two:casetwotwotwo:g} \end{align} Transition swapping performed on $\pi$ for obtaining $\pi'$ preserves the orders of the transitions given in Condition \ref{lema:seq:two:casetwotwotwo:f} and \ref{lema:seq:two:casetwotwotwo:g}. Thus, we have $\myenter^{C_0}_{r, \pi}$ appears before $t_p$ on $\pi$. Contradicting Assumption \ref{lema:seq:two:proof:a} under Case 2. \item[2.2.3] Considering the alternative $\pi' = \pi_0 \circ{} \pi_1$ mentioned in Case 1.1. There is \begin{align} \texttt{\acslguarantee{$p$}{$q$}{$r'$}} \in_{\pi_1} \Upsilon_1,\nonumber \end{align} where $r' = r \vee{} r' = q$. A contradiction to Assumption \ref{lema:seq:two:proof:a} under Case 2 can be proved with the same idea used in Case 2.2.2. \end{itemize} $\qed$ %%%% SEQ LEMMA THREE \begin{lema} Under the assumption made in Theorem \ref{lema:seq}, for an extended execution $\zeta$ with $n$ processes of $C_0C_1$, which starts from a pre-state of $C_0$ where $\psi$ and $\myallemptyguard$ hold for all processes, we have \begin{align} & \text{let } s = \mysrc(\myhead(\zeta)) \text{ in} \nonumber \\ & \forall{p, q \in \nprocs{n}}.\,\, \myinterfere{\zeta}{C_0C_1}(p, q) \Rightarrow (\exists{k \in \nprocs{n}}. \zeta \vdash{} \neg{}\myaeval{\textup{$\Gamma$}}_{C_0C_1}(s, k)). \nonumber \end{align} \label{lema:seq:three} \end{lema} \noindent\textbf{Proof} Let $p, q, r \in \nprocs{n}$ be some processes. Let $s = \mysrc(\myhead(\zeta))$. To prove by contradiction, we assume that \begin{align} & \myinterfere{\zeta}{C_0C_1}(p, q)~\wedge{}~ \forall{k\in\nprocs{n}}. \zeta \vdash{} \myaeval{\textup{$\Gamma$}}_{C_0C_1}(s, k), \tag{a} \label{lema:three:proof:a} \end{align} for an ordered pair of processes $(p, q)$. Without loss of generality, we further assume that \begin{itemize} \item $(p, q)$ is the only such order pair of processes that $\myinterfere{\zeta}{C_0C_1}(p, q)$, and \item let $\rho_p$ and $\rho_q$ be the prefixes of $\zeta$ such that end with $\myexit^{C_1}_{p, \zeta}$ and $\myexit^{C_1}_{q, \zeta}$, respectively, we have $\mynsends{\rho_p}{p}{q} + 1 = \mynrecvs{\rho_q}{p}{q}$. \end{itemize} Then $\zeta$ must have the form $\ldots{} \circ{} t_p \circ{} \ldots{} \circ{} t_q \circ{} \ldots{}$, where \begin{itemize} \item $\myproc(t_p) = p$, $\myproc(t_q) = q$, $\myact(t_p) = $ \myactsend{$v$}{$q$} and $\myact(t_q) = $ \myactrecv{$v'$}{$p$} for some $v, v'$, and \item $\mychan(\mysrc(t_p))(p, q) = \epsilon{}$, and \item $t_p$ appears after $\myexit^{C_1}_{p, \zeta}$ and $t_q$ appears before $\myexit^{C_1}_{q, \zeta}$ on $\zeta$. \end{itemize} There are two cases for $\zeta$ with respect to the order of $t_q$ and $\myexit^{C_0}_{q, \zeta}$ on $\zeta$: \begin{itemize} \item[1.] $t_q$ appears before $\myexit^{C_0}_{q, \zeta}$ on $\zeta$, and \item[2.] $t_q$ appears after $\myexit^{C_0}_{q, \zeta}$ and before $\myexit^{C_1}_{q, \zeta}$ on $\zeta$. \end{itemize} %% LEMMA:SEQ:THREE PROVE FOR CASE 1 For Case 1, we have $\myinterfere{\zeta}{C_0}(p, q)$ because $\zeta$ is also a extended execution of $C_0$. Then, by the assumption that the triple of $C_0$ is valid, we have \begin{align} & \gamma = \texttt{\acslgamma{$p$}{$q$}{$r$}} \in_\zeta \Gamma_0 \tag{b} \label{lema:three:proof:b} \end{align} such that $\zeta$ violates $\gamma$ for $C_0$. By Side Condition 4 of the sequence rule, there are two sub-cases. \begin{enumerate} \item[(1.1)] We have $\gamma \in_\zeta \Gamma$. According to our construction of $\zeta$. It contradicts Assumption \ref{lema:three:proof:a}. \item[(1.2)] By our construction of $\zeta$, we can apply Lemma \ref{lema:seq:reproduce} to $\zeta$ to get an extended execution $\zeta'$ of $C_0$ such that $\zeta' = \pi_0' \circ{} \xi_1'$, where $\pi_0'$ is an execution of $C_0$ and $\xi_1'$ is an extended execution of $C_1$. In this case, $\Upsilon_1~\rulecancels_{\zeta'}~\gamma_0$. Consequently, \[ \upsilon = \texttt{\acslwaitsfor{$p$}{$x$}} \in_{\zeta'} \Upsilon_1, \] where $x = r \vee{} x = q$. We need to show that $\upsilon$ is violated by $\xi_1$ for a contradiction to the validity of the collective triple of $C_1$. Recall in our construction of $\zeta$, \begin{center} $t_p$ appears after $\myexit^{C_1}_{p, \zeta}$ and before $\myexit^{C_0}_{q, \zeta}$ on $\zeta$. \end{center} Consequently, \begin{equation} \myexit^{C_1}_{p, \zeta} \text{ appears before } \myenter^{C_1}_{q, \zeta} \text{ on } \zeta. \tag{c} \label{lema:three:proof:c} \end{equation} Since the existence of $t_p$ leads to the violation of $\gamma$ by $\zeta$ for $C_0$ (Assumption \ref{lema:three:proof:b}), $t_p$ appears before $\myenter^{C_1}_{r, \zeta}$ on $\zeta$. Consequently, \begin{equation} \myexit^{C_1}_{p, \zeta} \text{ appears before } \myenter^{C_1}_{r, \zeta} \text{ on } \zeta. \tag{d} \label{lema:three:proof:d} \end{equation} Note that the order of $\myexit^{C_1}_{p, \zeta}, \myenter^{C_1}_{q, \zeta}$ and $\myenter^{C_1}_{r, \zeta}$ is preserved during the transition swapping performed on $\zeta$. Then, by Condition \ref{lema:three:proof:c} and \ref{lema:three:proof:d}, we have that $\upsilon$ is violated by $\xi_1'$ for $C_1$. \end{enumerate} %% LEMMA:SEQ:THREE PROVE FOR CASE 2 Now we prove for Case 2. Let us continue to consider the extended execution $\zeta' = \pi_0' \circ{} \xi_1'$ used in Case 1.2. Under Case 2, $\myinterfere{\xi_1'}{C_1}(p, q)$, because the order of $t_p$, $t_q$, $\myexit^{C_1}_{p, \zeta}$ and $\myexit^{C_1}_{q, \zeta}$ is preserved by the transition swapping performed on $\zeta$. Then, since the triple of $C_1$ is valid, there must be \[ \gamma = \texttt{\acslgamma{$p$}{$q$}{$r$}} \in_{\xi_1'} \Gamma_1 \nonumber \\ \tag{e} \label{lema:three:proof:e} \] s.t.\ $\gamma$ is violated by $\xi_1'$ for $C_1$. By Side Condition 4 of the sequence rule, we have \[ \gamma \in_{\zeta'} \Gamma. \tag{f} \label{lema:three:proof:f} \] Again, the order of $t_p$, $t_q$, $\myexit^{C_1}_{p, \zeta}, \myexit^{C_1}_{q, \zeta}$ and $\myexit^{C_1}_{r, \zeta}$ is preserved by transition swapping performed on $\zeta$ for obtaining $\zeta'$, we conclude that \[ \zeta \text{ has the form } \rho_0 \circ{} t_p \circ{} \rho_1 \circ{} t_q \circ{} \rho_2 \] s.t.\ \begin{itemize} \item $\myexit^{C_1}_{p, \zeta} \in \mypathtrans(\rho_0)$, by construction of $\zeta$, and \item $\myexit^{C_1}_{r, \zeta} \in \mypathtrans(\rho_1) \cup \mypathtrans(\rho'')$, by Condition \ref{lema:three:proof:e}, and \item $\myexit^{C_1}_{q, \zeta} \in \mypathtrans(\rho_2)$, by construction of $\zeta$. \end{itemize} Thus, together with Condition \ref{lema:three:proof:f}, $\upsilon$ is violated by $\zeta$. Contradicting Assumption \ref{lema:three:proof:a}. $\qed$ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{teom}[soundness of the consequence rule] Assuming the side conditions of the consequence rule over $\psi, \psi', \phi, \phi', \Gamma, \Gamma', \Upsilon$ and $\Upsilon'$ hold, \begin{center} $\model \models \cotriplenoloc$, if $\model \models \cocond{\psi', \Gamma'}~C~\cocond{\phi', \Upsilon'}$. \end{center} \label{lema:conseq} \end{teom} \noindent\textbf{Proof} Strengthening the state- or the path-requirement cannot invalidate a valid collective triple. Dually, weakening the state- or the path-guarantee cannot invalidate a valid collective triple. $\qed$ \param{} \begin{teom}[soundness of the collective loop rule] Assuming the side condition of the collective loop rule holds, \begin{center} $\model \models \cocond{\mymath{inv},\,\Gamma{}}~ {\texttt{while(}c\texttt{)}~C} ~\cocond{\neg{}c \wedge{} \mymath{inv},\, \Upsilon{}}$, if $\model \models \cocond{\mymath{inv} \wedge{} c,\, \Gamma}~C~ \cocond{\mymath{inv},\, \Upsilon}$. \end{center} \label{lema:loop} \end{teom} \noindent\textbf{Proof} Imagine unrolling the loop to a finite sequence $CC\ldots{}C$ of length $m$. The validity of the original triple of the loop can be proved by proving the following two tasks, \begin{enumerate} \item $\model \models{} \cocond{\mymath{inv} \wedge{} c,\, \Gamma}~CC\ldots{}C~ \cocond{\mymath{inv} \wedge{} c,\, \Upsilon}$, with the strengthened assumption $\model \models{} \cocond{\mymath{inv} \wedge{} c, \Gamma}~C~\cocond{\mymath{inv} \wedge{} c, \Upsilon}$, for the prefix $CC\ldots{}C$ of length $m-1$, and \item $\model \models{} \cocond{\mymath{inv} \wedge{} c, \Gamma}~C~\cocond{\mymath{inv}, \Upsilon}$. \end{enumerate} Task 1 can be proved by repeatedly applying the sequence rule. Task 2 is directly inferred by the assumption. $\qed$ \begin{teom}[soundness of the elaboration rule] \[ \model \models \cotriplenoloc \] if $ \cocond{\psi{}}~\overrightarrow{C} \subseteq{} \overrightarrow{C_0C_1} $ and $ \model \models \cocond{\psi{}, \Gamma}~{C_0}{C_1}~\cocond{\phi{}, \Upsilon}. $ \label{lema:elab} \end{teom} \noindent\textbf{Proof} According to the elaboration condition, for every execution $\pi$ of $C$, there is an equivalent execution $\pi'$ of $C_0C_1$ such that that both executions start from a same pre-state where $\psi$ holds. The only difference between $\pi$ and $\pi'$ is that they have different transitions in them that are all labeled by \texttt{skip}, which has no effect on neither the memory in state nor the order of process executions. So whenever $\pi'$ satisfies a specification, $\pi$ satisfies the same specification. $\qed$ \param{}