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

TL;DR

This paper demonstrates how to correctly encode synchronous message passing from the pi-calculus using Concurrent Haskell's MVars, ensuring semantic correctness and exploring efficient translation strategies.

Contribution

It provides the first formal correctness proofs for encoding pi-calculus channels with Concurrent Haskell's MVars, including automated translation generation and validation.

Findings

CH can accurately model synchronous pi-calculus communication

Automated translation suggests one MVar may be insufficient for correctness

Experimental results support the need for additional synchronization MVars

Abstract

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.