发表机构
University of Basel（巴塞尔大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
针对Python中Unix风格管道实现繁琐及JavaScript推送流协议规范不完整的问题，本文用TLA⁺和TLC形式化精化该协议，提出改进规范，支持同步异步模块结合、无界缓冲流控、明确终止，并验证其正确性。
AI 中文摘要
协程以生成器、异步函数以及通过管道通信的进程等形式，已广泛渗透到并发编程实践中。我们希望使用Python中的协程来创建单线程的Unix风格管道。遗憾的是，Python中可用的解决方案使用起来很繁琐。JavaScript的推送流协议似乎是一个不错的替代方案。然而，其规范不完整且存在歧义。我们使用TLA$^{+}$和TLC模型检查器重新推导了该协议，并获得了针对特定协议的验证工具。在本文中，我们提出了一个推送流协议的形式化规范，该规范：1）无缝结合同步和异步模块，将选择封装在每个模块内部；2）无需有界缓冲区即可提供流控制；3）优雅且无歧义地终止；4）不需要在堆上动态分配对象。除了完整描述预期行为外，我们的规范还对原始设计进行了改进：1）允许中间管道模块的输入和输出独立终止；2）明确报告模块何时在等待执行环境，以避免错误的恢复执行。我们将该协议规范为一系列精化步骤，并通过等价性推导出抽象模块可能行为的规范。然后，我们将后者精化为一个模块检查器，用于验证具体模块规范的一致性。我们使用TLC验证了所有规范的关键属性以及精化步骤的有效性。在补充材料中，我们提供了所有TLA$^{+}$规范，展示了该协议具有足够的表达能力来实现所有原始JavaScript模块的超集，并与Python替代方案和Unix管道进行了性能比较。
英文摘要
The coroutine has broadly diffused in the practice of concurrent programming in the form of generators and asynchronous functions as well as processes communicating through pipes. We wanted to use coroutines in Python to create single-threaded Unix-style pipelines. Unfortunately, available solutions in Python are cumbersome to use. The JavaScript push-stream protocol appeared to be a good alternative. However, its specification is incomplete and ambiguous. We have used TLA$^{+}$ and the TLC model checker to re-derive the protocol and obtain protocol-specific verification tools. In this paper, we present a formal specification of a push-stream protocol that 1) seamlessly combines synchronous and asynchronous modules, encapsulating the choice within each module; 2) provides flow control without using bounded buffers; 3) gracefully and unambiguously terminates; 4) does not require dynamic allocation of objects on the heap. In addition to completely describing expected behaviours, our specification improves on the original design by 1) allowing the input and output of intermediate pipeline modules to terminate independently and 2) explicitly reporting when a module is pending on the execution environment, to avoid incorrect resuming. We specify the protocol as a sequence of refinement steps and derive by equivalence a specification of what an abstract module may do. We then refine the latter into a module checker that can verify concrete module specifications for conformity. We have verified the key properties of all specifications and the validity of refinement steps with TLC. In supplemental material, we provide all TLA$^{+}$ specifications, show that the protocol is sufficiently expressive to implement a superset of all original JavaScript modules, as well as a performance comparison with Python alternatives and Unix pipes.
