Document Open Access Logo

Sized Types with Usages for Parallel Complexity of Pi-Calculus Processes

Authors Patrick Baillot, Alexis Ghyselen, Naoki Kobayashi

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2021.34.pdf
  • Filesize: 0.88 MB
  • 22 pages

Document Identifiers

Author Details

Patrick Baillot
  • Univ Lyon, CNRS, ENS de Lyon, Universite Claude-Bernard Lyon 1, LIP, F-69342, France
Alexis Ghyselen
  • Univ Lyon, CNRS, ENS de Lyon, Universite Claude-Bernard Lyon 1, LIP, F-69342, France
Naoki Kobayashi
  • The University of Tokyo, Japan

Funding

This work was partially supported by the LABEX MILYON (ANR-10-LABX-0070) of Universite de Lyon and JSPS KAKENHI Grant Number JP20H05703.

Acknowledgements

We would like to thank anonymous referees for useful comments.

Cite AsGet BibTex

Patrick Baillot, Alexis Ghyselen, and Naoki Kobayashi. Sized Types with Usages for Parallel Complexity of Pi-Calculus Processes. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 34:1-34:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.CONCUR.2021.34

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 the first two authors 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 sized types allow us to parametrize the complexity by the size of inputs, and the usages allow us to achieve a kind of rely-guarantee reasoning on the timing each process communicates with its environment. We prove that our new type system soundly estimates the parallel complexity, and show through examples that it is often more precise than the previous type system of the first two authors.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type structures
  • Theory of computation → Process calculi
  • Software and its engineering → Software verification
