% -*- Mode: LaTeX -*-

\section{Semantics of M-Barriers}
\label{sec:barrier}

\begin{myfig}{fig:mbar}{Semantics of M-barriers.}
\centering
$\begin{array}{lcl}
\multicolumn{3}{c}{\cbx{Expressions}} \\
\bbx{TE} & :: & \bx{Expression} \rightarrow \bx{Expression}\\[.1in]

\te{c}          & = & c,\hm \wconst \\
\te{x}          & = & x,\hm \wconst \\
\te{\tbx{mFetch}(x)} & = & \{\; y = \tbx{mFetch}(x); \\
& & \tbx{in}\;y,\hm \thnf{y} \;\} \\
\te{\tbx{mStore}(x,z)} & = & \{\; y = \tbx{mStore}(x,z); \\
& & \tbx{in}\;y,\hm \thnf{y} \;\} \\
\te{\ibx{PF}^{n}(x_{1},\ldots,x_{n})} & = &
\ibx{PF}^{n}(x_{1},\ldots,x_{n}),\hm \wconst \\
\te{\lambda x.\; E} & = & \lambda x.\; \te{E},\hm \wconst \\
\te{\tbx{case} \;(x, E_{1},\ldots,E_{n})} & = & 
\tbx{case} \;(x, \te{E_{1}}, \ldots, \te{E_{n}}) \\
\te{\tbx{ap}(f,x)} & = & \tbx{ap}(f,x) \\
\te{\{\;S\;\tbx{in}\;x\;\}} & = & \{\;S'\;\tbx{in}\;x,\hm s\;\} \\
\multicolumn{3}{l}{\bx{where}\hm S',s = \ts{S}} \\[.1in]
\multicolumn{3}{c}{\cbx{Statements}} \\
\ts{} & :: & \bx{Statement} \rightarrow \fn{List}{\bx{Statement}}\times\bx{Identifier}\\[.1in]
\ts{\epsilon} & = & (s=\wconst),\hm s \\
\ts{x = E} & = & (x,s = \te{E}),\hm s \\
\ts{S_{1};\ldots;S_{n}} & = & (S'_{1};\ldots;S'_{n}; s=s_{1}\;\tand\;\cdots\;\tand\; s_{n}),\hm s \\
\multicolumn{3}{l}{\bx{where}\hm S'_{i},s_{i} = \ts{S_{i}} \hm 1\leq{}i\leq{}n} \\
\ts{S_{1} \;\tbx{---}\; S_{2}} & = & (S'_{1}; \\ 
& & f = \lambda s.\{\;S'_{2}\;\tbx{in}\; y_{1},\ldots,y_{m},s_{2} \;\}; \\ 
& & y_{1},\ldots,y_{m},s'_{2} = \tbx{sap}(f,s_{1})),\hm s'_{2} \\
\multicolumn{3}{l}{\bx{where}\hm \begin{array}[t]{lcl}
S'_{i}, s_{i} & = & \ts{S} \hm 1\leq{}i\leq{}2 \\ 
y_{1},\ldots,y_{m} & = & \fn{BV}{S_{2}} \end{array}}
\end{array}$
\end{myfig}

In this section we describe the semantics of barriers by translating
them into ordinary block bindings. The idea is to systematically
construct a composite termination signal from all the side-effect
operations taking place within the pre-region of a barrier (including
its child regions) which would then be used to trigger the operations
present in the post-region of the barrier. The notion of signal
generation and composition may be understood by looking at the
translation of a simple parallel block as shown below.

\[\begin{array}[t]{l}
{\bf{}TE}\dlb\;\{\;x_{1}=E_{1}; \\
\hmm\;\;\;\cdots \\
\hmm\;\;\;x_{n}=E_{n}; \\
\hmm\;\;\tbx{in}\;x\;\}\;\drb
\end{array} \hm = \hm 
\begin{array}[t]{lcl}
\{\;x_{1},s_{1} & = & \te{E_{1}}; \\
\;\;\cdots & & \\
\;\;x_{n},s_{n} & = & \te{E_{n}}; \\
\multicolumn{3}{l}{\;\tbx{in}\;x,s_{1}\;\tand\;\cdots\;\tand\; s_{n}\;\}}
\end{array}\]

An expression $E_{i}$ is translated as \te{E_{i}} which dynamically
returns a value (bound to $x_{i}$) along with an explicit termination
signal $s_{i}$.  The operator \tbx{W} is used to detect the
termination of each side-effect operation (\tbx{mFetch} and
\tbx{mStore}) within $E_{i}$. The value of $s_{i}$ would become
$\wconst$ as soon as all the side-effect operations in $E_{i}$ have
terminated.  The operator $\tand$ is then used to combine all such
signals into a single signal for the whole block.  

The primitive \fbx{W} operator produces a signal \wconst when a given
identifier becomes a value. The general evaluation rule for strict
primitive functions would ensure that the identifier being tested is
touched before applying the \fbx{W} operator. Similarly, the primitive
\fbx{\&} operator is used to combine signals from two subexpressions
into one signal after they have been touched.

\begin{evalrule}{\fbx{W}:}
\inference{\state{\_}{\primapp{\fbx{W}}{\loc_{x}}:\insts}{\envs}%
                 {\works}{\store[\loc_{x}\mapsto\ftag{\val}]}{}}%
          {\state{\wconst}{\insts}{\envs}{\works}{\store}{}}
\end{evalrule}

\begin{evalrule}{\fbx{\&}:}
\inference{\state{\_}{\primapp{\fbx{\&}}{\loc_{1},\loc_{2}}:\insts}{\envs}{\works}%
                 {\store[\loc_{1}\mapsto\ftag{\wconst},\loc_{2}\mapsto\ftag{\wconst}]}{}}%
          {\state{\wconst}{\insts}{\envs}{\works}{\store}{}}
\end{evalrule}

The complete barrier translation appears in \fig{mbar}. Note that
tuple return values and non-refutable pattern matching is used only
for clarity---these operations are directly desugared into primitive
operators in the obvious way. The only non-trivial base cases for
signal generation are those for the \tbx{mFetch} and \tbx{mStore}
primitive operators. The \tbx{mFetch} operation is considered to have
terminated when the value of the location being fetched is returned.
Similarly, the \tbx{mStore} operation is considered to have terminated
when it returns the value being stored.

In the translation of $S_{1}\;\tbx{---}\;S_{2}$, note that $S_{2}$
gets protected by a $\lambda$-expression, so that it does not get
evaluated until the $\lambda$-expression is applied to something.
That something is the termination signal of $S_{1}$, and we use
\tbx{sap} to ensure that the application does not commence until the
termination signal is available.  Finally, since the bound variables
of $S_{2}$ have now gone into an inner scope (in the
$\lambda$-expression), we return them all and rebind them again in the
outer scope.

The barrier semantics shown here are different from the semantics
presented in \cite{Aditya95} in that here we are concerned only with
the termination of the side-effect operations present within the
pre-region of a barrier, while the semantics presented in
\cite{Aditya95} waited for the termination of the entire computation
within the pre-region.

