Reversibility in session-based concurrency: A fresh look

Mezzina, C. A. & Pérez, J. A. Aug-2017 In : The Journal of Logical and Algebraic Methods in Programming. 90, p. 2-30 29 p.

Research output: Scientific - peer-reviewArticle

Copy link to clipboard


  • Authors version Reversibility in Session-Based Concurrency

    Final author's version, 528 KB, PDF-document

    Embargo ends: 11/06/2019

  • Reversibility in session-based concurrency

    Final publisher's version, 826 KB, PDF-document


Much research has studied foundations for correct and reliable communication-centric software systems. A salient approach to correctness uses verification based on session types to enforce structured communications; a recent approach to reliability uses reversible actions as a way of reacting to unanticipated events or failures. In this paper, we develop a simple observation: the semantic machinery required to define asynchronous (queue-based), monitored communications can also support reversible protocols. We propose a framework of session communication in which monitors support reversibility of (untyped) processes. Main novelty in our approach are session types with present and past, which allow us to streamline the semantics of reversible actions. We prove that reversibility in our framework is causally consistent, and define ways of using monitors to control reversible actions.
Original languageEnglish
Pages (from-to)2-30
Number of pages29
JournalThe Journal of Logical and Algebraic Methods in Programming
StatePublished - Aug-2017



View graph of relations

ID: 48555899