CAMP: Cost-Aware Multiparty Session Protocols

摘要: 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 run-time systems is great importance identification bottlenecks optimisation opportunities. In setting, these are generally communication overheads synchronisation times. Despite its importance, reasoning about intensional properties software, such as performance, has received little attention, compared to verifying extensional properties, correctness. Behavioural protocol specifications sessions capture not only extensional, but also systems. CAMP augments MPST with annotations latency local computation cost, defined estimated execution times, that we use extract cost equations from descriptions. extendable analyse asynchronous built recent advance type theories. We apply our tool different existing benchmarks cases in literature wide range protocols, implemented C, MPI-C, Scala, Go, OCaml. Our show that, most cases, predict an upper-bound real costs < 15% error.