Local Reasoning for Global Graph Properties
Local Reasoning for Global Graph Properties
复制标题
DOI：
10.1007/978-3-030-44914-8_12
复制
发表时间：
2020-04-18
期刊：
影响因子：
--
通讯作者：
Wies T
中科院分区：
文献类型：
--
作者：
Krishna S;Summers AJ;Wies T
分离逻辑广泛用于验证操作复杂的基于堆的数据结构的程序。这些逻辑建立在所谓的分离代数上，分离代数允许表达堆区域的属性，使得对区域的修改不会使关于堆的其余部分的属性无效。这个概念是实现模块化推理的关键，也扩展到并发性。虽然堆与数学图自然相关，但许多普遍存在的图属性在特征上是非局部的，例如节点之间的可达性、路径长度、非循环性和其他结构不变量，以及与这些概念结合的联合收割机的数据不变量。众所周知，模块化地推理这种图的属性仍然非常困难，因为局部修改可能会对全局属性产生副作用，而全局属性不能轻易地局限于一个小区域。在本文中，我们解决的问题：什么分离代数可以用来避免证明参数恢复到繁琐的全球推理在这种情况下？为此，我们考虑一类一般的全局图形属性表示为代数方程的不动点图。我们提出的数学基础推理这一类的属性，施加最低要求的基础理论，使我们能够定义一个合适的分离代数。在此理论的基础上，我们开发了一种通用的证明技术，用于程序堆上表示的全局图形属性的模块化推理，以一种可以直接与现有分离逻辑集成的方式。为了证明我们的方法，我们提出了两个具有挑战性的例子：优先级继承协议和非阻塞并发哈里斯列表的本地证明。
Separation logics are widely used for verifying programs that manipulate complex heap-based data structures. These logics build on so-called separation algebras, which allow expressing properties of heap regions such that modifications to a region do not invalidate properties stated about the remainder of the heap. This concept is key to enabling modular reasoning and also extends to concurrency. While heaps are naturally related to mathematical graphs, many ubiquitous graph properties are non-local in character, such as reachability between nodes, path lengths, acyclicity and other structural invariants, as well as data invariants which combine with these notions. Reasoning modularly about such graph properties remains notoriously difficult, since a local modification can have side-effects on a global property that cannot be easily confined to a small region. In this paper, we address the question: What separation algebra can be used to avoid proof arguments reverting back to tedious global reasoning in such cases? To this end, we consider a general class of global graph properties expressed as fixpoints of algebraic equations over graphs. We present mathematical foundations for reasoning about this class of properties, imposing minimal requirements on the underlying theory that allow us to define a suitable separation algebra. Building on this theory, we develop a general proof technique for modular reasoning about global graph properties expressed over program heaps, in a way which can be directly integrated with existing separation logics. To demonstrate our approach, we present local proofs for two challenging examples: a priority inheritance protocol and the non-blocking concurrent Harris list.
登录
查看更多内容
影响因子：
1.1
作者：
Jung, Ralf;Krebbers, Robbert;Dreyer, Derek
通讯作者：
Dreyer, Derek
DOI：
10.1007/s10817-017-9442-4
发表时间：
2019-02-01
期刊：
JOURNAL OF AUTOMATED REASONING
影响因子：
--
作者：
Lammich, Peter;Sefidgar, S. Reza
通讯作者：
Sefidgar, S. Reza
DOI：
10.1007/s10817-017-9431-7
发表时间：
2019-03-01
期刊：
JOURNAL OF AUTOMATED REASONING
影响因子：
--
作者：
Chargueraud, Arthur;Pottier, Francois
通讯作者：
Pottier, Francois
影响因子：
1.3
作者：
Dodds, Mike;Jagannathan, Suresh;Birkedal, Lars
通讯作者：
Birkedal, Lars
影响因子：
1.8
作者：
Krishna, Siddharth;Shasha, Dennis;Wies, Thomas
通讯作者：
Wies, Thomas