{'fraction_non_alphanumeric': 0.050368494822986845, 'fraction_numerical': 0.008658497987973052, 'mean_word_length': 4.201058201058201, 'pattern_counts': {'":': 0, '<': 2, '<?xml version=': 0, '>': 26, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 11, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Correctly Implementing Synchronous Message Passing in the Pi-Calculus By Concurrent Haskell's MVars

Comparison of concurrent programming languages and correctness of program transformations in concurrency are the focus of this research. As criterion we use contextual semantics adapted to concurrency, where may -- as well as should -- convergence are observed. We investigate the relation between the synchronous pi-calculus and a core language of Concurrent Haskell (CH). The contextual semantics is on the one hand forgiving with respect to the details of the operational semantics, and on the other hand implies strong requirements for the interplay between the processes after translation. Our result is that CH embraces the synchronous pi-calculus. Our main task is to find and prove correctness of encodings of pi-calculus channels by CH's concurrency primitives, which are MVars. They behave like (blocking) 1-place buffers modelling the shared-memory. The first developed translation uses an extra private MVar for every communication.We also automatically generate and check potentially correct translations that reuse the MVars where one MVar contains the message and two additional MVars for synchronization are used to model the synchronized communication of a single channel in the pi-calculus.Our automated experimental results lead to the conjecture that one additional MVar is insufficient.


Introduction
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 [16,23,24], also under the premise not to worsen the runtime [30]. We propose to test mayand 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 [27], 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 [28,31] we developed notions of correctness of translations w.r.t. contextual semantics, and in [32] 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 π-calculus into a core-language of Concurrent Haskell, called 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↓) -at least one execution path terminates successfully, and should-convergence 1 (P⇓) -every intermediate state of a reduction sequence may-converges. For two processes P and Q, P ≤ c Q holds iff for all contexts C[·]: (C[P]↓ =⇒ C[Q]↓), and P and Q are contextually equivalent, P ∼ c Q, iff P ≤ c Q and Q ≤ c P. Showing equal expressivity of two (concurrent) calculi by a translation τ requires that may-and shouldconvergence 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 τ(P) ≤ c,CH τ(Q) implies P ≤ c,π Q, for all π-calculus processes P, Q. Full-abstraction, i.e. ∀P, Q : τ(P) ≤ c τ(Q) iff P ≤ c Q, only holds if the two calculi are more or less the same.
Source and Target Calculi. The well-known π-calculus [15,14,27] is a minimal model for mobile and concurrent processes. Dataflow is expressed by passing messages between them via named channels, where messages are channel names. Processes and links between processes can be dynamically created and removed which makes processes mobile. The interest in the π-calculus is not only due to the fact that it is used and extended for various applications, like reasoning about cryptographic protocols [1], applications in molecular biology [21], and distributed computing [13,7]. The π-calculus also permits the study of intrinsic principles and semantics of concurrency and the inherent nondeterministic behavior of mobile and communicating processes. We investigate a variant of the π-calculus which is the synchronous π-calculus with replication, but without sums, matching operators, or recursion. To observe termination of a process, the calculus has a constant Stop which signals successful termination.
The calculus CH, a core language of Concurrent Haskell, is a process calculus where threads evaluate expressions from a lambda calculus extended by data constructors, case-expressions, recursive letexpressions, and Haskell's seq-operator. Also monadic operations (sequencing and creating threads) are available. The shared memory is modelled by MVars (mutable variables) which are one-place buffers that can be either filled or empty. The operation takeMVar tries to empty a filled MVar and blocks if the MVar is already empty. The operation putMVar tries to fill an empty MVar and blocks if the MVar is already filled. The calculus CH is a variant (or a subcalculus) of the calculus CHF [23,24] which extends Concurrent Haskell with futures. A technical advantage of this approach is that we can reuse studies and results on the contextual semantics of CHF also for CH.
Details and Variations of the Translation. One main issue for a correct translation from π-processes to CH-programs is to encode the synchronous communication of the π-calculus. The problem is that the MVars in CH have an asynchronous behavior (communication has to be implemented in two steps: the sender puts the message into an MVar, which is later taken by the receiver). To implement synchronous communication, the weaker synchronisation property of MVars has to be exploited, where we must be aware of the potential interferences of the executions of other translated communications on the same channel. The task of finding such translations is reminiscent of the channel-encoding used in [20], but, however, there an asynchronous channel is implemented while we look for synchronous communication.
We provide a translation τ 0 which uses a private MVar per channel and per communication to ensure that no other process can interfere with the interaction. A similar idea was used in [12,3] for keeping channel names private in a different scenario (see [10,9] for recent treatments of these encodings). We prove that the translation τ 0 is correct. Since we are also interested in simpler translations, we looked for correct translations with a fixed and static number of MVars per channel in the π-calculus. Since this 1 An 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. [32]). task is too complex and error-prone for hand-crafting, we automated it by implementing a tool to rule out incorrect translations 2 . Thereby we fix the MVars used for every channel: a single MVar for exchanging the channel-name and perhaps several additional MVars of unit type to perform checks whether the message was sent or received (we call them check-MVars, they behave like binary semaphores that are additionally blocking for signal-operations on an unlocked semaphore). The outcomes of our automated search are: a further correct translation that uses two check-MVars, where one is used as a mutex between all senders or receivers on one channel, and further correct translations using three additional MVars where the filling and emptying operations for each MVar need not come from the same sender or receiver. The experiments lead to the conjecture that there is no translation using only one check-MVar.
Results. Our novel result is convergence-equivalence and adequacy of the open translation τ (Theorems 4.5 and 4.8), translating the π-calculus into CH. The comparison of the π-calculus with a concurrent programming language (here CH) using contextual semantics for may-and should-convergence in both calculi exhibits that the π-calculus is embeddable in CH where we can prove that the semantical properties of interest are kept. The adaptation of the adequacy and full abstraction notions (Definition 4.4) for open processes is a helpful technical extension of our work in [28,31].
We further define a general formalism for the representation of translations with global names and analyze different classes of such translations using an automated tool. In particular, we show correctness of two particular translations in Theorems 5.9 and 5.12. The discovered correct translations look quite simple and their correctness seems to be quite intuitive. However, our experience is that searching for correct translations is quite hard, since there are apparently correct (and simple) translations which were wrong. Our automated tool helped us to rule out wrong translations and to find potentially correct ones.
Discussion of Related Work on Characterizing Encodings. There are five criteria for valid translations resp. encodings proposed and discussed in [11,9], which mainly restrict the translations w.r.t. language syntax and reduction semantics of the source and target language, called: compositionality, name invariance, operational correspondence, divergence reflection and success sensitiveness. Compositionality and name invariance restrict the syntactic form of the translated processes; operational correspondence means that the transitive closure of the reduction relation is transported by the translation, modulo the syntactic equivalence; and divergence reflection and success sensitiveness are conditions on the semantics.
In our approach, we define semantical congruence (and precongruence) relations on the source and target language. Thus the first two conditions are not part of our notion of contextual equivalence, however, may be used as restrictions in showing non-encodability. We also omit the third condition and only use stronger variants of the fourth and fifth condition. Convergence equivalence as a tool for finding out may-and should-convergence is our replacement of Gorla's divergence reflection and success sensitiveness. We do not define an infinite reduction sequence as an error, which has as nice consequence that synchronization could be implemented by busy-wait techniques.
Further Related Work. Encodings of synchronous communication by asynchronous communication using a private name mechanism are given in [12,3] for (variants of the) π-calculus. Our idea of the translation τ 0 similarly uses a private MVar to encode the channel based communication, but our setting is different, since our target language is Concurrent Haskell. Encodings between π-calculi with synchronous and with asynchronous communication were, for instance, already considered in [12,3,19,18] P, Q ∈ Π Stop ::= νx.P | xy.P | x(y).P | !P | P|Q | 0 | Stop C ∈ Π Stop,C ::= [·] |x(y).C | x(y).C | C|P | P|C |!C | νx.C D ∈ PCtxt π ::= [·] | D|P | P|D | νx.D.  where encodability results are obtained for the π-calculus without sums [12,3], while in [18,19] the expressive power of synchronous and asynchronous communication in the π-calculus with mixed sums was compared and non-encodability is a main result. Translations of the π-calculus into programming calculi and logical systems are given in [2], where a translation into a graph-rewriting calculus is given and soundness and completeness w.r.t. the operational behavior is proved. The article [33] shows a translation and a proof that the π-calculus is exactly operationally represented. There are several works on session types which are related to the π-calculus, e.g., [17] studies encodings from a session calculus into PCF extended by concurrency and effects and also an embedding in the other direction, mapping PCF extended by effects into a session calculus. The result is a (strong) operational correspondence between the two calculi. In [4] an embedding of a session π-calculus into ReactiveML is given and operational correspondence between the two languages is shown. Encodings of CML-events in Concurrent Haskell using MVars are published in [22,5]. This approach is more high-level than ours (since it considers events, while we focus the plain π-calculus). In [5] correctness of a distributed protocol for selectivecommunication w.r.t. an excerpt of CML is shown and a correct implementation of the protocol in the π-calculus is given. The protocol is implemented in Concurrent-Haskell, but no correctness of this part is shown, since [5] focuses to show that CML-events are implementable in languages with first-order message-passing which is different from our focus (translating the π-calculus into CH).
Outline. We introduce the source and target calculi in Sections 2 and 3, the translation using private names in Section 4, and in Section 5 we treat translations with global names. We conclude and discuss future work in Section 6. Due to space constraints most proofs are in the technical report [29].

