一句话：提出支持提交、回滚与中止原语的会话语言，用类型级可判定合规性检查静态防止越界回滚，并证明无错误性与进展。
在以通信为中心（communication-centric）的系统中，程序常常需要撤销导致非期望状态的交互，为此会话（session）语言需要引入可逆机制。本文提出一种会话语言，提供三类编程设施：提交（commit）会话交互、将计算回滚到先前的提交点（commit point），以及中止会话。语言的设计保证回滚总是把系统带回此前访问过的状态，且回滚不能把系统带回最近一次提交之前的位置。关键难点在于：回滚不应恢复由不同于回滚请求者的会话参与者所设置的检查点；作者通过类型层的可判定合规性检查（compliance check）在设计阶段（静态地）排除这类不希望的情形，并在 MAUDE 中实现了该检查。文章进一步证明该语言满足无错误性（error-freedom）与会话进展性（progress）。
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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{MezzinaTY25,
title = {Checkpoint-based rollback recovery in session programming},
author = {Claudio Antares Mezzina and Francesco Tiezzi and Nobuko Yoshida},
journal = {Logical Methods in Computer Science},
volume = {Volume 21, Issue 1},
year = {2025},
doi = {10.46298/lmcs-21(1:2)2025}
}