\subsection{On The Fly Model Checking with Collective States} \label{sec:minimp:system:onthefly}

In \S\ref{sec:minimp:system:symExe} and
\S\ref{sec:minimp:system:symExeModular}, we described the model
checking algorithms $\mcalgo$ and $\mcalgo^{\Delta}$ with the
assumption that the full state space graphs have been constructed.
However, in reality, many model checkers do not construct the full
state space before searching.  Instead, they construct the graph along
with the searching algorithm.  This is called the \emph{on the fly}
model checking.

There are two reasons why on the fly model checking usually is more
efficient than searching in a constructed full state space.  First,
the user normally prefers a model checker to stop immediately once it
finds an error.  Second, with the state-of-art reduction techniques,
such as \emph{partial order reduction} (POR), a model checker only
needs to explore a sub-graph of the full state space graph at most of
the time.  In both cases above, it is ideal to avoid the construction
of the full state space graph.

During on the fly model checking, a model checker starts from an
initial state and performs \emph{depth first search} (or \emph{breath
  first search}) along with the transitions.  For every newly explored
\emph{current state}, properties of the state will be checked and
transitions emanating from the state will be computed.  The current
state then can be saved as a seen state.

In order to realize a $\mcalgo^{\Delta}$ based on the fly model
checking algorithm, the notion of collective states must be
incorporated into the algorithm.  The construction of a collective
state depends on a path.  So the model checker may have to keep track
of the relevant informations along with the state exploration.  In
addition, whether a path contains an error or is infeasible can depend
on the contract that is evaluated on the corresponding collective
state.  Therefore, a collective state shall be constructed as early as
possible.


We introduce a special data structure, \emph{collate}, for aggregating
informations, on which a collective state depends, along with state
exploration.  By saving collates in states, a collate is naturally
associated with the proper path.  Once a collate collects all
necessary information for a collective state, the collective state
will be constructed immediately.  The structure of a collate is showed
in Fig.\ \ref{fig:collate}.

A collate corresponds to a unique collective pre- or post-state of a
procedure call.  A collate is labeled by an identifier \textsf{id} of
a procedure and a \textsf{tag} indicating \textsf{pre} or
\textsf{post}.  A collate for $n$ processes has $n$ slots, each of
which is for holding a process state of a specific process.  In
addition, a collate maintains a copy of message channels of a state.
The message channels will keep being updated since being created until
the collate becomes \emph{complete}.  A collate is complete if all of
its slots are filled.

When a process enters (or exits) a call to a procedure with a
contract, it is either the case that this process is the first one
that enters (or exits) the instance of the call or it is not the first
one.  For the former case, a collate will be created to start to
collect information of a collective state of the called procedure.
For the latter case, a collate associated with the collective state
must have been created.  The process will update the existing collate.

On a path, a process can run ahead to execute several procedure calls
without another process getting executed.  To deal with such cases, we
use a \emph{collate queue} to maintain collates during the state
exploration.  The head of the queue stores the earliest enqueued
collate.

\begin{figure}
  \begin{center}
    \begin{tabular}{| l | c | r |}
      \hline
      \textsf{id} & \multicolumn{2}{|c|}{\textsf{tag: pre/post}} \\
    \hline
    $\textsf{slot}_0$ & \ldots{} & $\textsf{slot}_{n-1}$ \\
    \hline
    \multicolumn{3}{|c|}{\textsf{channels}} \\
    \hline
  \end{tabular}
\end{center}
\caption{The structure of a collate type object for $n$ processes.
  \textsf{id} denotes the identifier of the associated procedure,
  \textsf{tag} indicates whether the collate serves for a collective
  pre- or post-state.  Every $\textsf{slot}_i$ will hold a process
  state of a process $i$.  The \textsf{channels} stores a copy of
  message channels, which keeps being updated.}
  \label{fig:collate}
\end{figure}

We now describe the algorithm of collate queue management.
Let $f$ be a procedure annotated with a contract.

