Tue 17 Nov 2020 03:00 - 03:20 at SPLASH-I - M-5 Chair(s): Bernardo Toninho, Xiangzhe Xu
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.
Mon 16 NovDisplayed time zone: Central Time (US & Canada) change
15:00 - 16:20 | M-5OOPSLA at SPLASH-I +12h Chair(s): Jonathan Aldrich Carnegie Mellon University, Leonidas Lampropoulos University of Maryland, College Park | ||
15:00 20mTalk | CAMP: Cost-Aware Multiparty Session Protocols OOPSLA Link to publication DOI Media Attached | ||
15:20 20mTalk | Counterexample-Guided Correlation Algorithm for Translation Validation OOPSLA Link to publication DOI Media Attached | ||
15:40 20mTalk | Multiparty Motion Coordination: From Choreographies to Robotics Programs OOPSLA Link to publication DOI Media Attached | ||
16:00 20mTalk | On the Unusual Effectiveness of Type-Aware Operator Mutations for Testing SMT Solvers OOPSLA Link to publication DOI Media Attached |
Tue 17 NovDisplayed time zone: Central Time (US & Canada) change
03:00 - 04:20 | M-5OOPSLA at SPLASH-I Chair(s): Bernardo Toninho Nova University of Lisbon / NOVA-LINCS, Xiangzhe Xu Nanjing University | ||
03:00 20mTalk | CAMP: Cost-Aware Multiparty Session Protocols OOPSLA Link to publication DOI Media Attached | ||
03:20 20mTalk | Counterexample-Guided Correlation Algorithm for Translation Validation OOPSLA Link to publication DOI Media Attached | ||
03:40 20mTalk | Multiparty Motion Coordination: From Choreographies to Robotics Programs OOPSLA Link to publication DOI Media Attached | ||
04:00 20mTalk | On the Unusual Effectiveness of Type-Aware Operator Mutations for Testing SMT Solvers OOPSLA Link to publication DOI Media Attached |