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

Manfred Schmidt-Schauß
(Goethe-University, Frankfurt, Germany)
David Sabel
(LMU, Munich, Germany)

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.

In Ornela Dardha and Jurriaan Rot: Proceedings Combined 27th International Workshop on Expressiveness in Concurrency and 17th Workshop on Structural Operational Semantics (EXPRESS/SOS 2020), Online, 31 August 2020, Electronic Proceedings in Theoretical Computer Science 322, pp. 88–105.
Published: 27th August 2020.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: