Correctly Implementing Synchronous Message Passing in the Pi-Calculus By Concurrent Haskell’s MVars

Our goals are the comparison of programming languages, correctness of transformations, compilation and optimization of programs, in particular of concurrent programs. We already used the contextual semantics of concurrent (functional) programming languages to effectively verify correctness of transformations [(17), (24), (25)], also under the premise not to worsen the runtime [(31)]. We propose to test may- and should-convergence in the contextual semantics, since, in particular, it rules out transformations that transform an always successful process into a process that may run into an error, for example a deadlock. There are also other notions of program equivalence in the literature, like bisimulation based program equivalences [(28)], however, these tend to take also implementation specific behavior of the operational semantics into account, whereas contextual equivalence abstracts from the details of the executions.

In [(29), (32)] we developed notions of correctness of translations w.r.t. contextual semantics, and in [(33)] we applied them in the context of concurrency, but for quite similar source and target languages. In this paper we translate a synchronous message passing model into a shared memory model, namely a synchronous $\pi$-calculus into a core-language of Concurrent Haskell, called ${\mathit{CH}}$.

The contextual semantics of concurrent programming languages is a generalization of the extensionality principle of functions. The test for a program $P$ is whether $C[P]$ – i.e. $P$ plugged into a program context – successfully terminates (converges) or not, which usually means that the standard reduction sequence ends with a value. For a concurrent program $P$, we use two observations: may-convergence ($P{\downarrow}$) – at least one execution path terminates successfully, and should-convergence¹¹1An alternative observation is must-convergence (all execution paths terminate). The advantages of equivalence notions based on may- and should-convergence are invariance under fairness restrictions, preservation of deadlock-freedom, and equivalence of busy-wait and wait-until behavior (see e.g. [(33)]). ($P{\Downarrow}$) – every intermediate state of a reduction sequence may-converges. For two processes $P$ and $Q$, $P\leq_{c}Q$ holds iff for all contexts $C[\cdot]$: $(C[P]{\downarrow}\implies C[Q]{\downarrow})$, and $P$ and $Q$ are contextually equivalent, $P\sim_{c}Q$, iff $P\leq_{c}Q$ and $Q\leq_{c}P$. Showing equal expressivity of two (concurrent) calculi by a translation $\tau$ requires that may- and should-convergence make sense in each calculus. Important properties are convergence-equivalence (may- and should-convergencies are preserved and reflected by the translation) and adequacy (see Definition 4.4), which holds if $\tau(P)\leq_{c,CH}\tau(Q)$ implies $P\leq_{c,\pi}Q$, for all $\pi$-calculus processes $P,Q$. Full-abstraction, i.e. $\forall P,Q:\tau(P)\leq_{c}\tau(Q)$ iff $P\leq_{c}Q$, only holds if the two calculi are more or less the same.

We explain the synchronous $\pi$-calculus milner-parrow-walker:92 ; milner-pi-calc:99 ; sangiorgi-walker:01 without sums, with replication, extended with a constant Stop sabel-schmidt-schauss-pistop:2015 , that signals successful termination. The $\pi$-calculus with Stop and the $\pi$-calculus without Stop but with so-called barbed convergences sangiorgi-walker:2001 are equivalent w.r.t.  contextual semantics schmidt-schauss-sabel:frank-60:19 . Thus, adding the constant Stop is not essential, but our arguments are easier to explain with Stop.

As an example for a reduction sequence, consider sending name $y$ over channel $x$ and then sending name $u$ over channel $y$: $(x(z).\overline{z}u.0{\hskip 0.28453pt{\!\scalebox{2.0}[1.0]{\tt|}\!}\hskip 0.28453pt}\overline{x}y.y(x).0)\xrightarrow{ia}(\overline{z}u.0[y/z]{\hskip 0.28453pt{\!\scalebox{2.0}[1.0]{\tt|}\!}\hskip 0.28453pt}y(x).0)\equiv(y(x).0{\hskip 0.28453pt{\!\scalebox{2.0}[1.0]{\tt|}\!}\hskip 0.28453pt}\overline{y}u.0)\xrightarrow{ia}(0{\hskip 0.28453pt{\!\scalebox{2.0}[1.0]{\tt|}\!}\hskip 0.28453pt}0)\equiv 0.$

For the semantics of processes, we observe whether standard reductions successfully terminate or not. Since reduction is nondeterministic, we test whether there exists a successful reduction sequence (may-convergence), and we test whether all reduction possibilities are successful (should-convergence).

Should-convergence implies may-convergence, and must-divergence implies may-divergence.

Contextual preorder and equivalence are (pre)-congruences. Contextual preorder remains unchanged if observation is restricted to closing contexts:

