# Will it Fit? Verifying Heap Space Bounds of Concurrent Programs under Garbage Collection

Alexandre Moine, Arthur Charguéraud, François Pottier

## ► To cite this version:

Alexandre Moine, Arthur Charguéraud, François Pottier. Will it Fit? Verifying Heap Space Bounds of Concurrent Programs under Garbage Collection. ACM Transactions on Programming Languages and Systems (TOPLAS), 2025, 10.1145/3716312. hal-04946590

HAL Id: hal-04946590

https://inria.hal.science/hal-04946590v1

Submitted on 13 Feb 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Will it Fit? Verifying Heap Space Bounds of Concurrent Programs under Garbage Collection

ALEXANDRE MOINE*, New York University, USA

ARTHUR CHARGUÉRAUD, Inria & Université de Strasbourg, CNRS, ICube, France

FRANÇOIS POTTIER, Inria, France

We present IrisFit, a Separation Logic with space credits for reasoning about heap space in a concurrent call-by-value language equipped with tracing garbage collection and shared mutable state.

We point out a fundamental difficulty in the analysis of the worst-case heap space complexity of concurrent programs in the presence of tracing garbage collection: if garbage collection phases and program steps can be arbitrarily interleaved, then there exist undesirable scenarios where a root held by a sleeping thread prevents a possibly large amount of memory from being freed.

To remedy this problem and eliminate such undesirable scenarios, we propose several language features, namely possibly-blocking memory allocation, polling points, and protected sections. Polling points are meant to be automatically inserted by the compiler; protected sections are delimited by the programmer and represent regions where no polling points must be inserted.

The heart of our contribution is IrisFit, a novel program logic that can establish worst-case heap space complexity bounds and whose reasoning rules can take advantage of the presence of protected sections. IrisFit is formalized inside the Coq proof assistant, on top of the Iris Separation Logic framework. We prove that IrisFit offers both a safety guarantee—programs cannot crash and cannot exceed a heap space limit—and a liveness guarantee—provided enough polling points have been inserted, every memory allocation request is satisfied in bounded time. We illustrate the use of IrisFit via several case studies, including a version of Treiber’s stack whose worst-case behavior relies on the presence of protected sections.

**CCS Concepts:** • **Theory of computation** → **Program verification**; **Separation logic**; ** Concurrency**; • **Software and its engineering** → **Garbage collection**.

Additional Key Words and Phrases: program verification, separation logic, concurrency, tracing garbage collection

**ACM Reference Format:**

Alexandre Moine, Arthur Charguéraud, and François Pottier. 2025. Will it Fit? Verifying Heap Space Bounds of Concurrent Programs under Garbage Collection. *ACM Trans. Program. Lang. Syst.* 1, 1, Article 1 (January 2025), 71 pages. https://doi.org/10.1145/3716312

# 1 Introduction

*Program Verification.* The most common aim of program verification is to establish the safety and functional correctness of a program, that is, to prove that this program does not crash and computes a correct result. In the area of deductive program verification [Filliâtre 2011], a program is usually verified with the help of a *program logic*, that is, a set of deduction rules whose logical soundness has

Authors' Contact Information: Alexandre Moine, New York University, New York, USA, alexandre.moine@nyu.edu; Arthur Charguéraud, Inria & Université de Strasbourg, CNRS, ICube, Strasbourg, France, arthur.chargueraud@inria.fr; François Pottier, Inria, Paris, France, francois.pottier@inria.fr.

<figure><img src="image_2.png" /></figure>

This work is licensed under a Creative Commons Attribution 4.0 International License.

© 2025 Copyright held by the owner/author(s).

ACM 1558-4593/2025/1-ART1

https://doi.org/10.1145/3716312

<footnote>*This work was carried out while this author was affiliated with Inria, Paris, France.</footnote>
been demonstrated once and for all. Separation Logic [Reynolds 2002] and Concurrent Separation Logic [Brookes and O'Hearn 2016; O'Hearn 2019; Jung et al. 2018b] are examples of program logics that allow compositional reasoning (that is, reasoning about a program component in isolation) in the presence of challenging features such as dynamic memory allocation, mutable state, and shared-memory concurrency.

*Verification of Resource Bounds.* Beyond safety and functional correctness, it may be desirable to establish bounds on *resource consumption*, that is, to prove that the resource requirements of a program (or program component) do not exceed a certain bound. Indeed, a program that requires an unexpectedly large amount of *time* may be unresponsive. A program that requires an unexpectedly large amount of *stack space* may crash with a stack overflow. A program that requires an unexpectedly large amount of *heap space* may exhaust the available memory and make the system unstable.

Assuming that one is able to tell where in the code the resource of interest is consumed and produced, and how much of it is consumed or produced, reasoning about resource consumption can be reduced to reasoning about safety. To do so, one can construct a variant of the program that is instrumented with a *resource meter*, that is, a global variable whose value indicates what amount of the resource remains available. In this instrumented program, one places assertions that cause a runtime failure if the value of the meter becomes negative. If one can verify that the instrumented program is safe, then one has effectively established a bound on the resource consumption of the original program.

The principle of a resource meter has been exploited in many papers, using various frameworks for establishing safety. For instance, Crary and Weirich [2000] exploit a dependent type system; Aspinall et al. [2007] exploit a VDM-style program logic; Carbonneaux et al. [2015] exploit a Hoare logic; He et al. [2009] exploit Separation Logic. The manner in which one reasons about the value of the meter depends on the chosen framework. In the most straightforward approach, the value of the meter is explicitly described in the pre- and postcondition of every function. This is the case, for instance, in He et al.'s work [2009], where two distinct meters are used to measure stack space and heap space. In a more elaborate approach, which is made possible by Separation Logic, the meter is not regarded as an integer value but as a bag of *credits* that can be individually *owned*. The sum of all credits in circulation corresponds to the value of the meter. This removes the need to refer to the absolute value of the meter: instead, the specification of a function may indicate that this function requires a certain number of credits and produces a certain number of credits.

*Verification of Heap Space Bounds, without Garbage Collection.* A programming language that does not have garbage collection usually offers an explicit memory deallocation instruction. Thus, it is easy to tell where heap space is consumed and produced: an allocation instruction consumes the amount of space that it receives as an argument; a deallocation instruction recovers the space occupied by the heap block that is about to be deallocated.

In such a setting, traditional Separation Logic, extended with space credits, can be used to establish verified heap space bounds. Atkey [2011] presents a Separation Logic with an abstract resource that is consumed and produced by two distinct primitive operations, akin to space credits with explicit allocation and deallocation. Hofmann's work on the typed programming language LFPL [2000] can be viewed as a precursor of this idea: LFPL has explicit allocation and deallocation, which consume and produce values of a linear type, written $\diamond$, whose inhabitants behave very much like space credits.

*Verification of Heap Space Bounds, with Garbage Collection.* In the presence of garbage collection, how does one reason about heap space? In this setting, the programming language does not have
a memory deallocation instruction. Thus, it is not evident at which program points space can be reclaimed. A tracing garbage collector (GC) can be invoked at arbitrary points in time, and may deallocate any subset of the *unreachable blocks*. An unreachable block is a block that is not *reachable* from any *root* via a *path* in the heap. Thus, reasoning about heap space in the presence of garbage collection requires reasoning about roots and unreachability.

Madiot and Pottier [2022] make a first step towards addressing this problem. They extend Separation Logic with several concepts. To keep track of free space, they use space credits. They view memory deallocation as a *logical operation*: it is up to the person who verifies the program to decide at which points this operation must be used and which memory blocks must be *logically deallocated*. This decision is subject to a proof obligation: a memory block can be logically deallocated only if it is unreachable. Unfortunately, the concept of unreachability is not local: that is, this concept cannot easily be expressed in terms of traditional Separation Logic assertions. Therefore, Madiot and Pottier rephrase this proof obligation as follows: a memory block can be logically deallocated if it has no predecessors and is not a root. To record the predecessors of every memory block, they use *pointed-by* assertions [Kassios and Kritikos 2013]. To record which blocks are roots, they focus their attention on a low-level language, where the stack is explicitly represented in the heap as a collection of “stack cells”. Then, a block is a root if and only if it is a stack cell.

In previous work [Moine et al. 2023], we scale Madiot and Pottier’s ideas up to a high-level language, where the stack is implicit. We introduce *Stackable* assertions to implicitly record which memory locations are “invisible roots”, that is, which memory locations are roots because they appear in some indirect caller’s stack frame.

Neither of these papers focuses on concurrency. Madiot and Pottier [2022] technically support concurrency, but only for a low-level language with stack variables explicitly allocated in the heap, and without any concurrent example covered. Moine et al. [2023] do not support it. By design, their *Stackable* assertion keeps track of a single stack. Extending it with support for multiple stacks is a priori not straightforward.

*Verification of Heap Space Bounds, With Garbage Collection and Concurrency.* In the present paper, we target a high-level programming language equipped with garbage collection and shared-memory concurrency. In such a setting, multiple threads run concurrently. They share a common heap; each thread has its own implicit stack.

Our initial aim in this project was to *propose a program logic* that allows its user to reason about heap space, and to verify heap space complexity bounds, in a concurrent setting. However, in the course of this work, we came to realize that, unless some care is taken, concurrent programs can have bad worst-case heap space complexity—that is, worse complexity than one might naively imagine. Thus, in addition to our initial aim, which was to let our program logic serve as a tool to *describe* the worst-case scenarios, we decided to also propose *programming language features* that let the programmer *eliminate* some of the worst-case scenarios.

In terms of programming language design, our proposed changes and additions are as follows. First, we impose a limit on the size of the heap. To ensure that this limit is never exceeded, we make *memory allocation* a possibly *blocking* instruction: if a memory allocation instruction would cause the size of the heap to exceed the limit, then this instruction must wait for enough space to become available. Second, we introduce *polling points*. If any thread is waiting for space, then a polling point blocks the current thread. Polling points are intended to be automatically inserted by the compiler. By inserting sufficiently many of them, the compiler can ensure that a thread that is waiting for space cannot be forever starved. Third, to eliminate undesirable scenarios where a thread reaches a polling point while holding certain roots (which would prevent the garbage collector from reclaiming certain data structures), we let the programmer *delimit protected sections*.
where polling points must not be inserted. To ensure that a protected section terminates in bounded time, we forbid blocking instructions (that is, memory allocations and polling points) and function calls within protected sections. By decorating our implementation of Treiber’s lock-free stack with protected sections, we are able to prove that “pop frees up one list cell worth of heap space”, as desired (§3.3).

Regarding the heap size limit, we propose two variants of the semantics. Our *default* semantics uses a fixed limit, which must be set before the program is executed. Our *growing* semantics lets this limit grow at runtime under certain conditions: when no thread is inside a protected section, if (after garbage collection) there is insufficient space to satisfy a memory allocation request, then the limit is increased (say, doubled). The default semantics is slightly easier to understand, whereas the growing semantics is more realistic, as it does not require advance knowledge of a suitable limit.

We propose a program logic that lets users establish worst-case heap space complexity bounds. This program logic is independent of which variant of the semantics—default or growing—is chosen. It is sound, in a certain sense, with respect to each variant. Indeed, under each variant, we are able to establish a safety property. With respect to the default semantics, we prove: if a program has been statically verified with a budget of *S* space credits, and if at runtime the heap size limit is set to *S*, then the program cannot run out of space. With respect to the growing semantics, we prove: if a program has been statically verified with a budget of *S* space credits, then at runtime the (growing) heap size limit cannot exceed a bound that is expressed in terms of *S* (say, 2*S*). Furthermore, under both semantics, and under the assumption that enough polling points have been inserted, we establish a liveness property: no thread remains forever blocked. Our program logic includes reasoning rules that exploit the presence of protected sections to establish *improved* heap space complexity bounds: this is illustrated by the example of Treiber’s stack (§3.3, §11.5).

Although our program logic does include reasoning rules for polling points, these rules are not needed by the end user, who reasons about a source program in which polling points have not yet been inserted. This source program can be viewed as the description of a family of instrumented programs, which are obtained from the source program by inserting polling points in arbitrary places, outside of protected sections. If the source program can be verified (that is, if it abides by the rules of the program logic) then every instrumented program in this family can also be verified. Thus, the correctness and worst-case heap space complexity properties that are established by the user about the source program still apply after polling points are inserted by the compiler.

*Contributions.* The main contributions of this paper are the following:

* We present LambdaFit (§2, §4), an imperative language with shared-memory concurrency and tracing garbage collection. The novel aspects of LambdaFit include a heap size limit, blocking allocations, polling points, and protected sections.

* We introduce IrisFit (§5, §6, §10), a Separation Logic that allows establishing *safety*, *functional correctness*, and *worst-case heap space complexity* properties of concurrent programs, in the presence of garbage collection, and allows *compositional reasoning*.

* We prove the soundness of IrisFit (§8). More specifically, we establish two results. A *safety* theorem guarantees that a verified program cannot crash and that its heap size cannot exceed a certain bound. A *liveness* theorem guarantees that after enough polling points have been (automatically) inserted, no thread can be forever blocked by a memory allocation request. In fact, we prove a slightly stronger liveness statement: at all times, *in a bounded number of steps*, the system must reach a configuration where no thread is blocked by a memory allocation request. We establish this result *without formulating a fairness hypothesis*. We prove safety and liveness theorems for both variants of the semantics of LambdaFit, namely the fixed-limit variant and the growing-limit variant.
* We prove that IrisFit is sound also with respect to an *oblivious* semantics of LambdaFit, where there is no heap size limit, a memory allocation instruction is never blocked, and polling points have no effect. In such a setting, our safety theorem (§8.4) guarantees that a verified program cannot crash and that (when every thread is outside of a protected section) its *live* heap size cannot exceed a certain bound. There is no need in this setting for a liveness theorem. This result emphasizes that IrisFit is largely independent of the non-standard features of LambdaFit.

* We encode *closures* in LambdaFit and show how to reason about them with IrisFit (§9). Compared with our previous paper [Moine et al. 2023], we propose an improved treatment of closures: the *Spec* predicate, which describes the behavior of a closure, is persistent.

* We verify several case studies (§11), namely: an implementation of "fetch-and-add" as a CAS loop; a concurrent counter that is encapsulated as a pair of closures; a library for async/finish parallelism; and Treiber's lock-free stack [1986]. This gallery of challenging examples illustrates the expressive power of IrisFit.

All of our results, including the validity of our reasoning rules, our soundness theorems, and our case studies, are mechanized using the Coq proof assistant and the Iris framework [Jung et al. 2018b]. For details about the soundness proof and additional case studies, we refer the reader to our mechanization [Moine 2025] and to the first author's dissertation [Moine 2024].

Because we wish to make the present paper self-contained, we borrow some text from our previous paper [Moine et al. 2023]. The re-used material amounts to roughly 8 pages in total. The main re-used passages are the beginning of this introduction, the design and explanation of the pointed-by-heap assertion (§5.6), the discussion and definition of the closure macros (§2.7, §9.2), the concept and presentation of triples with souvenir (§10), and part of the discussion of the related work (§12.3, §12.4, §12.5).

# 2 Overview

LambdaFit is a call-by-value language with dynamic memory allocation, mutable state, shared-memory concurrency, and tracing garbage collection. Its syntax and semantics are standard, save for a few original aspects.

First, LambdaFit is restricted to closed functions, also known as *code pointers*. We encode closures as heap-allocated objects that store code and data (§2.7).

Second, LambdaFit exhibits several non-standard features related with memory management. First, a memory allocation instruction that would cause the size of the heap to exceed a certain limit is blocked. Second, LambdaFit's syntax includes three non-standard instructions, namely an instruction that represents a *polling point* and two instructions that mark the beginning and end of a *protected section*.

## 2.1 One Language, Several Semantics

In this paper, we define and use three semantics, or three variants of the semantics, of LambdaFit. Let us explain why each variant exists and what role it plays in the paper.

1. The most important semantics is the *default semantics*. This semantics involves the concept of a *root* and has explicit garbage collection steps (§2.2). It imposes a *fixed limit S* on the size of the heap. This limit is a parameter of the semantics. A "large" memory allocation request, which would cause this limit to be exceeded, is blocked (§2.3): we say that it is "waiting for space". Furthermore, if any thread is waiting for space, then a polling point is blocked (§2.4). Protected sections (§2.5) serve mainly to delimit areas where polling points must not be inserted by the compiler. In the semantics, they play a minor role: within a protected section,
polling points, memory allocation instructions, “fork” instructions, and function calls are forbidden—they cause a crash.

This semantics (as well as its variants, discussed next) is non-deterministic. This is due not only to concurrency but also to the fact that garbage collection can take place at an undetermined point in time and can deallocate an undetermined number of unreachable blocks. Our soundness theorems guarantee that, in every possible execution, the heap space usage of a verified program respects the bound *S*. Thus, the non-determinism that is inherent in the semantics makes our soundness theorems stronger. If a specific implementation of LambdaFit exhibits fewer behaviors than permitted by the semantics, then our soundness theorems still hold for this implementation.

A potential criticism that one might formulate about the default semantics is the fact that it requires setting the heap limit to a suitable value *S* before the program is executed. If the program has been fully verified using IrisFit, then a suitable value of *S* may be known. However, it is more realistic to expect that only part of the program has been verified. Furthermore, if the program receives data from the outside (via the file system or the network) then its space requirement may depend on the input that it receives. For these reasons, it seems worthwhile to design and discuss also a variant of the default semantics that is equipped with a *growing limit* on the size of the heap.

(2) In the *growing semantics*, as in the default semantics, there is a limit on the size of the heap, which serves to identify and block “large” memory allocation requests. However, in the *growing semantics*, the limit is not fixed. Instead, at runtime, if the current limit is found to be too low, then the limit is increased. Such an increase can take place only while no thread is inside a protected section.

A similar strategy for growing the size of the heap is used in real-world runtime systems, such as the OCaml runtime system [Madhavapeddy and Minsky 2022, §25.4.1] and the Haskell runtime system [Marlow et al. 2008, §5].

Our discussion of the growing semantics occupies only two sections of the paper (§4.2.10, §8.3). However, we believe that this discussion plays an essential role in arguing that a *practical* runtime system that obeys the design of LambdaFit can be implemented.

Finally, we define an *oblivious semantics*, which ignores the non-standard features of LambdaFit: in this semantics, memory allocation is never blocked, and polling points have no effect. This semantics serves two purposes. First, it enables us to state the *core soundness* guarantee that is offered by IrisFit in the absence of the non-standard features of LambdaFit. Second, it plays a key technical role. The soundness properties of IrisFit with respect to the default and growing semantics are obtained as corollaries of its core soundness property with respect to the oblivious semantics.

(3) In the oblivious semantics, no instruction is ever blocked. This semantics does not impose a limit on the size of the heap. Therefore, it does not need and does not have garbage collection: an unreachable block remains allocated forever. In this semantics, one cannot bound the total size of the heap (including garbage). Still, under the assumption that every thread is outside a protected section, one can bound the live heap size, that is, the size of the reachable fragment of the heap.

Our discussion of the oblivious semantics is limited to two sections of the paper (§4.2.7, §8.4).

We wish to reassure a reader who might be worried about an apparent proliferation of semantics. First, the three semantics share many auxiliary definitions, so there is limited redundancy. Second, throughout the paper, we focus on the default semantics. Where one of the other two semantics is discussed, this is explicitly indicated. Last but not least, we propose just one program logic, IrisFit, whose reasoning rules (§2.6) are independent of which semantics is considered. For each of the three semantics, we are able to prove that if a program has been verified using IrisFit then its heap space usage is bounded in a certain sense (§8).
## 2.2 Roots and Garbage Collection

Garbage collection [Jones and Lins 1996] deallocates some or all unreachable memory blocks, where a block is *reachable* if there exists a path from some *root*, through the heap, to this block. In the oblivious semantics of LambdaFit (§2.1), garbage collection is not explicitly modeled; nevertheless, one can define the worst-case heap space complexity of a program as the maximum value (over all possible executions) of its live heap size, where the *live heap size* is the sum of the sizes of all reachable heap blocks. In the default semantics of LambdaFit (§2.1), garbage collection is explicitly modeled: a garbage collection step deallocates an arbitrary number of unreachable heap blocks. In either approach, it is necessary to answer to the question: what is a root?

How can the intuitive concept of a root be formally defined in the setting of a small-step, substitution-based operational semantics? Before addressing this question, let us recall a few fundamental aspects of such a semantics. In an *operational* semantics, a program state, which represents the state of a running program, is a syntactic object. Here, because we are interested in concurrent programs with dynamic memory allocation, a program state includes a thread pool (a list of threads) and a heap (a finite map of memory locations to memory blocks). In a *small-step* semantics, the manner in which the program state evolves over time is described by a reduction relation, that is, a binary relation on program states. In a *substitution-based* semantics, within the thread pool, each running thread is represented as a closed term, that is, a term without free variables. The reduction rules ensure that, whenever the scope of a variable is entered, a closed value is substituted for this variable. Thus, a closed term that represents a running thread describes both the code that this thread is about to execute and the data to which this thread has access. In particular, a memory location $\ell$ is a closed value, and a closed term that represents a running thread can contain memory locations.

In such a setting, what is a root? A simple, commonly agreed-upon answer is: a *root is a memory location* $\ell$ that appears in at least one running thread $t$. By this, we mean that the closed term $t$, which represents one of the currently running threads, literally contains one or more occurrences of the memory location $\ell$.

This convention is known as the *free variable rule* (FVR) [Felleisen and Hieb 1992; Morrisett et al. 1995]. Intuitively, the FVR makes sense because the (computable) set of memory blocks that are reachable from the locations that the program knows about is a conservative approximation of the (uncomputable) set of memory blocks that might be accessed in the future by the program. However, one must keep in mind that the FVR is not a static approximation of the dynamic semantics. Instead, the FVR is *part of* the definition of the dynamic semantics. It defines the concept of *root*, which in turn is used to define reachability and garbage collection.

The reader may wonder whether real-world programming languages respect the FVR. As far as we know, many real-world implementations of garbage-collected languages, such as OCaml, SML, Haskell, Scala, Java, and more, are meant to respect the FVR. Unfortunately, this intention is often undocumented. A prominent example of a compiler that explicitly respects the FVR is the CakeML verified compiler. Gómez-Londoño et al. [2020] and Gómez-Londoño and Myreen [2021] prove that the CakeML compiler respects a cost model that is defined at the level of the intermediate language DataLang and that includes a form of the FVR.

## 2.3 Why Block Large Memory Allocation Requests

