Go with the Flow: Compositional Abstractions for Concurrent Data Structures
Go with the Flow: Compositional Abstractions for Concurrent Data Structures
复制标题
DOI：
10.1145/3158125
复制
发表时间：
2018-01-01
影响因子：
1.8
通讯作者：
Wies, Thomas
中科院分区：
文献类型：
--
作者：
Krishna, Siddharth;Shasha, Dennis;Wies, Thomas
并发分离逻辑有助于显著简化并发数据结构的正确性证明。然而，这种证明中反复出现的问题是，由于复杂的共享和覆盖，在顺序设置中工作良好的数据结构抽象在并发设置中更难推理。为了解决这个问题，我们提出了一种新的方法，通过将数据结构不变量编码为每个节点上的局部条件来抽象堆中的区域。该条件可以取决于与在整个堆图上被计算为固定点的节点相关联的量。我们把这个量称为流量。流可以编码堆的结构属性（例如从根形成树的可达节点）以及数据不变量（例如排序）。然后，我们引入流接口的概念，它表示依赖和保证堆区域施加在其上下文上，以保持局部流相对于全局堆不变。我们的主要技术成果是，这个概念导致了一个新的语义模型的分离逻辑。在这个模型中，流接口提供了一个通用的抽象机制来描述复杂的数据结构。这种抽象机制允许在各种数据结构上推广的证明规则。为了证明我们的方法的多功能性，我们展示了如何扩展逻辑RGSep流接口。我们已经使用这种新的逻辑来证明非平凡的并发数据结构的线性化和内存安全。特别是，我们获得参数线性化证明并发字典算法，抽象的底层数据结构表示的细节。这些证明不能很容易地表示使用现有的分离逻辑提供的抽象机制。
Concurrent separation logics have helped to significantly simplify correctness proofs for concurrent data structures. However, a recurring problem in such proofs is that data structure abstractions that work well in the sequential setting are much harder to reason about in a concurrent setting due to complex sharing and overlays. To solve this problem, we propose a novel approach to abstracting regions in the heap by encoding the data structure invariant into a local condition on each individual node. This condition may depend on a quantity associated with the node that is computed as a fixpoint over the entire heap graph. We refer to this quantity as a flow. Flows can encode both structural properties of the heap (e.g. the reachable nodes from the root form a tree) as well as data invariants (e.g. sortedness). We then introduce the notion of a flow interface, which expresses the relies and guarantees that a heap region imposes on its context to maintain the local flow invariant with respect to the global heap. Our main technical result is that this notion leads to a new semantic model of separation logic. In this model, flow interfaces provide a general abstraction mechanism for describing complex data structures. This abstraction mechanism admits proof rules that generalize over a wide variety of data structures. To demonstrate the versatility of our approach, we show how to extend the logic RGSep with flow interfaces. We have used this new logic to prove linearizability and memory safety of nontrivial concurrent data structures. In particular, we obtain parametric linearizability proofs for concurrent dictionary algorithms that abstract from the details of the underlying data structure representation. These proofs cannot be easily expressed using the abstraction mechanisms provided by existing separation logics.