\begin{itemize}
\item When a process $p$ reaches (resp.\ leaves) a call to $f$,
  iterating the collate queue (from the head).  The iteration
  
  \begin{enumerate}
  \item stops at a collate $c$ where the $\textsf{slot}_p$ is empty,
    or,
    
  \item creates and enqueues a new collate $c$, if no existing
    collate in the queue has its $\textsf{slot}_p$ empty.  For $c$,
    \textsf{id} is initialized to $f$, the \textsf{tag} is initialized
    to \textsf{pre} (resp.\ \textsf{post}) and the \textsf{channels}
    is initialized by copying the message channels from the current
    state.
  \end{enumerate}
  Then for $c$, if its \textsf{id} of $c$ mismatches $f$, report an
  error for mismatch of calls to a collective style procedure.
  Finally, process $p$ saves a copy of its own process state in the
  current state to $\textsf{slot}_p$ of $c$.  Such a copy is called a
  \emph{snapshot} of $p$ at the current state.

  
\item When a process $p$ executes a \texttt{\myactsend{$v$}{$q$}}
  (resp.\ \texttt{\myactrecv{$v$}{$q$}}) action, the same action will
  be performed to every collate $c$ in the collate queue that
  $\textsf{slot}_p$ of $c$ is still empty.

\item Once a collate is complete.  It is dequeued from the collate
  queue.  A collective state can be constructed from the contents of a
  complete collate.
\end{itemize}
This algorithm guarantees that the collective states are constructed
as early as possible during the state exploration.

\begin{exmp}
  Figure \ref{fig:collates:in:queue} shows the collates, which are
  associated with the collective pre- and post-states of $C_0$ of the
  MiniMP code $C_0C_1$ given in Example
  \ref{exmp:collective:state}.  Along the on-the-fly exploration of
  the execution given in Fig.\
  \ref{fig:minimp:example:collective:state} (below), process 0 first
  creates a collate for the collective pre-state of $C_0$ after state
  0, the rest of the processes follow up and complete this collate
  after state 2.  The completed collate is dequeued.  Process 0 then
  runs ahead and creates a collate for the collective post-state of
  $C_0$ after state 4.  The rest of the processes continue to modified
  the message channels on the collate until they have copied their
  snapshots to the collate respectively after state 6 and 7.
\end{exmp}

\begin{figure}
  \begin{center}
    \includegraphics[scale=.5]{collates}
  \end{center}
  \caption{Collates in states along the on-the-fly exploration of the
    execution showed in Fig.\
    \ref{fig:minimp:example:collective:state}.}
  \label{fig:collates:in:queue}
\end{figure}

\subsection{Absence Assertion Verification and Partial Order
  Reduction} \label{sec:minimp:system:por} \textbf{Absence Assertion
  Verification.}  With collective states, state-requirements and
guarantees of procedure calls can be checked on these states.  But
path-requirements and -guarantees of procedure calls need to be
checked in a different way since their correctness depends on not a
single state but a path.

In this subsection, we present a basic algorithm for checking the
correctness of path-requirements and -guarantees.  The algorithm is a
straightforward realization for detecting absence assertion violations
defined in Fig.\ \ref{fig:minimp:mono:error} and Fig.\
\ref{fig:modular:verify:error}.

Given a collate queue.  Let $c_i$ be a collate in the $i$-th position
of the queue.  $c_0$ is the head of the queue.  Let $\textsf{pos}(p)$
be the largest position of a collate in the queue where
$\textsf{slot}_p$ is non-empty.  It implies that $\textsf{slot}_p$ of
$c_{\textsf{pos}(p) + 1}$ must be empty, if $c_{\textsf{pos}(p) + 1}$
exists in the queue.  Let $\textsf{arrived}(c)$ denote the process set
$P$ such that $p \in P$ iff $\textsf{slot}_p$ in $c$ is non-empty.


Without breaking the properties provided by the collate queue
management algorithm given in \S\ref{sec:minimp:system:onthefly}, we
postpone the dequeue operation on a completed collate $c$, if $c$ is
associated with a collective pre-state, until the completion of the
collate that is associated with the corresponding collective
post-state.  Remark that the construction of collective states
from completed collates is never postponed.

A procedure annotated with a contract can be said a \emph{contracted}
procedure.  Since definitions of contracted procedures have been
abstracted away.  No procedure call can be reached in between a pair
of enter and exit of a contracted procedure in an execution.
Consequently, if a collate $c_i$ in a queue is associated with a
collective pre-state, the collate $c_{i+1}$, if it exists, in the
queue must be associated with the corresponding collective post-state.

