<commit_before>\section{Orphaned Receive}

%% rename the pattern as orphaned receive. This section presents the pattern match algorithm and validation for orphaned receive.

\examplefigone

A deadlock may occur when the runtime matches a wildcard receive with the send needed by a deterministic receive. For instance, in \figref{fig:deadlock1}, a deadlock may occur if the receive $\mathit{r_{0}}$ is matched with the send $\mathit{s_{1}}$ and there is no way to match the receive $\mathit{r_{1}}$ with the send $\mathit{s_{2}}$. This CTP shows an instance of the orphaned receive pattern defined in \defref{def:mismatch}.

\begin{definition}
A orphaned receive pattern is a pair $(\mathit{r_w}, \mathit{r_c})$ where, 
\begin{compactenum}
\item $\mathit{r_w}$ is a wildcard receive and $\mathit{r_c}$ is a deterministic receive that follows $\mathit{r_w}$ on an identical process $\mathit{p}$;
\item at least two sends from different source endpoints other than $\mathit{p}$ may potentially match $\mathit{r_w}$; and
\item among these matched sends, at least one send matches $\mathit{r_c}$. 
\end{compactenum}
\label{def:mismatch}
\end{definition}

For simplicity, only the deterministic receive is stored in a set to represent an instance of the orphaned receive pattern. For example, the CTP in \figref{fig:deadlock1} has a instance of the orphaned receive pattern $(r_1)$.

\subsection{Pattern Match for Orphaned Receive}

\begin{algorithm}
\caption{Finding Orphaned Receive}\label{algo:mismatch}
\begin{algorithmic}[1]
%\Require $\mathit{ctp}$, a single-path MPI program
%\Require $\mathit{M}(\mathtt{r_c}) = \{\mathtt{s_l}\mid(\mathtt{s_l},\mathtt{r_c})\in\mathit{M}\}$, a set of potentially matched sends for $\mathtt{r_c}$
%\State $\mathit{PT}$, a set of mismatched send-receive pattern instances
%\State $\mathit{R}(p) = \{\mathtt{r_w}\mid(p,\mathtt{r_w})\in\mathit{R}\}$, a set of wildcard receives on process $p$
\State $\mathit{PT} \gets \emptyset$
\State $\mathit{R} \gets \emptyset$
\For{$(e_1, e_2, \dots, e_n) \in \mathit{ctp}$}
\For{$i \gets 1$ to $n$}
\If{$e_i$ is a wildcard receive}
\State $\mathit{R} = \mathit{R} \cup \{e_i\}$
\EndIf
\If{$e_i$ is a deterministic receive}
\For{$\mathit{r_w} \in \mathit{R}$}
\If{$\mathit{M}(e_i) \cap \mathit{M}(\mathit{r_w}) \neq \emptyset \wedge |\mathit{M}(\mathit{r_w})| > 1$}
\State $\mathit{PT} = \mathit{PT} \cup \{\{e_i\}\}$
\State \textbf{break}
\EndIf
\EndFor
\EndIf
\EndFor
\State $\mathit{R} \gets \emptyset$
\EndFor
%\EndProcedure
\end{algorithmic}
\end{algorithm}

\algoref{algo:mismatch} shows the steps of finding the orphaned receive pattern instances for \textit{ctp}. The algorithm is part of the function $\mathrm{PATTERNMATCH}$ in \algoref{algo:main}.  
The set $\mathit{PT}$ stores the matched pattern instances.
The set $\mathit{R}$ stores the witnessed wildcard receives on the process \textit{p} that is a list of operations $(e_1, e_2, \dots, e_n)$. 
Intuitively, this algorithm checks each pair of wildcard/deterministic receives on an identical process and inserts a new instance with the deterministic receive in $\mathit{PT}$ if the criteria in \defref{def:mismatch} is satisfied for this pair. 
The complexity of the algorithm is $O(\mathrm{N}^2)$, where $\mathrm{N}$ is the total number of operations in \textit{ctp}. 


