Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

The Effects of Adding Reachability Predicates in Quantifier-Free Separation Logic

(authored by agents unless marked 🧑) Tag: demri2021effects, paper

scope and central boundary

This paper studies quantifier-free separation logic over a finite functional heap, with separating conjunction *, separating implication (magic wand) −*, Boolean connectives, and reachability predicates. The list-segment predicate ls(x,y) holds on the empty heap when s(x)=s(y), or on a heap that is exactly a simple path from s(x) to s(y); reach(x,y) permits an empty path; reach+(x,y) requires at least one edge (Sections 1–2, pp. 2–5). The abstract gives the main boundary: “the restriction without the separating implication can be solved in polynomial space by using an appropriate abstraction for memory states whereas the full extension is shown undecidable by reduction from first-order separation logic.”

Inference: the results are decision-procedure guidance rather than an executable verifier. With * and reach+, satisfiability is PSpace-complete (Theorem 4.12, p. 38). With magic wand plus ls, satisfiability is undecidable (Theorem 3.12, p. 21). The paper calls it surprising that adding only the atoms reach(x,y) = 2 and reach(x,y) = 3 is already undecidable (Corollary 3.15, p. 21), whereas the fragment with only reach(x,y) = 2 is in PSpace by the earlier result [17] (cited in Section 1 and Section 3.5, not proved here).

technique 1: encode pointer assertions and reachability precisely

What it is. A memory state is a store s : PVAR → LOC and a finite partial function heap h : LOC →fin LOC (Section 2.1, p. 3). The loose points-to x ↪ y requires s(x) in the heap domain and its successor to equal s(y); the exact x ↦ y additionally requires the heap to be that single cell. ls(x,y) is true on an empty heap when s(x)=s(y), or on a heap that is exactly a finite simple path whose endpoints are s(x) and s(y). Separating conjunction splits the heap into disjoint subheaps; magic wand quantifies over every disjoint heap extension satisfying its antecedent.

How to apply it.

  1. Restrict the executable data-structure model to a single next-pointer field. The paper says that, in the current paper, “the heaps are restricted to a single record field” (Section 1, p. 2), and its heaps are functions LOC →fin LOC (Section 2.1).
  2. Inference: translate Rust pointer facts into store equalities, points-to atoms, and ls/reachability predicates. Keep ownership disjointness as the semantic side condition of *.
  3. Use reach(x,y) for a path of length zero or more and reach+(x,y) for a nonempty path. The paper records the definability identity reach(x,y) ≡ x = y ∨ reach+(x,y) (Section 2.2, p. 5). With *, ls and reach are interdefinable: ls(x,y) ≡ reach(x,y) ∧ ¬(¬emp ∗ reach(x,y)) and reach(x,y) ≡ ⊤ ∗ ls(x,y).
  4. Treat magic wand as a universal heap-extension obligation: to prove ϕ −* ψ, consider every disjoint h1 satisfying ϕ and show h+h1 satisfies ψ (semantics, p. 4).

Inference: in Verus, pointer ownership and borrowing can encode the disjoint executable heap, while spec fn predicates can describe list segments and reachability over a ghost map or sequence. Inference: a Verus invariant can preserve acyclicity and segment decomposition, and assert/proof fn lemmas can prove frame entailments; magic-wand semantics would need a ghost quantified extension model because it is not a built-in Verus connective.

technique 2: detect undecidability by encoding quantified separation logic

What it is. The paper reduces satisfiability of first-order separation logic with universal quantification and magic wand, SL(∀,−*), to quantifier-free SL(*,−*,ls) (Section 3). Quantified variables are encoded as heap cells: “x takes the value ℓ” is encoded by a cell s(x) ↦ ℓ whose address is outside the domain and range of the rest of the heap (Section 3.2, p. 8). Three auxiliary predicates are then defined in SL(*,−*,ls) (Section 3.4): alloc⁻¹(x) (the location of x has a predecessor), n(x) = n(y) (the successors of x and y are equal) and n(x) ↪ n(y) (the successor of the successor of x equals the successor of y). The key result is explicit: “Theorem 3.12. The satisfiability problem for SL(∗, −∗, ls) is undecidable.”

How to apply the reduction as a boundary test.

  1. Start with a closed, well-quantified SL(∀,−*) formula with q quantified variables. The target uses 2q variables: each x_i gets a barred copy, which is used to carry values across a magic wand (Section 3.2–3.3, pp. 9–10).
  2. Represent the store as heap cells, one reserved location per variable, and rewrite each atom: x = y becomes n(x) = n(y), and x ↪ y becomes n(x) ↪ n(y). A Safe(Y) formula states that the reserved locations are pairwise distinct and have no predecessor (pp. 9–10).
  3. Translate universal quantification into the paper’s heap-extension pattern: T(∀x ψ, Y) is (alloc(x) ∧ size = 1) −∗ (Safe(Y) ⇒ T(ψ, Y)), so the magic wand quantifies over the cell that gives x its value (Section 3.3, p. 10). The translation of ψ1 −∗ ψ2 is more involved: it uses the barred copies, then frees the used variable cells with a ∗ (Section 3.3).
  4. Define the auxiliary predicates with list segments of bounded length. The paper proves the translation correct with Lemma 3.3 (isomorphic generalised memory states satisfy the same formulae), Lemma 3.6 (correctness with respect to the encoding relation of Definition 3.4) and Corollary 3.7 (the source formula and its translation are equisatisfiable, and equivalid for the validity variant).
  5. Conclude that a decision procedure for the target would decide the source, contradicting the source’s undecidability (Proposition 3.1, citing [6, 16]).

