Context-Aware Separation Logic

TL;DR

This work addresses the challenge that rich ghost-state abstractions in concurrent separation logic can enlarge the reasoning footprint to be effectively unbounded. It introduces context-aware (concurrent) separation logic (Co(Co)SL), which allows framing a known context $c$ across a computation when $c$ remains invariant under updates, thereby enabling more local reasoning. The authors develop an abstract-interpretation-based contextualization to compute suitable contexts, instantiate the theory for the Flow framework to reason about general heap graphs, and implement the approach in the proof outline checker nekton, validating several highly-concurrent BSTs. The results demonstrate practical proof automation for complex concurrent data structures and establish a framework that can be applied beyond the Flow setting to a broad class of ghost-state abstractions.

Abstract

Separation logic is often praised for its ability to closely mimic the locality of state updates when reasoning about them at the level of assertions. The prover only needs to concern themselves with the footprint of the computation at hand, i.e., the part of the state that is actually being accessed and manipulated. Modern concurrent separation logics lift this local reasoning principle from the physical state to abstract ghost state. For instance, these logics allow one to abstract the state of a fine-grained concurrent data structure by a predicate that provides a client the illusion of atomic access to the underlying state. However, these abstractions inadvertently increase the footprint of a computation: when reasoning about a local low-level state update, one needs to account for its effect on the abstraction, which encompasses a possibly unbounded portion of the low-level state. Often this gives the reasoning a global character. We present context-aware (concurrent) separation logic (Co(Co)SL) to provide new opportunities for local reasoning in the presence of rich ghost state abstractions. Co(Co)SL introduces the notion of a context of a computation, the part of the concrete state that is only affected on the abstract level. Contexts give rise to a new proof rule that allows one to reduce the footprint by the context, provided the computation preserves the context as an invariant. The context rule complements the frame rule of separation logic by enabling more local reasoning in cases where the predicate to be framed is known in advance. We instantiate our developed theory for the flow framework, enabling contextual reasoning about programs manipulating general heap graphs, and describe two other applications of the logic. We have implemented the flow instantiation of the logic in a proof outline checker and used it to verify two highly-concurrent binary search trees.

Figures (15)

• Figure 1: In-place removal of a key from an inner node $\mathit{x}$ in a binary search tree.
• Figure 2: In-place removal of the key in $\mathit{x}$ on a tree augmented with insets.
• Figure 3: Proof rules of context-aware separation logic (CoSL).
• Figure 4: A simple removal unlinks internal, marked nodes if they have at most one child. The operation does not alter the logical contents of the tree. Unlinking marked nodes with two children is done by complex removals.
• Figure 5: A complex removal unlinks internal, marked nodes with two children, not altering the logical contents.

Theorems & Definitions (46)

• theorem 1
• definition 1: Validity of CoSL statements
• definition 2
• theorem 2: Soundness of CoSL
• theorem 3: Conservative extension
• theorem 4
• theorem 5
• theorem 6
• theorem 7
• lemma 1: Unique Decomposition