Considering the on the fly
$\mcalgo^{\Delta}(\model,
\frac{\textsf{Tri}}{\mycosubtriple{g}{\psi_g}{\phi_g}{\textsf{body}(g)}},
n)$ algorithm.  Let $G$ be the searching state space graph.  Let $f,
h$ be some procedures such that 
\[
  \mycosubtriple{f}{\psi_f}{\phi_f}{\textsf{body}(f)},\,
  \mycosubtriple{h}{\psi_h}{\phi_h}{\textsf{body}(h)}
  \in \textsf{Tri}.
\]
Let $\pi$ be the execution that is currently being explored and
$\omega$ the current state.  For brevity, we define the following
shortcuts
\begin{align}
  \textsf{arrived}(c - c') \colon{}&
  \textsf{arrived}(c)\BSL{}\textsf{arrived}(c') \nonumber \\
  \textsf{arrived}( - c) \colon{}&
                                                               \nprocs{n}\BSL{}\textsf{arrived}(c') \nonumber 
\end{align}  
The free of path-requirement or -guarantee violation is checked by the
following conditions.

\begin{itemize}
\item If exists $t \in \emana_G(\omega)$ such that $\myproc(t) = q$
  and $\myact(t) = \myactrecv{$v$}{$p$}$, and
  
  \begin{enumerate}
  \item $\mayInterfere_G(\omega, p, q)$, and the collate $c$ for the
    post-state of $g$ exists in the queue in $\omega$, check
    \begin{align}
      &\forall{p \in
        \textsf{arrived}(c)}.\,
        \exists{r \in
      \textsf{arrived}(-c)}. \nonumber \\
      &
      \texttt{\acslgamma{$p$}{$q$}{$r$}} \in_\pi \Gamma_g, \nonumber
    \end{align}
    and
  \item $\mayInterfere^{\Delta}_G(\omega, p, q)$, then for every
    collate $c_i$ in the queue in $\omega$ such that
    $i > \textsf{pos}(q)$, $\textsf{id} = f$ and
    $\textsf{tag} = \textsf{pre}$, check
    \begin{align}
      & \forall{p \in
        \textsf{arrived}(c_i-c_{i+1})}.\,
        \exists{r \in \textsf{arrived}(-c_i)}. \nonumber\\
      & \texttt{\acslguarantee{$p$}{$q$}{$r$}} \in_\pi \Upsilon_f \nonumber
    \end{align}

  \end{enumerate}

\item If exists $t \in \emana_G(\omega)$ such that $\myproc(t) = p$
  and $\myact(t) = \myactsend{$v$}{$q$}$ for some $v$, 

  \begin{enumerate}
  \item for the first collate $c_0$ (if exists) in the queue in
    $\omega$, check
    \begin{align}
      &\forall{r \in
      \textsf{arrived}(-c_0)}. \nonumber \\
      &
      \texttt{\acslguarantee{$p$}{$q$}{$r$}} \not\in_\pi \Upsilon_g, \nonumber
    \end{align}
    and
    
  \item for every $c_i$ in the queue in $\omega$ such that
    $i \leq \textsf{pos}(p)$, $\textsf{id} = f$ and
    $\textsf{tag} = \textsf{pre}$, check
    \begin{align}
      &\forall{q \in        
        \textsf{arrived}(c_i-c_{i+1}),\, r  \in \textsf{arrived}(-c_{i+1})}. \nonumber \\
      &\texttt{\acslgamma{$p$}{$q$}{$r$}} \not\in_\pi \Gamma_f\nonumber
    \end{align}
  \end{enumerate}
  
\item if $\myenter^{\textsf{body}(f)}_{p, \pi} \in \emana_G(\omega)$
  and exists collate $c_i$ in the queue in $\omega$ such that
  $i = \textsf{pos}(p) + 1$, 
  
  \begin{enumerate}
  \item for every collate $c_j$ in the queue in $\omega$ such that
    $j + 1 < i$, $\textsf{id} = h$ and $\textsf{tag} = \textsf{pre}$,
    check
    \begin{align}
      & \forall{q \in \textsf{arrived}(c_j-c_{j+1}),\,
        r \in \textsf{arrived}(-c_{j+1})}.
        \nonumber \\
      &  \texttt{\acslgamma{$p$}{$q$}{$r$}{}} \in_\pi \Gamma_h\Rightarrow{} \nonumber
      \\
      & (\exists{r' \in \textsf{arrived}(-c_i)}. \nonumber \\
      & \texttt{\acslguarantee{$p$}{$q$}{$r'$}} \in_\pi \Upsilon_f), \nonumber
    \end{align}
    and
    
  \item $\forall{q \in \nprocs{n},\, r \in
        \textsf{arrived}(-c_0)}.$
    \begin{align}
      &\texttt{\acslguarantee{$p$}{$q$}{$r$}} \in_\pi \Upsilon_g
              \Rightarrow{}
        \nonumber \\
      & (\exists{r' \in \textsf{arrived}(-c_i)}.\,
        \nonumber \\ 
      &         \texttt{\acslguarantee{$p$}{$q$}{$r'$}} \in_\pi \Upsilon_f)
        \nonumber
    \end{align}
  \end{enumerate}

\item If $\myexit^{\textsf{body}(g)}_{p, \pi} \in \emana_G(\omega)$,
  let $c$ be the collate for  the post-state of $g$, check

  \begin{enumerate}
  \item $\forall{q \in
      \textsf{arrived}(-c_0)}.$
    \[
                  \texttt{\acslwaitsfor{$p$}{$q$}} \not\in_\pi
      \Upsilon_f 
    \]
    
  \item for every collate $c_i$ in the queue in $\omega$ such that
    $\textsf{id} = f$ and $\textsf{tag} = \textsf{pre}$,
    \begin{align}
      &    \forall{q\in\textsf{arrived}(c_i-c_{i+1}),\,r \in \textsf{arrived}(-c_{i+1})}.
        \nonumber \\
      & \texttt{\acslgamma{$p$}{$q$}{$r$}} \in_\pi \Gamma_f \Rightarrow
        \nonumber \\
      &\exists{r' \in
        \textsf{arrived}(-c)}.\nonumber \\
      & \texttt{\acslgamma{$p$}{$q$}{$r'$}} \in_\pi \Gamma_g\nonumber
    \end{align}
  \end{enumerate}
  
\end{itemize}  


\textbf{Partial Order Reduction.}  The \emph{partial order reduction}
(POR) technique is one of the important reasons that the on the fly
model checking can be more efficient than searching a constructed
state space graph.  The basic idea of POR is to let a model checker
only search a sub-graph of the complete state space graph by ignoring
commutative executions.

\begin{exmp}
  Suppose there are two processes executing the statement \texttt{x =
    1;} from a pre-state $\omega$ of it.  Then there are two
  executions in the state space graph of \texttt{x =
    1;} with two processes.
  \begin{align}
   & \omega \xrightarrow[p_0]{\texttt{x = 1}} \omega_1
    \xrightarrow[p_1]{\texttt{x = 1}} \omega' \text{ and
    }\nonumber \\
 &  \omega \xrightarrow[p_1]{\texttt{x = 1}} \omega_2
    \xrightarrow[p_0]{\texttt{x = 1}} \omega' \nonumber
  \end{align}
  Let assume that the order of transitions in a path cannot affect the
  properties being verified.  A typical POR algorithm determines that
  one of the executions can be ignored.  The ignoring will be achieved
  by only exploring one of the transitions emanating from
  $\omega$. $\qed$
\end{exmp}

In general, a POR algorithm is to safely approximate 1) the dependency
relation among transitions; 2) the visibility of the transitions to
the checking properties.  
Briefly, a transition $\omega \xrightarrow[p_0]{a_0} \omega_0$ is
independent of a transition $\omega \xrightarrow[p_1]{a_1} \omega_1$
if both the following two paths are feasible:
$\omega \xrightarrow[p_0]{a_0} \omega_0 \xrightarrow[p_1]{a_1}
\omega_2$ and
$\omega \xrightarrow[p_1]{a_1} \omega_1 \xrightarrow[p_0]{a_0}
\omega_2$.  A transition is invisible if the execution of it has no
effect on any path predicate that express a checking property.

POR algorithms for message-passing concurrent systems have been
studied by many work\cite{Palmer:2007:SDD:1273647.1273657,
  10.1007/978-3-540-30579-8_27, vakkalanka2008dynamic,
  Siegel:2005:MWM:1065944.1065957}.  For a simple message passing
system such as MiniMP, a transition $t$ depends on another transition
$t'$ iff $t$ is labeled by a \texttt{recv} action, $t'$ is labeled by
a \texttt{send} action and both transitions operate on a same message.
For properties that are expressed as state predicates, no transition
is visible.

However, our contract system checks path-requirements and -guarantees,
which are expressed by path predicates.  To check path predicates, the
visibility of transitions must be taken into consideration.  Typical
POR algorithms determines that for a set of transitions emanating from
a state, if there is a transition labeled by a non-communication
action, only the transition needs to be explored.  However, such a POR
algorithm can cause the miss of absence assertion violations.  For
example, given a procedure $f$ and two processes $p$ and $q$, from a
state where both exiting $f$ by $p$ and entering $f$ by $q$ can be
emanated, only one of the transitions needs to be explored.  If the
model checker chooses the former one, it is fine.  But if the model
checker chooses the latter one, it misses an execution where process
$p$ exits $f$ before the entering of $f$ by $q$.  If $f$ is specified
by a path-guarantee
\[
  \texttt{\acslwaitsfor{$p$}{$q$}},
\]
a violation of this assertion can be missed.

As aforementioned, POR algorithm performs over-approximation.  A safe
over-approximation can be as simple as blindly assuming that any
transition is visible.  But this will cause that the model checker has
to explore the full state space.  Without loss of safety, we designed
the following algorithm for determine whether a transition is visible
with improved precision.

Let $g$ be the procedure that is being verified.  Let $f$ be a
contracted procedure called inside $g$.  Let $\Gamma_g$ and
$\Upsilon_g$ be path requirement and path guarantee of $g$,
respectively.  Ditto for $\Gamma_f$ and $\Upsilon_f$.  Let $\pi$ be
the execution that is currently being explored by a model checker.

\begin{itemize}
\item $\myenter^{\textsf{body}(g)}_{p,\pi}$ is visible, if the event
  \texttt{enter($p$)} appears in any absence assertion in $\Gamma_g$.

\item $\myexit^{\textsf{body}(g)}_{p, \pi}$ is visible unless all
  other processes than $p$ have exited $g$.

\item $\myenter^{\textsf{body}(f)}_{p, \pi}$ is visible unless all
  other processes than $p$ have copied their snapshots to the collate
  $c$ associated with the collective pre-state of $f$ at state
  $\mysrc(\myenter^{\textsf{body}(f)}_{p, \pi})$.

\item $\myexit^{\textsf{body}(f)}_{p, \pi}$ is visible, if the event
  \texttt{\acslexit{($p$)}} appears in any absence assertion in
  $\Gamma_f$.

\item A transition $t$ such that $\myproc(t) = p$ and
  $\myact(t) = \myactsend{$v$}{$q$}$ is visible unless that for every
  collate $c$ tagged by \textsf{post} in the queue in $\mysrc(t)$,
  $p \in \textsf{arrived}(c) \Rightarrow{}$
  $\forall{q \in \nprocs{n}}.\,\textsf{arrived}(c)$.
\end{itemize}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsection{Infinite Reachable
  States} \label{sec:minimp:system:limitation}

Finally, we talk about one of the well-known limitations of the model
checking and symbolic execution approach: the searching state space
must have a finite number of states.

Recall that variables may hold unconstrained symbolic expressions, the
validity of branch and loop conditions may not always can be
determined.  Thus, a model checker may infinitely discover new states
for a loop or recursions.

To keep the searching state space stay finite, one solution is to add
bounds on some of the symbols that are involved in the branch and loop
conditions.  In our contract system, symbols are introduced by the
\myactrefresh{} actions and are constrained by the procedure
contracts.  Hence one can add bounds to symbols via strengthening the
procedure contracts.  The drawback of this solution is that the
contracts may be too strong to be general.

Summarizing the behavior of a loop using a loop invariant can be
another solution.  A loop invariant can be seen as a specification of
a loop.  Loop invariants can be generated automatically during the
symbolic execution \cite{Kauer:2010:MII:1860141.1860452,
  Sankaranarayanan04non-linearloop,
  McMillan:2010:LAP:2144310.2144323}, or annotated by the user
\cite{Hentschel2018}.