The π-Calculus with Stop
We explain the synchronous π-calculus [15,14,27] without sums, with replication, extended with a constant Stop [25], that signals successful termination. The π-calculus with Stop and the π-calculus without Stop but with so-called barbed convergences [26] are equivalent w.r.t. contextual semantics [29]. Thus, adding the constant Stop is not essential, but our arguments are easier to explain with Stop.
Definition 2.1 (Calculus Π Stop ). Let N be a countable set of (channel) names. The syntax of processes is shown in Fig. 1. Name restriction νx.P restricts the scope of name x to process P, P|Q is the parallel composition of P and Q, the process xy.P waits on channel x to output y over channel x and then becoming P, the process x(y).P waits on channel x to receive input, after receiving the input z, the process turns into P[z/y] (where P[z/y] is the substitution of all free occurrences of name y by name z in process P), the process !P is the replication of process P, i.e. it behaves like an infinite parallel combination of process P with itself, the process 0 is the silent process, and Stop is a process constant that signals success. We sometimes write x(y) instead of x(y).0 as well as xy instead of xy.0. Free names FN(P), bound names BN(P), and α-equivalence = α in Π Stop are as usual in the πcalculus. A process P is closed if FN(P) = / 0. Let Π c Stop be the closed processes in Π Stop . Structural congruence ≡ is the least congruence satisfying the laws shown in Fig. 3. Process contexts Π Stop,C and reduction contexts PCtxt π are defined in Fig Remark 2.2. We do not include "new" laws for structural congruences on the constant Stop, like Stop|Stop equals Stop, since this would require to re-develop a lot of theory known from the πcalculus without Stop. In our view, Stop is a mechanism for a notion of success that can be easily replaced by other similar notions (e.g. observing an open input or output as in barbed testing). However, it is easy to prove those equations on the semantic level. (i.e. w.r.t. ∼ c as defined below in Definition 2.5).
As an example for a reduction sequence, consider sending name y over channel x and then sending name u over channel y: 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). Definition 2.3. Let P be a Π Stop -process. We say process P is may-convergent and write P↓, if and only if there is a successful process P with P sr, * − − → P . We say P is should-convergent and write P⇓ if and only if for all P : P sr, * − − → P implies P ↓. If P is not may-convergent, then P we say is must-divergent (written P⇑). If P is not should-convergent, then we say it is may-divergent (written P↑). The first result is successful, and the second result is not successful. Hence, for P we have P ↓ and P ↑.
Contextual preorder and equivalence are (pre)-congruences. Contextual preorder remains unchanged if observation is restricted to closing contexts: Lemma 2.7. Let ξ ∈ {↓, ↑, ⇓, ⇑}, P, Q be Π Stop -processes. Then P ≤ c,ξ Q if, and only if ∀C ∈ Π Stop,C such that C[P] and C[Q] are closed: . . x ar(c T,|T | ) -> e |T | ) m ∈ MExpr CH ::= return e | e >>= e | forkIO e | takeMVar e | newMVar e | putMVar e e t ∈ Typ CH :: Figure 4: Syntax of processes, expressions, types, and context classes of CH Functional Evaluation: where v is a functional value Monadic Computations: Capture avoidance: We assume capture avoiding reduction for all reductions.