The calculus ${\mathit{CH}}$ (a variant of the language $\mathit{CHF}$, sabel-schmidt-schauss-PPDP:2011 ; sabel-schmidt-schauss-LICS:12 ) models a core language of Concurrent Haskell peyton-gordon-finne:96 . We assume a partitioned set of data constructors $c$ where each family represents a type $T$. The data constructors of type $T$ are $c_{T,1},\ldots,c_{T,|T|}$ where each $c_{T,i}$ has an arity $\mathrm{ar}(c_{T,i})\geq 0$. We assume that there is a type () with data constructor (), a type Bool with constructors True, False, a type List with constructors Nil and : (written infix), and a type Pair with a constructor $(,)$ written $(a,b)$.

Processes $P\in{\textit{Proc}_{{\mathit{CH}}}}$ in ${\mathit{CH}}$ have expressions $e\in{\textit{Expr}_{{\mathit{CH}}}}$ as subterms. See Fig. 5 where $u,w,x,y,z$ are variables from an infinite set Var. Processes are formed by parallel composition “  |  ”. The $\nu$-binder restricts the scope of a variable. A concurrent thread ${\Leftarrow}\,{e}$ evaluates $e$. In a process there is (at most one) unique distinguished thread, called main thread, written as ${\xLongleftarrow{\!\!\text{main}\!\!}}\,{e}$. MVars are mutable variables which are empty or filled. A thread blocks if it wants to fill a filled MVar ${x}\,{\textbf{{m}}}\,{e}$ or empty an empty MVar ${{x}}\,{\textbf{{m}}}\,{-}$. Here $x$ is called the name of the MVar. Bindings ${x}={e}$ model the global heap, of shared expressions, where $x$ is called a binding variable. If $x$ is a name of an MVar or a binding variable, then $x$ is called an introduced variable. In $Q{\hskip 0.28453pt{\!\scalebox{2.0}[1.0]{\tt|}\!}\hskip 0.28453pt}\nu x.P$ the scope of $x$ is $P$. A process is well-formed, if all introduced variables are pairwise distinct and there exists at most one main thread ${\xLongleftarrow{\!\!\text{main}\!\!}}\,{e}$.

Expressions ${\textit{Expr}_{{\mathit{CH}}}}$ consist of functional and monadic expressions ${{\textit{MExpr}_{{\mathit{CH}}}}}$. Functional expressions are variables, abstractions $\lambda x.e$, applications $(e_{1}~{}e_{2})$, seq-expressions $(\text{{seq}}~{}e_{1}~{}e_{2})$, constructor applications $(c~{}e_{1}~{}\ldots~{}e_{\mathrm{ar}(c)})$, letrec-expressions $(\text{letrec}~{}x_{1}=e_{1},\ldots,x_{n}=e_{n}~{}\text{{in}}~{}e)$, and case_T-expressions for every type $T$. We abbreviate case-expressions as $\text{{case}}_{T}~{}e~{}\text{{of}}~{}alts$ where $alts$ are the case-alternatives such that there is exactly one alternative $(c_{T,i}~{}x_{1}\ldots x_{\mathrm{ar}(c_{T,i})}\,\texttt{->}\,e_{i})$ for every constructor $c_{T,i}$ of type $T$, where $x_{1},\ldots,x_{\mathrm{ar}(c_{T,i})}$ (occurring in the pattern $c_{T,i}~{}x_{1}\ldots x_{\mathrm{ar}(c_{T,i})}$) are pairwise distinct variables that become bound with scope $e_{i}$. We often omit the type index $T$ in $\text{{case}}_{T}$. In $\text{letrec}~{}x_{1}=e_{1},\ldots,$ $x_{n}=e_{n}$ $\text{{in}}~{}e$ the variables $x_{1},\ldots,x_{n}$ are pairwise distinct and the bindings $x_{i}=e_{i}$ are recursive, i.e. the scope of $x_{i}$ is $e_{1},\ldots,e_{n}$ and $e$. Monadic operators ${\tt newMVar}$, takeMVar, and putMVar are used to create, to empty and to fill MVars, the “bind”-operator  >​>=  implements sequential composition of IO-operations, the forkIO-operator performs thread creation, and return lifts expressions into the monad.

Monadic values are $\text{{newMVar}}\,e$, $\text{{takeMVar}}\,e$, $\text{{putMVar}}\,e_{1}\,e_{2}$, $\text{return}\,e$, $e_{1}\,{\,\text{{$\texttt{\char 62\relax\!\char 62\relax=}$}}}\,\,e_{2}$, or $\text{{forkIO}}\,e$. Functional values are abstractions and constructor applications. A value is a functional or a monadic value.

