具有隐式和显式同步的无竞争信道的自动模块验证
Automated Modular Verification for Race-Free Channels with Implicit and Explicit Synchronization
摘要：
确保以通信为中心的程序的软件的正确性是重要的，但具有挑战性。在过去的十年中，基于会话类型的先前方法已经被深入研究。它们提供了一种简洁的方式来表达协议规范，并提供了一种轻量级的方法来检查它们的实现。当前的解决方案仅基于隐式同步，并且基于不太精确的类型而不是逻辑公式。在本文中，我们提出了一个更具表现力的会话逻辑来捕获多方协议。通过使用两种排序约束，即“happens-before”<HB和“communicates-before”<CB，我们展示了如何从第一原理确保公共信道上的竞争自由。我们的方法通过假设和证明义务来细化每个规范，以确保符合某些全球协议。然后，每个规范都被投射到每个参与方，然后是每个通道，以允许通过本地化自动验证进行合作证明。我们在自动化验证中的主要目标是确保竞争自由和通信安全，但该方法也可以扩展为无死锁。我们还将描述如何模块化协议可以捕获和处理我们的方法。
英文摘要：
Ensuring the correctness of software for communication centric programs is important but challenging. Previous approaches, based on session types, have been intensively investigated over the past decade. They provide a concise way to express protocol specifications and a lightweight approach for checking their implementation. Current solutions are based on only implicit synchronization, and are based on the less precise types rather than logical formulae. In this paper, we propose a more expressive session logic to capture multiparty protocols. By using two kinds of ordering constraints, namely "happens-before" <HB and "communicates-before" <CB, we show how to ensure from first principle race-freedom over common channels. Our approach refines each specification with both assumptions and proof obligations to ensure compliance to some global protocol. Each specification is then projected for each party and then each channel, to allow cooperative proving through localized automated verification. Our primary goal in automated verification is to ensure race-freedom and communication-safety, but the approach is extensible for deadlock-freedom as well. We shall also describe how modular protocols can be captured and handled by our approach.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
