journal article
Open Access
Jul 30, 2018
Parallel complexity analysis with temporal session types
Proceedings of the ACM on Programming Languages
Vol. 2
No. ICFP
pp. 1-30
·
Association for Computing Machinery (ACM)
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.
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.
Topics
No keywords indexed for this article. Browse by subject →
References
42
[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. 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.
[3]
Stephanie Balzer and Frank Pfenning . 2017 . Manifest Sharing with Session Types. In International Conference on Functional Programming (ICFP). ACM, 37:1–37:29 . Stephanie Balzer and Frank Pfenning. 2017. Manifest Sharing with Session Types. In International Conference on Functional Programming (ICFP). ACM, 37:1–37:29.
[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. 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.
[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. 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.
[19]
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. 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]
[22]
[25]
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. 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.
[27]
[28]
[30]
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. 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]
Rumyana Neykova , Laura Bocchi , and Nobuko Yoshida . 2014 . Timed Runtime Monitoring for Multiparty Conversations. In 3rd International Workshop on Behavioural Types (BEAT 2014). Rumyana Neykova, Laura Bocchi, and Nobuko Yoshida. 2014. Timed Runtime Monitoring for Multiparty Conversations. In 3rd International Workshop on Behavioural Types (BEAT 2014).
[33]
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. 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.
10.1007/bfb0036940
[35]
[36]
Marc Pouzet. 2006. Lucid Synchrone Release version 3.0 Tutorial and Reference Manual. (2006). Marc Pouzet. 2006. Lucid Synchrone Release version 3.0 Tutorial and Reference Manual. (2006).
[38]
Miguel Silva , Mário Florido , and Frank Pfenning . 2016 . Non-Blocking Concurrent Imperative Programming with Session Types. In Fourth International Workshop on Linearity. Miguel Silva, Mário Florido, and Frank Pfenning. 2016. Non-Blocking Concurrent Imperative Programming with Session Types. In Fourth International Workshop on Linearity.
Cited By
19
Nested Session Types
ACM Transactions on Programming Lan...
Ankush Das, Henry Deyoung · 2022
Metrics
19
Citations
42
References
Details
- Published
- Jul 30, 2018
- Vol/Issue
- 2(ICFP)
- Pages
- 1-30
- License
- View
Authors
Cite This Article
Ankush Das, Jan Hoffmann, Frank Pfenning (2018). Parallel complexity analysis with temporal session types. Proceedings of the ACM on Programming Languages, 2(ICFP), 1-30. https://doi.org/10.1145/3236786
Related
You May Also Like
code2vec: learning distributed representations of code
Uri Alon, Meital Zilberstein · 2019
880 citations
Grounded Copilot: How Programmers Interact with Code-Generating Models
Shraddha Barke, Michael B. James · 2023
275 citations