Heap-Dependent Ownership for malloc

Why People Wanted It

The interpreter keeps data in memory while it allocates more memory. A call to println("n = " + x), for example, allocates three strings and frees two; the variables and partially built result must remain intact throughout. To prove that, you need to say what malloc may change and why bytes the caller already owns survive the call.

A conventional specification gives a function a footprint: the fixed set of addresses it may write. For malloc, that is the wrong shape of answer. The allocator’s writes depend on which bytes are still free and which blocks have already been handed out. So the real question is not “which addresses may malloc always modify?” but “how can its permission to write follow the heap’s changing ownership?”

The Core Move

Specify the allocator as owning the arena’s free bytes, then transfer the newly allocated block from that ownership to the caller. The source gives this specification directly:

$$\{\ isHeap\ H\ \}\quad p := malloc(n)\quad \{\ (p = 0 \ast isHeap\ H) \lor (isHeap\ ((p,n)::H) \ast blockOwn\ p\ n)\ \}$$

In words: either allocation fails and the allocator still owns the same free heap, or it succeeds, the live-block list gains the new block, and the caller receives ownership of that block. Here $\ast$ separates disjoint memory ownership.

Why No Fixed Footprint Can Describe malloc

Here is the part that gets technical: the concrete counterexample is about one address whose status changes with the requested allocation size. From the same heap, malloc(32) writes a top-chunk header at 0x82000238. But malloc(64) returns [0x82000210, 0x82000250), a block containing that address.

A fixed footprint would have to include 0x82000238 so the first call may write it. Yet it would have to exclude that address so facts about the block returned by the second call remain protected in later calls. Those requirements conflict. The issue is not an awkward choice of set: no single set of addresses captures both cases.

The heap-dependent specification avoids choosing one. isHeap H owns every arena byte outside the live blocks in H; a byte can therefore be writable while free and become caller-owned when it falls inside a newly allocated block. What does that ownership transfer buy for memory the allocator does not mention?

Why the Frame Rule Preserves the Caller’s Other Data

Now the version for readers who want more of the machinery: the separating conjunction says its two assertions hold over disjoint parts of memory. In the successful branch, isHeap ((p,n)::H) describes the allocator’s remaining free arena, while blockOwn p n describes the returned block. In the failure branch, p = 0 leaves isHeap H unchanged.

The frame rule carries any disjoint caller-owned memory through a call unchanged. The allocator’s specification need not enumerate the interpreter’s variables or an unfinished string: because those bytes are not part of the allocator-owned free heap or the transferred block, the frame rule preserves them. This is the key distinction from a fixed footprint: the permission boundary is determined by current ownership, not by a global list of addresses.

Minimal Causal Code

This plain loop sketches the ownership update, not the allocator’s concrete implementation. The paper gives no formula for a byte-by-byte allocator algorithm; its stated formula is the separation-logic specification above.

# H is the list of live blocks; free_bytes are the arena bytes outside H.
def malloc_spec(H, free_bytes, n):
    p = choose_fresh_block(free_bytes, n)
    if p is None:
        return 0, H, free_bytes, None

    block = bytes_in(p, n)
    assert block <= free_bytes
    free_bytes = free_bytes - block
    H = H + [(p, n)]
    return p, H, free_bytes, block  # block ownership passes to caller

What You Gain, and What You Lose

You gain a specification that matches allocation’s changing ownership: free arena bytes may be used by the allocator, while a returned block becomes protected caller memory. The frame rule then preserves unrelated caller-owned data without listing it in every allocator contract.

You give up the simplicity of one fixed write set. The contract instead depends on a heap predicate and a live-block description, and proofs must maintain that ownership accounting. In this setting, that richer contract made the memory reasoning tractable: the reported proof work moved from a stalled fixed-footprint approach to a proof that closed after the separation-logic port. This module is about the allocator contract, not the separate refinement from interpreter semantics to compiled code.

Quiz

Why can’t one fixed set of addresses describe what malloc may write?

Because malloc always writes every byte in the arena.

Because the allocator’s writes depend on which bytes are still free and which blocks are live.

Because separation logic cannot describe disjoint memory.

Because the caller’s variables are part of the allocator’s fixed footprint.

$ check