| | |
| | |
Stat |
Members: 3645 Articles: 2'504'585 Articles rated: 2609
25 April 2024 |
|
| | | |
|
Article overview
| |
|
Correctly Implementing Synchronous Message Passing in the Pi-Calculus By Concurrent Haskell's MVars | Manfred Schmidt-Schauß
; David Sabel
; | Date: |
31 Aug 2020 | 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. | Source: | arXiv, 2008.13359 | Services: | Forum | Review | PDF | Favorites |
|
|
No review found.
Did you like this article?
Note: answers to reviews or questions about the article must be posted in the forum section.
Authors are not allowed to review their own article. They can use the forum section.
browser Mozilla/5.0 AppleWebKit/537.36 (KHTML, like Gecko; compatible; ClaudeBot/1.0; +claudebot@anthropic.com)
|
| |
|
|
|
| News, job offers and information for researchers and scientists:
| |