%%add text for the following algorithm of validating orphaned receive pattern
\subsection{Validation for Orphaned Receive}

\begin{algorithm}
\caption{Validate Orphaned Receive}\label{algo:vorphaned}
\begin{algorithmic}[1]
%\Require $\mathit{M}(\mathtt{r_c}) = \{\mathtt{s_l}\mid(\mathtt{s_l},\mathtt{r_c})\in\mathit{M}\}$, a set of potentially matched sends for $\mathtt{r_c}$
%\State  $\mathit{ctp_s}$, a potential schedule detected by the Call {FeasibleCheck}{}{}
\If{\textproc{SAT}({\Call {Encode}{$\mathit{ctp}_s$, $\mathit{pt}$, $\mathit{M}$}})}
\State report deadlock and exit.
\EndIf
\end{algorithmic}
\end{algorithm}

The validation step in \algoref{algo:vorphaned} is much more complicated because it requires a higher cost SMT encoding for $\mathit{ctp_s}$ that is generated from a modification of the abstract machine in \figref{fig:machine}.
This modification executes a CTP just like the old machine, only it has a new $\mathit{ctp_s}$ in the state such that only the reached commands are included. 
The function $\mathrm{ENCODE}$ encodes $\mathit{ctp_s}$ into an SMT problem based on the rules in \cite{DBLP:conf/kbse/HuangMM13}. Further, a new rule is extended for the match pair encoding: for the receive $\mathit{r_c}$ in the pattern instance \textit{pt}, $\bigvee_{\mathit{r_i}\in\mathit{M}(\mathit{s_l})}(\mathit{s_l},\mathit{r_i})$ is encoded for any $\mathit{s_l}\in\mathit{M}(\mathit{r_c})$ in $\mathit{ctp_s}$. This rule ensures that no send in $\mathit{ctp_s}$ can match $\mathit{r_c}$. The function $\mathrm{SAT}$ is true if the encoding is satisfiable. The existence of a satisfying assignment of the encoding implies a real deadlock for \textit{pt}. 

\examplefigtwo

The existence of a orphaned receive pattern instance does not mean a deadlock occurs. For example, the CTP in \figref{fig:nodeadlock1} has an instance of the orphaned receive pattern $(r_1)$ that is detected by \algoref{algo:mismatch}. However, \algoref{algo:vorphaned} reports no real deadlock for this pattern instance because the wildcard receive $r_0$ can only match the send $s_2$ so the receive $r_1$ can be matched eventually.

%%Soundness proof for pattern match needs to be added. the following proof needs to be revised to show that the validation is sound and complete.
The soundness proof of the validation in \algoref{algo:vorphaned} is given in \lemmaref{lemma:mismatch}.

\begin{lemma}[Soundness for Orphaned Receive]
For any single-path MPI program, \textit{ctp}, a deadlock detected by \algoref{algo:vorphaned} is a real deadlock existing for a instance of the orphaned receive pattern, $\mathit{pt}$. 
\label{lemma:mismatch}
\end{lemma}
\begin{proof}
Proof by showing the existence of a real deadlock. Since \algoref{algo:vorphaned} detects a deadlock, the function $\mathrm{ENCODE}$ returns a satisfying assignment, say $\mathit{t}, $for $ctp_s$. Based on the encoding rules, $\mathit{t}$ assigns a sequential order over all the commands in $ctp_s$, matches each receive in $ctp_s$ with a send, and matches 
This assignment 

