Thomas Wies
Flow Interfaces: Compositional Abstractions for Concurrent Data Structures
June 11, 2018 at 12:00pm (lunch talk) CSE 403
Abstract
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.
Flow interfaces provide a new semantic model for separation logic assertions that admits general implementation-agnostic proof rules for reasoning about concurrent data structures. We have used our approach to obtain linearizability proofs for concurrent dictionary algorithms that cannot be easily expressed using the abstraction mechanisms provided by existing program logics.
Bio
Thomas Wies is an Associate Professor in the NYU Computer Science Department and a member of the Analysis of Computer Systems Group in the Courant Institute. His research focuses on program analysis and verification, automated deduction, concurrent software, and software productivity.