一句话：首个全形式化工具，机械化关系验证带 call/cc 与 throw 的并发高阶命令式程序。
本文针对带续延（continuations，call/cc 与 throw）的并发高阶命令式语言难以推理的问题：非局部控制流破坏 Hoare 逻辑中关键的 bind 模块化规则。作者提出首个完全形式化的交互式机械化关系验证工具，并开发新型逻辑关系以机械化证明关系性质。为恢复模块化推理，他们引入 context-local 推理原则，使无异常控制流片段可模块化推理，并可与处理非局部控制流的 Hoare 逻辑结合。评估中，他们证明用续延实现的合作式并发的正确性，并证明基于续延模式实现的简易 web server 与不使用该模式的实现上下文等价；组合推理还简化了这些例子的验证。
Concurrent higher-order imperative programming languages with continuations are very flexible and allow for the implementation of sophisticated programming patterns. For instance, it is well known that continuations can be used to implement cooperative concurrency. Continuations can also simplify web server implementations. This, in particular, helps simplify keeping track of the state of server’s clients. However, such advanced programming languages are very challenging to reason about. One of the main challenges in reasoning about programs in the presence of continuations is due to the fact that the non-local flow of control breaks the bind rule, one of the important modular reasoning principles of Hoare logic. In this paper we present the first completely formalized tool for interactive mechanized relational verification of programs written in a concurrent higher-order imperative programming language with continuations (call/cc and throw). We develop novel logical relations which can be used to give mechanized proofs of relational properties. In particular, we prove correctness of an implementation of cooperative concurrency with continuations. In addition, we show that that a rudimentary web server implemented using the continuation-based pattern is contextually equivalent to one implemented without the continuation-based pattern. We introduce context-local reasoning principles for our calculus which allows us to regain modular reasoning principles for the fragment of the language without non-local control flow. These novel reasoning principles can be used in tandem with our (non-context-local) Hoare logic for reasoning about programs that do feature non-local control flow. Indeed, we use the combination of context-local and non-context-local reasoning to simplify reasoning about the examples.
@article{paperbot597,
title = {Mechanized relational verification of concurrent programs with continuations},
author = {Amin Timany and Lars Birkedal},
journal = {Proceedings of the ACM on Programming Languages},
volume = {3},
number = {ICFP},
year = {2019},
doi = {10.1145/3341709}
}