Document Open Access Logo

Concurrent Reversible Sessions

Authors Ilaria Castellani, Mariangiola Dezani-Ciancaglini, Paola Giannini

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2017.30.pdf
  • Filesize: 0.75 MB
  • 17 pages

Document Identifiers

Subject Classification

Keywords
  • Communication-centric Systems
  • Reversible Computation
  • Process Calculi
  • Multiparty Session Types

Metrics

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

Abstract

We present a calculus for concurrent reversible multiparty sessions, which improves on recent proposals in several respects: it allows for concurrent and sequential composition within processes and types, it gives a compact representation of the past of processes and types, which facilitates the definition of rollback, and it implements a fine-tuned strategy for backward computation. We propose a refined session type system for our calculus and show that it enforces the expected properties of session fidelity, forward and backward progress, as well as causal consistency. In conclusion, our calculus is a conservative extension of previous proposals, offering enhanced expressive power and refined analysis techniques.

Cite As Get BibTex

Ilaria Castellani, Mariangiola Dezani-Ciancaglini, and Paola Giannini. Concurrent Reversible Sessions. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 30:1-30:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.CONCUR.2017.30

Author Details

Ilaria Castellani
Mariangiola Dezani-Ciancaglini
Paola Giannini

References

  1. Franco Barbanera and Ugo de' Liguoro. Sub-behaviour relations for session-based client/server systems. Mathematical Structures in Computer Science, 25(6):1339-1381, 2015. URL: http://dx.doi.org/10.1017/S096012951400005X.
  2. Franco Barbanera, Mariangiola Dezani-Ciancaglini, and Ugo de'Liguoro. Reversible client/server interactions. Formal Aspects of Computing, 28(4):697-722, 2016. URL: http://dx.doi.org/10.1007/s00165-016-0358-2.
  3. Franco Barbanera, Mariangiola Dezani-Ciancaglini, Ivan Lanese, and Ugo de' Liguoro. Retractable contracts. In PLACES, volume 203 of EPTCS, pages 61-72, 2016. URL: http://dx.doi.org/10.4204/EPTCS.203.
  4. Giovanni Bernardi and Matthew Hennessy. Modelling session types using contracts. Mathematical Structures in Computer Science, 26(3):510-560, 2016. URL: http://dx.doi.org/10.1017/S0960129514000243.
  5. Gérard Boudol and Ilaria Castellani. Permutation of transitions: an event structure semantics for CCS and SCCS. In REX, volume 354 of LNCS, pages 411-427. Springer, 1988. URL: http://dx.doi.org/10.1007/BFb0013028.
  6. Gérard Boudol and Ilaria Castellani. Flow models of distributed computations: three equivalent semantics for CCS. Information and Computation, 114(2):247-314, 1994. URL: http://dx.doi.org/10.1006/inco.1994.1088.
  7. Giuseppe Castagna, Mariangiola Dezani-Ciancaglini, and Luca Padovani. On Global Types and Multi-Party Sessions. Logical Methods in Computer Science, 8:1-45, 2012. URL: http://dx.doi.org/10.2168/LMCS-8(1:24)2012.
  8. Ioana Cristescu, Jean Krivine, and Daniele Varacca. Rigid families for the reversible π-calculus. In RC, volume 9720 of LNCS, pages 3-19. Springer, 2016. URL: http://dx.doi.org/10.1007/978-3-319-40578-0_1.
  9. Vincent Danos and Jean Krivine. Reversible communicating systems. In CONCUR, volume 3170 of LNCS, pages 292-307. Springer, 2004. URL: http://dx.doi.org/10.1007/978-3-540-28644-8_19.
  10. Edsko de Vries, Vasileios Koutavas, and Matthew Hennessy. Communicating transactions - (extended abstract). In CONCUR, volume 6269 of LNCS, pages 569-583. Springer, 2010. URL: http://dx.doi.org/10.1007/978-3-642-15375-4_39.
  11. Edsko de Vries, Vasileios Koutavas, and Matthew Hennessy. Liveness of communicating transactions - (extended abstract). In APLAS, volume 6461 of LNCS, pages 392-407. Springer, 2010. URL: http://dx.doi.org/10.1007/978-3-642-17164-2_27.
  12. Pierre-Malo Deniélou and Nobuko Yoshida. Dynamic multirole session types. In POPL, pages 435-446. ACM Press, 2011. URL: http://dx.doi.org/10.1145/1926385.1926435.
  13. Pierre-Malo Deniélou and Nobuko Yoshida. Multiparty session types meet communicating automata. In ESOP, volume 7211 of LNCS, pages 194-213. Springer, 2012. URL: http://dx.doi.org/10.1007/978-3-642-28869-2_10.
  14. Mariangiola Dezani-Ciancaglini and Paola Giannini. Reversible multiparty sessions with checkpoints. In EXPRESS/SOS, volume 222 of EPTCS, pages 60-74, 2016. URL: http://dx.doi.org/10.4204/EPTCS.222.5.
  15. Elena Giachino, Ivan Lanese, Claudio Antares Mezzina, and Francesco Tiezzi. Causal-consistent rollback in a tuple-based language. Journal of Logic and Algebraic Methods in Programming, 88:99-120, 2017. URL: https://doi.org/10.1016/j.jlamp.2016.09.003, URL: http://dx.doi.org/10.1016/j.jlamp.2016.09.003.
  16. Eva Graversen, Iain Phillips, and Nobuko Yoshida. Towards a categorical representation of reversible event structures. In PLACES, volume 246 of EPTCS, pages 49-60, 2017. URL: http://dx.doi.org/10.4204/EPTCS.246.9.
  17. Kohei Honda, Vasco T. Vasconcelos, and Makoto Kubo. Language primitives and type disciplines for structured communication-based programming. In ESOP, volume 1381 of LNCS, pages 22-138. Springer, 1998. URL: http://dx.doi.org/10.1007/BFb0053567.
  18. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. In POPL, pages 273-284. ACM Press, 2008. URL: http://dx.doi.org/10.1145/1328897.1328472.
  19. Vasileios Koutavas, Carlo Spaccasassi, and Matthew Hennessy. Bisimulations for communicating transactions - (extended abstract). In FOSSACS, volume 8412 of LNCS, pages 320-334. Springer, 2014. URL: http://dx.doi.org/10.1007/978-3-642-54830-7_21.
  20. Ivan Lanese, Claudio Antares Mezzina, Alan Schmitt, and Jean-Bernard Stefani. Controlling reversibility in higher-order pi. In CONCUR, volume 6901 of LNCS, pages 297-311. Springer, 2011. URL: http://dx.doi.org/10.1007/978-3-642-23217-6_20.
  21. Ivan Lanese, Claudio Antares Mezzina, and Jean-Bernard Stefani. Reversing higher-order pi. In CONCUR, volume 6269 of LNCS, pages 478-493. Springer, 2010. URL: http://dx.doi.org/10.1007/978-3-642-15375-4_33.
  22. Claudio Antares Mezzina and Jorge A. Pérez. Reversible semantics in session-based concurrency. In ICTCS, volume 1720 of CEUR Workshop Proceedings, pages 221-226. CEUR-WS.org, 2016. Google Scholar
  23. Claudio Antares Mezzina and Jorge A. Pérez. Reversible sessions using monitors. In PLACES, volume 211 of EPTCS, pages 56-64, 2016. URL: http://dx.doi.org/10.4204/EPTCS.211.6.
  24. Claudio Antares Mezzina and Jorge A. Pérez. Causally consistent reversible choreographies. CoRR, abs/1703.06021, 2017. Google Scholar
  25. Claudio Antares Mezzina, Rudolf Schlatte, and al. COST Action on Reversible Computation, State of the Art Report, Working Group 2 on Software and Systems, 2012. URL: http://www.informatik.uni-bremen.de/ictcost/wg2_soar.pdf.
  26. Claudio Antares Mezzina and Emilio Tuosto. Choreographies for automatic recovery. CoRR, abs/1705.09525, 2017. Google Scholar
  27. Robin Milner. A Calculus of Communicating Systems, volume 92 of LNCS. Springer, 1980. URL: http://dx.doi.org/10.1007/3-540-10235-3.
  28. Rumyana Neykova and Nobuko Yoshida. Let it recover: multiparty protocol-induced recovery. In CC, pages 98-108. ACM Press, 2017. URL: http://dx.doi.org/10.1145/3033019.
  29. Iain Phillips and Irek Ulidowski. Reversing algebraic process calculi. Journal of Logic and Algebraic Methods in Programming, 73(1-2):70-96, 2007. URL: http://dx.doi.org/10.1016/j.jlap.2006.11.002.
  30. Iain Phillips and Irek Ulidowski. Reversibility and asymmetric conflict in event structures. Journal of Logic and Algebraic Methods in Programming, 84(6):781-805, 2015. URL: http://dx.doi.org/10.1016/j.jlamp.2015.07.004.
  31. Benjamin C. Pierce. Types and Programming Languages. MIT Press, 2002. Google Scholar
  32. Peter Thiemann and Vasco T. Vasconcelos. Context-free session types. In ICFP, pages 462-475. ACM Press, 2016. URL: http://dx.doi.org/10.1145/2951913.2951926.
  33. Francesco Tiezzi and Nobuko Yoshida. Reversible session-based pi-calculus. Journal of Logical and Algebraic Methods in Programming, 84(5):684-707, 2015. URL: http://dx.doi.org/10.1016/j.jlamp.2015.03.004.
  34. Francesco Tiezzi and Nobuko Yoshida. Reversing single sessions. In RC, volume 9720 of LNCS, pages 52-69. Springer, 2016. URL: http://dx.doi.org/10.1007/978-3-319-40578-0_4.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact