CAMP: cost-aware multiparty session protocols
CAMP: cost-aware multiparty session protocols
复制标题
DOI：
10.1145/3428223
复制
发表时间：
2020-09
影响因子：
--
通讯作者：
David Castro-Perez;N. Yoshida
中科院分区：
文献类型：
--
作者：
David Castro-Perez;N. Yoshida
本文提出了 CAMP，一种基于多方会话类型 (MPST) 理论的消息传递并发和分布式系统的新静态性能分析框架。了解并发和分布式系统的运行时性能对于识别瓶颈和优化机会非常重要。在消息传递设置中，这些瓶颈通常是通信开销和同步时间。尽管它很重要，但与验证外延属性（例如正确性）相比，对软件的这些内涵属性（例如性能）的推理很少受到关注。基于会话类型的行为协议规范不仅捕获并发和分布式系统的外延属性，还捕获内涵属性。 CAMP 通过通信延迟和本地计算成本（定义为估计执行时间）的注释来增强 MPST，我们用它们从协议描述中提取成本方程。 CAMP 还可以扩展来分析基于会话类型理论最新进展的异步通信优化。我们将我们的工具应用于不同的现有基准和文献中的用例，并使用各种通信协议，以 C、MPI-C、Scala、Go 和 OCaml 实现。我们的基准测试表明，在大多数情况下，我们预测实际执行成本的上限，误差小于 15%。
This paper presents CAMP, a new static performance analysis framework for message-passing concurrent and distributed systems, based on the theory of multiparty session types (MPST). Understanding the run-time performance of concurrent and distributed systems is of great importance for the identification of bottlenecks and optimisation opportunities. In the message-passing setting, these bottlenecks are generally communication overheads and synchronisation times. Despite its importance, reasoning about these intensional properties of software, such as performance, has received little attention, compared to verifying extensional properties, such as correctness. Behavioural protocol specifications based on sessions types capture not only extensional, but also intensional properties of concurrent and distributed systems. CAMP augments MPST with annotations of communication latency and local computation cost, defined as estimated execution times, that we use to extract cost equations from protocol descriptions. CAMP is also extendable to analyse asynchronous communication optimisation built on a recent advance of session type theories. We apply our tool to different existing benchmarks and use cases in the literature with a wide range of communication protocols, implemented in C, MPI-C, Scala, Go, and OCaml. Our benchmarks show that, in most of the cases, we predict an upper-bound on the real execution costs with < 15% error.