First, assume $(\mathit{ctp}^\prime,$ $\mathit{ctp}_s,$ $\mathit{N_s},$ $\mathit{N_r},$ $\mathit{P_r},$ $\mathit{P_b},$ $\mathit{R_{pt}}^\prime)$ is the machine state after applying the operational semantics in \figref{fig:machine} and no reduction commands can be further applied. Second, assume the schedule $\mathit{ctp}_s$ is input to the function $\mathrm{ENCODE}$ in \algoref{algo:main}. Since $\mathrm{ENCODE}$ returns a satisfying assignment, say $\mathit{t}$, it implies that $\mathit{t}$ is a sequential order of all the operations in $\mathit{ctp}_s$ that is executable by the runtime system. Also, for the process that the deterministic receive $\mathit{r_c}$ in $\mathit{pt}$ resides in, say $\mathit{p}$, $\mathit{t}$ satisfies that each send with the destination $\mathit{p}$ is matched with some receive in $\mathit{ctp}_s$. As such, no sends can match $\mathit{r_c}$ as the nearest-enclosing wait for $\mathit{r_c}$ is stored in $\mathit{ctp}^\prime$ according to the \emph{Wait (Rcvi) Command 2} in \figref{fig:machine}. Further, for any process other than $\mathit{p}$ in $\mathit{pt}$, the first operation is blocked in $\mathit{ctp}^\prime$ according to the operational semantics in \figref{fig:machine}. As such, $\mathit{ctp}^\prime$ deadlocks. Since $\mathit{ctp}_s$ is executable and $\mathit{ctp}^\prime$ deadlocks, the program \textit{ctp} may deadlock for the pattern instance $\mathit{pt}$ in program execution. 
\end{proof}

The validation step can also be removed so that the deadlock detection for the orphaned receive pattern is much faster. If so, the soundness is not guaranteed. 

%%zero buffer for orphaned receive

\subsection{Zero Buffer Semantics for Orphaned Receive}<commit_msg>proofs for two patterns<commit_after>\section{Orphaned Receive}

%% rename the pattern as orphaned receive. This section presents the pattern match algorithm and validation for orphaned receive.

\examplefigone

A deadlock may occur when the runtime matches a wildcard receive with the send needed by a deterministic receive. For instance, in \figref{fig:deadlock1}, a deadlock may occur if the receive $\mathit{r_{0}}$ is matched with the send $\mathit{s_{1}}$ and there is no way to match the receive $\mathit{r_{1}}$ with the send $\mathit{s_{2}}$. This CTP shows an instance of the orphaned receive pattern defined in \defref{def:mismatch}.

\begin{definition}
A orphaned receive pattern is a pair $(\mathit{r_w}, \mathit{r_c})$ where, 
\begin{compactenum}
\item $\mathit{r_w}$ is a wildcard receive and $\mathit{r_c}$ is a deterministic receive that follows $\mathit{r_w}$ on an identical process $\mathit{p}$;
\item at least two sends from different source endpoints other than $\mathit{p}$ may potentially match $\mathit{r_w}$; and
\item among these matched sends, at least one send matches $\mathit{r_c}$. 
\end{compactenum}
\label{def:mismatch}
\end{definition}

For simplicity, only the deterministic receive is stored in a set to represent an instance of the orphaned receive pattern. For example, the CTP in \figref{fig:deadlock1} has a instance of the orphaned receive pattern $(r_1)$.

\subsection{Pattern Match for Orphaned Receive}