The Process Calculus CH
The calculus CH (a variant of the language CHF, [23,24]) models a core language of Concurrent Haskell [20]. 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 , . . . , c T,|T | where each c T,i has an arity ar(c T,i ) ≥ 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 ∈ Proc CH in CH have expressions e ∈ Expr CH as subterms. See Fig. 4 where u, w, x, y, z are variables from an infinite set Var. Processes are formed by parallel composition "|". The ν-binder restricts the scope of a variable. A concurrent thread ⇐ e evaluates e. In a process there is (at most one) unique distinguished thread, called main thread, written as . . e ar(c) ), letrec-expressions (letrec x 1 = e 1 , . . . , x n = e n in e), and case Texpressions for every type T . We abbreviate case-expressions as case T e of alts where alts are the case-alternatives such that there is exactly one alternative (c T,i x 1 . . . x ar(c T,i ) -> e i ) for every constructor c T,i of type T , where x 1 , . . . , x ar(c T,i ) (occurring in the pattern c T,i x 1 . . . x ar(c T,i ) ) are pairwise distinct variables that become bound with scope e i . We often omit the type index T in case T . In letrec x 1 = e 1 , . . . , x n = e n in e the variables x 1 , . . . , x n are pairwise distinct and the bindings x i = e i are recursive, i.e. the scope of x i is e 1 , . . . , e n and e. Monadic operators 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 newMVar e, takeMVar e, putMVar e 1 e 2 , return e, e 1 >>= e 2 , or forkIO e. Functional values are abstractions and constructor applications. A value is a functional or a monadic value.
Abstractions, letrec-expressions, case-alternatives, and νx.P introduce variable binders. This induces bound and free variables (dentoted by FV(·)), α-renaming, and α-equivalence = α . If FV(P) = / 0, 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 α-renaming is applied to obey this convention. Structural congruence ≡ of CH-processes is the least congruence satisfying the laws 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 [29]). The syntax of types is in Fig. 4 where (IO t) is the type of a monadic action with return type t, (MVar t) is the type of an MVar with content type t, and t 1 → 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 CH. This operational semantics can be shown to be equivalent to a call-by-need semantics (see [23] for the calculus CHF). However, the equivalence of the reduction strategies is not important for this paper. That is why we do not include it.
In CH, a context is a process or an expression with a (typed) hole [·]. We introduce several classes of contexts in Fig. 4. They are used by the reduction rules.  We say that a CH-process P is successful if P ≡ νx 1 . . . x n .( main ⇐= = return e|P ) and if P is wellformed. This captures Haskell's behavior that termination of the main-thread terminates all threads. Definition 3.3. Let P be a CH-process. Then P may-converges (denoted as P↓), iff P is well-formed and ∃P : P sr, * − − → P such that P is successful. If P↓ does not hold, then P must-diverges and we write P⇑. Process P should-converges (written as P⇓), iff P is well-formed and ∀P : P sr, * − − → P =⇒ P ↓. If P is not should-convergent, then we say P may-diverges written as P↑. As an example, we consider the processes Process P 1 is may-convergent and may-divergent (and thus not should-convergent), since either the mainthread 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 ∼ c,↓ P 2 holds, but P 1 ∼ c P 2 , since P 2 is should-convergent and thus P 1 ∼ c,⇓ P 2 . As a further example, it is easy to verify that P 1 ∼ c,⇓ P 3 holds, since both processes are not should-convergent and a surrounding context cannot change this. However, P 1 ∼ c,↓ P 3 , since P 3 ⇑.
Contextual approximation and equivalence are (pre)-congruences. The following equivalence will help to prove properties of our translation.