In the presence of tracing garbage collection, two measures of the size of the heap must be distinguished, namely the allocated heap size and the live heap size. The *allocated heap size*, or simply *heap size*, is the sum of the sizes of all allocated heap blocks. The *live heap size* is the sum
of the sizes of all reachable heap blocks. In other words, it is the allocated heap size minus the sizes of the unreachable blocks.

Our main goal in this paper is to bound the heap size<fnref n="1" /> in a setting where LambdaFit is equipped with its default semantics (§2.1).

The default semantics is parameterized by a limit $S$ and is designed in such a way that the heap size always remains less than or equal to $S$. This property, which is stated by Lemma 4.2 (§4.2.9), is enforced as follows. Let us say that a memory allocation request is *large* if it would cause the heap size to exceed $S$, that is, if the sum of the current heap size and the number of requested words exceeds $S$. Otherwise, let us say that the allocation is *small*. Then, a large memory allocation instruction is not allowed to proceed: it is *blocked*. Once garbage collection takes place and is able to free enough space in the heap, this memory allocation instruction may become small, therefore unblocked.

This explains one aspect of the design of the default semantics: by blocking large memory allocation instructions, we ensure that one kind of undesirable behavior, namely *growing the heap too large*, is eliminated a priori. Two kinds of undesirable behavior remain permitted by the default semantics, namely *crashes* and *deadlocks*: a thread can crash or become forever blocked. Under certain assumptions about the placement of polling points, our program logic statically guarantees that these undesirable behaviors cannot arise: this is stated by our *safety* and *liveness* theorems (Theorems 8.1 and 8.2).

An alternative point of view is offered by the *oblivious* semantics of LambdaFit (§2.1). In that semantics, there is no limit on the size of the heap, and no instruction is ever blocked. Thus, a different kind of undesirable behavior, namely *deadlocks*, is eliminated a priori. The undesirable behaviors that remain possible are *crashes* and *growing the heap too large*. With respect to the oblivious semantics, our program logic provides two guarantees: first, no thread can crash; second, if the program has been verified under the hypothesis that $S$ space credits are initially granted, then, in every possible execution, provided every thread is currently outside a protected section, the current live heap size is at most $S$. These guarantees are stated in our *core soundness* theorem (Theorem 8.4). We emphasize that $S$ is not a parameter of the oblivious semantics; it appears only in the statement of the core soundness theorem.

The points of view offered by the default semantics and by the oblivious semantics are subtly different; we believe that it is enlightening to understand them both. Furthermore, there is a technical connection between them: we first establish the core soundness theorem (Theorem 8.4), then use this theorem as a stepping stone in the proof of Theorems 8.1 and 8.2.

## 2.4 Polling Points

The existence of blocking memory allocation instructions endangers *liveness*: for some programs, there exist adversarial schedules where a large memory allocation request is forever blocked. This can happen, for example, if some other threads are always scheduled, so the garbage collector is never allowed to run. More specifically, imagine that thread *A* is blocked by a large memory allocation request, while thread *B* is in an infinite loop. Then, the scheduler can choose to always execute thread *B* and never execute the garbage collector, so thread *A* remains forever blocked.

<footnote n="1">¹By adopting a measure whose definition is a sum of the sizes of the heap blocks that the program creates, we restrict our attention to a *logical* notion of heap size, that is, a notion that depends only on the program and on the semantics of the programming language. One might instead wish to control the *physical* heap size, that is, how much memory the runtime system requests from the operating system. This would require knowing which garbage collection technique is used, whether the garbage collector is able to perform compaction (so as to eliminate fragmentation), and so on. Our analysis does not require this information and does not bound the physical heap size.</footnote>
We wish to forbid this scenario and to formally establish a liveness guarantee of the form: *always, eventually, every thread can make progress* (Theorem 8.2).

To this end, we equip LambdaFit with *polling points*. A polling point is a synchronization instruction, a form of barrier. A thread may proceed past a polling point only if no large memory allocation request is currently outstanding. In other words, if any thread is currently waiting for space, then no thread can move past a polling point.

By inserting sufficiently many polling points into a program, one can ensure that every memory allocation request is eventually satisfied. Indeed, by inserting enough polling points, one can enforce the following property: as soon as one thread is blocked on a large memory allocation request, every thread must eventually reach a polling point or a large memory allocation request, where it, too, becomes blocked. At this point, no thread can make progress, so garbage collection must take place. Once garbage collection has made enough space available—which our program logic statically guarantees is possible!—all outstanding memory allocation requests can be satisfied.

In the example scenario that is outlined above, a polling point must be inserted in the infinite loop of thread B. Then, this thread must eventually reach a polling point, where it becomes blocked. The only permitted step is then a garbage collection step, which is expected to free up enough memory to satisfy thread A's large allocation request. Consequently, the two threads become unblocked.

In principle, polling points could be manually inserted by the programmer, but that would be tedious. In practice, we expect a compiler to automatically insert polling points where needed. In §8.2, we prove that a particular polling point insertion strategy, inspired by that of the OCaml 5 compiler, does indeed insert enough polling points to guarantee liveness. We establish this result without a fairness hypothesis about the scheduler.

## 2.5 Protected Sections

Polling points are meant to be inserted by the compiler in arbitrary places. However, inserting a polling point in a badly-chosen place can impact (that is, increase) the worst-case heap space complexity of a data structure: this is illustrated later on by the example of Treiber's stack (§3). To remedy this problem, we equip LambdaFit with *protected sections*, that is, sections of the code in which the compiler must not insert polling points. We require protected sections to be “short”, that is, to terminate in bounded time. Thus, when one thread is blocked by a large memory allocation request (§2.3), every other thread must eventually exit its protected section (if it is currently within such a section) and reach a polling point.

Protected sections provide the programmer with a means of controlling where polling points should *not* be placed. In comparison with manually placing polling points, this approach is not only more concise, but also more informative, as it lets the programmer explicitly document the places where a thread must not be blocked. The intuitive reason why a thread must not be blocked (in a specific place) is that it must instead be allowed to make progress and release some of its roots, thereby allowing the garbage collector to reclaim more space.

A protected section is explicitly delimited by two special instructions, enter and exit, which mark the beginning and end of the section. A single well-balanced construct “protected {$t}$” would be insufficiently flexible, because a protected section typically has one entry point and multiple exit points. This is illustrated by the example of Treiber’s stack (Figure 3).

Protected sections are subject to two restrictions. First, they cannot be nested. Second, a protected section must not contain a memory allocation instruction, a “fork” instruction,<fnref n="2" /> a polling point (§2.4),

<footnote n="2">²In our operational semantics, “fork” does not allocate any memory in the heap. We could technically allow “fork” inside a protected section without breaking any of our results. In the real world, though, “fork” is likely to allocate memory. Because we forbid memory allocation inside a protected section, it seems natural to disallow “fork” inside protected sections as well.</footnote>
or a function call.<fnref n="3" /> These restrictions ensure that a protected section cannot contain a blocking instruction and can be exited in a bounded number of steps. The syntax of LambdaFit does not enforce these restrictions; however, violating them causes a runtime error, and is statically forbidden by our program logic.

The reader may wonder whether protected sections are ghost code, that is, whether (after polling points have been inserted) protected sections can be erased. In the default semantics (§2.1), this is essentially true: provided protected sections are correctly used (that is, enter and exit instructions are well-balanced, and protected sections do not contain memory allocations, polling points, “fork” instructions, or function calls), they have no semantic effect. If such correct usage is statically enforced, then at runtime protected sections can be erased. In the growing semantics (§2.1), however, protected sections do play a role and cannot be erased. Indeed, the heap size limit can be increased *only when all threads are outside protected sections*. Without this restriction, we would not be able to establish Theorem 8.3, which states that the heap size remains bounded.

Earlier (§1), we have pointed out that a source program describes a family of instrumented programs, which are obtained from the source program by inserting polling points in arbitrary places outside of protected sections. By applying IrisFit to just the source program, the user obtains a heap space bound that holds regardless of where polling points are inserted; in other words, the user obtains a guarantee about the worst-case heap space complexity of every program in this family. In terms of space complexity, decorating the source program with protected sections is always beneficial. Indeed, adding or extending protected sections reduces the family of programs that the source program represents: this can reduce the worst-case heap space complexity of this family, and cannot increase it. This phenomenon is illustrated by the example of Treiber’s stack (§3).

On the flip side, in practice, protected sections can have a cost. While they can improve the worst-case heap space complexity of a program family, they can also increase *latency*. Indeed, larger protected sections potentially imply larger gaps between polling points, therefore a longer time until a thread that is waiting for space can be unblocked. In practice, it seems wise to use as few protected sections as possible and to keep them as short as possible.

## 2.6 A Concurrent Separation Logic for Heap Space

This paper presents IrisFit, a concurrent Separation Logic for LambdaFit. IrisFit shares many features with pre-existing Separation Logics. The behavior of a program fragment is described by a *triple*, an assertion whose parameters include a precondition (an assertion that describes the initial state), the program fragment of interest, and a postcondition (an assertion that describes the final state). In IrisFit, a triple also includes a thread identifier, as the logic assigns a unique name to each thread. A rich vocabulary of logical connectives, including *points-to* assertions, *separating conjunction*, and many more, is used to construct assertions, which encode both *knowledge* of the current state and *permission to update* this state in certain ways.

What sets IrisFit apart from traditional Separation Logics? IrisFit borrows ideas from previous Separation Logics equipped with support for reasoning about heap space in the presence of garbage collection [Madiot and Pottier 2022; Moine et al. 2023] and scales them up to a concurrent setting. *Space credits* keep track of available space and serve as permissions to allocate memory. Furthermore, several kinds of assertions record which memory locations are reachable and in what way they can be reached. *Pointed-by-heap* assertions [Madiot and Pottier 2022] keep track of predecessors of each location in the heap. *Pointed-by-thread* assertions (new in this paper) keep track of the threads in which each location is a root. Like previous logics [Madiot and Pottier 2022; Moine et al.

<footnote n="3">³Because loops are encoded as recursive functions, forbidding function calls inside protected sections also forbids loops inside protected sections.</footnote>
2023], IrisFit features a *ghost deallocation rule*. Because the programming language does not have an explicit memory deallocation instruction, it is up to the user of the logic to decide where to apply this rule. This rule requires proof that the memory block of interest is unreachable. This proof takes the form of pointed-by-heap and pointed-by-thread assertions, which are consumed; space credits are produced in their stead. A novelty of this paper is that logical deallocation *does not require or consume the points-to assertion*.

A crucial novel aspect of IrisFit is its ability to take advantage of protected sections while reasoning. Indeed, IrisFit offers a relaxed way of keeping track of roots inside protected sections. Ordinarily, pointed-by-thread assertions record which locations are roots, and as long as a location is a root, this location cannot be logically deallocated. Inside a protected section, however, an exception to this regime is made: the logic keeps track of a set of *temporary* roots. The user can turn an ordinary root into a temporary root (and vice-versa). The logic requires that, by the time the protected section ends, no temporary roots remain. Thus, by that time, every temporary root must no longer be a root (or must have been turned back into an ordinary root). Crucially, inside a protected section, the condition under which logical deallocation is permitted is: *if a location *l* is not an ordinary root in any thread, and if *l* has no live heap predecessors, then it can be logically deallocated*. In other words, logical deallocation is oblivious to the existence of temporary roots.<fnref n="4" /> Finally, perhaps surprisingly, because the points-to assertion survives logical deallocation and enables read and write access, *a temporary root that has already been logically deallocated can still be accessed* before the protected section ends. This pattern appears while verifying lock-free data structures (§11.5).

This overview of IrisFit may raise two questions about our approach. Why bother with garbage
collection? Assuming that a program has been verified using IrisFit, could one replace the logical
deallocation points identified by the proof with actual calls to free, thereby removing the need for
garbage collection? We answer these two questions separately.

First, garbage collection is a widely used memory management technique. It is used, among
other examples, in Scheme, Java, Scala, Haskell, OCaml, C#, JavaScript, and Go. There are arguably
strong reasons why a programmer might choose a programming language equipped with garbage
collection. These reasons include simplicity (garbage collection enables an elegant, high-level
programming style), safety (garbage collection removes a class of runtime errors, including double-
free and use-after-free errors), and performance (garbage collection allows bulk deallocation, which
in certain circumstances can be more efficient than individual object deallocation). That said,
garbage collection does make space usage analysis more difficult. IrisFit is the first program logic
that allows such an analysis in the presence of challenging features such as mutable state and
concurrency. Moreover, we believe that, in the future, IrisFit can serve as a logical foundation for
automated space complexity analyses (§13).

Second, although in simpler settings [Madiot and Pottier 2022; Moine et al. 2023] it could make
sense to transform logical deallocation points into physical memory deallocation instructions,
IrisFit is a more advanced logic, where such a transformation can be unsound or impossible. Indeed,
as explained earlier in this section, IrisFit allows for logically deallocating a block *in advance*
inside a protected section, even if this block is still in use within this protected section. In such
a situation, transforming a logical deallocation operation into a physical free instruction would
introduce a use-after-free error. Furthermore, IrisFit allows one thread to logically deallocate
a block whose address is available (at runtime) only to some other thread. This idiom, which we call

<footnote n="4">⁴Should space become scarce, in the worst-case scenario, the garbage collector will be invoked at a time where every thread is blocked at a memory allocation instruction or at a polling point. In such a situation, every thread is outside a protected section, so there are no temporary roots. Thus, the existence of temporary roots inside protected sections has no impact on the worst-case scenario.</footnote>
logical deallocation by proxy, appears in our analysis of Treiber’s stack (§11.5). In such a situation, transforming logical deallocation into a free instruction is impossible, because the address of the object that must be deallocated is not at hand! In conclusion, we remark that, in concurrent code, placing free instructions in a correct and optimal way is known to be an extremely hard problem, which IrisFit does not solve. This problem is the raison d’être of safe memory reclamation (SMR) schemes (§12.6) and one key argument in favor of general-purpose concurrent garbage collectors, which subsume SMR schemes.

## 2.7 Closures

To model the space complexity of programs that involve closures [Landin 1964; Appel 1992], we must somehow reflect the fact that a closure is a heap-allocated object. It has an address, a size, and may hold pointers to other objects. Thus, a closure has both direct and indirect impacts on space complexity: it occupies some space; and, by pointing to other objects, it keeps these objects live (reachable), preventing the GC from reclaiming the space that they occupy.

Thus, we cannot use the standard small-step, substitution-based semantics of the λ-calculus, where a λ-abstraction is a value that does not have an address or a size. Instead, two approaches come to mind. One approach is to view a λ-abstraction as a primitive expression (not a value) whose evaluation causes the allocation of a closure. Another approach is to adopt a restricted calculus that offers only closed functions (as opposed to λ-abstractions with free variables) and to define closure construction and closure invocation as macros, or canned sequences of instructions, on top of this calculus. As shown by Paraskevopoulou and Appel [2019], these two approaches yield the same space cost model. Furthermore, provided suitable syntax is chosen, the end user does not see the difference: it is just a matter of presentation in the metatheory.

We choose the second approach, because we find it simpler. In so doing, we follow Gómez-Londoño et al. [2020], who define the CakeML cost model at the level of DataLang, the language that serves as the target of closure conversion.

Thus, we equip LambdaFit with closed functions, which we also refer to as code pointers. We write $\mu_{ptr}f.\lambda\vec{x}.t$ for a (recursive, multi-argument) closed function, and write $(v\vec{u})_{ptr}$ for the invocation of the code pointer $v$ with arguments $\vec{u}$. LambdaFit does not have primitive closures. This allows us to present a program logic for LambdaFit and to establish the soundness of this logic without worrying about closures. Once this is done, we define closure construction $\mu_{clo}f.\lambda\vec{x}.t$ and closure invocation $(\ell\vec{u})_{clo}$ as macros, and we extend our program logic with high-level reasoning rules for closures (§9). This allows end users to reason about these macros without expanding them and without even knowing how they are defined. In summary, LambdaFit can macro-express closures, and our logic allows reasoning about closures in the same way as if they were primitive constructs.

Our construction of closures as macros is the same as in our previous paper [Moine et al. 2023]. Our treatment of closures in the logic, however, has been generalized to multiple threads and simplified by describing closures via persistent predicates (§9).

## 3 Why Treiber's Stack Needs Protected Sections

To illustrate how protected sections can lead to tighter space bounds, we use the example of Treiber's stack, a lock-free, linearizable stack [Treiber 1986]. We first present a naive implementation of this data structure without protected sections (§3.1). We point out that this implementation has unsatisfactory worst-case heap space complexity: there are scenarios where a successful pop operation does not allow any memory cell to be freed (§3.2). All memory can eventually be recovered, but this may require waiting until all threads have completed their interaction with the stack. This situation is unpleasant: pop cannot be given a simple logical specification of the form “a successful pop frees up one list cell worth of heap space”. We show that, by annotating the
<figure><img src="image_3.png" /><figcaption>Fig. 1. An unsafe-for-space implementation of Treiber's stack</figcaption></figure>

code with protected sections, one can eliminate these undesirable scenarios and obtain the desired specification (§3.3). Near the end of this paper (§11.5), we present the details of how we formally establish this specification in IrisFit.

## 3.1 Naive Implementation of Treiber's Stack

Treiber's stack is implemented as a mutable reference to an immutable linked list, whose head corresponds to the top of the stack. Pseudo-code is presented in Figure 1.

The function call `create()` creates a new stack, represented as a fresh reference to an empty list `nil`. The `nil` value takes up no heap space: it is in fact an integer value.

The functions `push` and `pop` make crucial use of the atomic *compare-and-swap* (CAS) instruction. Each of them is implemented as a “CAS loop”: it prepares an operation and attempts to atomically commit this operation using a CAS instruction. If the CAS succeeds, the function returns; otherwise, the loop continues with another attempt. Here, each loop is encoded as a tail-recursive function.

The function `push s v` inserts a new element `v` in a stack `s`. First, `s` is dereferenced (line 4) so as to obtain the address `h` of the head of the linked list. Then, a new list cell `h'` is allocated (line 5). The “data” and “tail” fields are initialized with `v` (line 6) and `h` (line 7). Then, a CAS instruction attempts to update the content of `s` from `h` to `h'` (line 8). If this attempt is successful, `push` returns (line 9); otherwise, it means that a concurrent `push` or `pop` has succeeded. In this case, another attempt is made (line 10).

The function `pop s` extracts the top element of the stack `s`. First, the head `h` of the linked list is read (line 12). If the list is empty, `pop` makes another attempt (line 14), waiting for the stack to become nonempty. Otherwise, the “tail” field of the cell `h` is read so as to obtain the address `h'` of the next list cell (line 16). Then, a CAS instruction attempts to update the content of `s` from `h` to `h'` (line 17). If this attempt is successful, `pop` reads the “data” field of the cell `h` and returns its value (line 18); otherwise, it means that a concurrent `push` or `pop` has succeeded. In this case, another attempt is made (line 19).

Treiber's stack is *linearizable* [Herlihy and Wing 1990], in the sense that `push` and `pop` atomically take effect at a certain point between the function call and return.

## 3.2 Space Consumption of Treiber's Stack without Protected Sections

What is the space consumption of `push` and `pop`? Let us write `W` for the number of memory words occupied by one list cell. A successful `push` operation consumes `W` memory words, as it allocates one single list cell. Symmetrically, one might expect a successful `pop` operation to free up `W` memory words. Indeed, the list cell that is extracted from the list becomes unused, so one might expect the garbage collector to be able to reclaim it.
<figure><img src="image_4.png" /><figcaption>Fig. 2. Initial and problematic states of the example scenario for Treiber’s stack. A box represents a memory block, whose location appears at the top left. A circled location is a root.</figcaption></figure>

However, this intuition is false: when pop returns, although the list cell that has just been extracted is indeed unused, it is not necessarily unreachable. Indeed, it might still be a root of other threads that are still in the process of executing a push or pop operation (which will fail) on this cell. In such a case, all descendants of this cell remain reachable as well. This issue can lead to bad worst-case heap space complexity, but this depends on the placement of polling points.

*A Potentially Problematic Scenario and a Way Out.* Let us examine the problematic scenario in greater detail. In this scenario, a cell that has been extracted by a successful pop operation remains reachable by other threads, preventing its immediate reclamation. Figure 2 depicts the initial state and the problematic state of this scenario. Suppose that the stack $s$ consists of a single list cell whose address is $\ell$. Suppose that thread $A$ attempts to push a new value onto $s$, while thread $B$ attempts to pop a value off $s$. Thread $A$ starts making progress while thread $B$ is asleep. Thread $A$ begins to execute push. At line 4, its local variable $h$ is bound to the address $\ell$. At line 5, it allocates a new list cell at address $\ell'$; its local variable $h'$ is bound to $\ell'$. At line 7, the “tail” field of the new cell is set to $\ell$. Then, suppose thread $A$ falls asleep. Thread $B$ wakes up and successfully pops one value off the stack. The reference $s$ now stores the value nil. The cell $\ell$ has been extracted by pop and is no longer logically part of the stack. The cell $\ell'$ has not yet been inserted by push and is not logically part of the stack.

Because the cell $\ell$ has been extracted by a pop operation that has successfully completed, one might expect this cell to be now unreachable. However, this is not the case. Thread $A$ has fallen asleep between lines 7 and 8. At this point, the local variables $h$ and $h'$ are still needed in the future: they occur on line 8. Therefore, the locations $\ell$ and $\ell'$ are *roots* in thread $A$. Besides, even if $\ell$ was not a root, it would still be reachable via the root $\ell'$, since the “tail” field of the cell $\ell'$ contains the pointer $\ell$. This is potentially problematic: a cell that has been extracted by pop is still reachable after pop has returned. So, *at this point, the garbage collector cannot reclaim this cell*. Therefore, the informal claim that “pop frees up $W$ words of memory” seems compromised. Can it be formalized in such a way that it is actually true?

To answer this question in a positive way, a tempting first idea is to somehow forbid this undesirable scenario. For example, forbidding thread $A$ from falling asleep at this particular point, between lines 7 and 8, might come to mind. However, this idea does not seem practical; we do not wish to impose restrictions on the scheduler.

Instead, we remark that *provided thread $A$ is allowed to make progress until line 10*, there really is no problem at all. That is, *provided no polling point prevents thread $A$ from reaching line 10*, the above claim is true, in a certain sense.