\begin{algorithm}
\caption{Finding Orphaned Receive}\label{algo:mismatch}
\begin{algorithmic}[1]
%\Require $\mathit{ctp}$, a single-path MPI program
%\Require $\mathit{M}(\mathtt{r_c}) = \{\mathtt{s_l}\mid(\mathtt{s_l},\mathtt{r_c})\in\mathit{M}\}$, a set of potentially matched sends for $\mathtt{r_c}$
%\State $\mathit{PT}$, a set of mismatched send-receive pattern instances
%\State $\mathit{R}(p) = \{\mathtt{r_w}\mid(p,\mathtt{r_w})\in\mathit{R}\}$, a set of wildcard receives on process $p$
\State $\mathit{PT} \gets \emptyset$
\State $\mathit{R} \gets \emptyset$
\For{$(e_1, e_2, \dots, e_n) \in \mathit{ctp}$}
\For{$i \gets 1$ to $n$}
\If{$e_i$ is a wildcard receive}
\State $\mathit{R} = \mathit{R} \cup \{e_i\}$
\EndIf
\If{$e_i$ is a deterministic receive}
\For{$\mathit{r_w} \in \mathit{R}$}
\If{$\mathit{M}(e_i) \cap \mathit{M}(\mathit{r_w}) \neq \emptyset \wedge |\mathit{M}(\mathit{r_w})| > 1$}
\State $\mathit{PT} = \mathit{PT} \cup \{\{e_i\}\}$
\State \textbf{break}
\EndIf
\EndFor
\EndIf
\EndFor
\State $\mathit{R} \gets \emptyset$
\EndFor
%\EndProcedure
\end{algorithmic}
\end{algorithm}

\algoref{algo:mismatch} shows the steps of finding the orphaned receive pattern instances for \textit{ctp}. The algorithm is part of the function $\mathrm{PATTERNMATCH}$ in \algoref{algo:main}.  
The set $\mathit{PT}$ stores the matched pattern instances.
The set $\mathit{R}$ stores the witnessed wildcard receives on the process \textit{p} that is a list of operations $(e_1, e_2, \dots, e_n)$. 
Intuitively, this algorithm checks each pair of wildcard/deterministic receives on an identical process and inserts a new instance with the deterministic receive in $\mathit{PT}$ if the criteria in \defref{def:mismatch} is satisfied for this pair. 
The complexity of the algorithm is $O(\mathrm{N}^2)$, where $\mathrm{N}$ is the total number of operations in \textit{ctp}. 


%%add text for the following algorithm of validating orphaned receive pattern
\subsection{Validation for Orphaned Receive}

\begin{algorithm}
\caption{Validate Orphaned Receive}\label{algo:vorphaned}
\begin{algorithmic}[1]
%\Require $\mathit{M}(\mathtt{r_c}) = \{\mathtt{s_l}\mid(\mathtt{s_l},\mathtt{r_c})\in\mathit{M}\}$, a set of potentially matched sends for $\mathtt{r_c}$
%\State  $\mathit{ctp_s}$, a potential schedule detected by the Call {FeasibleCheck}{}{}
\If{\textproc{SAT}({\Call {Encode}{$\mathit{ctp}_s$, $\mathit{pt}$, $\mathit{M}$}})}
\State report deadlock and exit.
\EndIf
\end{algorithmic}
\end{algorithm}

The validation step in \algoref{algo:vorphaned} is much more complicated because it requires a higher cost SMT encoding for $\mathit{ctp_s}$ that is generated from a modification of the abstract machine in \figref{fig:machine}.
This modification executes a CTP just like the old machine, only it has a new $\mathit{ctp_s}$ in the state such that only the reached commands are included. 
The function $\mathrm{ENCODE}$ encodes $\mathit{ctp_s}$ into an SMT problem based on the rules in \cite{DBLP:conf/kbse/HuangMM13}. Further, a new rule is extended for the match pair encoding: for the receive $\mathit{r_c}$ in the pattern instance \textit{pt}, $\bigvee_{\mathit{r_i}\in\mathit{M}(\mathit{s_l})}(\mathit{s_l},\mathit{r_i})$ is encoded for any send $\mathit{s_l}\in\mathit{M}(\mathit{r_c})$ in $\mathit{ctp_s}$. This rule ensures that no send in $\mathit{ctp_s}$ can match $\mathit{r_c}$. The function $\mathrm{SAT}$ is true if the encoding is satisfiable. The existence of a satisfying assignment of the encoding implies a real deadlock for \textit{pt}. 

\examplefigtwo

