\section{Draft}
\subsection{MiniMP and Specification}
\begin{enumerate}
\item MiniMP
  \begin{itemize}
  \item syntax
  \item semantics: an interpretation
    $\mymath{I(s, p, edge) \mapsto \{s\}}$
  \end{itemize}
\item Specification
  \begin{itemize}
  \item specification language
  \item $\{\phi\} \textbf{ co } S \textbf{ oc } \{\psi\}$: \\
    If all processes are at pre-state of $S$ where $\phi$ holds, after
    collectively executing $S$, all processes stop at post-state of
    $S$ where $\psi$ will hold. (will be formally expressed with
    respect to the semantics of MiniMP)
  \item proof system: 1) collective composition rule; 2) collective
    consequence rule
  \item proof of $\{\phi\} \textbf{ co } S \textbf{ oc } \{\psi\}$ is
    decomposed into proof of
    \begin{itemize}
    \item[] $\{\phi\} \textbf{ co } S_0 \textbf{ oc } \{Q_0\}$
    \item[] ...
    \item[]  $\{Q_{n-1}\} \textbf{ co } S_{n-1} \textbf{ oc } \{\psi\}$
    \end{itemize}
    for $S = S_0S_1...S_{n-1}$
  \end{itemize}
\item collective-style functions and contracts $C_f$ for function $f$
  \\
~~~~~~~~~~~~ $(C_f, f)$ ? $\{\phi\} \textbf{ co } f \textbf{ oc } \{\psi\}$
\item model checking and symbolic execution algorithm:
  $V(\model, \{C_f\}, \{Q_0\})$, $\model \models_{0 .. n} C_f$
  iff $V(\model, \{C_f\}, \{Q_0, Q_1, ..., Q_n\}) = T$
  
\end{enumerate}

\section{Collective Proof Rules}

Let $\preceq$ be an operator denoting ``no later than'', we have
\begin{align}
  & 1)~event \preceq event \nonumber \\
  \nonumber \\
  & 2)~\text{for a process } p \text{, if }\texttt{$S_0$;$S_1$}\text{, we have}\nonumber \\
  & enter_{S_0}(i) \preceq exit_{S_0}(i) = enter_{S_1}(i) \preceq
    exit_{S_1}(i) \nonumber
\end{align}

\textbf{Helper predicates:}
\begin{itemize}
\item  $\mymath{guarantee(\Gamma, a)}$  iff 
$\mymath{a[\texttt{enter}/\texttt{exit},\,
      \texttt{exit}(e_0) 
      / \texttt{send}(e_0, e_1)] \in \Gamma}$

  \item $\Gamma^{\sim}$ is the subset of $\Gamma$, each of which
    contains no \texttt{exit} event
\end{itemize}


