To react to unforeseen circumstances or amend abnormal situations in communication-centric systems, programmers are in charge of "undoing" the interactions which led to an undesired state. To assist this task, session-based languages can be endowed with reversibility mechanisms. In this paper we propose a language enriched with programming facilities to commit session interactions, to roll back the computation to a previous commit point, and to abort the session. Rollbacks in our language always bring the system to previous visited states and a rollback cannot bring the system back to a point prior to the last commit. Programmers are relieved from the burden of ensuring that a rollback never restores a checkpoint imposed by a session participant different from the rollback requester. Such undesired situations are prevented at design-time (statically) by relying on a decidable compliance check at the type level, implemented in MAUDE. We show that the language satisfies error-freedom and progress of a session.

翻译：为应对以通信为中心系统中不可预见的情况或修正异常状态，程序员需要负责"撤销"导致非期望状态的交互过程。为辅助此任务，会话式语言可配备可逆性机制。本文提出一种增强型语言，提供编程设施以实现会话交互的提交、将计算回滚至先前提交点以及终止会话的功能。本语言中的回滚操作始终将系统恢复至先前访问过的状态，且无法回滚至最近一次提交点之前的状态。程序员无需承担确保回滚不会恢复由非请求方会话参与者所设检查点的负担，此类非期望情况在设计阶段（静态）通过基于MAUDE实现的可判定类型级合规性检查予以预防。我们证明该语言能够保障会话的错误消除与执行进展。