干扰的复杂性：当依赖/保证方法失效时

中文摘要 AI 辅助

依赖/保证（Rely/Guarantee）是一种用于推理并发程序的著名验证技术。然而，对于某些算法，由于这些算法中表现出强烈的干扰，设计合适的依赖和保证条件颇具挑战性。Ben-Ari并发垃圾收集器就是这样一种算法，其中各组件之间的复杂交互阻碍了组合式依赖和保证条件的构建。本文研究了一种验证Ben-Ari算法的方法，该方法使得在组合式推理原本不可能的情况下，能够以更组合的方式进行推理。这是通过论证给定属性对特定变量的所有实例成立，然后将该变量实例化为所需的局部变量来实现的。除了提供一种更具组合性的推理方法外，该结果还识别了组件所需的核心属性，从而加深了对算法为何能正确工作的原因的理解。这有助于揭示为何依赖/保证方法在某些问题上不能直接起作用的原因。

英文摘要

Rely/Guarantee is a well-known verification technique for reasoning about concurrent programs. However, for some algorithms, devising suitable rely and guarantee conditions is challenging, due to the strong interference exhibited in these algorithms. The Ben-Ari concurrent garbage collector is an algorithm where the complex interactions between the components prevent the construction of compositional rely and guarantee conditions. This paper investigates an approach for verifying the Ben-Ari algorithm, which enables reasoning to be performed in a more compositional manner in cases where compositional reasoning would not otherwise be possible. This is accomplished by reasoning that a given property holds for all instances of a particular variable and then instantiating the variable to the local variable required. As well as providing a reasoning approach which is more compositional, the result is the identification of the core property required of a component, thus enabling a deeper understanding about the reasons why the algorithm works correctly. This helps to reveal the reasons why the rely/guarantee approach does not work directly for some problems.

发表机构

• School of Computing, The Australian National University（澳大利亚国立大学计算机学院）

机构由 AI 辅助整理，请以论文原文为准。