Indeed, should some other thread (say, thread $Z$) signal that it needs space, then the scheduler can choose to immediately invoke the garbage collector, which might or might not free up enough space; but, what is more interesting, the scheduler can also wake up thread $A$ and let it make
<figure><img src="image_5.png" /><figcaption>Fig. 3. A safe-for-space version of Treiber’s stack. Protected section entry and exit points are highlighted.</figcaption></figure>

progress. Recall the scenario that we are considering: thread *B* has successfully executed pop after the location *l* was read from *s* by thread *A* at line 4. Therefore, the CAS instruction in thread *A* must fail, and thread *A* must reach the second branch of the conditional construct, at line 10. At this point, the variables *h* and *h'* are no longer needed, so the locations *l* and *l'* are no longer roots in thread *A*. Moreover, *l'* does not appear in the heap at all, and *l* can be reached only via *l'*: therefore, both *l* and *l'* are unreachable. Hence, at this point, these cells can be reclaimed. Thus, they can be reclaimed *before* the request for space by thread *Z* must be satisfied.

In summary, provided no polling point prevents thread *A* from reaching line 10, there is no problem: the informal claim that “pop frees up *W* words of memory”, is true, provided one understands that it means: “once pop has returned, eventually, *W* words of memory will be freed”.

On the other hand, if a polling point was inserted by the compiler in the code of push between lines 7 and 8, that would be problematic. Assuming that thread *Z* is waiting for space, there would be no way for thread *A* to make progress past this polling point. So, the location *l'* would remain a root in thread *A*, and the garbage collector would be unable to reclaim the cell at address *l'*. With some bad luck, though, perhaps reclaiming this cell is *necessary* in order to recover enough space to satisfy the memory allocation request by thread *Z*. In such an event, the system would be in a deadlock. It would be impossible to prove that “once pop has returned, eventually, *W* words of memory will be freed”.

## 3.3 Space Consumption of Treiber’s Stack with Protected Sections

In the previous section (§3.2), we have argued that the compiler must not insert a polling point between the point where the address of the head cell is read and a point where this address ceases to be a root. To forbid this, a protected section can and must be used. The modified pseudo-code in Figure 3 illustrates one way of doing so. With respect to the original code in Figure 1, two main changes are made. First, protected sections, delimited by *enter* and *exit* instructions, are inserted into the functions *push* and *pop*. Second, the allocation of a new list cell in *push* must be anticipated (moved higher up in the code), because memory allocation inside protected sections is forbidden (§2.5).

The protected sections in Figure 3 are placed in such a way that, outside of these protected sections, no list cell is a root. Thus, there is no danger of a polling point being inserted at a point where a list cell is a root.

With respect to this version of the code, we are able to formally prove that “pop frees up *W* words of memory”. Technically, the list cell addresses that are read inside protected sections are registered in our program logic as temporary roots. This allows these addresses to be logically deallocated by a successful pop operation. More details about this statement and about its proof are given later on (§11.5).
```pascal
20 let rec push_aux s v h' =
21     set_data h' v;
22     enter; let h = !s in
23     set animal h' h;
24     if compare_and_swap s h h'
25     then exit
26     else ( exit; push_aux s v h')
27
28 let push' = push_aux s v (new_cell())
```

<caption>Fig. 4. A tempting yet unsafe-for-space optimization</caption>

*An Unsafe-For-Space Optimization.* The code for push that we present in Figure 3 may seem naive. Indeed, a new list cell is allocated at each iteration of the CAS loop (that is, at each recursive call to push). A tempting optimization is to allocate a list cell outside of the loop and to reuse this cell at each recursive call. Such an optimization is standard [Herlihy and Shavit 2012, §11.2]. Figure 4 presents a version of push, named push', which incorporates it.

Unfortunately, this optimization re-introduces the space complexity problem that was discussed earlier (§3.2): it can prevent a concurrent pop operation from freeing up memory. Indeed, push' does not satisfy the property "outside protected sections, no list cell is a root", which push satisfies, and which is sufficient (although not necessary) to achieve good space complexity. The culprit is the local variable h', which is mentioned on line 26, outside of the protected section. Let us write $\ell$ and $\ell'$ for the addresses to which the local variables h and h' are bound. Although the list cell at address $\ell'$ is not yet part of the data structure, it points to the list cell at address $\ell$, which is or has been part of the data structure. Therefore, via the root $\ell'$, the list cell $\ell$ and its descendants are reachable; this is undesirable.

To eliminate this problem, one solution would be to overwrite the pointer from $\ell'$ to $\ell$ in case the CAS instruction fails. One could do so by inserting a store operation just before the exit instruction on line 26. Then, the list cell at address $\ell'$ would still be a root outside of the protected section, but (because this cell has no successor) this would not cause any other cells to remain reachable. Thus, the desired heap space complexity would be achieved. However, we fear that, due to the extra store operation, this code may be more expensive in practice than the original unoptimized code, which allocates a new cell at each loop iteration. Furthermore, IrisFit, as presented in this paper, cannot verify this alternative version. Indeed, inside protected sections, IrisFit has a concept of temporary root, but does not have a concept of temporary heap-to-heap pointer.

Another tentative solution would be to place the entire loop inside a single protected section. Then, as in the unoptimized code, it would clearly be the case that, outside of a protected section, no list cell is a root. However, because we want to ensure that protected sections terminate in bounded time, we have forbidden loops inside protected sections. Even if we did allow provably terminating loops inside protected sections, that would not help: the loop in push_aux is potentially non-terminating.

# 4 Syntax and Semantics of LambdaFit

In this section, we formally present the syntax of LambdaFit (§4.1) and its small-step reduction relations (§4.2). These reduction relations define the three semantics of LambdaFit (§2.1).

## 4.1 Syntax

The syntax of LambdaFit appears in Figure 5. A value $v$ is a piece of data that fits in one word of memory. A value can be the unit value () , a Boolean value $b$ , an integer value $z$ , a memory
<table><caption>Fig. 5. LambdaFit: syntax</caption><tr><td>Primitives</td><td>Ο ::= &amp;&amp; | || | + | - | × | ÷ | =</td><td></td><td></td></tr><tr><td>Values</td><td>v, w ::= () | b ∈ {false, true} | z ∈ Z | ℓ ∈ L | μ<sub>ptr</sub>f. λx. t</td><td>where</td><td>fv(t) ⊆ {f} ∪ x</td></tr><tr><td>Terms</td><td>t, u ::= v<br/>x<br/>let x = t in t<br/>if t then t else t<br/>(t u̅)ptr<br/>t ⊙ t<br/>alloc t</td><td>value<br/>variable<br/>sequencing<br/>conditional<br/>code pointer invocation<br/>primitive operation<br/>heap allocation</td><td>t[t]<br/>t[t] ← t<br/>fork t<br/>CAS t[t] t t<br/>enter<br/>exit<br/>poll</td><td>heap load<br/>heap store<br/>thread creation<br/>compare-and-swap<br/>entering a protected section<br/>exiting a protected section<br/>polling point</td></tr><tr><td>Contexts</td><td>K ::= let x = □ in t<br/>alloc □<br/>v[□] ← t<br/>CAS □[t] t t</td><td>if □ then t else t<br/>□[t]<br/>v[v] ← □<br/>CAS v[□] t t</td><td>□ ⊙ t<br/>v[□]<br/>(□ u̅)ptr<br/>CAS v[v] □ t</td><td>v ⊙ □<br/>□[t] ← t<br/>(v (v̅ ++ □ ++ u̅))ptr<br/>CAS v[v] v □</td></tr></table>

location $ℓ$ (drawn from an infinite set $L$), or a code pointer $μ_{ptr}f. λ\bar{x}. t$. Such a code pointer is a closed, recursive, multi-argument function. The side condition $fv(t) \subseteq \{f\} \cup \bar{x}$ ensures that the function is closed: that is, the only variables that may appear in the body of the function are $f$ (a self-reference, allowing the function to invoke itself) and $\bar{x}$ (the formal parameters).

The syntax of terms (also known as expressions) includes a number of standard sequential constructs, such as sequencing, conditionals, code pointer invocations, and primitive operations. The heap allocation expression alloc $n$ allocates a fresh memory block of size $n$ and returns its address. The field at offset $i$ in the memory block at address $x$ is read by the “load” expression $x[i]$ and written by the “store” expression $x[i] \leftarrow y$.

Two standard concurrency-related constructs are “fork” and CAS. The expression `fork t` spawns a new thread whose code is `t`. This is *unstructured concurrency*: there is no primitive operation to wait until a thread terminates. This approach contrasts with the less-expressive *structured concurrency*, such as `fork/join` or `async/finish` [Charles et al. 2005; Lee and Palsberg 2010], where there is a primitive operation that waits for a thread or a group of threads to terminate. As we demonstrate later in this paper (§11.4), structured concurrency (async/finish) can be encoded as a library on top of unstructured concurrency.

The compare-and-swap expression `CAS ℓ[i] v v'` atomically loads a value from block $ℓ$ at offset $i$, compares this value with $v$, and, in case they are equal, overwrites this value with $v'$. Its Boolean result indicates whether the write took place.

The poll instruction is a polling point (§2.4). The instructions enter and exit mark the beginning and end of a protected section (§2.5).

## 4.2 Semantics

We now define the operational semantics of LambdaFit. We begin with our model of memory, that is, our view of the heap as a collection of memory blocks, and our notion of heap size (§4.2.1). We define thread pools and configurations (§4.2.2). Then, we introduce a series of reduction relations which, together, form the dynamic semantics of LambdaFit. The *head reduction relation* (§4.2.3) describes one elementary step of computation by one thread. The *step relation* (§4.2.4) allows head reduction to take place under an evaluation context. It represents one step of computation by one
thread. The *garbage collection relation* (§4.2.5) describes the effect of the GC on the heap. The *action relation* (§4.2.6) combines computation steps and garbage collection steps. Allowing any computation steps to take place and preventing garbage collection yields the oblivious semantics (§4.2.7). Restricting the action relation to a subset of *enabled actions* (§4.2.8), which depends on a heap size limit *S*, yields the *default reduction relation* (§4.2.9), which is the main reduction relation of the default semantics. Allowing for the heap size limit *S* to grow over time yields the *growing reduction relation* (§4.2.10).

### 4.2.1 Memory Blocks, Stores, and Heap Size.
A memory block is either a tuple of values, written $\vec{v}$, or a special deallocated block, written $\perp$. A store $\sigma$ (or heap) is a finite map of locations to memory blocks. We write $\emptyset$ for the empty store.

Our semantics does not recycle memory locations. When a heap block at address $\ell$ is reclaimed by the GC, the store is updated with a mapping of $\ell$ to $\perp$. The address $\ell$ continues to exist and is never re-used. Naturally, in an implementation, memory locations would be recycled. However, we work at a higher level of abstraction. The reasoning rules of our program logic guarantee that a memory allocation always produces a fresh address. One could in principle prove that our semantics is equivalent to a lower-level semantics where locations can be recycled once they have become unreachable. We have not done so.

As our semantics does not recycle memory locations, in particular, a reachable memory location cannot be recycled. As a result, one important source of ABA problems disappears. In fact, as noted by Michael [2004b, §2], in the presence of garbage collection, all ABA problems can be avoided by a skilled and careful programmer. However, a programmer who attempts to manually recycle memory can still run into ABA problems.

We assume that the space usage (in words) of a block of $n$ fields is $size(n)$, where $size$ is a mathematical function of $\mathbb{N}$ to $\mathbb{N}$. If, for instance, every memory block is preceded by a one-word header, then the function $size$ would be defined by $size(n) = n + 1$. LambdaFit and IrisFit are independent of the definition of $size$. For our case studies (§11), we chose $size(n) = n$. We write $size(\vec{v})$ as a shorthand for $size(n)$, where $n$ is the length of the list $\vec{v}$. By convention, we let $size(\perp)$ be 0. This reflects the fact that a deallocated block occupies no space.

We define the size of a store $\sigma$ as the sum of the sizes of its blocks. Thus, we do not measure the physical size of the heap, that is, how much memory has been borrowed from the operating system. Instead, we measure the total size of the memory blocks that are currently allocated. We ignore fragmentation.

### 4.2.2 Thread Pools and Configurations.
A thread $t$ is just a term. A thread's status $g$ is either In or Out. The status records whether the thread is currently inside or outside a protected section. A thread pool $\theta$ is a list of pairs $(t, g)$ of a thread $t$ and its status $g$. A thread identifier $\pi$ is an integer index into a thread pool.

A configuration $c$ is a pair $(\theta, \sigma)$ of a thread pool $\theta$ and a store $\sigma$. The initial configuration for a program $t$ consists of a thread pool that contains just the thread $(t, \text{Out})$ and the empty store $\emptyset$. We write $\text{init}(t)$ for this initial configuration. We define the heap size of a configuration as the size of its store: $size((\theta, \sigma)) = size(\sigma)$.

### 4.2.3 The Head Reduction Relation.
The head reduction relation $t / g / \sigma \xrightarrow{\text{head}} t' / g' / \sigma' / t^?$ describes an evolution of the term $t$ with status $g$ and store $\sigma$ to a term $t'$ with status $g'$ and store $\sigma'$, optionally forking off a new thread $t^?$. The variable $t^?$ denotes an optional term: it is either a term $t$ or $\varepsilon$, which means that no thread was forked off.

The head reduction relation describes the reduction of a single isolated instruction. Reduction under an evaluation context is handled by the step relation introduced shortly afterwards (§4.2.4).
<figure><img src="image_6.png" /><figcaption>Fig. 6. The head reduction relation</figcaption></figure>

<figure><img src="image_7.png" /><figcaption>Fig. 7. The step relation</figcaption></figure>

<figure><img src="image_8.png" /><figcaption>Fig. 8. The garbage collection relation</figcaption></figure>

<figure><img src="image_9.png" /><figcaption>Fig. 9. The action relation</figcaption></figure>
Moreover, the head reduction relation describes how an instruction is executed under the assumption that this instruction is enabled, that is, not blocked. The definition of enabled instructions, which describes under what conditions an instruction is blocked, is given later on (§4.2.8).

The head reduction relation is defined by the rules in Figure 6.

`HEADLETVAL`, `HEADIFTRUE`, `HEADIFFALSE`, `HEADPRIM` are standard.

`HEADLOAD`, `HEADSTORE`, `HEADCASSUCCESS` and `HEADCASFAILURE`, which describe memory accesses, are also standard. These rules require that the memory location $\ell$ be valid: this is expressed by the premise $\sigma(\ell) = \vec{w}$. Furthermore, they require the integer value $i$ to be a valid index into the memory block at address $\ell$: this is expressed by the premise $0 \le i < |\vec{w}|$. We write $\vec{w}(i)$ for the $i$-th value in the sequence $\vec{w}$, and $[i := v]\vec{w}$ for the sequence obtained by updating the sequence $\vec{w}$ at index $i$ with the value $v$. We write $[\ell := \vec{w}]\sigma$ for the store obtained by updating the store $\sigma$ at address $\ell$ with the block $\vec{w}$. Hence, $[\ell := [i := v]\vec{w}]\sigma$ describes an update of the $i$-th field of the block at location $\ell$.

`HEADENTER` and `HEADEXIT` cause the thread to change its status from Out to In and vice-versa. By design, no reduction rule describes the effect of enter when the thread's status is In or the effect of exit when the thread's status is Out. Such a situation is considered a runtime error: the thread is stuck.

`HEADCALL`, `HEADALLOC`, `HEADFORK`, and `HEADPOLL` require the thread's status to be Out. Thus, inside a protected section, a function call, a memory allocation request, a "fork" instruction, or a polling point causes a runtime error. Aside from this, `HEADCALL` and `HEADFORK` are standard. `HEADALLOC` allocates a block of $n$ fields at a fresh memory location and initializes each field with a unit value. We write $()^n$ for a sequence of $n$ unit values. `HEADPOLL` indicates that a polling point is a no-operation: poll acts as a form of barrier (§4.2.8), and is otherwise effectless.

### 4.2.4 The Step Relation.
The step relation has the same shape as the head reduction relation (§4.2.3). It takes the form $t/g/\sigma \xrightarrow{step} t'/g'/\sigma'/t?$. It is inductively defined by the rules `STEPHEAD` and `STEPCTX`. In Figure 7, these rules allow one head reduction step under a stack of evaluation contexts. An evaluation context $K$ is a term with a hole written $\square$ at depth exactly 1. The syntax of evaluation contexts, presented in Figure 5, dictates a left-to-right, call-by-value evaluation strategy. We write $K[t]$ for the term obtained by filling the hole of the evaluation context $K$ with the term $t$.

### 4.2.5 The Garbage Collection Relation.
Several concepts related with garbage collection are defined in Figure 8. The edge relation $\ell \rightsquigarrow_\sigma \ell'$, defined by the rule `EDGE`, means that the block at location $\ell$ contains a pointer to location $\ell'$.<fnref n="5" /> When this relation holds, we say that $\ell$ is a *predecessor* of $\ell'$. The *reachability relation* $\ell \rightsquigarrow_{\sigma}^* \ell'$ is the reflexive-transitive closure of the edge relation.

The garbage collection relation $R \vdash \sigma \xrightarrow{gc} \sigma'$, defined by the rule `GC`, describes the effect of the GC. This relation means that a garbage collection phase can transform the store $\sigma$ into a store $\sigma'$, while respecting the set of roots $R$, a set of memory locations. This relation is non-deterministic: the GC may reclaim any unreachable memory block, but need not reclaim every such block. According to the first premise of the rule `GC`, the stores $\sigma$ and $\sigma'$ have the same domain: garbage collection does not create or destroy any memory locations. According to the second premise, at each memory location $\ell$, either nothing happens ($\sigma'(\ell) = \sigma(\ell)$) or a memory block becomes deallocated ($\sigma'(\ell) = \emptyset$). The second case is permitted only if $\ell$ is not reachable from any of the roots in the set $R$.

### 4.2.6 The Action Relation.
The relations defined so far describes how a thread makes a step (§4.2.4) and how the GC makes a step (§4.2.5). We now define a relation that interleaves these two kinds of steps. It is a labeled transition relation: each step is labeled with an *action a*, which is either a thread

<footnote n="5">⁵A value either is a location or contains no location at all. Thus, in `EDGE`, we write just $\vec{w}(i) = \ell'$ instead of the seemingly more general condition $\ell' \in \text{locs}(\vec{w}(i))$.</footnote>
$$ \begin{array}{c} \text{OBLIVIOUS} \\ c \xrightarrow{\text{action}}_{\pi} c' \\ \text{oblivious} \\ c \xrightarrow{\text{oblivious}} c' \end{array} $$

<caption>Fig. 10. The oblivious reduction relation</caption>

$$ \begin{array}{ccccc} \text{ISALLOCHEAD} & & \text{ISALLOCCTX} & & \text{ISPOLLHEAD} \\ \text{IsAlloc } n \text{ (alloc } n \text{)} & & \frac{\text{IsAlloc } n t}{\text{IsAlloc } n (K[t])} & & \text{IsPoll poll} \\ & & & & \text{IsPollCTX} \\ & & & & \text{IsPoll } t \\ \text{ALLOCFITS} & & \forall n. \text{ IsAlloc } n t \implies \frac{\text{size}(\sigma) + n \le S}{\text{AllocFits}_S \sigma t} & & \text{IsPoll}(K[t]) \\ & & & & \text{EVERYALLOCFITS} \\ & & & & \frac{\forall t g. (t, g) \in \theta \implies \text{AllocFits}_S \sigma t}{\text{EveryAllocFits}_S (\theta, \sigma)} \\ \text{ENABLEDTHREAD} & & c = (\theta, \sigma) & & \text{ENABLEDGC} \\ \text{AllocFits}_S \sigma t & \text{IsPoll } t & \text{IsAllocFits}_S c & & \text{Enableds } c \text{ gc} \\ & & \frac{\text{Enableds } c \pi}{\text{Enableds } c \pi} & & \end{array} $$

<caption>Fig. 11. Enabled actions (and auxiliary predicates)</caption>

identifier $\pi$ or the fixed token "gc". The action relation $c \xrightarrow{\text{action}} a$ relates two configurations $c$ and $c'$ and is labeled with an action. It is defined by the two rules in Figure 9. ACTIONTHREAD allows a step by one thread whose identifier is $\pi$. This thread evolves from $(t, g)$ to $(t', g')$: the thread pool is updated accordingly. The heap, which is shared between all threads, evolves from $\sigma$ to $\sigma'$. A new thread $t'$ possibly appears: if so, the thread pool is extended with the new entry $(t', \text{Out})$. ACTIONGC describes a garbage collection step. The roots provided to the GC are $\text{locs}(\theta)$, that is, the locations that occur in the thread pool: this is the FVR (§2.2). The side condition $\sigma \neq \sigma'$ forbids stuttering steps, where the GC is invoked but frees no memory. Without this side condition, we would be unable to establish our liveness theorem (Theorem 8.2), whose statement asserts that at all times, in a bounded number of steps, the system must reach a configuration where no thread is blocked by a memory allocation request.

4.2.7 *The Oblivious Reduction Relation.* The oblivious reduction relation $c \xrightarrow{\text{oblivious}} c'$ is defined by the rule OBLIVIOUS in Figure 10. This relation simply allows one action by an arbitrary thread $\pi$. Garbage collection steps are not permitted: in this semantics, there is no need for garbage collection. There is no limit on the size of the heap. This is the oblivious semantics of LambdaFit (§2.1).

4.2.8 *Enabled Actions.* In the default and growing semantics, two LambdaFit instructions can have a blocking behavior: a large memory allocation instruction is blocking (§2.3); if a large memory allocation request is outstanding, then a polling point is blocking (§2.4). To reflect this, we must define under what conditions an action is *enabled* (allowed to proceed) or *disabled* (blocked).

The distinction between *small* and *large* memory allocation requests depends on the heap size limit $S$ (§2.3). Therefore, the notion of enabled action depends on the parameter $S$.

To define enabled actions, a few auxiliary predicates are needed. They appear in Figure 11.

The proposition `IsAlloc n t` means that the next instruction of the thread $t$ is "alloc $n$". In other words, this thread is now requesting a new memory block of $n$ fields. Similarly, the proposition `IsPoll t` means that the next instruction of the thread $t$ is "poll".
<figure><img src="image_10.png" /><figcaption>Fig. 12. The default reduction relation</figcaption></figure>

<figure><img src="image_11.png" /><figcaption>Fig. 13. The growing reduction relation</figcaption></figure>

The proposition `AllocFits<τ, σ>` means that, if the next instruction in thread `t` is an allocation request, then it is a small one: that is, there is currently enough free space in the store `σ` to satisfy it. When this is the case, we say that *thread t fits*. The proposition `EveryAllocFits<τ, σ>` `c` means that, in the configuration `c`, every thread fits. These propositions depend on the heap size limit `S`.

