论文标题
具有高阶并发分离逻辑的模块化终止验证（中间报告）
Modular termination verification with a higher-order concurrent separation logic (Intermediate report)
论文作者
论文摘要
我们还报告了有关lival属性推理的中间结果，除了具有高阶商店的命令性，并发的编程语言外，还具有深度正确的属性。目前，我们专注于一种特殊的伦理属性，即终止。通过保证终止，我们可以加强对总正确性的部分正确性的陈述。这是通过将终止变成安全性财产的经典方法来实现的。特别是，我们通过呼叫权限扩展了正在考虑的编程语言，这些语言已证明可以实现有关终止的模块化推理。添加原子块以提高我们基于呼叫的呼叫的方法的表现力。我们的工作以虹膜（基础，机器检查，更高阶的并发逻辑框架）为基础，而无需对其进行修改。通过这些添加，我们能够模块化地理解并发算法的终止。我们对所考虑的编程语言的增加，可以保留Iris推理帮助和预言的能力。例如，我们将当前系统应用于现有的案例研究，以提供无锁的并发堆栈，并在IRIS中证明了这一点。最后，我们绘制下一步的步骤，以扩展阻止并发的方法。
We report on intermediate results of our research on reasoning about liveness properties in addition to deep correctness properties for an imperative, concurrent programming language with a higher-order store. At present, we focus on one particular liveness property, namely termination. By guaranteeing termination we can strengthen statements of partial correctness to total correctness. This is achieved by the classic approach of turning termination into a safety property. In particular we extend the programming language under consideration with call permissions, which have been shown to enable modular reasoning about termination. Atomic blocks are added to increase the expressiveness of our call-permission-based approach. Our work builds on top of Iris -- a foundational, machine-checked, higher-order concurrent separation logic framework -- without modifying it. With these additions we are able to modularly reason about the termination of concurrent, but non-blocking algorithms. Our additions to the programming language under consideration preserve Iris' ability to reason about helping and prophecies. As an example, we apply the current system to an existing case study for a lock-free concurrent stack with helping that has been proven in Iris. Finally, we sketch the next steps to scale our approach to blocking concurrency.