The existence of a orphaned receive pattern instance does not mean a deadlock occurs. For example, the CTP in \figref{fig:nodeadlock1} has an instance of the orphaned receive pattern $(r_1)$ that is detected by \algoref{algo:mismatch}. However, \algoref{algo:vorphaned} reports no real deadlock for this pattern instance because the wildcard receive $r_0$ can only match the send $s_2$ so the receive $r_1$ can be matched eventually.

%%Soundness proof for pattern match needs to be added. the following proof needs to be revised to show that the validation is sound and complete.
The soundness proof of the validation in \algoref{algo:vorphaned} is given in \lemmaref{lemma:mismatch}.

\begin{lemma}[Soundness for Orphaned Receive]
For any single-path MPI program, \textit{ctp}, a deadlock detected by \algoref{algo:vorphaned} is a real deadlock for a instance of the orphaned receive pattern, $\mathit{pt}$. 
\label{lemma:mismatch}
\end{lemma}
\begin{proof}
Proof by showing the existence of a real deadlock. Since \algoref{algo:vorphaned} detects a deadlock, the function $\mathrm{ENCODE}$ returns a satisfying assignment, say $\mathit{t}, $for $ctp_s$.  Assume the receive $r_c \in pt$. Based on the encoding rules, $\mathit{t}$ assigns a sequential order over all the commands in $ctp_s$, matches each receive in $ctp_s$ with a send, and matches each send $\mathit{s_l}\in\mathit{M}(\mathit{r_c})$ in $\mathit{ctp_s}$ with a receive other than $r_c$. Therefore, $\mathit{t}$ implies a schedule that is executable by the runtime which leads to a deadlock for $pt$.
%First, assume $(\mathit{ctp}^\prime,$ $\mathit{ctp}_s,$ $\mathit{N_s},$ $\mathit{N_r},$ $\mathit{P_r},$ $\mathit{P_b},$ $\mathit{R_{pt}}^\prime)$ is the machine state after applying the operational semantics in \figref{fig:machine} and no reduction commands can be further applied. Second, assume the schedule $\mathit{ctp}_s$ is input to the function $\mathrm{ENCODE}$ in \algoref{algo:main}. Since $\mathrm{ENCODE}$ returns a satisfying assignment, say $\mathit{t}$, it implies that $\mathit{t}$ is a sequential order of all the operations in $\mathit{ctp}_s$ that is executable by the runtime system. Also, for the process that the deterministic receive $\mathit{r_c}$ in $\mathit{pt}$ resides in, say $\mathit{p}$, $\mathit{t}$ satisfies that each send with the destination $\mathit{p}$ is matched with some receive in $\mathit{ctp}_s$. As such, no sends can match $\mathit{r_c}$ as the nearest-enclosing wait for $\mathit{r_c}$ is stored in $\mathit{ctp}^\prime$ according to the \emph{Wait (Rcvi) Command 2} in \figref{fig:machine}. Further, for any process other than $\mathit{p}$ in $\mathit{pt}$, the first operation is blocked in $\mathit{ctp}^\prime$ according to the operational semantics in \figref{fig:machine}. As such, $\mathit{ctp}^\prime$ deadlocks. Since $\mathit{ctp}_s$ is executable and $\mathit{ctp}^\prime$ deadlocks, the program \textit{ctp} may deadlock for the pattern instance $\mathit{pt}$ in program execution. 
\end{proof}

The SMT encoding used in the validation step for the orphaned receive pattern can be solved by a state-of-art SMT solver with a higher cost \cite{}. The general algorithm, however, can be modified to remove the validation for the orphaned receive pattern, which leads to a much faster deadlock detection. If so, the algorithm is not sound but is complete.

%%zero buffer for orphaned receive

\subsection{Zero Buffer Semantics for Orphaned Receive}
{'fraction_non_alphanumeric': 0.12653110480902674, 'fraction_numerical': 0.0028962770771737163, 'mean_word_length': 5.095623390952556, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 5, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1311124', 'n_tokens_mistral': 5312, 'n_tokens_neox': 4958, 'n_words': 2044}