The proposition `Enabled<τ, c, a>` means that, in the configuration `c`, action `a` is enabled. This proposition also depends on the heap size limit `S`. It is defined by the rules `ENABLEDTHREAD` and `ENABLEDGC` in Figure 11. For a thread `π` to be enabled, it must be the case that (1) thread `π` fits and (2) if thread `π` is at a polling point then every thread fits. `ENABLEDGC` states that garbage collection is enabled at all times.

The following simple lemma states that if every thread fits then every action is enabled. It is used in the proof of our liveness theorem (§8.2). In the following, we say that a thread identifier `π` is valid with respect to the configuration `(θ, σ)` if `0 ≤ π < |θ|` holds.

**LEMMA 4.1 (ALL ENABLED).** *If EveryAllocFits<τ, σ> c holds, then, for every thread identifier π that is valid with respect to the configuration c, Enabled<τ, c, a> c holds.*

### 4.2.9 The Default Reduction Relation.
The auxiliary relation $c \xrightarrow{\text{enabled actions}} a$ $c'$, which is defined in Figure 12, is the restriction of the action relation to enabled actions.

The default reduction relation $c \xrightarrow{\text{default}} c'$ is obtained from this auxiliary relation by abstracting away the action `a`. Thus, a step in the default reduction relation corresponds to an enabled action by some thread or by the GC. This reduction relation is the *default semantics* of LambdaFit.

By design of this semantics, the size of the heap can never exceed the limit `S`. This is an immediate consequence of the fact that large memory allocation requests are blocked.

**LEMMA 4.2 (HEAP SIZE).** *If $size(c) \le S$ and $c \xrightarrow{\text{default}} c'$ then $size(c') \le S$.*

This simple lemma is not used anywhere; it serves to document the design of the semantics.

### 4.2.10 The Growing Reduction Relation.
The growing semantics (§2.1) is a variation of the default semantics where the limit on the size of the heap can be automatically adjusted at runtime. In this semantics, this limit is not fixed: instead, it is part of the current state of the machine. Thus, instead of relating two configurations `c` and `c'` (§4.2.2), the *growing reduction relation* relates two pairs `(S, c)` and `(S', c')`, where `S` and `S'` represent the value of the heap limit before and after the reduction step.

This relation is defined by the two rules in Figure 13. The rule `GROWINGSTEP` states that if *under the current heap limit* `S` a step is possible then this step can take place and the heap limit is unchanged. (This can be a computation step or a garbage collection step.) The rule `GROWINGINCREASELIMIT` states that if no thread is currently inside a protected section, and if in spite of the efforts of the
garbage collector the current heap limit blocks a memory allocation request, then the heap limit can be increased from S to grow(S). The requirement that “no thread is inside a protected section”<fnref n="6" /> is important: it ensures that the heap limit is increased only when there are no temporary roots. Without this assumption, we would not be able to bound the heap limit of verified programs (§8.3).

The function grow is fixed: it is a parameter of the semantics. We make the following assumption:

ASSUMPTION 4.2.1. The function grow : $\mathbb{N} \to \mathbb{N}$ satisfies the following two properties:

* $\forall x. x < grow(x)$

* $\forall x y. x \le y \implies grow(x) \le grow(y)$

A typical example would be $grow(S) = \max(2S, 1)$, which means that when the current limit is found to be too low, it is doubled (with special care for the case where the current limit is zero).

The default semantics and the growing semantics are close cousins: they are related by the following two lemmas. Lemma 4.3 states that if an execution under the growing semantics brings the heap limit up to the value $S'$, then the same execution is permitted by the default semantics with a fixed limit of $S'$. Conversely, Lemma 4.4 states that if an execution under the default semantics is possible, with a fixed limit of $S$, then the same execution is permitted by the growing semantics, without a need to increase the limit.