Keywords
  • Type Systems
  • Pi-calculus
  • Process Calculi
  • Complexity Analysis
  • Usages
  • Sized Types

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Elvira Albert, Jesús Correas, Einar Broch Johnsen, and Guillermo Román-Díez. Parallel cost analysis of distributed systems. In Static Analysis - 22nd International Symposium, SAS 2015, Saint-Malo, France, September 9-11, 2015, Proceedings, volume 9291 of Lecture Notes in Computer Science, pages 275-292. Springer, 2015. Google Scholar
  2. Elvira Albert, Antonio Flores-Montoya, Samir Genaim, and Enrique Martin-Martin. Rely-guarantee termination and cost analyses of loops with concurrent interleavings. Journal of Automated Reasoning, 59(1):47-85, 2017. Google Scholar
  3. Martin Avanzini and Ugo Dal Lago. Automating sized-type inference for complexity analysis. Proceedings of the ACM on Programming Languages, 1(ICFP):43, 2017. Google Scholar
  4. Patrick Baillot and Alexis Ghyselen. Types for complexity of parallel computation in pi-calculus. In Programming Languages and Systems - 30th European Symposium on Programming, ESOP 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, volume 12648 of Lecture Notes in Computer Science, pages 59-86. Springer, 2021. Google Scholar
  5. David Castro-Perez and Nobuko Yoshida. CAMP: cost-aware multiparty session protocols. Proc. ACM Program. Lang., 4(OOPSLA):155:1-155:30, 2020. Google Scholar
  6. Ugo Dal Lago and Marco Gaboardi. Linear dependent types and relative completeness. In Logic in Computer Science (LICS), 2011 26th Annual IEEE Symposium on, pages 133-142. IEEE, 2011. Google Scholar
  7. Ugo Dal Lago, Simone Martini, and Davide Sangiorgi. Light logics and higher-order processes. Mathematical Structures in Computer Science, 26(6):969-992, 2016. Google Scholar
  8. Ornela Dardha, Elena Giachino, and Davide Sangiorgi. Session types revisited. Information and Computation, 256:253-286, 2017. Google Scholar
  9. Ankush Das, Jan Hoffmann, and Frank Pfenning. Parallel complexity analysis with temporal session types. Proc. ACM Program. Lang., 2(ICFP):91:1-91:30, 2018. Google Scholar
  10. Ankush Das, Jan Hoffmann, and Frank Pfenning. Work analysis with resource-aware session types. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 305-314. ACM, 2018. Google Scholar
  11. Romain Demangeon, Daniel Hirschkoff, Naoki Kobayashi, and Davide Sangiorgi. On the complexity of termination inference for processes. In Gilles Barthe and Cédric Fournet, editors, Trustworthy Global Computing, Third Symposium, TGC 2007, Sophia-Antipolis, France, November 5-6, 2007, Revised Selected Papers, volume 4912 of Lecture Notes in Computer Science, pages 140-155. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-78663-4_11.
  12. Romain Demangeon and Nobuko Yoshida. Causal computational complexity of distributed processes. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '18, pages 344-353. ACM, 2018. Google Scholar
  13. Yuxin Deng and Davide Sangiorgi. Ensuring termination by typability. Information and Computation, 204(7):1045-1082, 2006. Google Scholar
  14. Paolo Di Giamberardino and Ugo Dal Lago. On session types and polynomial time. Mathematical Structures in Computer Science, -1, 2015. Google Scholar
  15. Elena Giachino, Einar Broch Johnsen, Cosimo Laneve, and Ka I Pun. Time complexity of concurrent programs - - A technique based on behavioural types -. In Formal Aspects of Component Software - 12th International Conference, FACS 2015, Niterói, Brazil, October 14-16, 2015, Revised Selected Papers, volume 9539 of Lecture Notes in Computer Science, pages 199-216. Springer, 2016. Google Scholar
  16. Stéphane Gimenez and Georg Moser. The complexity of interaction. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, pages 243-255, 2016. Google Scholar
  17. Jan Hoffmann, Klaus Aehlig, and Martin Hofmann. Multivariate amortized resource analysis. ACM Trans. Program. Lang. Syst., 34(3):14:1-14:62, 2012. Google Scholar
  18. Jan Hoffmann, Klaus Aehlig, and Martin Hofmann. Resource aware ML. In Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings, volume 7358 of Lecture Notes in Computer Science, pages 781-786. Springer, 2012. Google Scholar
  19. Jan Hoffmann and Martin Hofmann. Amortized resource analysis with polynomial potential. In Programming Languages and Systems, 19th European Symposium on Programming, ESOP 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings, volume 6012 of Lecture Notes in Computer Science, pages 287-306. Springer, 2010. Google Scholar
  20. Jan Hoffmann and Zhong Shao. Automatic static cost analysis for parallel programs. In Jan Vitek, editor, Programming Languages and Systems, pages 132-157, Berlin, Heidelberg, 2015. Springer Berlin Heidelberg. Google Scholar
  21. Martin Hofmann and Steffen Jost. Static prediction of heap space usage for first-order functional programs. In Conference Record of POPL 2003: The 30th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, New Orleans, Louisisana, USA, January 15-17, 2003, pages 185-197. ACM, 2003. Google Scholar
  22. Naoki Kobayashi. A partially deadlock-free typed process calculus. In Proceedings, 12th Annual IEEE Symposium on Logic in Computer Science, Warsaw, Poland, June 29 - July 2, 1997, pages 128-139. IEEE Computer Society, 1997. URL: https://doi.org/10.1109/LICS.1997.614941.
  23. Naoki Kobayashi. A type system for lock-free processes. Information and Computation, 177(2):122-159, 2002. Google Scholar
  24. Naoki Kobayashi. Type systems for concurrent programs. In Formal Methods at the Crossroads. From Panacea to Foundational Support, pages 439-453. Springer, 2003. Google Scholar
  25. Naoki Kobayashi. Type-based information flow analysis for the π-calculus. Acta Informatica, 42(4-5):291-347, 2005. Google Scholar
  26. Naoki Kobayashi. A new type system for deadlock-free processes. In International Conference on Concurrency Theory, pages 233-247. Springer, 2006. Google Scholar
  27. Naoki Kobayashi, Shin Saito, and Eijiro Sumii. An implicitly-typed deadlock-free process calculus. In Catuscia Palamidessi, editor, CONCUR 2000 - Concurrency Theory, pages 489-504. Springer Berlin Heidelberg, 2000. Google Scholar
  28. Antoine Madet and Roberto M. Amadio. An elementary affine λ-calculus with multithreading and side effects. In Typed Lambda Calculi and Applications - 10th International Conference, TLCA 2011, Novi Sad, Serbia, June 1-3, 2011. Proceedings, volume 6690 of Lecture Notes in Computer Science, pages 138-152. Springer, 2011. Google Scholar
  29. Robin Milner. Communication and concurrency. PHI Series in computer science. Prentice Hall, 1989. Google Scholar
  30. Eijiro Sumii and Naoki Kobayashi. A generalized deadlock-free process calculus. In Proc. of Workshop on High-Level Concurrent Language (HLCL'98), volume 16(3) of ENTCS, pages 55-77, 1998. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact