More Web Proxy on the site http://driver.im/

research-article

Open access

Parallel complexity analysis with temporal session types

Authors:

Frank PfenningAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 2, Issue ICFP

Article No.: 91, Pages 1 - 30

https://doi.org/10.1145/3236786

Published: 30 July 2018 Publication History

Abstract

We study the problem of parametric parallel complexity analysis of concurrent, message-passing programs. To make the analysis local and compositional, it is based on a conservative extension of binary session types, which structure the type and direction of communication between processes and stand in a Curry-Howard correspondence with intuitionistic linear logic. The main innovation is to enrich session types with the temporal modalities next (◯ A), always (□ A), and eventually (◇ A), to additionally prescribe the timing of the exchanged messages in a way that is precise yet flexible. The resulting temporal session types uniformly express properties such as the message rate of a stream, the latency of a pipeline, the response time of a concurrent queue, or the span of a fork/join parallel program. The analysis is parametric in the cost model and the presentation focuses on communication cost as a concrete example. The soundness of the analysis is established by proofs of progress and type preservation using a timed multiset rewriting semantics. Representative examples illustrate the scope and usability of the approach.

Supplementary Material

WEBM File (a91-das.webm)

Download
94.37 MB

References

[1]

Elvira Albert, Jesús Correas, Einar Broch Johnsen, and Guillermo Román-Díez. 2015. Parallel Cost Analysis of Distributed Systems. In Static Analysis, Sandrine Blazy and Thomas Jensen (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 275–292.

[2]

Martin Avanzini, Ugo Dal Lago, and Georg Moser. 2015. Analysing the Complexity of Functional Programs: Higher-Order Meets First-Order. In 29th Int. Conf. on Functional Programming (ICFP’15).

Digital Library

[3]

Stephanie Balzer and Frank Pfenning. 2017. Manifest Sharing with Session Types. In International Conference on Functional Programming (ICFP). ACM, 37:1–37:29.

[4]

Gérard Berry and Georges Gonthier. 1992. The ESTEREL Synchronous Programming Language: Design, Semantics, Implementation. Sci. Comput. Program. 19, 2 (Nov. 1992), 87–152.

Digital Library

[5]

Guy E. Blelloch and Margaret Reid-Miller. 1997. Pipelining with Futures. In Proceedings of the Ninth Annual ACM Symposium on Parallel Algorithms and Architectures (SPAA ’97). ACM, New York, NY, USA, 249–259.

Digital Library

[6]

Laura Bocchi, Weizhen Yang, and Nobuko Yoshida. 2014. Timed Multiparty Session Types. In CONCUR 2014 – Concurrency Theory, Paolo Baldan and Daniele Gorla (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 419–434.

[7]

Luís Caires, Jorge A. Pérez, Frank Pfenning, and Bernardo Toninho. 2013. Behavioral Polymorphism and Parametricity in Session-Based Communication. In Proceedings of the European Symposium on Programming (ESOP’13), M.Felleisen and P.Gardner (Eds.). Springer LNCS 7792, Rome, Italy, 330–349.

Digital Library

[8]

Luís Caires and Frank Pfenning. 2010. Session Types as Intuitionistic Linear Propositions. In Proceedings of the 21st International Conference on Concurrency Theory (CONCUR 2010). Springer LNCS 6269, Paris, France, 222–236.

Digital Library

[9]

Luís Caires, Frank Pfenning, and Bernardo Toninho. 2016. Linear Logic Propositions as Session Types. Mathematical Structures in Computer Science 26, 3 (2016), 367–423.

[10]

Iliano Cervesato and Andre Scedrov. 2009. Relating State-Based and Process-Based Concurrency through Linear Logic. Information and Computation 207, 10 (Oct. 2009), 1044–1077.

Digital Library

[11]

Norman Danner, Daniel R. Licata, and Ramyaa Ramyaa. 2015. Denotational Cost Semantics for Functional Languages with Inductive Types. In 29th Int. Conf. on Functional Programming (ICFP’15).

Digital Library

[12]

Ankush Das, Jan Hoffmann, and Frank Pfenning. 2017. Work Analysis with Resource-Aware Session Types. CoRR abs/1712.08310 (2017). arXiv: 1712.08310 http://arxiv.org/abs/1712.08310

Digital Library

[13]

Rowan Davies. 1996. A Temporal Logic Approach to Binding-Time Analysis. In Proceedings of the Eleventh Annual Symposium on Logic in Computer Science, E. Clarke (Ed.). IEEE Computer Society Press, New Brunswick, New Jersey, 184–195. http://www.cs.cmu.edu/afs/cs/user/rowan/www/papers/multbta.ps.Z

Digital Library

[14]

Nicolas Feltman, Carlo Angiuli, Umut Acar, and Kayvon Fatahalian. 2016. Automatically Splitting a Two-Stage Lambda Calculus. In Proceedings of the 25th European Symposium on Programming (ESOP), P. Thiemann (Ed.). Springer LNCS 9632, Eindhoven, The Netherlands, 255–281.

Digital Library

[15]

Jérôme Fortier and Luigi Santocanale. 2013. Cuts for Circular Proofs: Semantics and Cut Elimination. In 22nd Conference on Computer Science Logic (LIPIcs), Vol. 23. 248–262.

[16]

Simon J. Gay and Malcolm Hole. 2005. Subtyping for Session Types in the π -Calculus. Acta Informatica 42, 2–3 (2005), 191–225.

[17]

Dan R. Ghica and Alex I. Smith. 2014. Bounded Linear Types in a Resource Semiring. In Proceedings of the 23rd European Symposium on Programming Languages and Systems - Volume 8410. Springer-Verlag New York, Inc., New York, NY, USA, 331–350.

Digital Library

[18]

Stéphane Gimenez and Georg Moser. 2016. The Complexity of Interaction. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’16). ACM, New York, NY, USA, 243–255.

Digital Library

[19]

Dennis Griffith. 2016. Polarized Substructural Session Types. Ph.D. Dissertation. University of Illinois at Urbana-Champaign.

[20]

Dennis Griffith and Elsa L. Gunter. 2013. Liquid Pi: Inferrable Dependent Session Types. In Proceedings of the NASA Formal Methods Symposium. Springer LNCS 7871, 186–197.

[21]

Sumit Gulwani, Krishna K. Mehra, and Trishul M. Chilimbi. 2009. SPEED: Precise and Efficient Static Estimation of Program Computational Complexity. In 36th ACM Symp. on Principles of Prog. Langs. (POPL’09). 127–139.

Digital Library

[22]

N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud. 1991. The synchronous data flow programming language LUSTRE. Proc. IEEE 79, 9 (Sep 1991), 1305–1320.

[23]

Robert H. Halstead, Jr. 1985. MULTILISP: A Language for Concurrent Symbolic Computation. ACM Trans. Program. Lang. Syst. 7, 4 (Oct. 1985), 501–538.

Digital Library

[24]

Jan Hoffmann, Ankush Das, and Shu-Chun Weng. 2017. Towards Automatic Resource Bound Analysis for OCaml. In 44th Symposium on Principles of Programming Languages (POPL’17).

Digital Library

[25]

Jan Hoffmann and Zhong Shao. 2015. Automatic Static Cost Analysis for Parallel Programs. In Proceedings of the 24th European Symposium on Programming on Programming Languages and Systems - Volume 9032. Springer-Verlag New York, Inc., New York, NY, USA, 132–157.

Digital Library

[26]

Kohei Honda, Vasco T. Vasconcelos, and Makoto Kubo. 1998. Language Primitives and Type Discipline for Structured Communication-Based Programming. In 7th European Symposium on Programming Languages and Systems (ESOP’98). Springer LNCS 1381, 122–138.

Digital Library

[27]

Naoki Kobayashi. 2002. A Type System for Lock-Free Processes. Information and Computation 177 (2002), 122–159.

Digital Library

[28]

Neelakantan R. Krishnaswami and Nick Benton. 2011. Ultrametric Semantics of Reactive Programs. In 26th IEEE Symposium on Logic in Computer Science, (LICS’11). 257–266.

Digital Library

[29]

Ugo Dal Lago and Marco Gaboardi. 2011. Linear Dependent Types and Relative Completeness. In 26th IEEE Symp. on Logic in Computer Science (LICS’11). 133–142.

Digital Library

[30]

Julien Lange and Nobuko Yoshida. 2017. On the Undecidability of Asynchronous Session Subtyping. In Proceedings of the 20th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS). Springer LNCS 10203, 441–457.

Digital Library

[31]

Hugo A. López, Carlos Olarte, and Jorge A. Pérez. 2009. Towards a Unified Framework for Declarative Structure Communications. In Proceedings of the Workshop on Programming Language Approaches to Concurrency and Communication-Centric Software (PLACES), A. Beresford and S. Gay (Eds.). EPTCS 17, 1–15.

[32]

Hiroshi Nakano. 2000. A Modality for Recursion. In 15th IEEE Symposium on Logic in Computer Science (LICS’00). 255–266.

Digital Library

[33]

Rumyana Neykova, Laura Bocchi, and Nobuko Yoshida. 2014. Timed Runtime Monitoring for Multiparty Conversations. In 3rd International Workshop on Behavioural Types (BEAT 2014).

[34]

W. Paul, U. Vishkin, and H. Wagener. 1983. Parallel dictionaries on 2–3 trees. In Automata, Languages and Programming, Josep Diaz (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 597–609.

Digital Library

[35]

Frank Pfenning and Dennis Griffith. 2015. Polarized Substructural Session Types. In Proceedings of the 18th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2015), A. Pitts (Ed.). Springer LNCS 9034, London, England, 3–22. Invited talk.

[36]

Amir Pnueli. 1977. The Temporal Logic of Programs. In Proceedings of the 18th Symposium on Foundations of Computer Science (FOCS’77). IEEE Computer Society, 46–57.