The Translation τ 0 with Private MVars
We present a translation τ 0 that encodes Π Stop -processes as 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 [3] from the π-calculus into an asynchronous one, where a private channel name of the π-calculus was used to guarantee safe communication between sender and receiver.
For translating π-calculus channels into CH, we use a recursive data type Channel (with constructor Chan), which is defined in Haskell-syntax as data Channel = Chan (MVar (Channel, (MVar ()))) We abbreviate (case Chan e of (Chan m -> m)) as (unchan e).
We use a >> b for a >>= (λ . b) and also use Haskell's do-notation with the following meaning: As a further abbreviation, we write y ← newEmptyMVar inside a do-block to abbreviate the sequence y ← newMVar ⊥; takeMVar y, where ⊥ 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 3  We consider the Π Stop -process P := νx, y 1 , y 2 , z.(x(y 1 ).0|x(y 2 ).Stop|xz.0) which is may-convergent and may-divergent: depending on which receiver communicates with the sender, the result is the successful process νx, y 1 .(x(y 1 ).0|Stop) or the must-divergent process νx, y 2 .(x(y 2 ).Stop). The CH-process τ 0 (P) reduces after several steps to the process νstop, chanx, chany 1 , chany 2 , chanz, checkx, x, y 1 , y 2 , z. Now the first thread (which is the translation of sender xz.0) is blocked, since it tries to fill the full MVar checkx. The second thread (the encoding of x(y 1 ).0) and the third thread (the encoding of x(y 2 ).Stop) race for emptying the MVar chanx. If the second thread wins, then it will fill the MVar checkx which is then emptied by the first thread, and all other threads are blocked forever. If the third thread wins, then it will fill the MVar checkx which is then emptied by the first thread, and then the second thread will empty the MVar stop. This allows the main-thread to fill it, resulting in a successful process.
For the following definition of τ being compositional, adequate, or fully abstract, we adopt the view that τ is a translation from Π Stop into the CH-language with a special initial evaluation context C τ out . Since ≤ c,CH is a subset of ≤ c,τ 0 , we often can use the more general relations for reasoning. Definition 4.4. Let Π Stop,C be the contexts of Π Stop . We define the following properties for τ 0 and τ (see [31] for a general framework of properties of translations under observational semantics). For open processes P, P , we say that translation τ is convergence-equivalent iff for all P ∈ Π Stop : P↓ ⇐⇒ τ(P)↓ 0 and P⇓ ⇐⇒ τ(P)⇓ 0 , adequate iff for all processes P, P ∈ Π Stop : τ(P) ≤ c,τ 0 τ(P ) =⇒ P ≤ c P , and fully abstract iff for all processes P, P ∈ Π Stop : P ≤ c P ⇐⇒ τ(P) ≤ c,τ 0 τ(P ).
We show that the translation is adequate (see Theorem 4.8 below). The interpretation of this result is that the π-calculus with the concurrent semantics is semantically represented within 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 π-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.
The translation τ 0 is not fully abstract (see Theorem 4.9 below), which is rather natural, since it only means that it is mapped into a subset of the CH-expressions and that this is a proper subset w.r.t. the semantics. For proving both theorems, we first use a simple form of a context lemma: Lemma 4.6. Let e, e be CH-expressions, where the only free variable in e, e is stop.
Then We show that the translation τ transports Π Stop -processes into CH, such that adequacy holds. Thus the translated processes also correctly mimic the behavior of the original Π Stop -processes when plugged into contexts. If the translated open processes cannot be distinguished by ≤ c,τ 0 , i.e. there is no test that detects a difference w.r.t. may-and should-convergence, then the original processes are equivalent in the π-calculus. However, this open translation is not fully abstract, which means that there are CH-contexts (not in the image of the translation) that can see and exploit too much of the details of the translation. Theorem 4.8. The translation τ is adequate.
Proof. We prove the adequacy for the preorder ≤ c,τ 0 , for ∼ c,τ 0 and ∼ c the claim follows by symmetry. Let P, P be Π Stop -processes, such that τ(P) ≤ c,τ 0 τ(P ). We show that P ≤ c P . We use Lemma 3. Theorem 4.9. The translation τ is not fully abstract, but it is fully abstract on closed processes, i.e. for closed processes P 1 , P 2 ∈ Π Stop , we have P 1 ≤ c P 2 ⇐⇒ τ(P 1 ) ≤ c,τ 0 τ(P 2 ).
Proof. The first part holds, since an open translation can be closed by a context without initializing the ν-bound MVars. For P =x(y).Stop|x(z).Stop, we have P ∼ c Stop but τ(P) ∼ c,0 τ(Stop): let D be a context that does not initialize the MVars for x (as the translation does). Then D[τ(P)]⇑ 0 , but D[τ(Stop)]⇓ 0 . Restricted to closed processes, full abstraction holds: P 1 ≤ c P 2 =⇒ τ(P 1 ) ≤ c,τ 0 τ(P 2 ) follows from Lemma 4.6, since τ 0 produces closed processes in context C τ out . Theorem 4.8 implies the other direction.