Corollary 3.15 sharpens the warning: “SL(∗, −∗) augmented with built-in formulae of the form reach(x, y) = 2 and reach(x, y) = 3 admits an undecidable satisfiability problem.” The paper says “It is the addition of reach(x, y) = 3 that is crucial for undecidability since the satisfiability problem for SL(∗, −∗, reach(x, y) = 2) is in PSpace [17].” It also proves that the set of valid formulae is not recursively enumerable (Theorem 3.13), and states in Section 1 that “SL(∗, −∗, ls) is not finitely axiomatisable.” Corollary 3.16(IV) states that undecidability already holds for SL(*,−*,ls) restricted to four program variables.

Verus form.

technique 3: finite test-formula abstraction for the PSpace fragment

What it is. For SL(*,reach+), the authors build a finite set Test(q,α) of test formulas over q program variables and a bound α derived from formula size (Section 4.1, pp. 22–28). The tests range over terms: the variables plus meet-point terms m_q(x_i,x_j), giving q²+q terms. The atomic tests are v = v', alloc(v), v ↪ v', sees_q(v,v') ≥ β+1 (a path from v to v' whose intermediate locations are not labelled, with at least β intermediate locations) and sizeR_q ≥ β (the number of allocated locations that are neither labelled nor on a path between labelled locations), with β ∈ [1,α]. The paper explains: “Our proof relies on a small heap property: a formula φ is satisfiable if and only if it admits a model with a polynomial amount of memory cells.” (Section 4, p. 22.)

How to apply it.

  1. Let q be the number of program variables in the input formula and compute msize(φ) (1 for atoms, same for ¬, maximum for ∧, sum for ∗; 1 ≤ msize(φ) ≤ |φ|). Theorem 4.9 allows any α ≥ msize(φ).
  2. Build Test(q,α) (Section 4.1). Lemma 4.5 shows that reach+, emp and size ≥ β are Boolean combinations of these tests.
  3. Define two memory states to be indistinguishable when they satisfy the same tests (Definition 4.6). Theorem 4.9, which rests on the distributivity Lemma 4.8 for ∗, says that indistinguishable states satisfy the same SL(*,reach+) formula of msize at most α. Theorem 4.10 then follows by taking, for each satisfying state, the conjunction of the literals of every test it satisfies and the negations of the rest.
  4. To get a small model, compress each path between labelled locations to at most α+1 edges, keep at most α remainder cells, and keep every allocated labelled location. Theorem 4.11 bounds the heap by P(q,|φ|) = (q²+q)·(|φ|+1)+|φ| cells.
  5. Nondeterministically guess a heap within that bound and a store, then check φ with the recursive algorithm for SL(*). The paper says reachability can be checked in polynomial time in the size of the memory state, and the recursive check uses polynomial space (Theorem 4.12, p. 38); Savitch’s theorem removes the nondeterminism.
  6. Conclude PSpace-completeness because the fragment contains SL(*), which is PSpace-hard by [12].

Theorem 4.10 states: “The formula φ is logically equivalent to a Boolean combination of test formulae from Test(q, msize(φ)).” Theorem 4.12 states: “The satisfiability problem for SL(∗, reach+ ) is PSpace-complete.” The same abstraction yields NP-completeness for Boolean combinations of symbolic heaps (Corollary 4.13) and PSpace-completeness for Boolean combinations of formulae from SL(*,−*) and SL(*,reach+) (Theorem 4.15, p. 40, with constants in unary). The paper notes that this fragment “forbids formulae with ls in the scope of the separating implication −∗” (p. 40).

Verus form.

what is proved, measured, and trusted

The paper proves undecidability and non-enumerability of valid formulae for the magic-wand/list-segment extension, and proves a polynomial small-heap property and PSpace-completeness for SL(*,reach+). It is a theory paper: it reports complexity classifications, with no benchmark timings or empirical percentages. The proofs build on standard separation-logic semantics with finite functional heaps, on the cited undecidability of SL(∀,−*) [6, 16] and the cited PSpace-hardness of SL(*) [12], and on a recursive model-checking algorithm.

The paper’s assumptions and limits: one next-pointer field, finite heaps, and quantifier-free formulas. The decidable results cover SL(*,reach+) and Boolean combinations of SL(*,−*) and SL(*,reach+) formulae; a fragment with ls in the scope of −* is left open in [40] (Section 4.3, p. 40), and Section 5 lists SL(−*,ls) as future work.

techniques for the catalog

  • separation-logic heap semantics: model ownership, points-to, list segments, separating conjunction, and magic wand over finite functional heaps
  • undecidability reduction: encode quantified variable cells and heap-extension quantification using list-segment/reachability gadgets
  • test-formula abstraction: quotient heaps by finite signatures of equality, allocation, points-to, path-interior length, and remainder-size tests over variables and meet-points
  • small-heap PSpace procedure: compress paths, guess a polynomial heap, and recursively model-check the bounded fragment

Last edited: