论文标题
部分可观测时空混沌系统的无模型预测
Bringing Iris into the Verified Software Toolchain
论文作者
论文摘要
经过验证的软件工具链（VST）是使用分离逻辑证明C程序正确性的系统。通过连接到经过验证的编译器compcert，它可以为我们可以编译和运行的真实C代码提供最强的正确性保证。 VST以有关锁定不变的推理的形式包括从其成立开始的并发性，但是并发分离逻辑（CSL）从那以后就以突飞猛进的速度提出。在本文中，我们描述了将Iris（最先进的机械化CSL）的进步整合到VST中的努力。虹膜的某些特征（幽灵状态和不变式）从头开始重新启动。其他（虹膜证明模式）是从虹膜开发中进口的；还有其他（原子操作的证明规则）被公理化，希望它们能够在以后的版本中成为基础。结果是一个可以证明C中实现的复杂程序的系统，具有细粒度的锁定和非阻滞原子操作，可以根据所使用的功能产生不同的健全性保证。
The Verified Software Toolchain (VST) is a system for proving correctness of C programs using separation logic. By connecting to the verified compiler CompCert, it produces the strongest possible guarantees of correctness for real C code that we can compile and run. VST included concurrency from its inception, in the form of reasoning about lock invariants, but concurrent separation logic (CSL) has advanced by leaps and bounds since then. In this paper, we describe efforts to integrate advancements from Iris, a state-of-the-art mechanized CSL, into VST. Some features of Iris (ghost state and invariants) are re-implemented in VST from the ground up; others (Iris Proof Mode) are imported from the Iris development; still others (proof rules for atomic operations) are axiomatized, with the hope that they will be made foundational in future versions. The result is a system that can prove correctness of sophisticated concurrent programs implemented in C, with fine-grained locking and non-blocking atomic operations, that yields varying soundness guarantees depending on the features used.
