CAMP: cost-aware multiparty session protocols
File(s)3428223.pdf (901.08 KB)
Published version
Author(s)
Castro-Perez, David
Yoshida, Nobuko
Type
Conference Paper
Abstract
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 runtime 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.
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.
Date Issued
2020-11-01
Date Acceptance
2020-10-01
Citation
Proceedings of the ACM on Programming Languages, 2020, 4
ISSN
2475-1421
Publisher
Association for Computing Machinery (ACM)
Journal / Book Title
Proceedings of the ACM on Programming Languages
Volume
4
Copyright Statement
© 2020 Owner/Author(s). This work is licensed under a Creative Commons Attribution 4.0 International License (https://creativecommons.org/licenses/by/4.0/)
Sponsor
Engineering & Physical Science Research Council (EPSRC)
Engineering & Physical Science Research Council (EPSRC)
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (EPSRC)
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (EPSRC)
GCHQ
The National Cyber Security Centre (NCSC)
Engineering and Physical Sciences Research Council
Engineering & Physical Science Research Council (E
Grant Number
EP/T006544/1
EP/K011715/1
ERI 025567 (EP/K034413/1)
PO 20131167
EP/N027833/1
20103649
EP/T014709/1
4207702 / RFA 15845
4214176 / RFA 20601
EP/V000462/1
EP/V000462/1
Source
OOPSLA 2020
Publication Status
Published
Start Date
2020-11-15
Finish Date
2020-11-20
Coverage Spatial
Online