Abstractions, letrec-expressions, case-alternatives, and $\nu x.P$ introduce variable binders. This induces bound and free variables (dentoted by $\mathit{FV}(\cdot)$), $\alpha$-renaming, and $\alpha$-equivalence $=_{\alpha}$. If $\mathit{FV}(P)=\emptyset$, then we call process $P$ closed. We assume the distinct variable convention: free variables are distinct from bound variables, and bound variables are pairwise distinct. We assume that $\alpha$-renaming is applied to obey this convention. Structural congruence $\equiv$ of ${\mathit{CH}}$-processes is the least congruence satisfying the laws $P_{1}{\hskip 0.28453pt{\!\scalebox{2.0}[1.0]{\tt|}\!}\hskip 0.28453pt}P_{2}\equiv P_{2}{\hskip 0.28453pt{\!\scalebox{2.0}[1.0]{\tt|}\!}\hskip 0.28453pt}P_{1}$, $(P_{1}{\hskip 0.28453pt{\!\scalebox{2.0}[1.0]{\tt|}\!}\hskip 0.28453pt}P_{2}){\hskip 0.28453pt{\!\scalebox{2.0}[1.0]{\tt|}\!}\hskip 0.28453pt}P_{3}\equiv P_{1}{\hskip 0.28453pt{\!\scalebox{2.0}[1.0]{\tt|}\!}\hskip 0.28453pt}(P_{2}{\hskip 0.28453pt{\!\scalebox{2.0}[1.0]{\tt|}\!}\hskip 0.28453pt}P_{3})$, $\nu x_{1}.\nu x_{2}.P\equiv\nu x_{2}.\nu x_{1}.P$, $P_{1}\equiv P_{2}\text{ if $P_{1}=_{\alpha}P_{2}$}$, and $(\nu x.P_{1}){\hskip 0.28453pt{\!\scalebox{2.0}[1.0]{\tt|}\!}\hskip 0.28453pt}P_{2}\equiv\nu x.(P_{1}{\hskip 0.28453pt{\!\scalebox{2.0}[1.0]{\tt|}\!}\hskip 0.28453pt}P_{2})\text{ if $x\not\in\mathit{FV}(P_{2})$}$.

We assume expressions and processes to be well-typed w.r.t.  a monomorphic type system: the typing rules are standard (they can be found in schmidt-schauss-sabel:frank-60:19 ). The syntax of types is in Fig. 5 where $({\tt IO}~{}{\mathfrak{t}})$ is the type of a monadic action with return type ${\mathfrak{t}}$, $({\tt MVar}~{}{\mathfrak{t}})$ is the type of an MVar with content type ${\mathfrak{t}}$, and ${\mathfrak{t}}_{1}\to{\mathfrak{t}}_{2}$ is a function type. We treat constructors like overloaded constants to use them in a polymorphic way.

We introduce a call-by-name small-step reduction for ${\mathit{CH}}$. This operational semantics can be shown to be equivalent to a call-by-need semantics (see sabel-schmidt-schauss-PPDP:2011 for the calculus $\mathit{CHF}$). However, the equivalence of the reduction strategies is not important for this paper. That is why we do not include it.

In ${\mathit{CH}}$, a context is a process or an expression with a (typed) hole $[\cdot]$. We introduce several classes of contexts in Fig. 5. They are used by the reduction rules.

Functional evaluation includes $\beta$-reduction (beta), copying shared bindings into needed positions (cpce), evaluating case- and seq-expressions (case) and (seq), and moving letrec-bindings into the global bindings (mkbinds). For monadic computations, rule (lunit) implements the monadic evaluation. Rules (nmvar), (tmvar), and (pmvar) handle the MVar creation and access. A takeMVar-operation can only be performed on a filled MVar, and a putMVar-operation needs an empty MVar. Rule (fork) spawns a new thread. A concurrent thread of the form ${\Leftarrow}\,{\text{return}~{}e}$ is terminated (where $e$ is of type ()).

We say that a ${\mathit{CH}}$-process $P$ is successful if $P\equiv\nu x_{1}\ldots x_{n}.({\xLongleftarrow{\!\!\text{main}\!\!}}\,{\text{return}~{}e}{\hskip 0.28453pt{\!\scalebox{2.0}[1.0]{\tt|}\!}\hskip 0.28453pt}P^{\prime})$ and if $P$ is well-formed. This captures Haskell’s behavior that termination of the main-thread terminates all threads.

As an example, we consider the processes