Translations with Global MVars
In this section we investigate translations that do not use private MVars, but use a fixed number of global MVars. We first motivate this investigation. The translation τ is quite complex and thus we want to figure out whether there are simpler translations. A further reason is that τ is not optimal, since it generates one MVar per communication which can be garbage-collected after the communication, however, generation and garbage collection require resources and thus the translation τ may be inefficient in practice.
To systematically search for small global translations we implemented an automated tool. It searches for translations with global MVars (abstracting from a lot of other aspects of the translation) and tries to refute the correctness. As we show, most of the small translations are shown as incorrect by our tool. Analyzing correctness of the remaining translations can then be done by hand.
We only consider the aspect of how to encode the synchronous message passing of the π-calculus, the other aspects (encoding parallel composition, replication and the Stop-constant) are not discussed and we assume that they are encoded as before (as the translation τ did). We also keep the main idea to translate a channel of the π-calculus into CH by representing it as an object of a user-defined data type Channel that consists of an MVar for transferring the message (which again is a Channel), and additional MVars for implementing a correct synchronization mechanism. For the translation τ, we used a private MVar (created by the sender, and transferred together with the message). Now we investigate translations where this mechanism is replaced by one or several public MVars, which are created once together with the channel object. To restrict the search space for translations, only the synchronization mechanism of MVars (by emptying and filling them) is used, but we forbid to transfer specific data (like numbers etc.). Hence, we restrict these MVars (which we call check-MVars) to be of type MVar (). Such MVars are comparable to binary semaphores, where filling and emptying correspond to operations signal and wait. In summary, we analyze translations of π-calculus channels into a CH-data type Channel defined in Haskell-syntax as data Channel = Chan (MVar Channel) (MVar ()) . .

. (MVar ())
A π-calculus channel x is represented as a CH-binding x = Chan content check 1 . . . check n where content, check 1 , . . . , check n are appropriately initialized (i.e. empty) MVars. The MVars are public (or global), since all processes which know x have access to the components of the channel. After fixing this representation of a π-channel in CH, the task is to translate the input-and output-actions x(y) and xz into CH-programs such that the interaction reduction is performed correctly and synchronously. We call the translation of x(y), the receiver (program) and the translation of xz the sender (program). As a simplification, we restrict the allowed operations of the sender and receiver allowing only the operations: The sender puts its message into the contents-MVar of the channel. It represents the expression case Channel x of (Chan c a 1 . . . a n -> putMVar c z >> e) in CH where e is the remaining program of the sender. The operation occurs exactly once in the sender program. We write it as putS x z, or as putS, if x and z are clear.

takeS:
The receiver takes the message from the contents-MVar of channel x and replaces name y by the received name in the subsequent program. The operation occurs exactly once in the receiver program. We write it as takeS x y, or as takeS, if x and y are clear. It represents the CH-expression case Channel x of (Chan c a 1 . . . a n -> takeMVar c >>= λ y.e) where e is the remaining program of the receiver. In do-notation, we write do {y ← takeS x ; e} to abbreviate the above CH-expression.
putC and takeC: The sender and the receiver may synchronize on a check-MVar check i by putting () into it or by emptying the MVar. These operations are written as putC i x and takeC i x , or also as putC i , takeC i if the name x is clear. We write putC and takeC if there is only one check-MVar. Let e be the remaining program of the sender or receiver. Then putC i x represents the CH-expression case Channel x of (Chan c a 1 . . . a n -> putMVar a i () >> e) and takeC i x represents the expression case Channel x of (Chan c a 1 . . . a n -> takeMVar a i >> e).
We restrict our search for translations to the case that the sender and the receiver programs are sequences of the above operations, assuming that they are independent of the channel name x. With this restriction, we can abstractly write the translation of the sender and the receiver as a pair of sequences, where only putS, takeS, putC i and takeC i operations are used. We make some more restrictions: Definition 5.1. Let n > 0 be a number of check-MVars. A standard global synchronized-to-buffer translation (or gstb-translation) is a pair (T send , T receive ) of a send-sequence T send and a receive-sequence T receive consisting of putS, takeS, putC i and takeC i operations, where the send-sequence contains putS once, the receive-sequence contains takeS once, and for every putC i -action in (T send , T receive ), there is also a takeC i -action in (T send , T receive ). W.l.o.g., we assume that in the send-sequence the indices i are ascending. I.e. if putC i or takeC i is before putC j or takeC j , then i < j holds.
We often say translation instead of gstb-translation, if this is clear from the context. Definition 5.2. Let T = (T send , T receive ) be a gstb-translation. We write T x,y send for the program T send instantiated for xy, i.e. putS is putS x y, and all other operations are indexed with x. We write T x,y receive for the program T receive instantiated for x(y), i.e. takeS is takeS x y, and all other operations are indexed with x. The induced translations φ 0,T and φ T of (T send , T receive ) are defined in Fig. 7.
The induced translations are defined similar to the translations τ 0 and τ, where the differences are the representations of the channel. The translation of νx, x(y), and xy is different, but the other cases remain the same. Since φ 0,T (P) = C τ out [φ T (P)] and by the same arguments as in Theorem 4.8, we have: Proposition 5.3. If φ T is closed convergence-equivalent, then φ T is adequate.
An execution of a translation (T send , T receive ) for name x is the simulation of the abstract program, i.e. a program that starts with empty MVars x, x 1 , . . . , x n , and is an interleaved sequence of actions from the send and receive-sequence T send and T receive , respectively.
To speak about the translations we make further classifications: We say that a translation allows multiple uses, if a check-MVar is used more than once, i.e. the sender or receiver may contain takeC i or putC i more than once for the same i. A translation has the interprocess check restriction, if for every i: takeC i and putC i do not occur both in T send , and also not both in T receive . • communicating, if T send contains at least one takeC i -action; • overlap-free if for a fixed name x, starting with empty MVars, every interleaved (concurrent) execution of (T send , T receive ) cannot be disturbed by starting another execution of T send and/or T receive . More formally, let ((s 1 ; ...; s i ); (r 1 ; ....r j )) and ((s 1 ; ...; s i ); (r 1 ; ....r j )) be two copies of (T send , T receive ) for a fixed name x. We call a command a k from one of the four sequences, an a-action for a ∈ {s, s , r, r }. The translation T is overlap-free if every execution of the four sequences has the property that it can be split into a prefix and a suffix (called parts in the following) such that one of the following properties holds 1. One part contains only s-and r-actions, and the other part contains only s -and r -actions. 2. One part contains only s-and r -actions and the other part contains only s -and r-actions.
We implemented a tool to enumerate translations and to test whether each translation preserves and reflects may-and should-convergence for a (given) finite set of processes. Hence, our tool can refute the correctness of translations, but it can also output (usually small) sets of translations which are not refuted and which are promising candidates for correct translations. The above mentioned parallel execution of T send and T receive is not sufficient to refute most of the translations, since it corresponds to the evaluation of the π-program νx.(x(y)|xz) (which is must-divergent). Thus, we apply the translation to a subset of π-processes, which we view as critical and for which we can automatically decide may-and shouldconvergence (before and after the translation). We consider only π-programs of the form (νx 1 , . . . , x n .P) where P contains only 0, Stop, parallel composition, and input-and output-prefixes. These programs are replication free and the ν-binders are on the top, and hence terminate. In the following we omit the ν-binders, but always mean them to be present. We also implemented techniques to generates all such programs until a bound on the size of the program is reached.
Our simulation tool 4 can execute all possible evaluations of those π-processes and -since all evaluation paths are finite -the tool can check for may-and should-convergence of the π-program. For the translated program, we do not generate a full CH-program, but generate a sequence of sequences of takeS x , putS x , takeC i x , putC i x z and Stop-operations by applying the translation to all action prefixes in the π-program and by encoding Stop as Stop, 0 into an empty sequence. We get a sequence of sequences, since we have several threads and each thread is represented by one sequence. For executing the translated program, we simulate the global store (of MVars) and execute all possible interleavings where we check for may-and should-convergence by looking whether the Stop eventually occurs at the beginning of the sequence. This simulates the behavior of the real CH-program in a controllable manner.
With the encoding of the sender-and receiver program and a π-calculus process P we 1. translate P with the encodings in the sequence of sequences consisting of takeS x , putS x , takeC i x , putC i x z and Stop-operations; 2. simulate the execution on all interleavings; 3. test may-and should convergence of the original π-program P as well as the encoded program (w.r.t. the simulation); 4. compare the convergence before and after the translation. If there is a difference in the convergence behavior, then P is a counter-example for the correctness of the encodings.
Applying (T send , T receive ) to P yields the abstract program For q, our tool inspects all executions. Among them there is the sequence putC x ; takeC x ; putS x y; putC x ; takeS x z; Stop which can be executed ending in Stop. Thus q is may-convergent, and thus the process P is a counterexample that refutes the correctness of the translation.
The case that there is no check-MVar leads to one possible translation ([putS], [takeS]) which means that xz is translated into putS x y and x(y) is translated into takeS x y. This translation is not correct, since for instance the π-process xz.x(y).Stop is neither may-nor should-convergent, but the translation (written as an abstract program) is [[putS x z, takeS x y, Stop]]. I.e., it consists of one process which is may-and should-convergent (since putS x z; takeS x y; Stop is the only evaluation sequence and its execution ends in Stop). Note that the translation into CH will generate two threads: the main threads that will wait until the MVar stop is filled, and a concurrent thread that will do the above operations.

