Practical interruptible conversations: distributed dynamic verification with multiparty session types and Python
Practical interruptible conversations: distributed dynamic verification with multiparty session types and Python
复制标题
DOI：
10.1007/s10703-014-0218-8
复制
发表时间：
2015-06-01
影响因子：
0.8
通讯作者：
Yoshida, Nobuko
中科院分区：
文献类型：
--
作者：
Demangeon, Romain;Honda, Kohei;Yoshida, Nobuko
对基于通信的软件进行严格而全面的验证是分布式系统中一个重要的工程挑战。从我们的工业合作（海洋观测站倡议，JBoss Savara项目，关于Scribble，一种基于多方会话类型的编排描述语言及其理论基础（本田等人，in POPL，pp 273-284，2008），这篇文章提出了一种用于结构化可中断对话编程的动态验证框架。我们首先提出了我们的扩展Scribble支持异步中断对话的规范。然后，我们实现了一个简洁的API，用于在Python中使用中断进行会话编程，使会话类型属性能够为分布式进程进行动态验证。最后，我们揭示了中断机制的基本原理，研究了中断机制的语法和语义，以及中断机制与MPST理论的结合，证明了中断机制设计的正确性。我们的框架通过对每个端点进行独立的运行时监控，检查本地执行跟踪与指定协议的一致性，确保系统在存在异步中断的情况下的全局安全。我们的框架描述和验证编排通信的可用性已经通过集成到海洋观测站倡议开发的大型科学网络基础设施中进行了测试。异步中断已被证明具有足够的表达能力来表示和验证其主要通信模式类，包括异步流和各种基于超时的协议，而无需引入任何隐式同步。基准测试表明，会话编程和监控可以以很小的开销实现。
The rigorous and comprehensive verification of communication-based software is an important engineering challenge in distributed systems. Drawn from our industrial collaborations (Ocean Observatories Initative, JBoss Savara Project, on Scribble, a choreography description language based on multiparty session types, and its theoretical foundations (Honda et al., in POPL, pp 273-284, 2008), this article proposes a dynamic verification framework for structured interruptible conversation programming. We first present our extension of Scribble to support the specification of asynchronously interruptible conversations. We then implement a concise API for conversation programming with interrupts in Python that enables session types properties to be dynamically verified for distributed processes. Finally, we expose the underlying theory of our interrupt mechanism, studying its syntax and semantics, its integration in MPST theory and proving the correctness of our design. Our framework ensures the global safety of a system in the presence of asynchronous interrupts through independent runtime monitoring of each endpoint, checking the conformance of the local execution trace to the specified protocol. The usability of our framework for describing and verifying choreographic communications has been tested by integration into the large scientific cyberinfrastructure developed by the Ocean Observatories Initiative. Asynchronous interrupts have proven expressive enough to represent and verify their main classes of communication patterns, including asynchronous streaming and various timeout-based protocols, without introducing any implicit synchronisations. Benchmarks show conversation programming and monitoring can be realised with little overhead.