Process $P_{1}$ is may-convergent and may-divergent (and thus not should-convergent), since either the main-thread succeeds in emptying the MVar $m$, or (if the other threads empties the MVar $m$) the main-thread is blocked forever. The process $P_{2}$ is sucessful. The process $P_{3}$ is must-divergent. The equivalence $P_{1}\sim_{c,{\downarrow}}P_{2}$ holds, but $P_{1}\not\sim_{c}P_{2}$, since $P_{2}$ is should-convergent and thus $P_{1}\not\sim_{c,{\Downarrow}}P_{2}$. As a further example, it is easy to verify that $P_{1}\sim_{c,{\Downarrow}}P_{3}$ holds, since both processes are not should-convergent and a surrounding context cannot change this. However, $P_{1}\not\sim_{c,{\downarrow}}P_{3}$, since $P_{3}{\Uparrow}$.

Contextual approximation and equivalence are (pre)-congruences. The following equivalence will help to prove properties of our translation.

We present a translation $\tau_{0}$ that encodes $\Pi_{\text{{Stop}}}$-processes as ${\mathit{CH}}$-programs. It establishes correct synchronous communication by using a private MVar, which is created by the sender and its name is sent to the receiver. The receiver uses it to acknowledge that the message was received. Since only the sender and the receiver know this MVar, no other thread can interfere the communication.The approach has similarities with Boudol’s translation boudol:1992 from the $\pi$-calculus into an asynchronous one, where a private channel name of the $\pi$-calculus was used to guarantee safe communication between sender and receiver.

For translating $\pi$-calculus channels into ${\mathit{CH}}$, we use a recursive data type Channel (with constructor Chan), which is defined in Haskell-syntax as

We abbreviate $(\text{{case}}_{\texttt{Chan}}~{}e~{}\text{{of}}~{}(\text{{Chan}}~{}m~{}\,\texttt{->}\,~{}m))$ as $(\mathit{unchan}~{}e)$.

We use $a~{}{\,\text{{$\texttt{\char 62\relax\!\char 62\relax}$}}}\,~{}b$ for $a{\,\text{{$\texttt{\char 62\relax\!\char 62\relax=}$}}}\,(\lambda\_\,.\,b)$ and also use Haskell’s do-notation with the following meaning:

As a further abbreviation, we write $y\leftarrow\text{{newEmptyMVar}}$ inside a $\mathbf{do}$-block to abbreviate the sequence $y\leftarrow\text{{newMVar}}~{}\bot;\text{{takeMVar}}~{}y$, where $\bot$ is a must-divergent expression. Our translation uses one MVar per channel which contains a pair consisting of the (translated) name of the channel and a further MVar used for the synchronization, which is private, i.e. only the sender and the receiver know it. Privacy is established by the sender: it creates a new MVar for every send operation. Message $y$ is sent over channel $x$ by sending a pair $(y,check)$ where $check$ is an MVar containing (). The receiver waits for a message $(y,check)$ by the sender. After sending the message, the sender waits until check is emptied, and the receiver acknowledges by emptying the MVar check³³3A variant of the translation would be to change the roles for the acknowledgement such that an empty MVar is created, which is filled by the receiver and emptied by the sender. The reasoning on the correctness of the translation is very similar to the one presented here.

The translation $\tau_{0}$ generates a main-thread and an MVar ${\mathit{stop}}$. The main thread is then waiting for the MVar ${\mathit{stop}}$ to be emptied. The inner translation $\tau$ translates the constructs and constants of the $\Pi_{\text{{Stop}}}$-calculus into ${\mathit{CH}}$-expressions. Except for the main-thread (and using keyword let instead of letrec), the translation $\tau_{0}$ generates a valid Concurrent Haskell-program, i.e. if we write $\tau_{0}(P)={\xLongleftarrow{\!\!\text{main}\!\!}}\,{e}$ as $\texttt{main}=e$ , we can execute the translation in the Haskell-interpreter.

For the following definition of $\tau$ being compositional, adequate, or fully abstract, we adopt the view that $\tau$ is a translation from $\Pi_{\text{{Stop}}}$ into the ${\mathit{CH}}$-language with a special initial evaluation context $C_{\mathit{out}}^{\tau}$.

Since $\leq_{c,{\mathit{CH}}}$ is a subset of $\leq_{c,\tau_{0}}$, we often can use the more general relations for reasoning.

Convergence-equivalence of translation $\tau_{0}$ for may- and should-convergence holds. For readability the proof is omitted, but given in the technical report schmidt-schauss-sabel:frank-60:19 , where we show:

We show that the translation is adequate (see Theorem 4.8 below). The interpretation of this result is that the $\pi$-calculus with the concurrent semantics is semantically represented within ${\mathit{CH}}$. This result is on a more abstract level, since it is based on the property whether the programs (in all contexts) produce values or may run into failure, or get stuck; or not. Since the $\pi$-calculus does not have a notion of values, also the translated processes cannot be compared w.r.t. values other than a single form of value.