Translations with Interprocess Check Restriction
We consider translations with the interprocess check restriction (each takeC i and putC i must be distributed between the sender and the receiver). There are n! · 2 n · (n + 1) 2 Table 1, there are two further π-programs used as counterexample. However, also the programs xy.Stop|x(y) and xy.x(z).zq|x(z)| x(z)|xz|y(u).Stop suffice to refute all 72 translations.
Theorem 5.6. There is no valid gstb-translation with the interprocess check restriction for less than three check-MVars.
A reason for the failure of translations with less than three check-MVars may be: Theorem 5.7. There is no executable, communicating, and overlap-free gstb-translation with the interprocess check restriction for n < 3.

Translation (sender,receiver)
Counter-example (π-process)  Proof. We only consider overlaps. For T 1 -T 4 , only if all 8 actions are finished, the next send or receive can start. For T 5 , T 6 , after executing putC 1 , takeC 1 , we can again execute putC 1 .
In [29] we argue that the induced translation φ T 1 leaves may-and should-convergence invariant. The main help in reasoning is that there is no unintended interleaving of send and receive sequences according to Proposition 5.8. Application of Proposition 5.3 then shows: Theorem 5.9. Translation φ T 1 is adequate.
For 4 MVars, our tool refutes 9266 and there remain 334 candidates for correct translations.

