Sized Types with Usages for Parallel Complexity of Pi-Calculus Processes
Abstract
We address the problem of analysing the complexity of concurrent programs written in Pi-calculus. We are interested in parallel complexity, or span, understood as the execution time in a model with maximal parallelism. A type system for parallel complexity has been recently proposed by Baillot and Ghyselen but it is too imprecise for non-linear channels and cannot analyse some concurrent processes. Aiming for a more precise analysis, we design a type system which builds on the concepts of sized types and usages. The new variant of usages we define accounts for the various ways a channel is employed and relies on time annotations to track under which conditions processes can synchronize. We prove that a type derivation for a process provides an upper bound on its parallel complexity.
Cite
@article{arxiv.2104.07293,
title = {Sized Types with Usages for Parallel Complexity of Pi-Calculus Processes},
author = {Patrick Baillot and Alexis Ghyselen and Naoki Kobayashi},
journal= {arXiv preprint arXiv:2104.07293},
year = {2021}
}