协作调度进程的通信：实现纯CSP通道的难度

《Formal Aspects of Computing》：Communicating Cooperatively Scheduled Processes: On the Unlikelihood of Implementing a Pure CSP Channel

本文提出使用ProcessJ协同运行环境实现CSP启发的通信通道建模，并利用FDR工具验证其正确性，解决了现有ProcessJ运行时资源分配不足的问题。但研究指出，当硬件无法同时执行所有进程时，通道实现可能无法完全满足抽象规格要求，需综合考虑执行环境对行为的影响。

　　

摘要

本文介绍了ProcessJ协作运行时环境的建模，用于实现一种受CSP（ Communicative Sequential Process）启发的通信通道。我们使用了CSP工具FDR来验证ProcessJ运行时及其原语的正确性，展示了如何克服现有ProcessJ运行时中的局限性以改进其行为。然而，我们的研究也揭示了一个问题：当试图证明协作调度的通道实现符合CSP通道的抽象规范时，存在一定的局限性。我们的结论是：在没有足够的硬件能够同时执行所有进程的情况下，通道实现无法完全满足其规范要求，尤其是在考虑通道运行所处的执行环境时。我们确信ProcessJ通道能够正确工作，其他实现（如JCSP和CSO）也是如此；但由于在资源不足导致无法实现完全并发时可能会产生意外的优先级分配，因此我们无法保证在建模时可以使用纯CSP通道来替代ProcessJ通道或其他实现方式。我们的研究表明，必须考虑执行环境，因为这可能会导致在仅进行抽象建模时无法发现的行为问题。