Digital Library

[37]

Marc Pouzet. 2006. Lucid Synchrone Release, version 3.0 Tutorial and Reference Manual. (2006).

[38]

Neda Saeedloei and Gopal Gupta. 2014. Timed π -Calculus. In 8th International Symposium on Trustworthy Global Computing - Volume 8358 (TGC 2013). Springer-Verlag New York, Inc., New York, NY, USA, 119–135.

[39]

Miguel Silva, Mário Florido, and Frank Pfenning. 2016. Non-Blocking Concurrent Imperative Programming with Session Types. In Fourth International Workshop on Linearity.

[40]

Bernardo Toninho, Luís Caires, and Frank Pfenning. 2013. Higher-Order Processes, Functions, and Sessions: A Monadic Integration. In Proceedings of the European Symposium on Programming (ESOP’13), M.Felleisen and P.Gardner (Eds.). Springer LNCS 7792, Rome, Italy, 350–369.

Digital Library

[41]

Bernardo Toninho, Luís Caires, and Frank Pfenning. 2014. Corecursion and Non-Divergence in Session-Typed Processes. In Proceedings of the 9th International Symposium on Trustworthy Global Computing (TGC 2014), M. Maffei and E. Tuosto (Eds.). Springer LNCS 8902, Rome, Italy, 159–175.

[42]

Philip Wadler. 2012. Propositions as Sessions. In Proceedings of the 17th International Conference on Functional Programming (ICFP 2012). ACM Press, Copenhagen, Denmark, 273–286.

Digital Library

[43]

Ezgi Çiçek, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Jan Hoffmann. 2017. Relational Cost Analysis. In 44th Symposium on Principles of Programming Languages (POPL’17).

Digital Library

Cited By

Yao YIraci GChuang CBalzer SZiarek L(2025)Semantic Logical Relations for Timed Message-Passing ProtocolsProceedings of the ACM on Programming Languages10.1145/37048959:POPL(1750-1781)Online publication date: 9-Jan-2025
https://doi.org/10.1145/3704895
Colledan ADal Lago U(2025)Flexible Type-Based Resource Estimation in Quantum Circuit Description LanguagesProceedings of the ACM on Programming Languages10.1145/37048839:POPL(1386-1416)Online publication date: 9-Jan-2025
https://dl.acm.org/doi/10.1145/3704883
Iraci GChuang CHu RZiarek L(2023)Validating IoT Devices with Rate-Based Session TypesProceedings of the ACM on Programming Languages10.1145/36228547:OOPSLA2(1589-1617)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622854
Show More Cited By

Index Terms

