论文标题
通过并发的Haskell的MVARS正确实现通过Pi-Calculus传递的同步消息
Correctly Implementing Synchronous Message Passing in the Pi-Calculus By Concurrent Haskell's MVars
论文作者
论文摘要
该研究的重点是并发语言的并发语言的比较和程序转换的正确性。作为标准，我们使用适合并发的上下文语义，可以观察到可能以及应该观察到的收敛性。我们研究了同步PI-Calculus与并发Haskell（CH）的核心语言之间的关系。关于操作语义的细节，上下文语义是宽恕的，另一方面意味着对翻译后过程之间相互作用的强烈要求。我们的结果是CH包含同步Pi-Calculus。我们的主要任务是通过CH的并发原语（MVARS）找到并证明PI-Calculus通道编码的正确性。它们的行为就像（阻止）1位缓冲区建模共享内存。 第一个开发的翻译在每次通信中都使用额外的私人MVAR。我们还会自动生成和检查潜在的正确的翻译，以重复使用MVAR，其中一个MVAR包含消息，并使用两个其他用于同步的MVAR来模拟PI-Calculus中单个通道的同步通信。
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.