Dropping the Interprocess Check Restriction
We now consider gstb-translations without the interprocess check restriction, i.e. putC i and takeC i both may occur in the sender-program (or the receiver program, resp.). If we allow one check-MVar without reuse, then there are 20 candidates for translations. All are refuted by our simulation. Allowing reuse of the single check-MVar seems not to help to construct a correct translation: We simulated this for up to 6 uses, leading to 420420 candidates for a correct translation -our simulation refutes all of them.
Conjecture 5.10. We conjecture that there is no correct translation for one check-MVar where re-uses are permitted and the interprocess check restriction is dropped, i.e., T send is a word over {putS, putC, takeC} and T receive a word over {takeS, putC, takeC}, where putS, takeS occur exactly once. 5 For two MVars, one use and without the interprocess check restriction there are 420 translations. Our tool refutes all except for two: T 7 = ([putC 1 , putS, takeC 2 , takeC 1 ], [takeS, putC 2 ]) and T 8 = ([takeC 1 , putS], [putC 2 , putC 1 , takeS, takeC 2 ]). In T 7 the second check-MVar is used as a mutex for the senders, ensuring that only one sender can operate at a time. T 8 does the same on the receiver side.
Proof. The translations are executable and communicating. For T 7 , putC 1 , putS and takeS are performed in this order. An additional sender cannot execute its first command before the original sender performs takeC 1 and this again is only possible after the receiver program is finished. An additional receiver can only be executed after a putS is performed, which cannot be done by the current sender and receivers. For T 8 , putC 2 , putC 1 and takeC 1 are performed in this order. An additional receiver can only start after takeC 2 was executed by the original receiver, which can only occur after the original sender and receiver program are fully evaluated. An additional sender can only start after putC 1 has been executed again, but the current sender and receiver cannot execute this command.
We are convinced that the same holds for T 8 . We conclude the statistics of our search for translations without the interprocess restriction: For 3 MVars, there are 10080 translations and 9992 are refuted, i.e. 98 are potentially correct. One is ([putC 1 , putS, takeC 2 , takeC 1 ], [putC 3 , takeS, putC 2 , takeC 3 ]) which is quite intuitive: check-MVar 1 is used as a mutex for all senders on the same channel, check-MVar 3 is used as a mutex for all receivers, and check-MVar 2 is used to send an acknowledgement. For