Parallel complexity analysis with temporal session types
1. Theory of computation
  1. Logic
    1. Linear logic
    2. Modal and temporal logics
  2. Models of computation
    1. Concurrency

Recommendations

Work Analysis with Resource-Aware Session Types
LICS '18: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science

While there exist several successful techniques for supporting programmers in deriving static resource bounds for sequential code, analyzing the resource usage of message-passing concurrent processes poses additional challenges. To meet these challenges,...
Mechanizing Session-Types using a Structural View: Enforcing Linearity without Linearity

Session types employ a linear type system that ensures that communication channels cannot be implicitly copied or discarded. As a result, many mechanizations of these systems require modeling channel contexts and carefully ensuring that they treat ...
Intrinsically-Typed Mechanized Semantics for Session Types
PPDP '19: Proceedings of the 21st International Symposium on Principles and Practice of Declarative Programming

Session types have emerged as a powerful paradigm for structuring communication-based programs. They guarantee type soundness and session fidelity for concurrent programs with sophisticated communication protocols. As type soundness proofs for languages ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 2, Issue ICFP

September 2018

1133 pages

EISSN:2475-1421

DOI:10.1145/3243631

Issue’s Table of Contents

Copyright © 2018 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 30 July 2018

Published in PACMPL Volume 2, Issue ICFP

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

17
Total Citations
View Citations
609
Total Downloads

Downloads (Last 12 months)90
Downloads (Last 6 weeks)15

Reflects downloads up to 02 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Yao YIraci GChuang CBalzer SZiarek L(2025)Semantic Logical Relations for Timed Message-Passing ProtocolsProceedings of the ACM on Programming Languages10.1145/37048959:POPL(1750-1781)Online publication date: 9-Jan-2025
https://doi.org/10.1145/3704895
Colledan ADal Lago U(2025)Flexible Type-Based Resource Estimation in Quantum Circuit Description LanguagesProceedings of the ACM on Programming Languages10.1145/37048839:POPL(1386-1416)Online publication date: 9-Jan-2025
https://dl.acm.org/doi/10.1145/3704883
Iraci GChuang CHu RZiarek L(2023)Validating IoT Devices with Rate-Based Session TypesProceedings of the ACM on Programming Languages10.1145/36228547:OOPSLA2(1589-1617)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622854
De Sá LToninho BPfenning F(2023)Intuitionistic Metric Temporal LogicProceedings of the 25th International Symposium on Principles and Practice of Declarative Programming10.1145/3610612.3610621(1-13)Online publication date: 22-Oct-2023
https://dl.acm.org/doi/10.1145/3610612.3610621
Nigam RAzevedo de Amorim PSampson A(2023)Modular Hardware Design with Timeline TypesProceedings of the ACM on Programming Languages10.1145/35912347:PLDI(343-367)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591234
Murgia MPinciroli RTrubiani CTuosto E(2023)Comparing perfomance abstractions for collective adaptive systemsInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-023-00728-925:5-6(785-798)Online publication date: 1-Dec-2023
https://dl.acm.org/doi/10.1007/s10009-023-00728-9
Das ADeyoung HMordido APfenning F(2022)Nested Session TypesACM Transactions on Programming Languages and Systems10.1145/353965644:3(1-45)Online publication date: 15-Jul-2022
https://dl.acm.org/doi/10.1145/3539656
Niu YSterling JGrodin HHarper R(2022)A cost-aware logical frameworkProceedings of the ACM on Programming Languages10.1145/34986706:POPL(1-31)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498670
Baillot PGhyselen A(2022)Types for Complexity of Parallel Computation in Pi-calculusACM Transactions on Programming Languages and Systems10.1145/349552944:3(1-50)Online publication date: 15-Jul-2022
https://dl.acm.org/doi/10.1145/3495529
Murgia MPinciroli RTrubiani CTuosto E(2022)On Model-Based Performance Analysis of Collective Adaptive SystemsLeveraging Applications of Formal Methods, Verification and Validation. Adaptation and Learning10.1007/978-3-031-19759-8_17(266-282)Online publication date: 17-Oct-2022
https://doi.org/10.1007/978-3-031-19759-8_17
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Figures

Tables

Media

View Issue’s Table of Contents