Part 6 — Heap & Concurrency

Separation logic, mutable state, and verified concurrent Python

Why This Part Matters

Everything in Python is an object on the heap. Every variable is a reference. Every assignment is a pointer copy. This makes Python wonderfully flexible — and fiendishly hard to reason about formally. In this part we bring two complementary systems to bear: the cubical heap (Deppy's native model) and classical separation logic (the framework Pulse and Iris use). The two coexist; they describe the same property surface from different angles.

Python's Memory Model

CPython's runtime has three properties that distinguish it from the C / Rust / F* worlds where separation logic was originally developed:

1. Everything Is an Object

Integers, strings, functions, classes — every value lives on the heap and is accessed through a reference (a PyObject* in C terms). There is no "stack allocation" of primitives.

# x and y refer to the *same* heap object
x = [1, 2, 3]
y = x
y.append(4)
assert x == [1, 2, 3, 4]  # surprise!

2. Reference Counting + Cycle GC

Each object carries a reference count. When the count drops to zero, CPython deallocates immediately. A supplementary tracing GC catches reference cycles. For verification, this means:

• Deterministic destruction of acyclic data — useful for resource-cleanup proofs.
• Non-deterministic collection of cycles — we must be careful when reasoning about finaliser order.

3. The Global Interpreter Lock (GIL)

Only one thread executes Python bytecode at a time. The GIL guarantees atomicity of individual bytecodes but not atomicity of compound operations. A statement like counter += 1 compiles to multiple bytecodes — LOAD_FAST, BINARY_ADD, STORE_FAST — and a thread switch can occur between any two of them.

# Classic GIL misconception — this is NOT thread-safe
import threading

counter = 0

def bump():
    global counter
    for _ in range(100_000):
        counter += 1   # LOAD, ADD, STORE — not atomic!

threads = [threading.Thread(target=bump) for _ in range(4)]
for t in threads: t.start()
for t in threads: t.join()
print(counter)  # Almost certainly != 400_000

Why Separation Logic?

Classical Hoare logic describes a heap as a monolithic map from addresses to values. Separation logic adds a critical operator — the separating conjunction ★ — that asserts two sub-heaps are disjoint. This lets you reason locally: a function that operates on its own slice of the heap cannot corrupt yours.

For Python, separation logic is a natural fit because every object reference is a potential alias. By tracking ownership — which references a function is permitted to read or write — we can verify that mutations are safe even in the presence of shared mutable state.

Deppy's Approach

Deppy expresses separation-logic specifications as Python decorators. The proof engine discharges obligations to Z3 (for decidable fragments) or to an LLM oracle (for domain-specific semantics), exactly as in earlier parts of this book. The key new ingredients are:

1. SLProp — a type of separation-logic propositions (analogous to F*'s slprop).
2. pts_to(ref, value) — the fundamental "points-to" assertion: ref currently holds value.
3. @requires / @ensures — pre- and post-conditions in separation logic.
4. Lock(invariant) — locks that own a piece of the heap described by an SLProp.
5. @parallel_safe — proof that a function can be called from multiple threads without data races.

from deppy.separation import SLProp, pts_to, emp
from deppy.heap import Ref, requires, ensures

@requires(pts_to(x, 'v'))
@ensures(lambda result: pts_to(x, 'v + 1'))
def incr(x: Ref[int]):
    """Increment a heap-allocated integer."""
    x.value += 1

The body of incr is ordinary Python. The decorators express the contract in separation logic, and Deppy verifies that the implementation satisfies the contract at import time (or via python -m deppy.pipeline.run_verify).

What You'll Learn

This part contains five chapters:

Prerequisites

Before starting Part 6 you should be comfortable with:

• Refinement types and Z3 integration (Part 1)
• Dependent types and inductive proofs (Part 2)
• Python's decorator and metaclass machinery (Part 3)
• Basic homotopy type theory — path types and transport (Part 5)

No prior knowledge of separation logic is assumed — we build it from scratch.

Cubical Heap vs Pulse: The Big Picture

Pulse (Microsoft Research's concurrent separation-logic verifier built on F^★) is the best-known production tool in the separation-logic tradition. Deppy's cubical heap reaches similar soundness via a different mathematical route. Both are honest, both are sound; they just slice the problem differently.

Pulse's frame rule is an arrow you draw around a Hoare triple; Deppy's PathComp is an arrow you compose through a sequence of effects. Pulse forbids what it cannot prove disjoint; Deppy admits everything but forces transport when a proof is reused across mutations. The two systems are dual, in a precise category-theoretic sense.

Below: the same example expressed in both systems. The Pulse version uses points-to and the frame rule; the Deppy version emits an EffectWitness on the cell and lets the kernel sequence it through PathComp.

(* Pulse syntax *)
fn incr (x: ref int)
  requires pts_to x 'i'
  ensures  pts_to x 'i+1'
{
  let v = !x;
  x := v + 1;
}

# PSDL inside @verify / @psdl_proof
# or inside a .deppy verify block
def push(xs):
    xs.append(1)
# compile_psdl emits:
#   EffectWitness(mutate:xs.append@epoch1, Refl)
# final_epoch == 1; effect_sequence == [(2, 'mutate', 'xs.append')]

Key differences from Pulse:

• No new syntax — Deppy specifications are valid Python decorators and type annotations.
• Aliasing is a first-class path, not a permission fraction — Python idioms (b = a; a.append(…)) compile unmodified.
• GIL-aware — Deppy's runtime concurrency layer (deppy.concurrency.Lock) understands the GIL. The kernel itself does not model concurrency; Lock is enforced at runtime via invariant checks.
• Async-native — built-in support for asyncio coroutines as coalgebras (Part 3.4) and the deppy.async_verify contracts (Part 6.6).

Key Concepts at a Glance

SLProp — Heap Propositions

A value of type SLProp describes a region of the Python heap. The primitives are emp (empty heap), pts_to(ref, val) (a reference holding a value), and the separating conjunction ** (two disjoint heap regions). These compose to describe arbitrarily complex heap states.

Ownership Transfer

When you call a function whose precondition mentions pts_to(x, v), you transfer ownership of x to that function. It gives you back ownership via its postcondition. This is how Deppy prevents data races and use-after-free without runtime overhead.

The Frame Rule

If {P} f {Q}, then {P ** R} f {Q ** R} for any R. In words: anything the function doesn't mention is automatically preserved. This enables local reasoning — you never have to describe the entire heap in a specification.

Lock Invariants

A lock owns a heap region described by its invariant. Acquiring the lock transfers that region to the acquiring thread; releasing returns it. This is how shared mutable state is safely partitioned among threads.

a = [1, 2, 3]
b = a
b[0] = 99
print(a[0])