Causal Consistency for Reversible Multiparty Protocols
In programming models with a reversible semantics, computational steps can be undone. This paper addresses the integration of reversible semantics into process languages for communication-centric systems equipped with behavioral types. In prior work, we introduced a monitors-as-memories approach to...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2021-10-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/6997/pdf |
| _version_ | 1797268503711973376 |
|---|---|
| author | Claudio Antares Mezzina Jorge A. Pérez |
| author_facet | Claudio Antares Mezzina Jorge A. Pérez |
| author_sort | Claudio Antares Mezzina |
| collection | DOAJ |
| description | In programming models with a reversible semantics, computational steps can be
undone. This paper addresses the integration of reversible semantics into
process languages for communication-centric systems equipped with behavioral
types. In prior work, we introduced a monitors-as-memories approach to
seamlessly integrate reversible semantics into a process model in which
concurrency is governed by session types (a class of behavioral types),
covering binary (two-party) protocols with synchronous communication. The
applicability and expressiveness of the binary setting, however, is limited.
Here we extend our approach, and use it to define reversible semantics for an
expressive process model that accounts for multiparty (n-party) protocols,
asynchronous communication, decoupled rollbacks, and abstraction passing. As
main result, we prove that our reversible semantics for multiparty protocols is
causally-consistent. A key technical ingredient in our developments is an
alternative reversible semantics with atomic rollbacks, which is conceptually
simple and is shown to characterize decoupled rollbacks. |
| first_indexed | 2024-04-25T01:33:31Z |
| format | Article |
| id | doaj.art-89a7c7f5dcf14789af5fb509029036b6 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:33:31Z |
| publishDate | 2021-10-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-89a7c7f5dcf14789af5fb509029036b62024-03-08T10:35:55ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742021-10-01Volume 17, Issue 410.46298/lmcs-17(4:1)20216997Causal Consistency for Reversible Multiparty ProtocolsClaudio Antares MezzinaJorge A. PérezIn programming models with a reversible semantics, computational steps can be undone. This paper addresses the integration of reversible semantics into process languages for communication-centric systems equipped with behavioral types. In prior work, we introduced a monitors-as-memories approach to seamlessly integrate reversible semantics into a process model in which concurrency is governed by session types (a class of behavioral types), covering binary (two-party) protocols with synchronous communication. The applicability and expressiveness of the binary setting, however, is limited. Here we extend our approach, and use it to define reversible semantics for an expressive process model that accounts for multiparty (n-party) protocols, asynchronous communication, decoupled rollbacks, and abstraction passing. As main result, we prove that our reversible semantics for multiparty protocols is causally-consistent. A key technical ingredient in our developments is an alternative reversible semantics with atomic rollbacks, which is conceptually simple and is shown to characterize decoupled rollbacks.https://lmcs.episciences.org/6997/pdfcomputer science - logic in computer scienced.3.1f.3.2 |
| spellingShingle | Claudio Antares Mezzina Jorge A. Pérez Causal Consistency for Reversible Multiparty Protocols Logical Methods in Computer Science computer science - logic in computer science d.3.1 f.3.2 |
| title | Causal Consistency for Reversible Multiparty Protocols |
| title_full | Causal Consistency for Reversible Multiparty Protocols |
| title_fullStr | Causal Consistency for Reversible Multiparty Protocols |
| title_full_unstemmed | Causal Consistency for Reversible Multiparty Protocols |
| title_short | Causal Consistency for Reversible Multiparty Protocols |
| title_sort | causal consistency for reversible multiparty protocols |
| topic | computer science - logic in computer science d.3.1 f.3.2 |
| url | https://lmcs.episciences.org/6997/pdf |
| work_keys_str_mv | AT claudioantaresmezzina causalconsistencyforreversiblemultipartyprotocols AT jorgeaperez causalconsistencyforreversiblemultipartyprotocols |