\begin{enumerate}
\item collective composition rule:
  \begin{align}
    &\frac{
      \cocond{\psi{} \wedge \bigwedge{\Gamma}} C_0
      \cocond{Q \wedge \bigwedge{\Upsilon^{\sim}}},\,\,
      \cocond{Q \wedge \bigwedge{\Delta}} C_1
      \cocond{\phi{} \wedge \bigwedge{\Upsilon}}
      }
      {
      \cocond{\psi{} \wedge \bigwedge{\Gamma'}}~C_0\texttt{;}C_1~
      \cocond{\phi{} \wedge \bigwedge{\Upsilon'}}      
      }
      \nonumber
  \end{align}
  \begin{enumerate}
  \item $\mymath{\Gamma' \cup \Delta\subseteq \Gamma \wedge
    (\forall{a}.\, guarantee(\Upsilon, a), a \in \Gamma)}$
  \item $\mymath{\Delta = \{a |\, \neg{}guarantee(\Upsilon, a)
      \wedge a \in \Gamma'\}}$
  \item $\Upsilon = \Upsilon' - \Upsilon^{\sim}$
  \end{enumerate}
  
\item collective consequence rule:
  \begin{align}
    \frac{
    \cocond{\psi \wedge \bigwedge{\Gamma}} C \cocond{\phi \wedge \bigwedge{\Upsilon}}
    }
    {
    \cocond{\psi' \wedge \bigwedge{\Gamma'}} C \cocond{\phi' \wedge \bigwedge{\Upsilon'}}
    } \nonumber
  \end{align}
  \begin{enumerate}
  \item $\Gamma \subseteq{} \Gamma' \wedge \psi' \Rightarrow \psi$
  \item $\Upsilon' \subseteq{} \Upsilon \wedge \phi \Rightarrow \phi'$
  \end{enumerate}

\item collective loop rule
  \begin{align}
    \frac{
    \cocond{\mymath{inv} \wedge{} c \wedge{} \bigwedge{\Gamma}}~C~
    \cocond{\mymath{inv} \wedge{} \bigwedge{\Upsilon}}
    }{
    \cocond{\mymath{inv} \wedge{} \bigwedge{\Gamma{}}}~ \texttt{while(}c\texttt{)}
    \{inv\} C ~\cocond{\neg{}c \wedge{} \mymath{inv} \wedge{} \bigwedge{\Upsilon{}}}
    } \nonumber
  \end{align}
  \begin{itemize}
  \item $\mymath{\forall{a}.\, guarantee(\Upsilon{}, a), a \in \Gamma}$
  \end{itemize}  

\item symbolic execution rule
  \begin{align}
    \frac{
    \cocond{\psi{} \wedge{} \bigwedge{\Gamma}}~
    \overrightarrow{C} := \overrightarrow{C_0\texttt{;}C_1}~
    ,\,\,
    \cocond{\psi{} \wedge{} \bigwedge{\Gamma}}~
    C_0\texttt{;}C_1~
    \cocond{\phi{} \wedge{} \bigwedge{\Upsilon}}
    }{
    \cocond{\psi{} \wedge{} \bigwedge{\Gamma}}~
    C~
    \cocond{\phi{} \wedge{} \bigwedge{\Upsilon}}
    } \nonumber 
  \end{align}
  \begin{itemize}
  \item
    $\cocond{\psi{} \wedge{} \bigwedge{\Gamma}}~\overrightarrow{C} :=
    \overrightarrow{C_0\texttt{;}C_1}$ means that if starting from a
    pre-state of $C$ where
    $\cocond{\psi{} \wedge{} \bigwedge{\Gamma}}$ holds and there is no
    unreceived message in any channel, for any execution $\pi$ of $C$ there
    exists an execution $\pi'$ of $C_0\texttt{;}C_1$ such that $\pi =
    \pi'$, then we have
    \begin{center}
      $\cocond{\psi{} \wedge{} \bigwedge{\Gamma}}~
      C_0\texttt{;}C_1~
      \cocond{\phi{} \wedge{} \bigwedge{\Upsilon}}$ if and only if
      $    \cocond{\psi{} \wedge{} \bigwedge{\Gamma}}~
      C~
      \cocond{\phi{} \wedge{} \bigwedge{\Upsilon}}$.
    \end{center}
  \end{itemize}
\end{enumerate}

\begin{lema}
  \begin{align}
    \frac{
    \cocond{\psi' \wedge{}
    \Gamma{}}~S\texttt{;}C~\cocond{\phi' \wedge{} \Upsilon}
    }{
    \{P\} ~S~ \{Q\},\,\, \cocond{\psi \wedge{}
    \Gamma{}}~C~\cocond{\phi \wedge{} \Upsilon}
    } \nonumber
  \end{align}
\end{lema}

\subsection{Proof Examples}
\subsubsection{1.}
\begin{itemize}
\item \textcolor{blue}{$\cocond{\psi}$} \texttt{gather(root); bcast(root)}
  \textcolor{blue}{$\cocond{\phi ~\wedge{}~ absent(exit(\PID), enter(\PID),
    enter(\texttt{root}))}$}  \textcolor{red}{(seq 1, 2)}
  \begin{enumerate}
  \item \textcolor{blue}{$\cocond{\psi \wedge{} \forall{p}.\, absent(send(\PID, p), exit(\PID),
      exit(\texttt{root}))}$}\\ \texttt{gather(root)} \\\textcolor{blue}{$\cocond{Q}$}
    \textcolor{red}{(conseq)}
    \begin{itemize}
    \item \textcolor{blue}{$\cocond{\psi \wedge{} absent(send(\PID, \texttt{root}), exit(\PID),
        exit(\texttt{root}))}$}\\ \texttt{gather(root)} \\\textcolor{blue}{$\cocond{Q
        \wedge{} absent(exit(\texttt{root}), enter(\texttt{root}), exit(\texttt{PID}))}$}
    \end{itemize}
  \item \textcolor{blue}{$\cocond{Q}$} \\\texttt{bcast(root)}\\
    \textcolor{blue}{$\cocond{\phi \wedge{} absent(exit(\PID), enter(\PID),
      enter(\texttt{root}))}$} \textcolor{red}{(conseq)}
    \begin{itemize}
    \item \textcolor{blue}{$\cocond{Q}$}\\ \texttt{bcast(root)} \\\textcolor{blue}{$\lco{}\phi
      ~\wedge{}~ absent(exit(\PID), enter(\PID),
      enter(\texttt{root}))  ~\wedge{}$ \\
      $absent(send(\PID, \texttt{root}), enter(\PID),
      enter(\texttt{root})) \rco{}
      $}
    \end{itemize}
  \end{enumerate}
\end{itemize}

\subsubsection{2.}
\textcolor{blue}{$\cocond{\psi ~\wedge{}~ absent(send(\PID, \texttt{root}), exit(\PID),
  exit(\texttt{root}))}$} \\
\texttt{bcast(root); gather(root)} \\
\textcolor{blue}{$\lco{}\phi ~\wedge{}~ absent(send(\PID, \texttt{root}), enter(\PID),
enter(\texttt{root})) \wedge{}$ $absent(exit(\texttt{root}),
enter(\texttt{root}), exit(\PID))\rco{}$}  \textcolor{red}{(seq)}
\begin{enumerate}
\item
  \textcolor{blue}{
  $\cocond{\psi}$} \texttt{bcast(root)} \textcolor{blue}{$\cocond{Q \wedge{} absent(send(\PID, \texttt{root}), enter(\PID),
    enter(\texttt{root}))}$} \textcolor{red}{(conseq)}
  \begin{itemize}
  \item \textcolor{blue}{$\cocond{\psi}$} \\
    \texttt{bcast(root)}  \\
    \textcolor{blue}{$\lco{}Q \wedge{} absent(send(\PID, \texttt{root}), enter(\PID),
    enter(\texttt{root})) \wedge{}$  \\
    $absent(exit(\PID), enter(\PID),
    enter(\texttt{root})) \rco{}$}
  \end{itemize}
\item \textcolor{blue}{$\cocond{Q \wedge{} absent(send(\PID, \texttt{root}),
    enter(\PID)}$} \\ \texttt{gather(root)} \\
  \textcolor{blue}{$\cocond{\phi{} \wedge{} absent(exit(\texttt{root}), enter(\texttt{root}), exit(\PID))}$}  
\end{enumerate}


\subsubsection{3.}

\textcolor{blue}{
  $\mymath{\cocond{\psi{} \wedge absent(send(\PID{}, \texttt{root}), exit(\PID), exit(\texttt{root}))}}$
}\\
\texttt{gather(root); exchange(left, right)} \\
\textcolor{blue}{
  $\lco{}$
  $\mymath{\phi{} \wedge{} absent(exit(\PID{}), enter(\PID), exit(\texttt{left})) \wedge}$ $\mymath{absent(exit(\PID{}), enter(\PID), exit(\texttt{right})) \rco{}}$
} \textcolor{red}{(seq 1, 2)}
\begin{enumerate}
\item 
\textcolor{blue}{
  $\mymath{\cocond{\psi{} \wedge{} \cocond{absent(send(\PID{}, \texttt{root}), exit(\PID), exit(\texttt{root}))}}}$
}\\
\texttt{gather(root)} \\
\textcolor{blue}{
  $\cocond{Q}$
} \textcolor{red}{(conseq)}
\begin{itemize}
\item ...
\end{itemize}

\item 
  \textcolor{blue}{$\cocond{Q}$} \\
  \texttt{exchange(left, right)} \\
  \textcolor{blue}{
  $\lco{}$
  $\mymath{\phi{} \wedge{} absent(exit(\PID{}), enter(\PID),
    exit(\texttt{left})) \wedge}$ $\mymath{absent(exit(\PID{}), enter(\PID),
    exit(\texttt{right})) \wedge{}}$ \\
  $\mymath{absent(send(\PID{}, \texttt{root}), enter(\PID{}), enter(\texttt{root})) \rco{}}$
} \textcolor{red}{(conseq)}
\begin{itemize}
\item   \textcolor{blue}{$\cocond{Q}$} \\
  \texttt{exchange(left, right)} \\
  \textcolor{blue}{
  $\lco{}$
  $\mymath{\phi{} \wedge{} absent(exit(\PID{}), enter(\PID),
    exit(\texttt{left})) \wedge}$ $\mymath{absent(exit(\PID{}), enter(\PID),
    exit(\texttt{right})) \wedge{}}$ \\
  $\mymath{\forall{p}.\, (p \not=\texttt{left} \wedge p \not= \texttt{right})
    \Rightarrow absent(send(\PID{}, p), enter(\PID{}), exit(\PID{})) \rco{}}$
}
\end{itemize}
\end{enumerate}


$\cocond{\psi \wedge a}$ $C_0$\texttt{;}$C_1$ $\cocond{\phi}$  \\
choose which ? \\
\begin{itemize}
\item 
  \begin{itemize}
  \item  $\cocond{\psi \wedge a}$ $C_0$ $\cocond{Q}$
  \item  $\cocond{Q}$ $C_1$ $\cocond{\psi \wedge b}$ \ \ \ \ \ \ \ \ \
    \ ($guarantee(b, a)$)
  \end{itemize}
\item 
  \begin{itemize}
  \item  $\cocond{\psi}$ $C_0$ $\cocond{Q}$
  \item  $\cocond{Q \wedge{} a}$ $C_1$ $\cocond{\psi}$
  \end{itemize}
\end{itemize}


Proof symbolic execution (with collective states) $\leftrightarrow$
triple:

$\cocond{\psi{} \wedge{} \Gamma}~ C_0; C_1 ~\cocond{\phi{} \wedge{}
  \Upsilon}$ 
\begin{enumerate}
\item $\cocond{\psi{}}~ barrier; C_0; barrier; C_1; barrier
  ~\cocond{\phi{}}$
  \begin{enumerate}
  \item collective states $\leftrightarrow$  pre-state, post-state
    with barriers
  \end{enumerate}
\item $\cocond{\Gamma}~ C_0; C_1 ~\cocond{\Upsilon}$ 
  \begin{enumerate}
  \item fully explore all possible behaviors can check for temporal assertions
  \end{enumerate}
\end{enumerate}