Reversible sessions with flexible choices (Q2329306)

From MaRDI portal
scientific article
Language Label Description Also known as
English
Reversible sessions with flexible choices
scientific article

    Statements

    Reversible sessions with flexible choices (English)
    0 references
    17 October 2019
    0 references
    This paper presents and studies a type system for reversible communication protocols. In particular, the main purpose of the session-type inspired system is to structure and enforce multiple properties on a reversible concurrent calculus endowed with a ``flexible'' choice operator. In addition to forward ``expected'' properties, such as subject reduction and progress, their reversible counterparts are also proven to hold, along with a ``session fidelity'' property. As the authors detail in the ``Related work and conclusion'' section, the calculus under study is a patchwork of good ideas: they adopt a ``static'' rollback operator that carries the memory of previous failures; represents both internal and external choices; makes the distinction between user processes and runtime processes. This gives an interesting rule BackA that ``throws away'' the branch on which the process wants to backtrack, while maintaining causal consistency, but at the cost of the loop lemma. Their session type system takes inspiration from existing approaches when it labels the choice operators with checkpoints, but also introduces novelty, e.g., by studying the interplay of (a relaxed version of) connecting actions with reversible computation. This blend of choices gives an interesting, technical and original paper that manages to make a difficult topic accessible. The interplay between connecting communications and reversibility makes some parts of the paper tedious, but the level of rigor maintained all along helps build trust in this interesting paper that tackles a difficult problem.
    0 references
    reversible computation
    0 references
    session type
    0 references
    process algebra
    0 references
    choices
    0 references
    rollback
    0 references

    Identifiers