用并发Haskell的MVars正确实现Pi演算中的同步消息传递
Correctly Implementing Synchronous Message Passing in the Pi-Calculus By Concurrent Haskell's MVars
摘要：
并发程序设计语言的比较和并发环境下程序转换的正确性是本文研究的重点。作为标准，我们使用的上下文语义适应并发，在那里可能-以及应该-收敛观察。本文研究了并发Haskell（CH）核心语言与同步π演算的关系。上下文语义一方面对操作语义的细节给予宽容，另一方面对翻译后过程之间的相互作用提出了强烈的要求。我们的结果是，CH包含同步π演算。我们的主要任务是通过CH的并发原语（MVars）来发现和证明π演算通道编码的正确性。它们的行为类似于（阻塞）1位缓冲区，对共享内存进行建模。第一个开发的翻译使用一个额外的私人MVar的每一个通信。我们还自动生成和检查潜在的正确的翻译，重用MVar，其中一个MVar包含的消息和两个额外的MVar同步用于模拟一个通道的同步通信的pi演算。我们的自动实验结果导致推测，一个额外的MVar是不够的。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