LEMMA 4.3 (GROWING TO DEFAULT). $(S, c) \xrightarrow{growing} * (S', c')$ implies $c \xrightarrow{default_{S'}} * c'$ and $S \le S'$.

LEMMA 4.4 (DEFAULT TO GROWING). $c \xrightarrow{default_S} * c'$ implies $(S, c) \xrightarrow{growing} * (S, c')$.

Furthermore, in the growing semantics, by design, the size of the heap cannot exceed the current heap limit:

LEMMA 4.5 (HEAP SIZE). If $size(c) \le S$ and $(S, c) \xrightarrow{growing} * (S', c')$ then $size(c') \le S'$.

Later on (§8.3), we prove that, under the growing semantics, a verified program can be executed in bounded space.

# 5 Program Logic: Assertions

This section offers an overview of the various kinds of assertions that play a role in IrisFit. We introduce the syntax of each assertion, its intuitive meaning, and the ghost reasoning rules that help understand this meaning, such as splitting and joining rules. We informally explain the life cycle of each assertion: where it typically appears, where it is exploited, and where it is consumed. A presentation of the reasoning rules for terms is deferred to the following section (§6).

We begin with a presentation of triples (§5.1) and ghost updates (§5.2). Then, we briefly present the standard points-to assertion (§5.3), the novel “`sizeof`” assertion (§5.4), and space credits (§5.5). We then devote our attention to the assertions that record reachability or unreachability information, namely the pointed-by-heap assertion (§5.6), the novel pointed-by-thread assertion (§5.7), the novel “inside” and “outside” assertions (§5.8), and deallocation witnesses (§5.9). Finally, we explain liveness-based cancellable invariants (§5.10), a useful idiom that expresses that a certain invariant holds as long as a certain location is live.

IrisFit is a variant of the Iris program logic [Jung et al. 2018b, §6–7] and is built on top of the Iris base logic [Jung et al. 2018b, §5]. We write $\Phi$ for assertions, $\lceil P \rceil$ for a pure assertion, $\Phi * \Phi'$ for a separating conjunction, and $\Phi * \Phi'$ for a separating implication. We express the logical equivalence of two assertions as $\Phi \equiv \Phi'$. A postcondition $\Psi$ is a function of a value to an assertion: in other words, it is the form $\lambda v. \Phi$.

<footnote n="6">⁶The requirement that “no thread is inside a protected section” is expressed by the premise AllOutside c. We write fullGC(c) for the configuration obtained from the configuration c by deallocating all unreachable heap blocks. The formal definition of the function fullGC can be found in our Coq mechanization [Moine 2025].</footnote>
<figure><img src="image_12.png" /><figcaption>Fig. 14. Structural reasoning rules</figcaption></figure>

## 5.1 Triples

A triple takes the form {$\Phi$} $\pi: t$ {$\Psi$}. Its intuitive meaning is that if the store satisfies the assertion $\Phi$ then it is safe for thread $\pi$ to execute the term $t$; furthermore, if and when this computation terminates and produces a value $v$, then the store satisfies the assertion $\Psi v$.

Even though the default reduction relation (§4.2.9) is parameterized with a heap size limit $S$, the meaning of triples is independent of $S$. Indeed, triples are internally defined in terms of the *oblivious* reduction relation (§8.4), which does not depend on $S$. Therefore, none of the reasoning rules mentions $S$. Our program logic is compositional: each program component can be verified in isolation and without knowledge of $S$.

Formally, a triple is also parameterized by a *mask* [Jung et al. 2018b, §2.2]. Masks prevent the user from opening an invariant twice. As our treatment of invariants and masks is standard, we omit masks everywhere. The interested reader is referred to our mechanization [Moine 2025].

We write {$\Phi$} $\pi: t$ {$\lambda\ell. \Phi'$}, where the *metavariable* $\ell$ denotes a memory location, as syntactic sugar for {$\Phi$} $\pi: t$ {$\lambda\nu. \exists\ell. \neg v = \ell^\neg * \Phi'$}. We adopt the convention that multi-line assertions are implicitly joined by a separating conjunction.

## 5.2 Ghost Updates

Iris features *ghost state* and *ghost updates* [Jung et al. 2018b, §5.4]. A ghost update is written $\Phi \Rightarrow \Phi'$. It is an assertion, which means that (up to an update of the ghost state) the assertion $\Phi$ can be transformed into $\Phi'$.

In IrisFit, it is sometimes necessary for a ghost update to refer to “the identifier of the current thread” or to “the roots of the current thread”. For this purpose, we introduce a *custom ghost update*, written $\Phi \pi \Rightarrow^V \Phi'$, whose extra parameters are a thread identifier $\pi$ and a set of memory locations $V$. It is weaker than a standard ghost update: the law ($\Phi \Rightarrow \Phi'$) $\dashv$ ($\Phi \pi \Rightarrow^V \Phi'$) is valid.

Custom ghost updates are exploited in the CONSEQUENCE rule, which appears in Figure 14. This rule allows strengthening the precondition and weakening the postcondition of a triple. Updating the precondition requires a custom ghost update where the parameter $V$ is instantiated with $\text{locs}(t)$. Indeed, this set represents the roots at the point where this update takes place. Updating the postcondition requires a custom ghost update where $V$ is instantiated with $\text{locs}(v)$, where $v$ denotes the result value of the term $t$. Indeed, these are the roots at the point where that update takes place.

When a custom ghost update is independent of the parameters $\pi$ and $V$, we omit them: we write $\Phi \Rightarrow \Phi'$ for $\forall \pi V$. $\Phi \pi \Rightarrow^V \Phi'$. Examples of custom ghost updates appear in Figures 18, 19, and 20 and are discussed in the following sections.

The FRAME rule, also shown in Figure 14, retains its standard form.

## 5.3 Points-to Assertions

IrisFit features standard points-to assertions of the form $\ell \mapsto_p \vec{w}$, where $p$ is either a fraction in the semi-open interval $[0, 1]$ or the *discarded fraction* $\square$ [Vindum and Birkedal 2021]. In the latter case, the points-to assertion is persistent.
<figure><img src="image_13.png" /><figcaption>Fig. 15. Reasoning rules of the “sizeof” assertion</figcaption></figure>

<figure><img src="image_14.png" /><figcaption>Fig. 16. Reasoning rules for space credits</figcaption></figure>

*Rules.* Points-to assertions can be split and joined in the usual way, and a points-to assertion that carries a fraction *p* can be permanently transformed into one that carries the discarded fraction *q*. We do not show these standard rules.

*Life cycle.* A points-to assertion appears when a memory block is allocated. It is required (and possibly updated) when this block is accessed by a load, store, or CAS instruction (§6.2). It is *not* required or consumed when this block is logically deallocated (§6.1). This is an original feature of IrisFit.

## 5.4 Sizeof Assertions

The assertion `sizeof *l* n` means that there is or there used to be a block of size *n* at address *l*. It is persistent: indeed, once the size of a block has been fixed, it can never be changed.

*Rules.* Two reasoning rules allow introducing and exploiting “*sizeof*” assertions (Figure 15). `SIZEOFPOINTSTO` creates a “*sizeof*” assertion out of a points-to assertion. `SIZEOFCONFRONT` states that two “*sizeof*” assertions for the same address must agree on the size of the block at this address.

*Life cycle.* The “*sizeof*” assertion is produced by `SIZEOFPOINTSTO`. It is consulted by the logical deallocation rules (§6.1, §6.6) to determine the number of space credits that must be produced.

## 5.5 Space Credits

To reason about free space, we use *space credits* [Madiot and Pottier 2022; Moine et al. 2023]. The assertion `◊n` denotes the unique ownership of *n* space credits. It can be understood as a permission to allocate *n* words of memory. At a lower level of understanding, this assertion means that *n* memory words *are currently free or can be freed* by the GC *once it is given a chance to run*. This interpretation of space credits is the same as in the earlier papers cited above.

Following Moine et al. [2023], space credits are measured using non-negative *rational* numbers. Of course, a physical word of memory cannot be split, so the total number of space credits in existence is a natural number; so are the numbers involved in the reasoning rules for memory allocation and deallocation. Still, rational numbers appear essential in certain amortized complexity analyses, as illustrated by the example of chunked stacks [Moine et al. 2023]. Rational credits also appear in amortized *time* complexity analyses [Charguéraud and Pottier 2019; Mével et al. 2019].

*Rules.* Figure 16 presents two basic reasoning rules about space credits. `ZEROSC` asserts that zero credits can be forged out of thin air. `SPLITJOINSC` asserts that space credits can be split and joined.

*Life cycle.* Space credits are consumed by memory allocation (§6.2) and produced by logical deallocation (§6.1). Because there is no way of creating space credits out of nothing, a program or program component is usually verified under the assumption that a number of space credits are
<figure><img src="image_15.png" /><figcaption>Fig. 17. Reasoning rules for the pointed-by-heap assertion</figcaption></figure>

provided. For example, our safety theorem for the default semantics (§8.1) states that if a (complete) program is verified under the precondition $\diamond S$, where $S$ is the heap size limit, then this program can be safely executed. When a program component is considered in isolation, it is given a specification that does not mention $S$. For instance, our specification of Treiber’s stack (Figure 41) states that push consumes two space credits and that pop produces two space credits.

## 5.6 Pointed-By-Heap Assertions

Our pointed-by-heap assertions are the “pointed-by” assertions of our earlier paper [Moine et al. 2023]. The longer name “pointed-by-heap” avoids confusion with our novel “pointed-by-thread” assertions (§5.7). To make this paper self-contained, we recall what form these assertions take, what they mean, and what purpose they serve.

A pointed-by-heap assertion for the location $\ell'$ keeps track of a multiset $L$ of predecessors of $\ell'$ (§4.2.5). It takes the form $\ell' \leftarrow_q L$, where $L$ is a signed multiset of locations and $q$ is a possibly-null fraction, that is, a rational number in the closed interval $[0; 1]$.

Signed multisets. Signed multisets [Hailperin 1986], also known as generalized sets [Whitney 1933; Blizard 1990] or hybrid sets [Loeb 1992], are a generalization of multisets: they allow an element to have negative multiplicity. A signed multiset is a total function of elements to $\mathbb{Z}$. The disjoint union operation $\cup$ is the pointwise addition of multiplicities. We write $+x$ for a positive occurrence of $x$ and $-x$ for a negative occurrence of $x$. For example, $\{+x; +x\} \cup \{-x\}$ is $\{+x\}$. We write NoNegative($L$) when no element has negative multiplicity in $L$. Symmetrically, we write NoPositive($L$) when no element has positive multiplicity in $L$.

Possibly-Null Fractions. In traditional Separation Logics with fractional permissions [Boyland 2003; Bornat et al. 2005], a fraction is a rational number in the semi-open interval $[0, 1]$. If there exists a share that carries the fraction 1, then no other shares can separately exist. With possibly-null fractions, the fraction 0 is allowed, so a full pointed-by-heap assertion $\ell' \leftarrow_1 L$ does not exclude the existence of a separate pointed-by-heap assertion with fraction zero, say $\ell' \leftarrow_0 L'$.

Nevertheless, we enforce the following null-fraction invariant: in a pointed-by-heap assertion $\ell' \leftarrow_q L$, if the fraction $q$ is 0, then no location can have positive multiplicity in $L$; or, in short, $q = 0$ implies NoPositive($L$).

Signed multisets and possibly-null fractions let us use the assertion $\ell' \leftarrow_0 \{-\ell\}$ as a permission to remove one occurrence of $\ell$ from the predecessors of $\ell'$. This lets us formulate the reasoning rule for store instructions (§6.2) in a simpler way than would otherwise be possible.

Over-Approximation of Live Predecessors. We say that a location $\ell$ is dead if it has been allocated and logically deallocated already (§5.9, §6.1). We say that it is live if it has been allocated but not logically deallocated yet.

The true purpose of pointed-by-heap assertions is to keep track of live predecessors. A dead predecessor is irrelevant: increasing its multiplicity in a multiset of predecessors is sound; decreasing
<figure><img src="image_16.png" /><figcaption>Fig. 18. Reasoning rules for the pointed-by-thread assertion</figcaption></figure>

it is sound, too. As far as live predecessors are concerned, only over-approximation is permitted. Increasing the multiplicity of a live predecessor is sound; decreasing it is not.

In light of this, and in light of the null-fraction invariant, a full pointed-by-heap assertion $\ell' \leftarrow_1 L$, where the fraction is 1, guarantees that the multiset $L$ contains all live predecessors of the location $\ell'$. In particular, the assertion $\ell' \leftarrow_1 \emptyset$ guarantees that $\ell'$ has no live predecessors. Such full knowledge of the live predecessors is required by the logical deallocation rule (§6.1, §6.6).

**Rules.** Pointed-by-heap assertions obey the splitting, joining, and weakening rules in Figure 17. `JOINPBHEAP` joins two pointed-by-heap assertions by adding the fractions $q_1$ and $q_2$ and by adding the signed multisets $L_1$ and $L_2$. In the reverse direction, `SPLITPBHEAP` splits a pointed-by-heap assertion. Its side condition ensures that the null-fraction invariant is preserved. `COVPBHEAP` asserts that a pointed-by-heap assertion (whose fraction is nonzero) is covariant in its multiset: that is, over-approximating the multiset of predecessors is sound. It is a direct consequence of `SPLITPBHEAP`, instantiated with $q_2 \triangleq 0$ and $L_2 \triangleq \{-\ell'\}$. In the reverse direction, the rule `CLEANPBHEAP`, which is discussed later on (§5.9), allows removing a dead predecessor from a multiset of predecessors.

**Life cycle.** A full pointed-by-heap assertion for the location $\ell$ appears when this location is allocated. Fractional pointed-by-heap assertions are required, updated, and produced by store instructions. For example, consider a store instruction that updates the field $\ell[i]$ and overwrites the value $\ell'_1$ with the value $\ell'_2$. The reasoning rule for this instruction (§6.2) requires a pointed-by-heap assertion $\ell'_2 \leftarrow_q \emptyset$, which it transforms into $\ell'_2 \leftarrow_q \{+\ell\}$. Furthermore, the pointed-by-heap assertion $\ell'_1 \leftarrow_0 \{-\ell\}$ is produced. A full pointed-by-heap assertion for the location $\ell$ is consumed when $\ell$ is logically deallocated.

**Notation.** We define a generalized pointed-by-heap assertion $v \leftarrow_q L$ whose first argument is a value, as opposed to a memory location. If $v$ is a location $\ell'$, then this assertion is defined as $\ell' \leftarrow_q L$. Otherwise, it is defined as $\neg \mathrm{True}$. Furthermore, we write $v \leftarrow_q^0 L$ for the assertion $\neg q > 0 \land v \leftarrow_q L$. This notation is used in the reasoning rule `STORE` (§6.2), among other places.

## 5.7 Pointed-By-Thread Assertions

The pointed-by-heap assertions presented in the previous section record which heap blocks contain pointers to a location $\ell$. This information is useful but is not sufficient for our purposes. The logic must also record which threads have access to $\ell$, that is, in which threads $\ell$ is a root. For this purpose, we introduce two distinct yet cooperating mechanisms. The first mechanism, presented here, is the pointed-by-thread assertion. The second mechanism, presented next (§5.8), is the “inside” assertion. When the fact that $\ell$ is a root in thread $\pi$ is recorded by a pointed-by-thread assertion, we say that $\ell$ is an ordinary root in thread $\pi$; when this fact is recorded by an “inside” assertion, we say that $\ell$ is a temporary root in thread $\pi$. The motivation for this distinction has been given earlier (§3, §2.5).

A pointed-by-thread assertion takes the form $\ell \Leftarrow_p \Pi$, where $p$ is a fraction in the semi-open interval $[0; 1]$ and $\Pi$ is a set of thread identifiers. These assertions intuitively generalize the Stackable assertions of our earlier paper [Moine et al. 2023] to a multi-threaded setting.
<figure><img src="image_17.png" /><figcaption>Fig. 19. Reasoning rules for “inside” and “outside” assertions</figcaption></figure>

A full pointed-by-thread assertion $\ell \Leftarrow_I \Pi$, where the fraction is 1, guarantees that $\Pi$ is the set of all threads in which $\ell$ is an ordinary root. Such full knowledge is required by the logical deallocation rule (§6.1, §6.6).

*Rules.* Figure 18 presents the splitting, joining, weakening, and trimming rules associated with the pointed-by-thread assertion. `FRACPBTHREAD` allows splitting and joining pointed-by-thread assertions. `COVPBTHREAD` asserts that a pointed-by-thread assertion is covariant in the set $\Pi$: that is, over-approximating $\Pi$ is sound. `TRIMPBTHREAD` allows trimming a pointed-by-thread assertion, that is, removing the thread identifier $\pi$ from a pointed-by-thread assertion for the location $\ell$, provided it is evident that $\ell$ is no longer a root in thread $\pi$. This rule is expressed as a custom ghost update $\pi \Rightarrow^V$. It transforms $\ell \Leftarrow_I \{\pi\}$ into $\ell \Leftarrow_I \emptyset$, provided $\ell$ is not a member of the set $V$, which denotes the set of roots of the thread $\pi$ (recall §5.2). The condition $\ell \notin V$ means indeed that $\ell$ is not a root in thread $\pi$. This condition explains why `TRIMPBTHREAD` must be expressed as a custom update $\pi \Rightarrow^V$ as opposed to a standard update $\Rightarrow$. Indeed, a standard update has no means of referring to “the identifier of the current thread” or “the roots of the current thread”.

A curious reader may wonder whether and why `TRIMPBTHREAD` remains sound in combination with the `BIND` rule. Indeed, `BIND` lets the user focus on a subterm, therefore implies that the set $V$ is a strict subset of the set of all roots of the current thread. This aspect is explained later on (§6.4).

*Life cycle.* A full pointed-by-thread assertion $\ell \Leftarrow_I \{\pi\}$ appears when a location $\ell$ is allocated by a thread $\pi$. A fractional pointed-by-thread assertion is ordinarily required and updated by load instructions: when a thread $\pi$ obtains the location $\ell$ as the result of a load instruction, an assertion $\ell \Leftarrow_I \emptyset$ is updated to $\ell \Leftarrow_I \{\pi\}$. If the thread $\pi$ is currently outside a protected section, such an update is mandatory. If the thread $\pi$ is currently inside a protected section, then it can be avoided by recording $\ell$ as a temporary root (§6.3). Once $\ell$ is no longer a root in any thread, `TRIMPBTHREAD` can be used to obtain $\ell \Leftarrow_I \emptyset$, which is consumed by the logical deallocation of $\ell$. In fact, when reasoning outside of protected sections, `TRIMPBTHREAD` is the only way to trim an assertion $\ell \Leftarrow_I \Pi$ into $\ell \Leftarrow_I \emptyset$.

*Notation.* We define a generalized pointed-by-thread assertion $v \Leftarrow_I \Pi$, whose first argument is a value, as opposed to a memory location. If $v$ is a location $\ell$, then this assertion is defined as $\ell \Leftarrow_I \Pi$. Otherwise, it is defined as $\lceil \text{True} \rceil$. Besides, we write an iterated conjunction of pointed-by-thread assertions under the form $M \Leftarrow_I \Pi$, where $M$ is a finite map of memory locations to fractions and $\Pi$ is a set of thread identifiers. It is defined by $M \Leftarrow_I \Pi \doteq \*_{(\ell, p) \in M} (\ell \Leftarrow_I \Pi)$.

## 5.8 Inside and Outside Assertions

The assertion `outside π` means that the thread $π$ is currently outside a protected section. The assertion `inside π T` means that thread $π$ is currently inside a protected section and that the set of its temporary roots (§2.6) is $T$. The set $T$ is a set of memory locations.

*Rules.* Figure 19 presents a number of reasoning rules related to “inside” and “outside” assertions. `INSIDE NOT OUTSIDE` states that a thread cannot be both inside and outside a protected section.
<figure><img src="image_18.png" /><figcaption>Fig. 20. Reasoning rules for deallocation witnesses</figcaption></figure>

ADDTEMPORARY converts an ordinary root to a temporary root. The pointed-by-thread assertion $\ell \Leftrightarrow_p \{\pi\}$ is transformed to $\ell \Leftrightarrow \emptyset$; meanwhile, $\ell$ is added to the set of temporary roots carried by the “inside” assertion. In the reverse direction, REMTEMPORARY converts a temporary root to an ordinary root. TRIMINSIDE trims the set of temporary roots by removing any locations that are no longer roots in the current thread. It is analogous to TRIMPBTHREAD.

*Life cycle.* The assertion *outside* $\pi$ appears when thread $\pi$ is created and is consumed when this thread terminates. This will be visible in the statement of Theorem 8.1, which describes the creation and termination of the main thread, and in the reasoning rule for “fork” instructions (§6.2). The assertion *outside* $\pi$ is required and preserved by the instructions that must not appear inside a protected section, namely memory allocations, function calls, “fork” instructions, and polling points. Entering a protected section transforms *outside* $\pi$ into *inside* $\pi \emptyset$; exiting a protected section causes the reverse transformation.

## 5.9 Deallocation Witnesses

The persistent assertion $\dagger \ell$ is a deallocation witness for the location $\ell$. This assertion guarantees that $\ell$ has been logically deallocated, that is, $\ell$ is dead.

The fact that $\ell$ is dead implies that $\ell$ cannot be reached from an ordinary root. However, this does not imply that $\ell$ is unreachable: indeed, it could still be reachable via a temporary root.

The assertion $\dagger \ell$ can be read as a permission to remove $\ell$ from the multiset of predecessors carried by a pointed-by-heap assertion. Indeed, the purpose of pointed-by-heap assertions is to keep track of live predecessors (§5.6).

A non-persistent deallocation witness $x \not\Leftrightarrow$ appears in Incorrectness Separation Logic [Raad et al. 2020]. In RustBelt [Jung et al. 2018a], the fact that a lifetime $\kappa$ has ended is expressed by a persistent assertion, known as a dead token, written $[\dagger\kappa]$. Persistent deallocation witnesses appear in Madiot and Pottier’s work [2022] and in our earlier paper [Moine et al. 2023]. These two papers do not have protected sections, therefore have no distinction between ordinary and temporary roots. There, a dead location is unreachable.

*Rules.* Figure 20 presents reasoning rules for deallocation witnesses. CLEANPBHEAP requires a deallocation witness for $\ell$ and produces the assertion $\ell' \leftarrow_0 \{-\ell\}$, a permission to remove $\ell$ from the predecessors of an arbitrary location $\ell'$. DEADPBHEAP and DEADPBTHREAD reflect the fact that logical deallocation consumes full pointed-by-heap and pointed-by-thread assertions. Therefore, the assertions $\dagger \ell$ and $\ell \leftarrow_q L$ cannot coexist, except in the special case where $q$ is zero, and the assertions $\dagger \ell$ and $\ell \Leftrightarrow_p \Pi$ cannot coexist. However, in contrast with our earlier work [Madiot and Pottier 2022; Moine et al. 2023], our deallocation witness is compatible with the points-to assertion. Indeed, our logical deallocation rule does not consume the points-to assertion. NODANGLINGROOTOUT and NODANGLINGROOTIN both state that it is impossible for a dead location
to be an ordinary root. A dead location can, however, be a temporary root: indeed, our logical deallocation rule allows deallocating a temporary root (§6.1).

## 5.10 Liveness-Based Cancellable Invariants

An Iris invariant [Jung et al. 2018b, §2.2] is written in the form $Φ$.<fnref n="7" /> It is a persistent assertion, whose meaning is that the assertion $Φ$ in the rectangular box holds at all times. The assertion $Φ$ itself is usually not persistent. An invariant can be temporarily accessed so as to gain access to the assertion $Φ$.

A cancellable invariant [Jung et al. 2018b, §7.1.3] is an invariant that comes with a teardown mechanism, allowing the user to recover ownership of the assertion $Φ$ once the invariant is canceled. This is a one-shot mechanism: once a cancellable invariant is torn down, it cannot be restored. Naturally, accessing a cancellable invariant requires proving that this invariant has not been torn down already. This is done by presenting a fractional access permission.

In IrisFit, a form of liveness-based cancellable invariants (LCIs, for short) naturally arises. An LCI is tied to a memory location $ℓ$, and remains in force as long as this location is live. When the location $ℓ$ is logically deallocated, all LCIs associated with $ℓ$ are implicitly torn down. Therefore, to access an LCI associated with the location $ℓ$, one must prove that this location is still live: that is, one must prove that $†ℓ$ implies $¬False$. This can be done using any of the rules DEADPBHEAP, DEADPBTHREAD, NODANGLINGROOTOUT, and NODANGLINGROOTIN in Figure 20. When the location $ℓ$ is logically deallocated, the assertion $Φ$ can be recovered at the same time. We have used LCIs to reason about closures (§9.5) and about Treiber’s stack (§11.5).

The implementation of LCIs is simple. A liveness-based cancellable invariant tied to the location $ℓ$, whose content is the assertion $Φ$, is just $†ℓ ∨ Φ$, that is, a plain Iris invariant whose content is the disjunction $†ℓ ∨ Φ$. By proving that $†ℓ$ is contradictory, the user excludes the left-hand disjunct, therefore obtains access to $Φ$. In particular, when one is about to logically deallocate $ℓ$, the assertion $ℓ ⇐= ∅$ is at hand, so $†ℓ$ is excluded. One can therefore open the invariant, extract $Φ$, deallocate $ℓ$, and close the invariant by supplying $†ℓ$, keeping $Φ$. (This is a somewhat unusual variation on the “golden idol” technique [Kaiser et al. 2017], with the persistent assertion $†ℓ$ in the role of the “bag of sand”.)

# 6 Program Logic: Reasoning Rules

In this section, we present the reasoning rules of IrisFit. Because most of our design is guided by the desire for a flexible logical deallocation rule, we begin with a presentation of this rule, in the simplified case where a single memory location is deallocated (§6.1). Then, we present the reasoning rules for terms (§6.2), devoting special attention to protected sections (§6.3) and to the BIND rule, whose form is non-standard (§6.4). The standard statement of the BIND rule can be recovered when the user enters a restricted mode where certain rules are disabled (§6.5). Finally, we present the general form of the logical deallocation rule, which can deallocate cycles (§6.6).

## 6.1 Logical Deallocation

As in the previous papers by Madiot and Pottier [2022] and Moine et al. [2023], a key aspect of IrisFit is to provide a logical deallocation rule. This rule produces space credits: by logically deallocating a memory block, the user recovers the space credits that were consumed when this block was allocated. It can be applied to a memory location $ℓ$ as soon as one is able to prove that this memory location is eligible for collection during the next garbage collection phase.

<footnote n="7">⁷Formally, an invariant also carries a namespace, a technicality that prevents the user from accessing the invariant twice and obtaining two copies of $Φ$ at the same time. For simplicity, we hide namespaces in this paper.</footnote>
As in the previous work cited above, *if $\ell$ is unreachable* then it can be logically deallocated. Furthermore, what is new in this paper, *if $\ell$ is reachable only via temporary roots* (that is, via roots that will disappear by the time all protected sections are exited), then it can also be logically deallocated.

This reasoning rule may seem surprising, as it involves a form of anticipation: it exploits the fact that $\ell$ will be eligible for collection *once all protected sections have been exited*, yet it produces space credits *immediately*, at the point where the rule is applied. The intuitive reason why this is sound is related with the following property: “once a large allocation request is outstanding, eventually, either this allocation request becomes unblocked or every thread is outside of a protected section”.<fnref n="8" /> Hence, *only* in the ideal situation where every thread is outside of a protected section, must one prove that a large allocation request can be satisfied. In such a situation, there are no temporary roots; every location that has been logically deallocated is effectively unreachable.

In §6.6, we present the general form of the logical deallocation rule, which can deallocate multiple memory locations at once, even if they form a cycle. Here, we present FREEONE, a simplified rule that is also useful in practice and that deallocates a single location $\ell$:

$$ \mathrm{sizeof}\ \ell n \ast \ell \leftarrow_1 \emptyset \ast \ell \leftarrow_1 \emptyset \Rightarrow \diamond\mathrm{size}(n) \ast \dagger\ell \quad \mathrm{FREEONE} $$

Because logical deallocation is a ghost operation, FREEONE is expressed as a ghost update. It consumes three assertions: the “`sizeof`” assertion `sizeof \ell n`, the pointed-by-heap assertion $\ell \leftarrow_1 \emptyset$, and the pointed-by-thread assertion $\ell \leftarrow_1 \emptyset$. The assertion `sizeof \ell n` indicates that the memory block at address $\ell$ has size $n$. The assertion $\ell \leftarrow_1 \emptyset$ guarantees that $\ell$ has no predecessor in the heap, that is, no memory block contains the pointer $\ell$. The assertion $\ell \leftarrow_1 \emptyset$ guarantees that $\ell$ is not an ordinary root of any thread: that is, if $\ell$ is a root at all in a thread $\pi$, then it must be a temporary root for this thread (§2.6, §5.8). Together, the last two assertions imply that $\ell$ will be eligible for collection in the next garbage collection phase.

On the right-hand side of the ghost update, FREEONE produces two assertions, namely the recovered space credits $\diamond n$ and the deallocation witness $\dagger \ell$. As noted earlier (§5.9), the latter assertion is a permission to remove $\ell$ from the predecessor multisets of other locations. Thus, by iterated application of FREEONE, acyclic chains of unreachable blocks can be logically deallocated.

FREEONE can be applied to a reachable location if this location is a temporary root inside a protected section. Our logic thereby allows such a location to be read or written *post mortem*, after it has been logically deallocated. This is made possible by the fact that the points-to assertion survives logical deallocation. This pattern appears, for example, in the verification of Treiber’s stack (§11.5).

Contrary to the logical deallocation rule presented by Moine et al. [2023], our rule does not consume or even mention a points-to assertion for the location $\ell$. Indeed, the points-to assertion is not needed to guarantee that the location is unreachable, nor is it needed to prevent a location from being deallocated twice. The size of the deallocated block is obtained in this paper from the “`sizeof`” assertion, whereas in the previous paper this assertion did not exist, so the size was obtained from a points-to assertion.

## 6.2 Reasoning Rules for Terms

Figure 21 presents most of the reasoning rules that concern instructions, except for the rules that are specific to protected sections, which are presented later on (§6.3). The reasoning rule `BIND`, which

<footnote n="8">⁸This property itself holds, under the assumption that enough polling points have been inserted, because as soon as one thread is waiting for space, every thread must eventually reach a large memory allocation instruction or a polling point, where it becomes blocked; and, at this point, this thread must be outside of a protected section.</footnote>
<figure><img src="image_19.png" /></figure>

PRIM

CALLPTR

$$v = \mu_{ptr} f . \lambda \vec{x} . t \qquad |\vec{x}| = |\vec{w}| \\ \{\text{outside } \pi * \Phi\} \pi : [v/f] [\vec{w}/\vec{x}] t \{\Psi\} \\ \{\text{outside } \pi * \Phi\} \pi : (v \vec{w})_{ptr} \{\Psi\}$$

VAL

$$\{\text{True}\} \pi : v \{\lambda v' . \text{True} = v\}$$

POLL

$$\{\text{outside } \pi\} \pi : \text{poll } \{\lambda(). \text{ outside } \pi\}$$

ALLOC

$$0 < n \\ \left\{ \begin{array}{c} \diamond n \\ \text{outside } \pi \end{array} \right\} \pi : \text{alloc size}(n) \left\{ \begin{array}{l} \ell \mapsto 1 \quad (\ell)^n \\ \ell \mapsto 1 \quad \emptyset \\ \ell \rightleftharpoons 1 \quad \{\pi\} \\ \text{outside } \pi \end{array} \right\}$$

LOAD

$$0 \le i < |\vec{w}| \qquad \vec{w}(i) = v \\ \left\{ \begin{array}{l} \ell \mapsto p \quad \vec{w} \\ v \right\} \pi : \ell[i] \left\{ \begin{array}{l} \text{True} = v \\ \lambda v' . \ell \mapsto p \quad \vec{w} \\ v \right\} \right\}$$

STORE

$$0 \le i < |\vec{w}| \qquad \vec{w}(i) = v \\ \left\{ \begin{array}{l} \ell \mapsto 1 \quad \vec{w} \\ v' \right\} \pi : \ell[i] \left\{ \begin{array}{l} \text{True} = v' \\ \lambda(). \ell \mapsto 1 \quad [i:=v'] \vec{w} \\ v \end{array} \right\} \right\}$$

CASSUCCESS

$$0 \le i < |\vec{w}| \qquad \vec{w}(i) = v \\ \left\{ \begin{array}{l} \ell \mapsto 1 \quad \vec{w} \\ v' \end{array} \right\} \pi : \text{CAS } \ell[i] v v' \left\{ \begin{array}{l} \text{true} \\ \lambda b . \ell \mapsto 1 \quad [i:=v'] \vec{w} \\ v' \end{array} \right\} \right\}$$

CASFAILURE

$$0 \le i < |\vec{w}| \qquad \vec{w}(i) \neq v \\ \left\{ \begin{array}{l} \ell \mapsto p \quad \vec{w} \\ \pi : \text{CAS } \ell[i] v v' \left\{ \begin{array}{l} \text{false} \\ \lambda b . \ell \end{array} \right\} \end{array} \right\}$$

FORK

$$\frac{\text{dom}(M) = \text{locs}(t)}{(\forall \pi'. \{\text{outside } \pi' * M \rightleftharpoons \{\pi' * \Phi\} \pi' : t \{\lambda(). \text{ outside } \pi'\} \} \rightleftharpoons \{\pi' * \Phi\} \pi' : \text{fork } t \{\lambda(). \text{ outside } \pi'\})}$$

<figure><img src="image_20.png" /><figcaption>Fig. 22. Reasoning rules: protected-section-specific rules</figcaption></figure>
allows reasoning under an evaluation context, is presented after that (§6.4). In every rule, the thread identifier $\pi$ represents the current thread, that is, the thread about which one is reasoning (§5.1).

`IFTRUE`, `IFFALSE`, `LETVAL`, `PRIM` and `VAL` are standard rules.

`CALLPTR` governs calls to (recursive, closed) functions, also known in this paper as code pointers. Its only unusual aspect is the presence of the assertion *outside* $\pi$, which ensures that the current thread is currently outside a protected section. The presence of this assertion forbids function calls inside protected sections.

Similarly, `POLL` forbids polling points inside a protected section. Outside of this aspect, a polling point is a no-operation.

`ALLOC` exhibits three differences with the allocation rule of Separation Logic. First, it requires and consumes `size(n)` space credits, so as to pay for the space occupied by the new block. Second, the presence of the assertion *outside* $\pi$ forbids allocation inside a protected section. Third, in addition to a points-to assertion for the new block, allocation produces pointed-by-heap and pointed-by-thread assertions. These assertions indicate that there is initially no pointer from the heap to the new block, and that this new block is a root for the current thread (and only for this thread).

As in standard Separation Logic, `LOAD` requires a (fractional) points-to assertion for the memory location $\ell$ that is accessed. Furthermore, it requires a pointed-by-thread assertion $v \Leftarrow_p \emptyset$ for the value $v$ that is read from memory. This assertion is updated to $v \Leftarrow_p \{\pi\}$, reflecting the fact that the value $v$ becomes a root for the current thread.

As in standard Separation Logic, `STORE` requires a full points-to assertion $\ell \mapsto_1 \vec{v}$ and produces an updated assertion $\ell \mapsto_1 [i := v']\vec{v}$. Furthermore, it performs bookkeeping of predecessor multisets, so as to reflect the fact that the value $v$ that was stored in the field $\ell[i]$ is overwritten with the value $v'$. First, to reflect the *creation* of an edge from $\ell$ to the value $v'$, an assertion of the form $v' \leftarrow_q \emptyset$ is changed to $v' \leftarrow_q \{+\ell\}$. Here, because $\ell$ has positive multiplicity in $\{+\ell\}$, the null-fraction invariant requires that $q$ be positive; it cannot be 0. Second, to reflect the *deletion* of an edge from $\ell$ to the value $v$, the assertion $v \leftarrow_0 \{-\ell\}$ appears in the postcondition. As explained earlier (§5.6), this assertion is a permission to remove one occurrence of $\ell$ from a multiset of predecessors of $v$.

`CASSUCCESS` is similar to `STORE`, but returns the Boolean value true rather than the unit value. Because a failed CAS does not modify the heap or create a new root, `CASFAILURE` is standard.

`FORK` reasons about the operation of spawning a new thread whose code is the term $t$. This operation must take place outside a protected section. Its impact on roots is as follows. Suppose, for a moment, that fork $t$ is the last instruction in the parent thread. Then, the locations that occur in the term $t$ cease to be roots of the parent thread $\pi$ and become roots of the child thread $\pi'$. The reasoning rule reflects this intuition by updating a group of pointed-by-thread assertions. The iterated pointed-by-thread assertion $M \Leftarrow \{\pi\}$ is taken away from the parent thread, and the updated assertion $M \Leftarrow \{\pi'\}$ is transmitted to the child thread. $M$ is a map of locations to fractions, whose domain is the set `locs($t$)`. This is a form of *trimming*, similar in effect to the rules `TRIMPBTHREAD` and `TRIMINSIDE`.

If fork $t$ is not the last instruction in the parent thread, then the user must use the reasoning rules `BIND` and `FORK` in combination. The interaction between the `BIND` rule and the “trimming” rules is discussed later on (§6.4, §6.5).

Still looking at `FORK`, an arbitrary assertion $\Phi$ is transmitted from the parent thread to the child thread. The assertion *outside* $\pi'$ is made available in the child thread, reflecting the fact that a new thread initially runs outside a protected section. The child thread $t$ must be verified with the nontrivial postcondition *outside* $\pi'$, thereby disallowing a thread to terminate while inside a protected section.

In our Coq mechanization, the postconditions of many reasoning rules contain a *later credit* [Spies et al. 2022]. Later credits play a role in eliminating the “later” modality. They are orthogonal to
the main concern of this paper, namely the analysis of space complexity, so we hide them in the presentation of our reasoning rules. We do explain how later credits are used in our case study of the async-finish library (§11.4).

## 6.3 Reasoning about Protected Sections

Within a protected section, the reasoning rules presented in the previous section (§6.2) can still be used, except for `CALLPTR`, `ALLOC`, and `POLL`, which require the assertion `outside π`. In addition, a number of reasoning rules, shown in Figure 22, specifically concern protected sections.

ENTER allows entering a protected section. This rule transforms the assertion `outside π` into the assertion `inside π ∅`, thereby witnessing that the current thread is now inside a protected section and has no temporary roots.

Conversely, EXIT allows exiting a protected section. By consuming the assertion `inside π ∅`, this rule requires the user to prove that the current thread has no remaining temporary roots.

LOADINSIDE allows reading a value `v` from a location `ℓ` in the heap. The locations that appear in the value `v` become temporary roots of the current thread: the assertion `inside π T` is updated to `inside π (T ∪ locs(v))`. In contrast with LOAD, no pointed-by-thread assertion is required or updated. In fact, the location `ℓ` or some locations in the set `locs(v)` might be logically deallocated already.

STOREDEAD allows writing a logically deallocated block. The rule requires and updates a points-to assertion. A deallocation witness `†ℓ` is also required. Compared with STORE, no pointed-by-heap assertion is required or updated. Indeed, there is no need to do so. Pointed-by-heap assertions keep track of which blocks are reachable via ordinary roots; but, because the block at address `ℓ` is logically deallocated, it is not reachable via ordinary roots. This is reminiscent of CLEANPBHEAP.

Although STOREDEAD does not require an "inside" assertion, it can be used only inside a protected section. Indeed, the rule applies to a store instruction `ℓ[i] ← v'`, where the address `ℓ` occurs. This means that `ℓ` is a root, yet `ℓ` is also logically deallocated. This is possible only if the current thread is currently inside a protected section. Indeed, outside a protected section, a logically deallocated location cannot be a root: the rule NODANGLINGROOTOUT says so (§5.9).

CASSUCCESSDEAD is analogous to STOREDEAD. It concerns a successful CAS instruction on a logically deallocated location. Because a failed CAS does not write anything, the rule CASFAILURE can be applied to a logically deallocated location without change.

## 6.4 Reasoning under Evaluation Contexts

A proof in Separation Logic is traditionally carried out under an unknown context. That is, one reasons about a term `t` without knowing in what evaluation context `K` this term is placed. There are specific points in the proof where this unknown context grows and shrinks. As an archetypical example, consider the sequencing construct let `x = t₁` in `t₂`. To reason about this construct, one first focuses on the term `t₁`, thereby temporarily forgetting the frame let `x = □` in `t₂`, which is pushed onto the unknown context. After the verification of `t₁` is completed, this focusing step is reversed: the frame let `x = □` in `t₂` is popped and one continues with the verification of `t₂`. These focusing and defocusing steps are described by the "BIND" rule [Jung et al. 2018b, §6.2].

In our setting, however, a complication arises. An evaluation context contains memory locations. When one applies the BIND rule, so as to temporarily forget about this evaluation context, one must still somehow record that these locations are roots. We use pointed-by-thread assertions for this purpose.

Suppose we wish to decompose the sequence let `x = t₁` in `t₂` into a subterm `t₁` and an evaluation context let `x = □` in `t₂`. For simplicity, let us further assume that `locs(t₂)` is a singleton set `{ℓ}`. This implies that, while `t₁` is being executed, the location `ℓ` is a root. In this specific case, our BIND rule
takes the following form:

$$ \begin{array}{c} \text{PARTICULAR CASE OF BIND} \\ \text{locs}(t_2) = \{\ell\} \quad \{\Phi\} \pi: t_1 \{\Psi'\} \quad \forall v. \{\ell \Leftrightarrow \pi \{\pi\} * \Psi' v\} \pi: [v/x]t_2 \{\Psi\} \\ \{\ell \Leftrightarrow \pi \{\pi\} * \Phi\} \pi: \text{let } x = t_1 \text{ in } t_2 \{\Psi\} \end{array} $$

What is unusual, compared with the standard `BIND` rule of Separation Logic, is that the fractional pointed-by-thread assertion $\ell \Leftrightarrow \pi \{\pi\}$ is required in the beginning, taken away from the user while focusing on the term $t_1$, and given back to the user once she is done reasoning about $t_1$ and ready to reason about $t_2$. In other words, this assertion is *forcibly framed out* while reasoning about $t_1$.

The assertion $\ell \Leftrightarrow \pi \{\pi\}$ records that $\ell$ is a root in thread $\pi$. By taking it away from the user and by giving it back once she is done reasoning about $t_1$, we ensure that the information that "$\ell$ is a root in thread $\pi$" is carried up to this point and cannot be prematurely destroyed.

What could go wrong if we did not do this? Then, the user would be allowed to keep the full pointed-by-thread assertion $\ell \Leftrightarrow_1 \{\pi\}$ while reasoning about $t_1$. Technically, the user would do so by instantiating $\Phi$ with $\ell \Leftrightarrow_1 \{\pi\}$ in the `BIND` rule. Then, the user would focus on establishing the first premise, $\{\ell \Leftrightarrow_1 \{\pi\}\} \pi: t_1 \{\Psi'\}$. Now suppose $\ell \notin \text{locs}(t_1)$, that is, $\ell$ does not occur in $t_1$. Then, the user could apply `TRIMPBTHREAD` to transform the assertion $\ell \Leftrightarrow_1 \{\pi\}$ into $\ell \Leftrightarrow_1 \emptyset$. Oops! The assertion $\ell \Leftrightarrow_1 \emptyset$ means that $\ell$ is not a root. Yet $\ell$ really is still a root, as it occurs in the evaluation context that has been abstracted away, namely let $x = \square$ in $t_2$.

Besides `TRIMPBTHREAD`, two reasoning rules, namely `FORK` and `TRIMINSIDE`, involve a form of "trimming" of sets of thread identifiers. The soundness of these rules relies on the fact that `BIND` forcibly frames out fractional pointed-by-thread assertions.

The general form of our `BIND` rule, shown in Figure 23, extends this idea to an arbitrary evaluation context $K$, in which an arbitrary number of locations may occur. Then, for every location in `locs($K$)`, a fractional pointed-by-thread assertion is forcibly framed out.

$$ \begin{array}{c} \text{BIND} \\ \text{dom}(M) = \text{locs}(K) \quad \{\Phi\} \pi: t \{\Psi'\} \quad \forall v. \{M \Leftrightarrow \{\pi\} * \Psi' v\} \pi: K[v] \{\Psi\} \\ \{M \Leftrightarrow \{\pi\} * \Phi\} \pi: K[t] \{\Psi\} \end{array} $$

<caption>Fig. 23. Reasoning rules: the `BIND` rule</caption>

## 6.5 Locally Trading Trimming for a Simpler and More Powerful Bind Rule

Forcing pointed-by-thread assertions to be framed out at each application of `BIND` is cumbersome, and can be restrictive, as there are situations where no pointed-by-thread assertion is at hand. (An example appears later on in this section.) Fortunately, such forced framing is unnecessary if the user promises not to exploit any of the trimming rules `TRIMPBTHREAD`, `FORK` and `TRIMINSIDE`. Thus, we introduce a mode that the user may choose to enter at any time, in which the trimming rules are disabled and, in exchange, a simpler, more powerful `BIND` rule is made available.

We parameterize IrisFit triples with a mode $m$, which is either the normal mode $\bowtie$ or the "no trim" mode $\times$. Thus, in general, our triples have the form $\{\Phi\} m/\pi: t \{\Psi\}$, and our custom ghost update has the form $\Phi \pi \Rightarrow_V^m \Phi'$. All of the reasoning rules presented so far are polymorphic in the mode, except for the trimming rules `TRIMPBTHREAD`, `FORK`, and `TRIMINSIDE`, which are disabled in "no trim" mode. For example, `TRIMPBTHREAD` is written $(\neg \ell \notin V^* \ell \Leftrightarrow \pi \{\pi\}) \pi \Rightarrow_V^m \ell \Leftrightarrow \pi \emptyset$, which prevents its use when in the "no trim" mode $\times$. The public specification of a function is always stated in the normal mode. The "no trim" mode is intended for local use, inside the body of a function. It is an adaptation of Moine et al.'s "NOFREE" mode [2023].
$$ \frac{\text{SWITCHMODE} \quad \{\Phi\} \times / \pi : t \{\Psi\}}{\{\Phi\} m / \pi : t \{\Psi\}} \qquad \frac{\text{BINDNoTRIM} \quad \{\Phi\} \times / \pi : t \{\Psi'\}}{\{\Phi\} m / \pi : K[t] \{\Psi\}} \quad \forall v. \{\Psi'v\} m / \pi : K[v] \{\Psi\} $$

<caption>Fig. 24. Reasoning rules: additional mode-specific rules</caption>

$$ \begin{array}{l @{\quad} l @{\quad} l @{\quad} c @{\quad} l} \top \text{True} & \leftarrow & \emptyset \boxplus \emptyset & \multicolumn{2}{c}{\text{CLOUDEMPTY}} \\ \ell \Leftarrow \emptyset & \ast & \ell \leftarrow \emptyset & L & \ast & \text{NoNegative}(L) \top \\ \top \mathcal{P} \subseteq D \top & \ast & \mathcal{P} \boxplus^n D & \Rightarrow & \diamond n & \ast \top \mathcal{D} \mathcal{L} & \multicolumn{2}{c}{\text{CLOUDFREE}} \\ \multicolumn{7}{l}{\text{CLOUDADD}} \end{array} $$

<caption>Fig. 25. Reasoning rules: logical deallocation</caption>

Figure 24 presents two new reasoning rules, `SWITCHMODE` and `BINDNoTRIM`, which allow entering “no trim” mode and taking advantage of it.

When read from bottom to top, `SWITCHMODE` lets the user locally enter “no trim” mode, whenever she so wishes, in a subproof. When read from top to bottom, this rule asserts that if a triple holds in “no trim” mode then it also holds in normal mode. Indeed, every reasoning rule that is available in “no trim” mode is available in normal mode as well.

`BINDNoTRIM` is the standard `BIND` rule of Separation Logic, but imposes a switch to “no trim” mode `×` in its left-hand premise. Thus, unlike our `BIND` rule, it does not force pointed-by-thread assertions to be framed out. Because of this, it must disable the trimming rules while the user reasons about the subterm `t`.

We remark that, inside a protected section, one can switch to “no trim” mode without loss of expressive power. Indeed, there, the trimming rules are never needed. `FORK` is forbidden inside protected sections; the effect of `TRIMPBTHREAD` can be simulated by `ADDTEMPORARY`; and all uses of `TRIMINSIDE` can be postponed until the protected section is about to be exited.

At a high level, `BINDNoTRIM` is needed for reasoning about code that, within a protected section, reads or writes in a location after it has been logically deallocated. Indeed, in this case, `BIND` can be too restrictive. To illustrate this case, consider the following code, where we assume that the location `r` is not accessible via the heap and is not known to any thread other than the current thread:

$$ \text{enter}; (\text{let } x = t \text{ in } x + r[0]); \text{exit} $$

Just after entering the protected section, the user may wish to logically deallocate `r`, in order to recover the corresponding space credits without waiting for the end of the protected section. In this case, just after entering the protected section, she would use `ADDTEMPORARY` to obtain a pointed-by-thread assertion `r \Leftarrow \emptyset`, then use `FREEONE` to logically deallocate `r`. `FREEONE` consumes this pointed-by-thread assertion but preserves the points-to assertion for `r`, which the load instruction `r[0]` needs. Thereafter, the user may wish to decompose the let construct. Yet, the `BIND` rule cannot be used, as it would require a (fractional) pointed-by-thread assertion for `r`, which no longer exists, because the fraction 1 was consumed by `FREEONE`. Fortunately, `BINDNoTRIM` is applicable.
demo ≜ µptr... λ[].
let x = alloc 1 in
let y = alloc 1 in
x[0] ← y;
fork (x[0] ← x);
.wait [x])ptr

wait ≜ µptr.f. λ[x].
if x[0] = x
then ()
else (f [x])ptr

<caption>Fig. 26. The demo function and its auxiliary function wait</caption>

## 6.6 Logical Deallocation of Cycles

Figure 25 presents our rules for deallocating an unreachable heap fragment, as opposed to a single location. This fragment may contain an arbitrary number of heap blocks, which may point to each other in arbitrary ways. In particular, these pointers may form one or more cycles.

These rules make use of the “cloud” assertion $P \blacktriangle^n D$, whose parameters $P$ (for “predecessors”) and $D$ (for “domain”) are sets of locations, and whose parameter $n$ is a natural integer. This assertion means that the memory blocks at locations $D$ have total size $n$, that the locations $D$ are not roots in any thread, and that these locations can be reached only via the locations $P$. We refer to $P$ also as the *entry points* of the cloud.

If $P \subseteq D$ holds, then the locations in the set $D$ are reachable only via $D$ itself. In other words, the set $D$ is closed under predecessors. This means that the locations in the set $D$ are in fact *unreachable*, and can safely be logically deallocated. This explains the side condition $P \subseteq D$ in the logical deallocation rule CLOUDFREE. We do not require $P \subseteq D$ to hold at all times: while constructing large “cloud” assertions out of smaller “cloud” assertions, one must allow the sets $P$ and $D$ to be unrelated.

Figure 25 presents two cloud construction rules as well as the logical deallocation rule, which consumes a cloud.

Out of nothing, CLOUDEMPTY creates an empty cloud $\emptyset \blacktriangle^0 \emptyset$.

CLOUDADD adds the memory block at location $\ell$ to an existing cloud $P \blacktriangle^n D$. This consumes the full pointed-by-thread assertion $\ell \Leftarrow_1 \emptyset$, which guarantees that $\ell$ is not a root in any thread, and the full pointed-by-heap assertion $\ell \Leftarrow_1 L$, which guarantees that $L$ contains all of the predecessors of the location $\ell$ in the heap. A “sizeof” assertion determines the size $m$ of the memory block at address $\ell$. CLOUDADD produces an extended cloud, where $L$ is added to the cloud’s entry points, $m$ is added to the cloud’s size, and $\ell$ is added to the cloud’s domain.

CLOUDFREE logically deallocates a cloud that is closed under predecessors, that is, a cloud such that $P \subseteq D$ holds. The “cloud” assertion is consumed. In exchange for it, the rule produces $n$ space credits, where $n$ is the size of the cloud. Furthermore, it produces a deallocation witness for every location in the cloud.

The rule FREEONE that was presented earlier (§6.1) is easily derived from the rules in Figure 25.

## 7 Interlude: Verifying a Small Example

Before diving into the soundness statements of IrisFit, extensions of IrisFit, and case studies, let us showcase how one proves a small program, with concurrency, but without protected sections.

*Demo Program.* The program, named demo, appears in Figure 26. Following standard practice, we write $t_1$; $t_2$ as sugar for let $x = t_1$ in $t_2$ where $x \notin fv(t_2)$. The demo program proceeds as follows. First, two blocks of size 1 are allocated. Their addresses, say $\ell_x$ and $\ell_y$, are bound to the variables $x$ and $y$. Then, the address $\ell_y$ is stored inside the block at address $\ell_x$. Next, a new thread is forked.
This new thread executes the store instruction $\ell_x[0] \leftarrow \ell_x$: that is, it writes the address $\ell_x$ into the block at address $\ell_x$, creating a cyclic pointer from this block to itself. Meanwhile, the main thread launches an active waiting loop, which runs until it observes that $\ell_x$ points to itself—that is, until it observes the effect of the store instruction executed by the child thread. This loop is implemented by means of the auxiliary function wait.

*Specification.* Our goal is to establish that executing demo requires two words of memory and that these two words are recovered once demo terminates. In IrisFit, this specification is expressed by this triple:

$$ \{\text{outside } \pi * \diamond 2\} \pi : (\text{demo })_{\text{ptr}} \{\lambda(). \text{ outside } \pi * \diamond 2\}. $$

The challenge is to prove that, by the time the main thread completes, the blocks $\ell_x$ and $\ell_y$ can be logically deallocated. To this end, we must argue that, upon completion of the main thread, the blocks $\ell_x$ and $\ell_y$ are not pointed by any other heap block and that they are no longer roots in any thread. We begin by presenting the high-level arguments.

*Intuition for the Proof.* Let us focus in turn on the addresses $\ell_x$ and $\ell_y$. For each of these locations, let us examine in turn which heap blocks point to it and in which threads it is a root.

As soon as the child thread executes the instruction $\ell_x[0] \leftarrow \ell_x$, the location $\ell_x$ becomes stored in the heap. However, it is stored in the block $\ell_x$ itself, and nowhere else. The block $\ell_x$ is never pointed to by another heap block.

The location $\ell_x$ ceases to be a root for the main thread when the test $\ell_x[0] = \ell_x$ in wait succeeds. Indeed, the call to wait is the last instruction of the function demo, and the “then” branch in the function wait contains the trivial instruction (), which does not mention $\ell_x$. Furthermore, by means of the invariant that is described further on, one can prove that the success of the test $\ell_x[0] = \ell_x$ guarantees that the child thread has executed its store instruction. Therefore, when the main thread completes, $\ell_x$ is no longer a root for the child thread. Thus, at that point, $\ell_x$ is no longer a root at all.

The location $\ell_y$ is initially stored in the block $\ell_x$. However, as soon as the child thread executes its store instruction, which overwrites $\ell_y$ with $\ell_x$, the location $\ell_y$ ceases to appear in the heap. Furthermore, as explained earlier, the main thread does not complete until the child thread has executed this store instruction. Therefore, when the main thread completes, the address $\ell_y$ is no longer stored in the heap.

The location $\ell_y$ is not mentioned in the child thread, and is not read from the heap by this thread, hence $\ell_y$ is never a root for the child thread. Furthermore, clearly, once the main thread completes, $\ell_y$ is no longer a root for the main thread.<fnref n="9" />

As mentioned above, we exploit an *Iris invariant* to transfer knowledge between the child thread and the main thread. An invariant can be thought of as a description of the states of a state machine, which governs how threads interact and what resources they exchange. The transitions of this state machine are not mentioned in the invariant: they are implicit. In a proof, an invariant is typically *opened, analyzed* so as to determine which state (or states) may be current, then *closed* in the same state or in a new state.

<footnote n="9">⁹A look at the code suggests that the *variable y* ceases to be a root immediately after the instruction $x[0] \leftarrow y$ is executed. Indeed, beyond this point in the code, the *variable y* does not occur. However, this remark is irrelevant. The truly relevant question is not which *variables* are roots, but which *memory locations* are roots. Here, as long as the waiting loop runs, the *location* $\ell_y$ may be a root for the main thread, because the instruction $\ell_x[0]$ in the function wait can read $\ell_y$ from the heap and return $\ell_y$. Thus, $\ell_y$ definitively ceases to be a root for the main thread only once the instruction $\ell_x[0]$ has returned $\ell_x$.</footnote>
The invariant involved in reasoning about demo is the following:

$$ 
\begin{array}{l}
\ell_x \mapsto_1 [\ell_y] \\
I \quad \triangleq \quad \begin{array}{l} \lor \quad \ell_x \mapsto_1 [\ell_x] * \ell_x \leftarrow_1 \{+\ell_x\} * \ell_x \iff_{\frac{1}{2}} \emptyset * \ell_y \leftarrow_1 \emptyset \\ \lor \quad \dagger \ell_y \end{array}
\end{array}
$$

The first disjunct of the invariant $I$ represents the initial state, in which the block at address $\ell_x$ contains a pointer to the block at address $\ell_y$. The second disjunct represents the intermediate state in which the child thread has terminated and given up its resources, but the main thread has not yet observed that $\ell_x$ now points to itself. The third disjunct $\dagger \ell_y$ corresponds to the final state, which is reached at the point where the block $\ell_y$ can be logically deallocated. (The presence of a disjunct of the form $\dagger \ell_y$ makes $I$ an example of a liveness-based cancellable invariant, in the sense of §5.10.)

*Formal Arguments Involved in the Proof.* Let us begin by reasoning on the instructions from demo. First, we apply the rule `CALLPTR` and enter the function body. Then, we face two allocations of blocks of size 1. We apply `SPLITJOINSC` to the assertion $\diamond 2$ to obtain $\diamond 1 * \diamond 1$. To be more precise, the first allocation that we face lies under a let binding. To enter the left-hand side of this let binding, we use `BINDNoTRIM`. Then, we apply `ALLOC`: we lose one space credit, we name the resulting location $\ell_x$, and we obtain the assertions $\ell_x \mapsto_1 [())$ and $\ell_x \iff_1 \{\pi\}$ and $\ell_x \leftarrow_1 \emptyset$. We then use `LETVAL` to substitute $\ell_x$ for $x$ in the remaining term. We repeat the exact same three steps to reason about the second allocation and name its result $\ell_y$. We apply the rule `SIZEOfPOINTSTo` to obtain `sizeof \ell_y` 1. We deduce from the two points-to assertions that $\ell_x$ and $\ell_y$ are distinct. Because $\ell_y$ is never read or written, we throw away its points-to assertion. At this point, we hold the permissions `sizeof \ell_y` 1 and $\ell_y \iff_1 \{\pi\}$ and $\ell_y \leftarrow_1 \emptyset$.

The term that remains to reason about is:

$$ \ell_x[0] \leftarrow \ell_y; \text{ fork}(\ell_x[0] \leftarrow \ell_x); (\text{wait}[\ell_x])_{\text{ptr}} $$

We apply the rule `BINDNoTRIM` to focus on the store instruction $\ell_x[0] \leftarrow \ell_y$. For this instruction, we apply the rule `STORE`, thereby trading the assertion $\ell_x \mapsto_1 [()) * \ell_y \leftarrow_1 \emptyset$ for the assertion $\ell_x \mapsto_1 [\ell_y] * \ell_y \leftarrow_1 \{+\ell_x\}$.

We now reach the fork instruction. We initialize the aforementioned invariant $I$ by entering the initial state, that is, by providing the assertion $\ell_x \mapsto_1 [\ell_y]$. At this stage, we need to split the assertion $\ell_x \iff_1 \{\pi\}$ in two halves, because we will need one half to witness a root held by the context, and one half to transmit to the child thread. Concretely, we apply `FRACPBTHREAD` to this assertion and obtain $\ell_x \iff_1 \{\pi\} * \ell_x \iff_2 \{\pi\}$. To focus on the fork instruction, we apply the rule `BIND`. (We cannot exploit `BINDNoTRIM` because `FORK` involves trimming.) Applying `BIND` requires us to temporarily give up the fractional pointed-by-thread permission $\ell_x \iff_2 \{\pi\}$.

We next apply the rule `FORK`. Thereafter, we focus on the child thread, whose code is $\ell_x[0] \leftarrow \ell_x$. We name the new thread identifier $\pi'$. To the child thread, we transmit the invariant $I$ as well as the assertions $\ell_x \leftarrow_1 \emptyset$ and $\ell_y \leftarrow_1 \{+\ell_x\}$. The application of `FORK` updates the assertion $\ell_x \iff_2 \{\pi\}$ into $\ell_x \iff_2 \{\pi'\}$, which is transmitted to the child thread.

To reason about the store instruction $\ell_x[0] \leftarrow \ell_x$, we first open the invariant $I$. We eliminate the third disjunct $\dagger \ell_y$ by using `DEADPBHEAP`. We also eliminate the second disjunct $(\cdots * \ell_y \leftarrow_1 \emptyset)$ by using `JOINPBHEAP` together with fractional reasoning about the pointed-by-heap assertion for $\ell_y$ (a fraction cannot exceed 1). Only the first disjunct remains: so, we acquire the assertion $\ell_x \mapsto_1 [\ell_y]$. Then, we can apply the rule `STORE`, trading $\ell_x \mapsto_1 [\ell_y] * \ell_x \leftarrow_1 \emptyset$ for $\ell_x \mapsto_1 [\ell_x] * \ell_x \leftarrow_1 \{+\ell_x\} * \ell_y \leftarrow_0 \{-\ell_x\}$. We use `JOINPBHEAP` to transform $\ell_y \leftarrow_1 \{+\ell_x\} * \ell_y \leftarrow_0 \{-\ell_x\}$ into $\ell_y \leftarrow_1 \emptyset$. A store instruction returns the unit value (), so, after the store takes place, we use `CONSEQUENCE` and `TRIMPBTHREAD` to update the assertion $\ell_x \iff_2 \{\pi'\}$ into $\ell_x \iff_2 \emptyset$, witnessing that $\ell_x$ is not
a root of the child thread any more. We then close the invariant *I* by giving up all of the assertions at hand, forming the second disjunct of *I*.

We now turn our attention back to the main thread, whose sole remaining instruction is: (wait [*l*<sub>x</sub>])<sub>ptr</sub>. We exploit the fact that *l*<sub>y</sub> is not a root for this term, together with the rules CONSEQUENCE and TRIMPBTHREAD, to obtain *l*<sub>y</sub> ⇐ 1 ∅. At this point, there remains to prove the following triple, which corresponds to a specification of the auxiliary function wait.

$$
\{ \text{outside } \pi * \mathbf{I} * \text{sizeof } \ell_y 1 * \ell_y \Leftarrow 1 \emptyset * \ell_x \Leftarrow \frac{1}{2} \{\pi\} \} \pi: (\text{wait } [\ell_x])_{\text{ptr}} \{\lambda(). \text{outside } \pi * \diamond 2\}
$$

We establish this triple using Löb induction [Jung et al. 2018b]. We use `CALLPTR` and enter the function body. We face the term: if $\ell_x[0] = \ell_x$ then () else ($f[\ell_x]_{\text{ptr}}$). We first use `BINDNOTRIM` to focus on the condition of the if statement, $\ell_x[0] = \ell_x$, and use `BINDNOTRIM` again to focus on the load $\ell_x[0]$.

By making use of the information stored in the invariant, we will now prove that this load must
return $\ell_x$ or $\ell_y$. We open the invariant $\mathbf{I}$ and perform a case analysis on $I$, giving rise to three cases.
In each of the first two cases, we explain how to close the invariant; the third case, we rule out.

(1) In the first case, we have $\ell_x \mapsto 1 [\ell_y]$. We apply `LOAD`, which updates the assertion $\ell_y \Leftarrow 1 \emptyset$ into $\ell_y \Leftarrow 1 \{\pi\}$, and close the invariant in the same state as it was just opened.

(2) In the second case, we have $\ell_x \mapsto 1 \ell_x * \ell_x \leftarrow 1 \{+\ell_x\} * \ell_x \leftarrow \frac{1}{2} \emptyset * \ell_y \leftarrow 1 \emptyset$. This case involves logical deallocation. First, we use CONSEQUENCE and FREEONE to logically deallocate $\ell_y$. We obtain one space credit and a deallocation witness $\dagger \ell_y$. Then, we apply LOAD, which updates the assertion $\ell_x \Leftarrow 1 \emptyset$ into $\ell_x \Leftarrow 1 \{\pi\}$. We close the invariant using the third disjunct, that is, by providing $\dagger \ell_y$.

(3) In the third case, we have $\dagger \ell_y$. This case is eliminated by using DEADPBTHREAD. Indeed, we hold the pointed-by-thread assertion $\ell_y \Leftarrow 1 \emptyset$ therefore $\ell_y$ cannot be deallocated.

Let $\ell_z$ be the result of the load $\ell_x[0]$. If we went through case (1) above, then we have $\ell_z = \ell_y$. If we went through case (2), then we have $\ell_z = \ell_x$. We apply the rule PRIM to reason about the test that compares $\ell_z$ with $\ell_x$. Let us show, in each of the two cases, how to conclude the proof.

(1) Case $\ell_z = \ell_y$. Because $\ell_y$ and $\ell_x$ are distinct addresses, the test must evaluate to false. We apply `IFFALSE` and enter the second branch of the conditional: we now face the recursive call ($f[\ell_x]_{\text{ptr}}$). Using `CONSEQUENCE` and `TRIMPBTHREAD`, we trim the pointed-by-thread assertion for $\ell_y$, changing the assertion $\ell_y \Leftarrow 1 \{\pi\}$ back into $\ell_y \Leftarrow 1 \emptyset$. We conclude by applying the induction hypothesis.

(2) Case $\ell_z = \ell_x$. This time, the test must evaluate to true. We apply `IFTRUE` and enter the first branch of the conditional. There remains to establish the following triple:

$$
\left\{
\begin{array}{l}
\text{outside } \pi * \diamond 1 \\
\ell_x \mapsto 1 [\ell_x] \\
\ell_x \Leftarrow \frac{1}{2} \{\pi\} * \ell_x \Leftarrow \frac{1}{2} \emptyset \\
\ell_x \Leftarrow 1 \{+\ell_x\}
\end{array}
\right\}
\quad \pi: () \ \{\lambda(). \text{outside } \pi * \diamond 2\}
$$

Using FRACPBTHREAD, we obtain $\ell_x \Leftarrow 1 \{\pi\}$. Next, using CONSEQUENCE and TRIMPBTHREAD, we obtain $\ell_x \Leftarrow 1 \emptyset$. In order to logically deallocate the single-cell cycle $\ell_x$, we use the cloud rules presented in §6.6 to construct the cloud assertion $\{\ell_x\} \underset{\ell_x}{\overset{1}{\bullet}} \{\ell_x\}$. Then, using CONSEQUENCE and CLOUDFREE, we obtain one space credit. Finally, using SPLITJOINSC, we join the two space credits. We conclude using VAL.
<figure><img src="image_21.png" /><figcaption>Fig. 27. Predicates used in the statement of the safety theorem</figcaption></figure>

# 8 Safety and Liveness

In this section, we state several theorems about programs that have been verified using IrisFit. In short, we wish to establish three properties, namely *safety* (no thread can crash), *liveness* (no thread can be blocked forever), and *bounded space consumption* (the size of the heap cannot exceed a certain bound). We first state these properties about the default semantics (§4.2.9), then discuss the growing semantics (§4.2.10) and the oblivious semantics (§4.2.7).

The *safety theorem* (§8.1) guarantees that no thread crashes. More precisely, it states that if a thread is enabled (§4.2.8) then this thread is not stuck: either it has reached a value or it can make a step.

The *liveness theorem* (§8.2) guarantees that no thread can be blocked forever. More precisely, under the assumption that there is a polling point in front of every function call, we prove that every thread is eventually enabled. Furthermore, we prove that inserting a polling point in front of every function call preserves safety. Thus, after a source program without polling points has been verified with IrisFit, one can let a compiler automatically insert polling points, and obtain both safety and liveness for this instrumented program.

In the default semantics of LambdaFit, by design, the size of the heap cannot exceed the limit *S* (Lemma 4.2). Therefore, the *bounded space consumption* property comes for free.

With respect to the growing semantics, we are able to establish similar results. In this semantics, the heap size limit can grow at runtime, so the statement of the *bounded space consumption* property must be slightly relaxed (§8.3).

All of our results about the default and growing semantics follow from a single *core soundness* theorem stated with respect to the oblivious semantics (§8.4). This theorem spells out the guarantee that is offered by IrisFit when a LambdaFit program is executed with blocking instructions ignored and garbage collection disabled.

All of our results are mechanized using the Coq proof assistant. For more details about our proofs, the reader is referred to our mechanization [Moine 2025] and to the first author's dissertation [Moine 2024].

## 8.1 Safety

A concurrent Separation Logic typically comes with a safety guarantee, formulated in the form: "no thread can crash". A more precise statement is: "always, every thread is not stuck". In other words, in every reachable configuration of the system, every thread either has terminated or is able to make a reduction step. A thread that has not reached a value and is unable to make a step is stuck: by convention, this is considered an undesirable situation, akin to a crash.

In our setting, however, this statement must be amended, because LambdaFit has blocking instructions. A blocking instruction is sometimes *disabled* (§4.2.8), therefore unable to make a step; yet, this situation is not considered a crash.

Our amended safety guarantee is qualified as follows: "always, every *enabled* thread is not stuck". A thread that is not enabled is considered blocked: this is a normal situation.
$$ \frac{\text{HOLDSNOW}}{\text{AfterAtMost (\rightarrow) } n P c} $$

$$ \frac{\text{HOLDSAFTER} \quad \exists c'. c \to c' \quad \forall c'. c \to c' \implies \text{AfterAtMost (\rightarrow) } n P c'}{\text{AfterAtMost (\rightarrow) } (n+1) P c} $$

$$ \frac{\text{ALWAYS} \quad \forall c'. c \to^* c' \implies P c'}{\text{Always (\rightarrow) } P c} $$

$$ \frac{\text{EVENTALLY} \quad \text{AfterAtMost (\rightarrow) } n P c}{\text{Eventually (\rightarrow) } P c} $$

<caption>Fig. 28. Temporal logic predicates</caption>

Figure 27 defines a few auxiliary predicates that appear in the statement of the safety theorem. The proposition NotStuck<sub>S</sub> c π means that, in the configuration c, the thread identified by π is not stuck. It is defined by two rules. NOTSTUCKVAL states that if a thread has reached a value and is outside a protected section, then it is not stuck. (Terminating inside a protected section is forbidden.) NOTSTUCKSTEP states that if a thread can take a step, then it is not stuck. The proposition Safe<sub>S</sub> c, defined by the rule SAFE, means that no enabled thread in the configuration c is stuck.

The proposition Always (\rightarrow) P c, which is defined by the rule ALWAYS in Figure 28, means that every configuration that is reachable from the configuration c via the reduction relation \rightarrow satisfies the predicate P.

The safety theorem (Theorem 8.1) can be read as follows. Suppose that the program t has been verified using IrisFit, with an arbitrary identifier π for the main thread, under the precondition ◊S * outside π and the postcondition outside π. The precondition provides S space credits and guarantees that the main thread initially runs outside a protected section. The postcondition forbids termination inside a protected section. Then, the initial configuration init(t) (§4.2.2) is always safe: that is, beginning in this configuration, running the program under the default semantics with heap limit S cannot reach a configuration where a thread is stuck.

**THEOREM 8.1 (SAFETY).** Assume that the following triple holds:

$$ \forall \pi. \{◊S * \text{ outside } \pi\} \pi : t \{\lambda_{\_}. \text{ outside } \pi\} $$

Then Always (default<sub>S</sub>) Safe<sub>S</sub> (init(t)) holds.

Although this theorem mentions S, the meaning of a triple is independent of S. Therefore, the reasoning rules are independent of S as well. One can verify a program component without mentioning S and without knowing its value. A concrete value of S must be chosen and fixed only when Theorem 8.1 is applied to a complete (closed) program.

## 8.2 Liveness

The safety theorem guarantees that no thread can crash, but allows a thread to become blocked. Therefore, a liveness guarantee is also desirable: one would like to be assured that always, every thread is eventually enabled. In other words, there is no execution scenario where, past a certain point, a thread remains forever blocked (i.e., is never enabled).

In fact, we are able to offer a stronger guarantee: we prove that always, eventually, every allocation fits. In other words, in every execution scenario, infinitely often, the system reaches a point where
no allocation request is blocked due to a lack of memory. This property is indeed stronger, because it guarantees that, at that point, all threads are simultaneously enabled.<fnref n="10" />

However, our liveness guarantee is subject to a condition: the program must contain enough polling points. To see why this is necessary, imagine a program where thread A is blocked on a large allocation request and thread B is running in an infinite loop, without allocating memory or encountering a polling point. Then, there exists a scenario where thread B runs forever, the garbage collector is never invoked, and thread A never becomes enabled. Thus, the desired liveness property does not hold. However, suppose that a polling point is inserted in the loop: thread B is not allowed to proceed past this polling point. Then, in every scenario, a garbage collection step eventually takes place, at which time both thread A and thread B become unblocked.

How can one tell whether a program has enough polling points? Or how can one tell where polling points must be inserted so that the program has enough polling points? We propose a simple approach, which is to insert a polling point in front of every function call.<fnref n="11" /> This ensures that every thread must reach a polling point in a bounded number of steps. Up to an administrative side condition,<fnref n="12" /> we prove that this polling point insertion strategy preserves safety and ensures liveness. We refer to this polling point insertion strategy as addpp. Thus, if t is a term, then addpp(t) is the term obtained by inserting a polling point in front of every function call in the term t.

Figure 28 introduces several auxiliary predicates that appear in the statement of the liveness theorem. The proposition AfterAtMost (—> n P c) means that, out of the configuration c, every execution path via the reduction relation —> reaches, in at most n steps, a configuration that satisfies P. This proposition is inductively defined by the rules HOLDSNOW and HOLDSAFTER. HOLDSAFTER guarantees not only that the predicate continues to hold after every possible step, but also that there exists such a step. The proposition Eventually (—> P c), defined by the rule EVENTUALLY, means that in a bounded number of steps, out of the configuration c, every execution path reaches a configuration that satisfies P. It is defined via an existential quantification over n.<fnref n="13" />

The following theorem combines a safety guarantee and a liveness guarantee. It states that if the program t has been verified using IrisFit, under the exact same conditions as in Theorem 8.1, then the program addpp(t), in which enough polling points have been inserted, is safe and live.

**THEOREM 8.2 (COMBINED SAFETY AND LIVENESS AFTER POLLING POINT INSERTION).** Let t be a term in administrative normal form. Assume that the following triple holds:

$$ \forall \pi. \{\diamond S * \text{ outside } \pi\} \pi : t \{\lambda.. \text{ outside } \pi\} $$

<footnote n="10">¹⁰By Lemma 4.1, the property always, eventually, every allocation fits implies that always, eventually, all threads are enabled at the same time; which, in turn, implies that always, every thread is eventually enabled.</footnote>

<footnote n="11">¹¹LambdaFit does not have loops: instead, loops must be simulated via tail-recursive functions. Thus, inserting a polling point in front of every function call effectively implies inserting a polling point inside every loop as well. Incidentally, because function calls are forbidden inside protected sections, a polling point is never inserted into a protected section, satisfying our restriction that polling points in protected sections are forbidden. Our polling point insertion strategy is loosely inspired by the (undocumented) polling point insertion strategy of the OCaml compiler. The OCaml compiler inserts a polling point at the beginning of every function (except possibly small leaf functions), inside every loop, and views memory allocation instructions as polling points.</footnote>

<footnote n="12">¹²Prior to inserting polling points, we require the program to be in administrative normal form (ANF). That is, in every function call, we require the function itself and the actual arguments to be variables or values, as opposed to arbitrary expressions. This guarantees that the polling point that is inserted in front of the function call is executed after the actual arguments have been computed and just before the function is invoked.</footnote>

<footnote n="13">¹³We propose a strong definition of Eventually, whose quantifier prefix is of the form $\exists\forall$: "there exists n such that every execution path reaches in at most n steps a point where P is satisfied." A weaker definition would involve a quantifier prefix of the form $\forall\exists$: "every execution path eventually reaches a point where P is satisfied." This alternative definition is strictly weaker, because an infinitely branching tree where each branch is finite does not necessarily have finite depth [Bertot and Castéran 2004]. Our reduction relations have infinite non-determinism because memory allocation picks an arbitrary fresh address.</footnote>
$$ \frac{\text{EveryAllocFits}_S c}{\text{EveryAllocFitsPair}(S, c)} \qquad \frac{\text{Safe}_S c}{\text{SafePair}(S, c)} \qquad \frac{S \le S'}{\text{LimitIsAtMost } S'(S, c)} $$

<caption>Fig. 29. Predicates used in the statements of soundness for the growing semantics</caption>

Let $t'$ stand for the term `addpp(t)`. Then, the following propositions hold:

(1) Always ($\xrightarrow{\text{defaults}_S}$) Safe$_S$ (`init(t')`)

(2) Always ($\xrightarrow{\text{defaults}_S}$) (Eventually ($\xrightarrow{\text{defaults}_S}$) EveryAllocFits$_S$) (`init(t')`).

This statement reflects how we envision the practical use of IrisFit. We expect the user to verify a program $t$ in which polling points have not yet been inserted. Thus, the user need not know where polling points will be placed. The uninstrumented verified program $t$ enjoys safety but not necessarily liveness. Nevertheless, the theorem guarantees that, once enough polling points have been inserted, the program enjoys both safety and liveness.

Although Theorem 8.2 makes use of polling points and fixes a specific polling point insertion strategy to ensure liveness, namely `addpp`, we do support other approaches. Our mechanization [Moine 2025] includes a more general liveness theorem that splits the burden into (1) proving that always, at least one thread or the GC can take a step, and (2) proving that always, eventually, the program crashes or every allocation fits. Regarding `addpp`, under the assumption that the original program $t$ has been verified, we prove that both properties hold for the transformed program `addpp(t)`. The more general liveness theorem and the proof that it implies Theorem 8.2 are presented in the first author's dissertation [Moine 2024, §7.5.2].

## 8.3 Safety and Liveness for the Growing Semantics

For the growing semantics, we establish the following theorem, whose general structure is the same as that of Theorem 8.2. It uses several auxiliary predicates whose definitions appear in Figure 29.

**THEOREM 8.3 (COMBINED SAFETY AND LIVENESS AFTER POLLING POINT INSERTION).** Let $t$ be a term in administrative normal form. Assume that the following triple holds:

$$ \forall \pi. \{\diamond S * \text{ outside } \pi\} \pi : t \{\lambda\dots. \text{ outside } \pi\} $$

Let $t'$ stand for the term `addpp(t)`. Let $\rho$ stand for the initial state (0, `init(t')`), where the heap limit is 0, the heap is empty, and the program $t'$ is ready to run. Then, the following propositions hold:

(1) Always ($\xrightarrow{\text{growing}}$) SafePair $\rho$

(2) Always ($\xrightarrow{\text{growing}}$) (Eventually ($\xrightarrow{\text{growing}}$) EveryAllocFitsPair) $\rho$

(3) Always ($\xrightarrow{\text{growing}}$) (`LimitIsAtMost(grow(S))`) $\rho$.

This theorem states that if the program $t$ has been verified under the precondition $\diamond S$ then the program `addpp(t)`, in which polling points have been inserted, is safe (no thread can crash—item 1), is live (always, eventually, all threads are enabled—item 2), and never needs more than `grow(S)` words of memory (item 3). Indeed, item 3 is a bounded space consumption property: it states that, always, the current heap limit is at most `grow(S)`. By Lemma 4.5, this implies that the size of the heap, too, is at most `grow(S)`.

In summary, even though the current heap limit is automatically increased when the runtime system finds that the current limit is too low, if one has (statically) verified (using IrisFit) that the program needs at most $S$ words of memory, then (at runtime) the heap size is bounded by `grow(S)`. If one sets for example `grow(S) = max(2S, 1)`, as suggested earlier (§4.2.10), then one finds that the heap size is $O(S)$.
<figure><img src="image_22.png" /><figcaption>Fig. 30. Predicates used in the statement of the Core Soundness theorem</figcaption></figure>

Our motivation for proposing the growing semantics is that it does not require a suitable value of the limit to be known before execution begins. Indeed, imagine that the program *t* has not been fully verified. Then, one does not know what value *S* is large enough to guarantee that the triple $\forall \pi. \{\diamond S * \text{ outside } \pi\} \pi: t \{\lambda\_ \text{ outside } \pi\}$ holds. Nevertheless, under the optimistic assumption that such a value *S* exists, one can be assured that running the program under the growing semantics will not require more than *grow(S)* words of memory.

## 8.4 Core Soundness

A provocative yet fundamental remark is that IrisFit has nothing to do with garbage collection. Indeed, its deallocation rule is purely logical. More generally, its reasoning rules are independent of *when* garbage collection takes place, or *whether* it takes place at all. In reality, IrisFit is concerned with the *live heap size* of a program, that is, the sum of the sizes of the reachable blocks.

Our earlier results, namely Theorems 8.1, 8.2, and 8.3, follow from a *core soundness* result, which is expressed with respect to the *oblivious semantics*, a semantics in which no garbage collection takes place and no instructions are blocking (§2.1, §2.3, §4.2.7).

In this setting, we must redefine what it means for a thread to be *not stuck*. The proposition *NotStuckOblivious c π*, defined in Figure 30, serves this purpose. A thread is not stuck if either it has reached a value outside a protected section or it can make a step.

Let us write *livesize(R, σ)* for the total size of the fragment of the store *σ* that is reachable from the set of roots *R*. Let us write *livesize(c)* for the live heap size of the configuration *c*. It is defined by $livesize((\theta, \sigma)) = livesize(locs(\theta), \sigma)$.

Our core soundness theorem states that always (with respect to the oblivious semantics), the following two properties hold. First, no thread is stuck. Furthermore, if every thread is currently outside a protected section, then the live heap size is at most *S*, where *S* is the number of space credits that was granted when the program was statically verified.

**THEOREM 8.4 (CORE SOUNDNESS).** Assume that the following triple holds:

$$ \forall \pi. \{\diamond S * \text{ outside } \pi\} \pi: t \{\lambda\_ \text{ outside } \pi\} $$

Then, for every configuration *c* such that $init(t) \xrightarrow{\text{oblivious}}^* c$,

(1) for every identifier $\pi$ of a thread in *c*, the property *NotStuckOblivious c π* holds;

(2) *AllOutside c* implies *livesize(c)* ≤ *S*.

This statement may seem surprisingly weak, as it offers no guarantee about *livesize(c)* at a time where *AllOutside c* does not hold, that is, at a time where at least one thread is inside a protected section. Moreover, this statement offers just a safety guarantee; it offers no liveness guarantee. Nevertheless, this core soundness theorem is sufficiently strong to derive Theorems 8.1, 8.2, and 8.3, which express the purpose of our logic in a different manner.

Our internal definition of IrisFit triples [Moine 2025] is relative to the oblivious semantics. The proof of Theorem 8.4, as well as the proofs of our reasoning rules, involve the oblivious semantics only. Thus, in many of our proofs, there is no need for us to reason about garbage collection or about the distinction between enabled and disabled reduction steps.
# 9 Closures

As explained earlier (§2.7), LambdaFit does not have primitive closures. Instead, we define closure construction $\mu_{clo}f. \lambda\vec{x}. t$ and closure invocation $(\ell \vec{u})_{clo}$ as macros, which expand to sequences of primitive LambdaFit instructions. These macros implement flat closures [Appel 1992, Chapter 10]. That is, a closure is represented as a record whose fields store a code pointer (at offset 0) and a series of values (at offset 1 and beyond). The implementation of these macros (§9.2) is the same as in our earlier paper [Moine et al. 2023]. Our reasoning rules for closure construction, invocation, and deallocation are improved versions of the rules presented in our earlier paper [Moine et al. 2023]. In particular, they involve pending substitutions (§9.3). The main improvement is that the assertions that describe closures are now persistent. From an end user's point of view, this makes closures much easier to work with. Internally, this is made possible by using liveness-based cancellable invariants (§5.9).

Our reasoning rules for closures are abstract and do not reveal how closures are implemented. They reveal only how much space a closure occupies and which pointers it keeps live. A user can apply these rules without knowing how closures are internally represented.

Our construction of the reasoning rules for closures is in two layers. First, we introduce a low-level assertion *Closure* *E* *f* *x̃* *t* *ℓ*, which asserts that, at location *ℓ* in the heap, one finds a closure that behaves like the function *μf*.λx̃. *t* under the environment *E*. Crucially, in this assertion, the term *μf*.λx̃. *t* can have free variables, whose values are given by *E*. This assertion does not reveal how a closure is represented in memory, but does reveal its code. We give an overview of this low-level API (§9.4), then describe some details of its implementation (§9.5). Second, we define a high-level assertion *Spec* *n* *E* *P* *ℓ*, which describes the behavior of a closure in a more abstract way. It asserts that, at location *ℓ*, one finds a closure that corresponds to a *n*-ary function, whose behavior is described by the predicate *P*, and whose environment is *E*. The exact type and meaning of *P* are explained later on; roughly speaking, it is a Hoare triple. Although the environment *E* does not participate in the description of the behavior of the closure, it remains needed in order to reason about the pointers that it contains and about the size of the closure block. We give an overview of this high-level API (§9.6), then describe its implementation (§9.7). Only the high-level layer is exposed to the end user; the low-level layer remains internal.

## 9.1 Environments

We write $fvclo(f, \vec{x}, t)$ for a list of the free variables of the function $\mu f. \lambda \vec{x}. t$, that is, for a list of the variables in the set $fv(t) \setminus \{f, \vec{x}\}$. The order in which the variables occur in this list does not matter, but is fixed: this is reflected in the fact that $fvclo$ is a function of $f, \vec{x}$, and $t$.

An environment *E* is a list of pairs (*v*, *q*) of a value *v* and a nonzero fraction *q*. This fraction is used in a pointed-by-heap assertion, as follows: we write $E \leftarrow L$ for the conjunction $*(v, q) \in E \quad \vec{v} \leftarrow q L$. The assertion $E \leftarrow L$ can be understood as a collective fractional pointed-by-heap assertion that covers every memory location that occurs in the environment *E*.

The length and order of the list *E* are intended to match the length and order of the list $fvclo(f, \vec{x}, t)$. An environment *E* is not a runtime object: it is a mathematical object that we use as a parameter of the predicates *Closure* and *Spec*.

## 9.2 Closure Implementation

The definitions of the closure macros $\mu_{clo}f. \lambda\vec{x}. t$ and of $(\ell \vec{v})_{clo}$ appear in Figure 31. Both macros generate LambdaFit syntax: that is, the result of their expansion is a LambdaFit expression.

The code produced by the macro $\mu_{clo}f. \lambda\vec{x}. t$ allocates a block of size *n* + 1, stores a code pointer in the first field, stores the values currently bound to the variables $y_0, \dots, y_{n-1}$ in the remaining
**Closure construction:**

$\mu_{clo}f \cdot \lambda\vec{x} \cdot t \triangleq$

let $f = \text{alloc}(n+1)$ in
$f[0] \leftarrow \text{codeclo}(f, \vec{x}, t)$;
$f[i+1] \leftarrow y_i$; \# for each $i$ in $[0, n)$
$f$

**Closure invocation:**

$(v \vec{w})_{clo} \triangleq$
$(v[0] (v \cdot \vec{w}))_{ptr}$

**Closure code pointer:**

`codeclo(f, x̂, t) ≜`
`μptr_. λ(f :: x̂).`
`let yᵢ = f[i + 1] in # for each i in [0, n)`
`t`

**Side condition:**

`fvclo(f, x̂, t) = [y₀; ... ; yₙ₋₁]`

<caption>Fig. 31. Closures: macros for closure construction and invocation</caption>

fields, and returns the address of this block. The variables $y_0, \dots, y_{n-1}$ are the free variables of the function $\mu f \cdot \lambda\vec{x} \cdot t$, that is, $fvclo(f, \vec{x}, t)$.

The code pointer is produced by the auxiliary macro `codeclo(f, x̂, t)`. It is a closed function whose parameters are `f` (the closure itself) followed with `x̂`. This function loads the values stored in the closure and binds them to the variables $y_0, \dots, y_{n-1}$ before executing the body `t`.

The code produced by the closure invocation macro $(v \vec{v})_{clo}$ first fetches the code pointer that is stored in the first field of the closure, then invokes this code pointer, passing it the closure $v$ itself as well as the actual arguments $\vec{v}$.

## 9.3 Pending Substitutions

Our specifications of closure construction (§9.4, §9.6) involve *pending substitutions*. A pending substitution, written $[\vec{v}/\vec{y}]$ ($\mu_{clo}f \cdot \lambda\vec{x} \cdot t$), is the application of the substitution $[\vec{v}/\vec{y}]$ to the closure construction macro $\mu_{clo}f \cdot \lambda\vec{x} \cdot t$. In this substitution, we may assume that the variables $\vec{y}$ are the free variables of the function $\mu f \cdot \lambda\vec{x} \cdot t$. Any other variables can be removed from the domain of the substitution, as they do not impact the closure. The reason why we must be prepared to reason about a pending substitution is that the premise of `LETVAL` gives rise to substitutions which (after being propagated down) become blocked in front of the *opaque* macro $\mu_{clo}f \cdot \lambda\vec{x} \cdot t$. The values $\vec{v}$ that appear in this substitution are the values “captured” by the closure, that is, the values that are stored in the closure when it is constructed.

To illustrate these rules, let us take the example of a generator of integers:

$$ \text{let } r = \text{alloc } 1 \text{ in } r[0] \leftarrow 0; \ (\mu_{clo-} \ \lambda_{-} \ \text{let } x = r[0] \ \text{in } r[0] \leftarrow (x+1); x) $$

This code allocates a reference `r`, initializes it to 0, then allocates a closure that loads the content of `r`, names it `x`, increments `r`, and returns `x`. This closure captures the free variable `r`.

Now, let us briefly describe which reasoning rules must be applied in order to verify this code, and how the code that appears in the goal evolves as the proof progresses. After applying `BIND` and `ALLOC` to reason about the memory allocation instruction, the term looks as follows, where we have named `ℓ` the memory location produced by the instruction `alloc 1`:

$$ \text{let } r = \ell \text{ in } r[0] \leftarrow 0; \ (\mu_{clo-} \ \lambda_{-} \ \text{let } x = r[0] \ \text{in } r[0] \leftarrow (x+1); x) $$

Applying `LETVAL` gives rise to the substitution $[\ell/r]$, which is applied to the right-hand side of the let binding. Thus, after applying `BIND` and `STORE` to reason about the store instruction, the term that appears in the goal is:

$$ [\ell/r](\mu_{clo-} \ \lambda_{-} \ \text{let } x = r[0] \ \text{in } r[0] \leftarrow (x+1); x) $$
<figure><img src="image_23.png" /><figcaption>Fig. 32. Closures: low-level API</figcaption></figure>

As explained above, the macro $\mu_{clo}f \cdot \lambda\vec{x} \cdot t$ is opaque, so a substitution cannot be pushed into it. This explains why our reasoning rules for closure construction must allow reasoning about a term of the form $[\vec{v}/\vec{y}](\mu_{clo}f \cdot \lambda\vec{x} \cdot t)$.

## 9.4 Low-Level Closure API

Our low-level reasoning rules for closures, shown in Figure 32, involve the predicate *Closure*, which describes the layout of a closure in memory. Its definition is given in the next section (§9.5).

The rule `MKCLO` specifies a closure construction operation with a pending substitution. In the second premise of `MKCLO`, an environment `E` is built by pairing up the values $\vec{v}$ with nonzero fractions $\vec{q}$. Then, according to the precondition in `MKCLO`, closure construction consumes $E \leftrightarrow \emptyset$. In other words, for each memory location that occurs in `E`, it consumes a fractional pointed-by-heap assertion. This records the fact that there exists a pointer from the closure to each such memory location.

According to the precondition in `MKCLO`, closure construction consumes $size(1 + |E|)$ space credits, reflecting the space needed to store a code pointer and the values $\vec{v}$ in a flat closure.

Because closure construction involves an allocation, `MKCLO` requires the thread $\pi$ to be outside a protected section.

According to the postcondition in `MKCLO`, closure construction produces a memory location $\ell$. Pointed-by-heap and pointed-by-thread assertions for this memory location are produced, indicating that this memory location is fresh. Furthermore, the assertion *Closure E f x̄ t ℓ*, which guarantees that there is a well-formed closure at address $\ell$, is also produced. In this paper, in contrast with our earlier work [Moine et al. 2023], this assertion is *persistent* [Jung et al. 2018b, §2.3]. This means that the knowledge that there is a closure at address $\ell$ can be shared without any restriction. The pointed-by-heap and pointed-by-thread assertions $\ell \Leftarrow \{\pi\} * \ell \Leftarrow \emptyset$ are *not persistent*. Indeed, these assertions allow deallocating the closure, and our program logic ensures that every object is deallocated at most once.

The rule `CALLCLO` closely resembles the rule `CALLPTR` for primitive function calls (Figure 21). One difference is that `CALLCLO` requires the assertion *Closure E f x̄ t ℓ*, which describes the closure. Another difference is that, whereas a primitive function $\mu_{ptr}f \cdot \lambda\vec{x} \cdot t$ must be closed, a general function can have a nonempty list of free variables $\vec{y}$, an alias for `fvclo(f, x̄, t)`. In the last premise of `CALLCLO`, which requires reasoning about the function's body, the variables $\vec{y}$ are replaced with the values $\vec{v}$ captured at closure construction time, which are recorded in the environment `E`.
$$ \begin{align*} \text{Closure } E f \vec{x} t \ell &\triangleq \quad \begin{array}{@{}l@{}} \lceil f \notin \vec{x} \land |E| = |fvclo(f, \vec{x}, t)| \rceil * \\ \ell \mapsto \square (codeclo(f, \vec{x}, t) :: \text{map } \text{fst } E) * \end{array} \\ &\boxed{\quad \dagger \ell \lor E \leftarrow \{+\ell\}} \end{align*} $$

<caption>Fig. 33. Definition of the predicate Closure</caption>

The precondition of `CALLCLO` requires a pointed-by-thread assertion `M ⇐ {π}`, where the domain of the map `M` includes all of the locations that appear in $\vec{v}$, that is, all of the locations that appear in the closure's environment. This assertion is not consumed: it appears again in the precondition of the triple that forms the last premise of `CALLCLO`. In other words, it is transmitted from the caller to the callee. The presence of this assertion is imposed to us by the fact that, when the closure is invoked, these values are read from memory: the load instructions that appear in the definition of `codeclo(f, \vec{x}, t)` in Figure 31 require pointed-by-thread assertions for the values that are read. If desired, the pointed-by-thread assertion `M ⇐ {π}` can be transmitted back from the callee to the caller via a suitable instantiation of the postcondition $\Psi$. Alternatively, it may be consumed by the callee to justify a logical deallocation operation.

Together, the rules `MKCLO` and `CALLCLO` express the correctness of our closure construction and invocation macros. They guarantee that a closure at address `l` constructed by $[\vec{v}/\vec{y}] \mu_{clo} f . \lambda \vec{x} . t$, when invoked with actual arguments $\vec{w}$, behaves like the term $[\vec{v}/\vec{y}][l/f][\vec{w}/\vec{x}]t$. This is the operational behavior that is expected of a closure.

`CLOFREE` logically deallocates a closure. It resembles `FREEONE`, but, instead of a "`sizeof`" assertion, requires the abstract assertion `Closure E f \vec{x} t \ell`. Like `FREEONE`, it produces space credits and a deal-location witness for the closure. Furthermore, `CLOFREE` lets the user recover the pointed-by-heap assertion `E ← 0`, thereby undoing the effect of `MKCLO`.

## 9.5 Low-Level Closure API: Implementation Details

Figure 33 presents the internal definition of the assertion `Closure E f \vec{x} t \ell`. It records two pure facts: the name `f` is disjoint from the parameters $\vec{x}$ and the length of the environment `E` matches the number of free variables of the closure.

Then, a points-to assertion states that the location `l` points to a block of size $1 + |E|$, whose first field contains the code of the closure, `codeclo(f, \vec{x}, t)`, and whose remaining fields contain the values recorded in the environment `E`. Because this points-to assertion carries a discarded fraction $\square$ [Vindum and Birkedal 2021], it is a persistent points-to assertion. This reflects the fact that the closure is immutable.

The last component in this definition is a liveness-based cancellable invariant (§5.10): a persistent assertion that we can tear down and regain full ownership when we deallocate `l`.

Because every assertion involved in its definition is persistent, the assertion `Closure E f \vec{x} t \ell` is itself persistent.

The liveness-based cancellable invariant contains the pointed-by-heap assertion `E ← {+l}`, which means that every memory location in `E` is pointed to by the closure. In the proof of the reasoning rule `CLOFREE`, we tear down the liveness-based cancellable invariant, and gain back the assertion `E ← {+l}`. Because `l` is now dead, we use the `CLEANPBHEAP` rule to change `E ← {+l}` into `E ← 0`. This explains how, in the proof of `CLOFREE`, we are able to produce the assertion `E ← 0`.
$$
\begin{array}{r@{\quad}l@{\qquad}l}
\text{MKSPEC} & \vec{y} = fvclo(f, \vec{x}, t) & E = zip \, \vec{v} \, \vec{q} \quad |\vec{v}| = |\vec{y}| \quad f \notin \vec{x} \quad n = |\vec{x}| \\
& \forall \vec{w}. \quad \Box ( \mathit{Spec} \ n \mathit{E} \ P \ \ell \ \mathit{-} \ P \ \ell \ \vec{w} \ (|\vec{v}/\vec{y}|[\ell/f][\vec{w}/\vec{x}]t) ) \\
& \left\{ \begin{array}{@{}l@{}}
    \diamond (\mathit{size}(1 + |E|)) * \ \mathit{outside} \ \pi \\
    E \leftrightarrow \emptyset
  \end{array} \right\} & \pi: [\vec{v}/\vec{y}] (\mu_{clo} f. \lambda \vec{x}. t) \quad \left\{ \begin{array}{@{}l@{}}
    \lambda \ell. \ \mathit{outside} \ \pi \ * \ \mathit{Spec} \ n \mathit{E} \ P \ \ell \\
    \ell \Leftarrow \{\pi\} \ * \ \ell \leftrightarrow \emptyset
  \end{array} \right\}
\end{array}
$$

$$
\begin{array}{r@{\quad}l@{\qquad}l}
\text{CALLSPEC} & E = zip \, \vec{v} \, \vec{q} & \mathrm{dom}(M) = \mathrm{locs}(\vec{v}) \qquad |\vec{w}| = n \\
& (\forall u. \, P \, \ell \, \vec{w} \, u \ \mathit{-} \ \{\mathit{outside} \, \pi \, * \ M \ \Leftarrow \ \{\pi\} \, * \ \Phi\} \ \pi: u \ \{\Psi\}) \\
& \{\mathit{Spec} \ n \mathit{E} \ P \ \ell \, * \ \mathit{outside} \, \pi \, * \ M \ \Leftarrow \ \{\pi\} \, * \ \Phi\} \ \pi: (\ell \, \vec{w})_{\mathrm{clo}} \ \{\Psi\}
\end{array}
$$

$$
\begin{array}{l @{\quad} l @{\quad} l @{\quad} l @{\quad} l}
\Box (\forall \vec{w} \ t. \ P_1 \ \ell \ \vec{w} \ t \ \mathit{-} \ P_2 \ \ell \ \vec{w} \ t) & \ast & \mathit{Spec} \ n \mathit{E} P_1 \ \ell & \mathit{-} & \mathit{Spec} \ n \mathit{E} P_2 \ \ell & \mathit{SPECWEAK} \\
\mathit{Spec} \ n \mathit{E} P \ \ell \ \ast \ \ell \leftrightarrow \emptyset & \ast & \ell \leftrightarrow \emptyset & \Rightarrow & \diamond (\mathit{size}(1 + |E|)) & \ast \ \dagger \ \ell \ \ast \ E \leftrightarrow \emptyset & \mathit{SPECFREE} \\
\mathit{Spec} \ n \mathit{E} P \ \ell & \mathit{is persistent} & & & & \mathit{SPECPERSIST}
\end{array}
$$

<caption>Fig. 34. Closures: high-level API</caption>

9.6 High-Level Closure API

The user of a program logic is ultimately interested in the specification of a function, not in the details of its implementation. Yet, the predicate *Closure E f x̄ t ℓ* reveals the code of the closure. As a result, a user naturally wishes to hide this information via an existential quantification over this code. This pattern is common enough and technical enough that we offer a higher-level API where this existential quantification is built in. To this end, we introduce the assertion *Spec n E P ℓ* (defined further on in §9.7), where *n* is the arity of the function, *E* is the environment of the closure, *P* describes the behavior of the closure, and *ℓ* is the location of the closure in memory.

Like the *Closure* predicate (§9.4, §9.5), and unlike the *Spec* predicate presented in our previous paper [Moine et al. 2023], the predicate *Spec* is persistent. This enables a better separation of concerns between the persistent assertion *Spec n E P ℓ*, which views the closure as an eternal service provider, and the affine assertion *ℓ ⇔ {π} * ℓ ⇔ 0*, which views it as an object in memory, allowing it to participate in the object graph and (eventually) to be logically deallocated.

Figure 34 presents the reasoning rules associated with the *Spec* predicate. Let us first examine the rule *CALLSPEC*. In many ways, this rule is the same as the low-level rule *CALLCLO*. The main difference is that, to prove that the call $(\ell \, \vec{w})_{clo}$ admits the postcondition $\Psi$, the user must prove the entailment $\forall u. P \, \ell \, \vec{w} \, u \ \mathit{-} \ \{\mathit{outside} \, \pi * M \ \Leftarrow \ \{\pi\} * \Phi\} \ \pi: u \ \{\Psi\}$. Intuitively, *u* denotes the instantiated function body that was visible in *CALLCLO*; however, this function body is now abstracted away by the universal quantification over *u*. The predicate *P* represents the specification of the function,

$$
\begin{align*}
\mathit{Spec} \ n \mathit{E} \ P \ \ell &\triangleq \\
\exists f \, \vec{x} \ t \ P'. & \\
\quad |\vec{x}| &= n \neg \quad * \ \mathit{Closure} \ E \ f \, \vec{x} \ t \quad * \\
\quad \mathit{let} \, \vec{v} &= \mathit{map} \ \mathit{fst} \ E \ \mathit{in} \\
\quad \mathit{let} \, \vec{y} &= \mathit{fvclo}(f, \vec{x}, t) \ \mathit{in} \\
\quad \mathit{let} \ \mathit{body} \, \vec{w} &= [\vec{v}/\vec{y}][\ell/f][\vec{w}/\vec{x}]t \ \mathit{in} \\
\quad \triangleright \Box (\forall \vec{w}. \ \mathit{Spec} \ n \mathit{E} \ P' \ \ell \ \mathit{-} \ P' \ \ell \ \vec{w} \ (\mathit{body} \, \vec{w})) \quad * \\
\quad \triangleright \Box (\forall \vec{w} \ u. \ P' \ \ell \ \vec{w} \ u \ \mathit{-} \ P \ \ell \ \vec{w} \ u)
\end{align*}
$$

<caption>Fig. 35. Definition of the predicate *Spec*</caption>
and is typically instantiated with a triple. For example, in the specification of a closure of arity 1 whose effect is to increment a reference *r* that it receives as an argument, *P* takes the form: $\lambda\ell \vec{w} u. \forall r n. \Gamma \vec{w} = [r] \neg \ast \{r \mapsto [n]\} \pi: u \{\lambda(). r \mapsto [n+1]\}$. In short, the user must prove that the specification needed by the caller follows from the specification *P*.

Let us now consider the rule **MKSPEC**. It is again quite similar to the low-level rule **MKCLO**. The premise on the second line ensures that *P* is a valid description of the behavior of the function body, whose concrete form $[\vec{v}/\vec{y}][\vec{w}/\vec{x}]t$ is visible. In comparison with the low-level API (§9.4), the work of reasoning about the function body is shifted from the closure invocation site to the closure construction site. Moreover, while establishing $P \ell \vec{w} ([\vec{v}/\vec{y}][\ell/f][\vec{w}/\vec{x}]t)$, the user is allowed to assume *Spec n E P*<sub>1</sub> *ℓ*: this allows verifying recursive calls.

The rule **SPECWEAK** is a consequence rule: it allows weakening the assertion *Spec n E P*<sub>1</sub> *ℓ* into *Spec n E P*<sub>2</sub> *ℓ*, under the hypothesis that *P*<sub>1</sub> is stronger than *P*<sub>2</sub>. This hypothesis is expressed as □ (*∀* *w* *t*. *P*<sub>1</sub> *ℓ* *w* *t* *∗* *P*<sub>2</sub> *ℓ* *w* *t*), where □ is the *persistence modality* [Jung et al. 2018b, §5.3]. This modality requires the proof of the implication (*∀* *w* *t*. *P*<sub>1</sub> *ℓ* *w* *t* *∗* *P*<sub>2</sub> *ℓ* *w* *t*) to depend only on persistent resources.

The rule **SPECFREE** is similar to the rule **CLOFREE**.

## 9.7 High-Level Closure API: Implementation Details

Figure 35 presents the definition of the assertion *Spec n E P*<sub>l</sub>. This is a guarded recursive definition: *Spec* appears (under a “later” modality) in its own definition. The definition is existentially quantified over the code of the closure, represented by *f*, $\vec{x}$, and *t*. It is also existentially quantified over a predicate *P'* that is required to be stronger than *P*. This lets us establish **SPECWEAK**.

## 10 Triples with Souvenir

In this section, we propose triples with souvenir [Moine et al. 2023], a syntactic sugar that allows for simpler reasoning rules—in particular, a simpler **BIND** rule—while reasoning about code that lies outside a protected section. We first present the reasoning rules of triples with souvenir (§10.1), then cover how they are defined (§10.2).

### 10.1 Those Who Cannot Remember the Past Are Condemned to Repeat It

IrisFit, as presented until this point, can be cumbersome to use, for two unrelated reasons.

One reason is that the user must give up pointed-by-thread assertions at each application of **BIND**, even in the common case where such a fraction has been framed already at a previous application of **BIND**, which encloses the current application. This obligation to split off and give up pointed-by-thread assertions becomes especially heavy when a variable *x* denotes a location and has a long *live range*, that is, when this location remains a root throughout a long sequence of instructions. In such a situation, at each point in the sequence, the user is required to split off and give up a fractional pointed-by-thread assertion for *x*.<fnref n="14" />

A second reason is that, typically, the large majority of instructions are placed outside protected sections. Yet, the user must provide the assertion *outside* $\pi$ at each application of the *outside rules* **ALLOC**, **CALLPTR**, **FORK**, **POLL**, **MKSPEC**, and **CALLSPEC**. This is not difficult, but the presence of this assertion creates visual clutter in pre- and postconditions.

To alleviate both problems at once, we follow Moine et al. [2023] and introduce triples with souvenir. A triple with souvenir takes the form $[R]\{\Phi\} \pi: t\{\Psi\}$, where *R* is a set of locations for which the user has already given up a pointed-by-thread assertion. Recording this souvenir

<footnote n="14">¹⁴The problem is partly mitigated by the “no trim” mode × (§6.5). However, this mode is designed for very local use, and cannot be exploited if trimming is needed.</footnote>