@@ -3,6 +3,7 @@
3\usepackage{amsmath, amssymb, stmaryrd}
3\usepackage{amsmath, amssymb, stmaryrd}
4\usepackage{mathpazo, times}
4\usepackage{mathpazo, times}
5\usepackage{float}
5\usepackage{float}
7\newcommand{\sLam}[2]{\lambda {#1} \cdot {#2}}
8\newcommand{\sLam}[2]{\lambda {#1} \cdot {#2}}
8\newcommand{\sApp}[2]{{#1} {#2}}
9\newcommand{\sApp}[2]{{#1} {#2}}
@@ -60,6 +61,8 @@
60\floatstyle{boxed}
61\floatstyle{boxed}
61\restylefloat{figure}
62\restylefloat{figure}
64+\lstset{basicstyle=\ttfamily\small}
63\begin{document}
66\begin{document}
65\title{Cloud Haskell Semantics (DRAFT)}
68\title{Cloud Haskell Semantics (DRAFT)}
@@ -256,8 +259,8 @@ Figure~\ref{fig:disconnect} gives the semantics for disconnecting and
256reconnecting. Rule \textsc{Disconnect} models random network disconnect
259reconnecting. Rule \textsc{Disconnect} models random network disconnect
257between nodes $\sNid_1$ and $\sNid_2$. We assume that entire \emph{nodes} get
260between nodes $\sNid_1$ and $\sNid_2$. We assume that entire \emph{nodes} get
258disconnected from each other, not individual processes. \emph{Reconnecting}
261disconnected from each other, not individual processes. \emph{Reconnecting}
259−however is on a per process basis (\textsc{Recon-Ex}). Connections to and from
262+however is on a per connection basis (\textsc{Recon-Ex}). Connections to and
260−node controllers can be implicitly reconnected ($\textsc{Recon-Im}_1$ and
263+from node controllers can be implicitly reconnected ($\textsc{Recon-Im}_1$ and
261$\textsc{Recon-Im}_2$).
264$\textsc{Recon-Im}_2$).
263\begin{figure}
266\begin{figure}
@@ -648,6 +651,55 @@ silently, unless monitors are setup.
648\caption{\label{fig:termination}Process Termination}
651\caption{\label{fig:termination}Process Termination}
649\end{figure}
652\end{figure}
654+\section{Open Issues}
656+\subsection{Ordering of Monitor/Link Notifications}
658+The semantics as described above, like the original Unified semantics, does not
659+guarantee that messages send from process $P$ to process $Q$ (\textsc{Send})
660+are ordered with respect to the link or monitor notification sent when process
661+$P$ terminates normally or abnormally (\textsc{Mon-Ret}, \textsc{Mon-Throw}). This means that if process $P$ does
665+ match $ \(Reply reply) -> ...
666+ , match $ \(ProcessMonitorNotification ..) -> ...
673+send pidA (Reply reply)
674+// terminate or indeed throw an exception
677+then the semantics does not guarantee that the reply from process $Q$ will
678+arrive at process $P$ before the monitor notification; hence, this results in
679+an (artificial) race condition in process $P$.
681+One possible solution is to regard such a link notification as a message from
682+process $Q$ to process $P$, which should be ordered along with the other
685+\subsection{Ordering and Typed Channels}
687+The situation is more tricky still than sketched above because we of typed
688+channels. The semantics does not provide ordering guarantees between messages
689+sent directly to the process and messages sent on typed channels. That means
690+that even if we consider a link or monitor notification as a message sent to
691+the process, to be ordered with other messages sent to that process, it is
692+still unordered with respect to messages sent on typed channels. This means
693+that we have similar race conditions\footnote{Even ignoring the fact that we
694+currently don't even provide a way to wait for a message on a typed channel
695+\emph{or} a direct message.}
697+A possible solution is to insist that \emph{all} messages from process $P$ to
698+process $Q$ are ordered, no matter how they are sent. From a implementation
699+point of view, this would entail the use of a single ordered network connection
700+for all messages from $P$ to $Q$, rather than using an ordered connection per
701+typed channel plus one for direct messages.
651\bibliographystyle{apalike}
703\bibliographystyle{apalike}
652\bibliography{references}
704\bibliography{references}