一句话:提出 Oven:首个基于合成行为类型分析、在 Scala 中保障并发通信协议安全性与活性的实用工具集。
并发程序中线程间通信协议的安全性与活性难以保证,现有行为类型分析的表达力亦有局限。作者提出 Oven:一个 Scala 工具集,建立在其新近提出的合成行为类型(synthetic behavioural type analysis)理论基础上,用于在 Scala 现有类型系统中编码新的合成行为类型规则,从而检查线程间通信协议是否符合规约。论文介绍了 Oven 的用法,总结了设计与实现,并讨论了表达力的初步评估;结果表明,Oven 相较于两个最先进的工具具有改进,首次提供了其实用性与表达力优势的证据。
We present Oven: a toolset to assure safety and liveness of communication protocols among threads in concurrent programs in Scala. Oven is the first practical toolset that is built on top of new theoretical foundations of synthetic behavioural type analysis, recently developed by us to improve the expressiveness of existing work. We explain Oven's usage, summarise its design and implementation (main challenge: how to encode the new synthetic behavioural typing rules in Scala's existing type system), and discuss a preliminary evaluation of expressiveness (the results provide first evidence that Oven is an improvement over two state-of-the-art tools).