Reversing Single Sessions

TL;DR

This paper explores how reversibility affects structured session-based communication, analyzing different notions of reversing interactions in binary and multiparty sessions, and assessing the associated costs.

Contribution

It systematically studies the integration of reversibility in single sessions, including binary and multiparty interactions, and evaluates the costs involved.

Findings

Reversibility can be integrated into both binary and multiparty sessions without affecting the machinery.

Different notions of reversibility, including single-step and multi-step, are analyzed.

Extending to multiparty sessions does not increase the costs of reversibility.

Abstract

Session-based communication has gained a widespread acceptance in practice as a means for developing safe communicating systems via structured interactions. In this paper, we investigate how these structured interactions are affected by reversibility, which provides a computational model allowing executed interactions to be undone. In particular, we provide a systematic study of the integration of different notions of reversibility in both binary and multiparty single sessions. The considered forms of reversibility are: one for completely reversing a given session with one backward step, and another for also restoring any intermediate state of the session with either one backward step or multiple ones. We analyse the costs of reversing a session in all these different settings. Our results show that extending binary single sessions to multiparty ones does not affect the reversibility machinery and its costs.