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.
翻译:本文件介绍了CAMP,这是基于多会议类型理论的关于信息传递同时和分布的系统的一个新的静态业绩分析框架。了解同时和分布的系统的运行时间性能对于查明瓶颈和优化机会非常重要。在信息传递的设置中,这些瓶颈通常是通信间接费用和同步时间。尽管其重要性,关于软件这些强化特性的推理,例如性能,与核实扩展性(如正确性)相比,没有受到多少关注。基于会议类型的行为协议规格,不仅包括扩展性,而且还包括同时和分布的系统的强化性能。CAMP增加MPST,配有通信延迟性说明和当地计算成本(按估计执行时间定义),用于从协议描述中提取成本方程式。C、MPC、Scala、Go和分布式系统的强化性能性能。我们还可以根据近期会议类型理论的进展,分析无节制通信优化的通信功能。我们将工具应用于现有的不同基准,并在文献中使用范围广泛的通信协议案例,在C、MPI、Scala、Go、Go和O等15个案例中,我们用最精确的预测性基准,显示我们15个案例的上限。