<figure><img src="image_24.png" /><figcaption>Fig. 36. Key reasoning rules for triples with souvenir</figcaption></figure>

(or remembrance) relieves the user from the obligation of giving up another pointed-by-thread assertion at future applications of the `BIND` rule. Furthermore, a triple with souvenir implicitly carries an `outside π` assertion: this allows for more concise statements of the “outside rules”.

For each reasoning rule in Figure 21, we provide a new rule (not shown) that operates on triples with souvenir and that is polymorphic in `R`. This is done simply by inserting `[R]` in front every triple that appears in the rule. We do not provide new reasoning rules for protected sections, as triples with souvenir are applicable only outside protected sections.

The new reasoning rules that make use of souvenirs appear in Figure 36. `BINDWITHSOUVENIR` is what we aimed for: it is our motivation for introducing triples with souvenir. It closely resembles `BIND`, but does not require the user to give up pointed-by-thread assertions for the locations that are already part of the souvenir `R`. The first premise requires the domain of `M` (a map of locations to nonzero fractions) to cover all roots of the evaluation context `K`, except those that are already in the souvenir `R`. In other words, if a location already appears in `R` then there is no need to again split off and give up a pointed-by-thread assertion for this location. Furthermore, `BINDWITHSOUVENIR` augments the current souvenir by changing `R` to `R ∪ locs(K)` in its second premise. Thus, nested applications of this rule do not require repeatedly and redundantly giving up pointed-by-thread assertions. The rule `ADDSouvenir` extends the current souvenir with a location `ℓ`. This requires framing out (temporarily giving up) a pointed-by-thread assertion for `ℓ`. The rule `FORGETSouvenir` shrinks the current souvenir. The rule `EMPTYSouvenir` shows that a triple with an empty souvenir is equivalent to a triple without souvenir and with an “outside” assertion in its pre- and postcondition.

By exploiting triples with souvenir, each of the “outside rules” (`ALLOC`, `CALLPtr`, `FORK`, `POLL`, `MkSPEC` and `CALLSPEC`), can be given a more concise statement. For example, the reasoning rule `POLL` can be more concisely formulated as `POLLWITHSOUVENIR`:

<figure><img src="image_25.png" /><figcaption>Fig. 37. Definition of triples with souvenir</figcaption></figure>
## 10.2 Internals of Souvenirs

The definition of triples with souvenir appears in Figure 37. A triple with souvenir $[R] \{\Phi\} \pi: t \{\Psi\}$ is expressed as an ordinary triple where the assertions outside $\pi$ and $M \Leftarrow \{\pi\}$ are framed out. That is, these assertions appear in the pre- and postcondition, so they are required and preserved, but they are not made available to a user who views a triple with souvenir as an abstract assertion. The domain of the map $M$ is the set $R$: this ensures that, for every location in this set, a fractional pointed-by-thread assertion is indeed framed out.

A triple with souvenir describes a piece of code whose execution begins and ends outside a protected section: it cannot be used to describe a code fragment that lies inside a protected section. To establish a triple with souvenir about a whole protected section, the user must unfold the definition of triples with souvenir and drop down to the level of standard triples. Then, all of the reasoning rules for standard triples are applicable.

In our mechanization [Moine 2025], we use a more general triple that allows both “no trim” mode (§6.5) without a souvenir and normal mode with a souvenir. This general triple always frames out an “outside” assertion. In our case studies, this is the triple that we use most of the time.

## 11 Case Studies

We now showcase the expressiveness of IrisFit via a series of representative case studies. We first present logically atomic triples [da Rocha Pinto et al. 2014; Jung et al. 2015], a standard way of specifying operations on concurrent data structures. We begin our case studies with an encoding of the fetch-and-add operation in LambdaFit, which makes use of protected sections (§11.2). Then, we present an implementation of a concurrent counter object, implemented as a pair of closures that share an internal reference (§11.3). We continue with a library for async/finish parallelism, which exploits our implementation of fetch-and-add (§11.4). We conclude this section by presenting our version of Treiber’s stack (§11.5), which exploits protected sections, along the lines sketched earlier (§3). For each case study, we present the code, the specification, and some insights into the proof. For establishing concrete heap bounds, we pose in this section that a block of $n$ fields is represented by $n$ memory words, that is, we pose $size(n) = n$. Another practical choice such as $size(n) = n + 1$ would only affect the constant values that appear behind diamond symbols in specifications.

Our mechanization [Moine 2025] contains additional case studies that we do not cover here. They include sequential examples (a sequential algorithm written in continuation-passing style; a sequential singly-linked circular list; three distinct implementations of sequential stacks) and concurrent examples (a spin lock; Michael and Scott’s lock-free queue, with protected sections).

### 11.1 Atomic triples

Our specifications for fetch-and-add (§11.2) and for Treiber’s stack (§11.5) involve logically atomic triples, also known simply as atomic triples [da Rocha Pinto et al. 2014; Jung et al. 2015]. In our work, an atomic triple takes the form:

$$[R] \left\langle \frac{\Phi_{\text{private}}}{\forall \vec{x}. \Phi_{\text{public}}} \right\rangle \pi: t \left\langle \frac{\lambda v. \Phi'_{\text{private}}}{\Phi'_{\text{public}}} \right\rangle$$

The parameter $R$ between square brackets is a souvenir (§10). We construct our atomic triples on top of our triples with souvenir (§10) in the same way that atomic triples are usually constructed on top of ordinary triples. Intuitively, an atomic triple that carries a souvenir $[R]$ is an atomic triple whose private pre- and postconditions are extended with a pointed-by-thread assertion
<figure><img src="image_26.png" /></figure>

<figure><img src="image_27.png" /><figcaption>Fig. 38. Code and specification of fetch-and-add</figcaption></figure>

that covers $R$ (that is, a pointed-by-thread assertion $M \Leftarrow \{\pi\}$ where $R = \text{dom}(M)$) and with the assertion outside $\pi$.

The private precondition $\Phi_{\text{private}}$ and the private postcondition $\lambda v. \Phi'_{\text{private}}$ play the same role as the precondition and postcondition of a standard triple. The private precondition is given up by thread $\pi$ when the execution of the term $t$ begins; the private postcondition is gained by thread $\pi$ when the execution of the term $t$ ends. They are private in the sense that they are invisible to other threads.

The characteristic feature of atomic triples is the presence of a public precondition $\Phi_{\text{public}}$ and of a public postcondition $\Phi'_{\text{public}}$. An atomic triple guarantees that the public precondition $\Phi_{\text{public}}$ continuously holds until a certain point in time, the linearization point [Herlihy and Wing 1990], where it is atomically transformed into the public postcondition $\Phi'_{\text{public}}$ [Birkedal et al. 2021]. Technically, an atomic triple involves a quantification over a list of variables $\vec{x}$, whose scope is $\Phi_{\text{public}}$, $\Phi'_{\text{private}}$, and $\Phi'_{\text{public}}$. The existentially quantified public precondition $\exists \vec{x}$. $\Phi_{\text{public}}$ continuously holds until the linearization point is reached. There, a specific instantiation of the variables $\vec{x}$ becomes fixed. For this specific choice of $\vec{x}$, the public precondition is transformed into the public postcondition $\Phi'_{\text{public}}$, and the value $v$ that is eventually returned satisfies $\Phi'_{\text{private}}$.

## 11.2 Fetch-and-Add

The “fetch-and-add” (FAA) operation atomically increments the content of an integer reference, and returns the previous content of the reference. Although this operation is commonly provided in hardware, implementing it in LambdaFit is a fairly instructive exercise. Indeed, this code and its proof offer a typical example of the use of protected sections.

**Code.** In our setting, FAA takes three parameters: an address $l$, an offset $i$, and the desired increment $n$, an integer value. We encode FAA as a tail-recursive function whose body contains a CAS instruction enclosed in a protected section. The code is shown in Figure 38. The recursive function is named $f$; its parameters are $l$, $i$ and $n$. Initially, the content of the memory at address $l$ and offset $i$ is loaded into the variable $m$. Then, a protected section is entered, and a CAS instruction attempts to update the content of the memory from $m$ to $m+n$. In case of success, the protected section is exited and the value $m$ is returned. In case of failure, the protected section is also exited, and a recursive call is performed, so as to try again.

Thanks to the protected section, as soon as the CAS instruction succeeds, the memory location $l$ can be made a temporary root, as opposed to an ordinary root. Indeed, as soon as CAS succeeds, it is known that the first branch of the conditional construct will be taken, so the protected section will be exited via the first exit instruction, where $l$ is no longer a root.
Without a protected section, at the program point that follows CAS and precedes the separation of the two branches, *l* would still be considered a root (that is to say, an ordinary root), because it occurs inside the “else” branch, and according to the FVR (§2.2), every location that occurs in the code that lies ahead is a root.

*Specification.* Our specification of FAA appears in Figure 38. The private precondition consumes a pointed-by-thread assertion for the location *l*, carrying some fraction *p* and the current thread identifier π. The public precondition requires that *l* point to a block $\tilde{v}$ and that the value stored at offset *i* in this block be *m*. The public postcondition asserts that FAA atomically updates *m* into *m* + *n*. Crucially, it also produces an updated pointed-by-thread assertion for *l*, carrying the same fraction *p* and an empty set of thread identifiers. This means that as soon as the linearization point is reached, one can consider that *l* is not a root in thread π. This turns out to be crucial while reasoning about our async/finish library (§11.4). The private postcondition asserts that the result of FAA is *m*.

*Proof insights.* Here is how we use the reasoning rules of protected sections (Figure 22) while verifying that FAA obeys its specification. Upon entering the protected section, we use `ENTER` and transform the assertion *outside* π into the assertion *inside* π ∅. Then, we face the CAS instruction, a possible linearization point. We open the public precondition,<fnref n="15" /> and gain the points-to assertion for *l*. By case analysis on the value that is currently stored at address *l* and offset *i*, we consider the case where CAS succeeds and the case where it fails. Let us focus on the case where it succeeds. We use `CASSUCCESS`, which updates the points-to assertion, and effectively execute the linearization point. At this point, the atomic triple requires us to prove that the public postcondition holds. Using `ADDTEMPORARY`, we make *l* a temporary root: this changes the assertions *l* ⇐$_p$ {π} and *inside* π ∅ into *l* ⇐$_p$ ∅ and *inside* π {*l*}. By giving up the points-to and pointed-by-thread assertions, we fulfill the public postcondition. Then, we use `IFTRUE` and enter the first branch of the “if” statement. There, `TRIMINSIDE` lets us change the assertion *inside* π {*l*} to *inside* π ∅. This allows us to exit the protected section using `EXIT`. We finish the proof with `VAL`.

## 11.3 A Concurrent Counter Object

Our next example is a concurrent monotonic “counter” object, whose internal state is stored in a mutable reference, and whose access is mediated by a pair of closures: a closure *i* increments the counter; a closure *g* gets its current value. This is an example of a procedural abstraction [Reynolds 1975], also known as an *object*: indeed, “an object is a value exporting a procedural interface to data or behavior” [Cook 2009]. Crucially, a counter can be used concurrently by several threads.

*Code.* The top of Figure 39 presents the code that we verify. The function call (ref `[x]`)ptr allocates a mutable reference, that is, a block of size 1. The function call (pair `[x, y]`)ptr allocates a mutable pair, that is, a block of size 2. The function call (ignore `[x]`)ptr ignores its argument and returns the unit value. The function call (create `[]`)ptr returns a fresh “counter”, that is, a pair of two closures *i* and *g*. Both closures point to an internal reference *r*, which is initialized to the value 0. The closure *i* uses our fetch-and-add function (§11.2) and ignores its result.

*Specifications.* Figure 39 presents the specification of our concurrent counter. It is inspired by a specification that appears in lecture notes [Birkedal and Bizjak 2023]. It relies on an abstract assertion *counter* *i* *g* *p* *n* where *i* is the location of the “increment” closure, *g* is the location of the

<footnote n="15">¹⁵As noted earlier (§11.1), while establishing an atomic triple, until the linearization point is reached, one can assume that the public precondition continuously holds. Thus, to some extent, the public precondition is analogous to an Iris invariant: it can be accessed, or “opened”, during an atomic instruction.</footnote>
ref $\triangleq$ $\mu_{ptr-}$. $\lambda[x]$.
let $r$ = alloc 1 in
$r[0] \leftarrow x; r$
pair $\triangleq$ $\mu_{ptr-}$. $\lambda[x, y]$.
let $r$ = alloc 2 in
$r[0] \leftarrow x; r[1] \leftarrow y; r$
ignore $\triangleq$ $\mu_{ptr-}$. $\lambda[x]$. ()
create $\triangleq$ $\mu_{ptr-}$. $\lambda[\cdot]$.
let $r$ = (ref $[0]$)$_ptr$ in
let $i = \mu_{clo-}$. $\lambda_{-}$. (ignore [(faa $[r, 0, 1]$)$_ptr$])$_ptr$ in
let $g = \mu_{clo-}$. $\lambda_{-}$. $r[0]$ in
(pair $[i, g]$)$_ptr$

<figure><img src="image_28.png" /><figcaption>Fig. 39. Code and specification of a concurrent monotonic counter</figcaption></figure>

“get” closure, $p \in \{0; 1\}$ is a fraction that represents a *share* of the ownership of the counter, and $n$, a natural number, represents a *past contribution* to the current value of the counter. If $p$ is 1 then the contribution $n$ is in fact the current value of the counter.

The equivalence axiom in Figure 39 shows that “counter” assertions can be split and joined; both the fraction and the contribution are then split or joined by addition. This allows a counter to be used in a concurrent setting: the user can split the “counter” predicate into several parts and give a part to each participating thread. In the end, the user can gather all parts, draw conclusions about the final value of the counter, and logically deallocate the counter.

The specification of $(create \, \dots \, \mathrm{ptr})$ states that this call consumes 7 space credits (1 credit for the shared reference, 2 credits for each closure, and 2 credits for the pair). It returns a pair $\ell$ of two locations $i$ and $g$ such that *counter ig 1 0* holds. This assertion captures the full ownership of the counter, and specifies that its current value is 0.

Figure 39 also shows the specifications of calls to $i$ and $g$. Both calls require an assertion of the form *counter ig p n*. The postcondition of a call to the “increment” closure contains an updated assertion *counter ig p* ($n+1$). The postcondition of a call to the “get” closure contains an unmodified “counter” assertion. Furthermore, it guarantees that the natural number $m$ that is returned by this call is no less than the past contribution $n$ and, in the case where $p$ is 1, is equal to the past contribution.

Last, Figure 39 shows the reasoning rule for deallocating a counter. This rule requires full ownership of the counter as well as pointed-by-heap and pointed-by-thread assertions for the closures $i$ and $g$, with fraction 1 and empty sets—this witnesses that both closures are unreachable. In exchange, the rule produces 5 spaces credits. The 2 credits corresponding to the pair produced by create can be recovered independently.
<figure><img src="image_29.png" /><figcaption>Fig. 40. Code and specification of an async/finish library</figcaption></figure>

*Proof insights.* The proof that the counter obeys its specification uses ghost state in a standard way [Birkedal and Bizjak 2023, §8.7]. The internal definition of the abstract predicate "counter" involves an existential quantification over the shared location *r*: indeed, this location does not appear in the specification. The assertion *counter igp n* contains an empty pointed-by-thread assertion for the location *r* with fraction *p*. Moreover, the assertion *counter igp n* contains *Spec* assertions (§9.6) for the closures *i* and *g*. The environments that appear in these *Spec* assertions map *r* to the fraction 1/2, which means that each closure owns one half of the pointed-by-heap assertion for the location *r*.

The proof of the logical deallocation rule for a counter (that is, the last rule in Figure 39) is straightforward. We first deallocate the closures *i* and *g*, and recover 2 × 2 space credits as well as an empty pointed-by-heap assertion for the shared location *r*. Then, by exploiting the empty pointed-by-thread assertion for *r*, which is contained inside the *counter* assertion, we logically deallocate the location *r*, thereby recovering one more space credit. In total, 5 space credits are recovered, as expected.

## 11.4 An Async/Finish Library

The async/finish paradigm was introduced in X10 [Charles et al. 2005; Lee and Palsberg 2010] as a generalization of the spawn/sync mechanism of Cilk [Blumofe et al. 1996], which itself was a generalization of the fork/join paradigm. where exactly two child threads are spawned and awaited. The async/finish paradigm allows spawning an arbitrary number of tasks before waiting at a common join point. More precisely, "async" allows spawning new tasks, whereas "finish" performs synchronization: it blocks until all previously spawned tasks terminate. In this section, we encode these constructs in LambdaFit using a shared mutable reference that is updated via
a fetch-and-add operation (§11.2). We then provide specifications in IrisFit, and show that the space credits associated to the shared reference can be recovered as soon as “finish” returns.<fnref n="16" /> A strength of our specification is that it allows for *nested spawns*: a spawned task can itself spawn tasks.

**Code.** The code of our async/finish library is presented in the top part of Figure 40. The library uses a reference that we call the *session*. A session is a channel through which tasks communicate. It stores the number of currently running tasks.

The function `(create[])ptr` returns a fresh session, with zero running tasks.

The function `(async [l, f])ptr` expects a session `l` and a closure `f` as arguments. It first atomically increments the session, hence recording the existence of a new running task, then forks off a thread that invokes the closure `f` with no arguments. When this invocation terminates, it atomically decrements the session, thereby recording that this task is finished.

The function `(finish [l])ptr` consists of an active waiting loop. This loop ends when it observes that the session contains the value 0, which guarantees that all previously spawned tasks have terminated.

**Specifications.** The bottom part of Figure 40 presents the specification of our async/finish library.

According to `AFCREATE`, `(create[])ptr` consumes one space credit, which corresponds to the space occupied by the session, and returns a location `l` such that `AF l` holds. This persistent assertion guarantees that `l` is a session. The postcondition also provides pointed-by-thread and pointed-by-heap assertions for the location `l`. The pointed-by-heap assertion carries the fraction $1/2$; the other half is hidden from the user.

The specification of `(async [l, f])ptr` is stated as a triple featuring a souvenir on `l`. This means that, for the duration of this call, `l` is a root. The precondition requires `l` to be a session. A fractional pointed-by-thread assertion for the closure `f`, as well as an arbitrary assertion $\Phi$, are consumed and transmitted to the new task, which invokes the closure `f`. The premise of the rule `AFASYNC` requires the user to prove that, under an arbitrary thread identifier $\pi'$, this invocation is safe and satisfies some postcondition $\Psi$. The postcondition of `(async [l, f])ptr` provides a witness that this task was spawned, in the form of the assertion *spawned* $l \Psi$. This assertion is not persistent: it can be understood as a unique permission to collect $\Psi$ once the task is finished.

The specification of `f` in the premise of `AFASYNC` is again a triple with a souvenir of `l`. This formulation allows `f` to itself use `async`. Using an ordinary triple there would place a stronger requirement on `f` and would forbid the use of `async` inside `f`.

According to `AFFINISH`, `(finish [l])ptr` consumes the pointed-by-thread assertion that was produced by create. This forbids any further use of the session `l`: indeed, both `AFASYNC` and `AFFINISH` require a pointed-by-thread assertion for `l`.<fnref n="17" /> The postcondition contains the persistent assertion *finished* `l`, which witnesses that this session has been ended.

The ghost update `FINISHEDSPAWNED` states that if the witness *finished* `l` is at hand then the assertion *spawned* `l` $\Psi$ can be converted to $\Psi$. This reflects the idea that if the session has been ended, then all tasks must have terminated: so, a permission to collect $\Psi$ can indeed be converted to $\Psi$. The ghost update `FINISHEDFREE` states that if the session has ended then abandoning the pointed-by-heap assertion for `l` allows recovering the space credit associated with the session `l`.

**Proof insights.** The assertion `AF l` is internally defined as an Iris invariant, with a part consisting of a liveness-based cancellable invariant (§5.10). Among other things, this invariant imposes a protocol

<footnote n="16">¹⁶That is to say, as soon as every task reaches the linearization point of the fetch-and-add operation to signal that it is done. A task can still execute some code past the linearization point before actually terminating.</footnote>

<footnote n="17">¹⁷In the case of `AFASYNC`, this is implicit in the fact that the conclusion of the rule is a triple with a souvenir on `l`.</footnote>
<figure><img src="image_30.png" /><figcaption>Fig. 41. Specification of Treiber’s Stack</figcaption></figure>

on the pointed-by-thread assertion for the session $\ell$. Initially, the invariant contains a pointed-by-thread assertion carrying the fraction $\frac{1}{2}$ and an empty set; the other half is given to the user by **AFCREATE**. Each spawned task gets a fraction of this assertion: indeed, spawning a task involves “fork”, and our **FORK** rule requires updating a pointed-by-thread assertion so as to reflect the fact that $\ell$ is a root of the new thread. When a task signals that it is finished, it surrenders its fractional pointed-by-thread assertion, carrying an *empty* set of thread identifiers. Hence, once every task has terminated, the invariant again contains $\ell \Leftarrow \frac{1}{2} \emptyset$.

How and when exactly does a task signal that it is finished? This is done via a fetch-and-add (FAA) operation, which decrements the count of active tasks, and takes effect precisely at the linearization point of this FAA operation. Hence, as soon as this linearization point is reached, the invariant requires this task to surrender its fractional pointed-by-thread assertion. Fortunately, our specification of FAA (§11.2) allows this: the pointed-by-thread assertion $\ell \Leftarrow_p \emptyset$ appears in the public postcondition in FAA.

The absence of a “later” modality in front of $\Psi$ in **FINISHED** **SPAWNED** may seem surprising. As the assertion $\Psi$ has transited through an invariant, an Iris expert might expect it to be guarded by such a modality. The usual way to eliminate a “later” modality is through a physical step, yet this rule is a ghost update. Fortunately, IrisFit supports and takes advantage of *later credits* (§6.2). A later credit is a piece of ghost state that is produced by a physical step and that can later be used to eliminate a “later” modality. With each spawned task, we are able to internally associate one later credit, which we obtain from the function call (*async* [$\ell, f$])$_{ptr}$. By exploiting this later credit, we can eliminate the “later” modality in front of $\Psi$ before giving this assertion back to the user.

## 11.5 Treiber's Stack

**Code.** The code that we verify is the code of Figure 3, translated to LambdaFit syntax. A reference is a block of size 1 and a list cell is a block of size 2.

**Specifications.** Figure 41 presents our specification of Treiber’s stack. The stack is described in terms of the abstract predicate `stack ℓ vpqs`, where `ℓ` is the location of the stack and `vpqs` is its mathematical model. This model is a list of triples (`v`, `p`, `q`) of a value `v` and two positive fractions `p` and `q`. The list of the values `v` describes the content of the stack. For each value `v`, the fractions `p` and `q` describe what quantity of the pointed-by-thread and pointed-by-heap assertions for the value `v` have been acquired by the stack. Having the stack acquire a fractional pointed-by-heap
assertion for the value $v$ lets us record that this value is pointed to by a list cell without revealing or even mentioning the address of this cell. Having the stack acquire a fractional pointed-by-thread assertion for the value $v$ lets us express a plausible specification for “pop”. Indeed, “pop” needs to read the value $v$ from the heap: then, the `LOAD` rule requires (and updates) a fractional pointed-by-thread assertion for $v$. Expecting the caller to supply this assertion seems impractical, so it must be found in the stack itself.

The assertion `stack l vpqs` is not fractional: it represents the full ownership of the stack. To allow the stack to be accessed by several concurrent threads, the user must share this assertion. This is typically achieved via an Iris invariant [Birkedal and Bizjak 2023].

According to `STACKCREATE`, creating a new stack consumes one space credit. This is the size of the reference that holds the address of the top list cell. The result is a fresh location $l$ that represents an empty stack.

The specification of `(push [l; v])_{ptr}`, expressed by `STACKPUSH`, is an atomic triple with a souvenir on $l$. The private precondition requires two space credits, which is the size of a new list cell, as well as fractional pointed-by-heap and pointed-by-thread assertions for the value $v$ that is pushed onto the stack. Together, the public precondition and postcondition indicate that the model of the stack is atomically updated from `vpqs` updated to $(v, p, q) :: vpqs$ at the linearization point.

The specification of `(pop [l])_{ptr}`, expressed by `STACKPOP`, is also an atomic triple with a souvenir on $l$. The public precondition and postcondition indicate that the model of the stack is atomically updated from $(v, p, q) :: vpqs$ to `vpqs`. Furthermore, according to the public postcondition, at the linearization point, two space credits are produced, and a pointed-by-heap assertion for $v$, carrying an empty multiset of predecessors, is produced as well, as a pointer from the stack to $v$ has been destroyed.

Our specification of “pop” exhibits a certain asymmetry: whereas the space credits and the pointed-by-heap assertion appear in the *public* postcondition, which means that they are produced at the linearization point, the pointed-by-thread assertion appears in the *private* postcondition. which means that it is produced when the function returns. The space credits and the pointed-by-heap assertion can be produced at the linearization point because there we are already able to logically deallocate the list cell and to argue that a pointer from the stack to $v$ has been destroyed. However, the pointed-by-thread assertion cannot be surrendered as part of the public postcondition, because the value $v$ is read from the heap *after* the linearization point has been passed.

The last rule in Figure 41, `STACKFREE`, logically deallocates a (possibly nonempty) stack. The assertion `stack l vpqs`, as well as empty pointed-by-thread and pointed-by-heap assertions for $l$, are consumed. A number of space credits are produced, which reflect the overall size occupied by the stack data structure in the heap: one credit for the toplevel reference, plus two credits per list cell. The pointed-by-thread and pointed-by-heap assertions associated with every triple $(v, p, q)$ in the stack are also produced. Of course, in the common case where `vpqs` is an empty list, this rule can be significantly simplified.

*Proof insights.* As argued earlier (§3), the main difficulty of the proof is to produce space credits when a “pop” operation succeeds. This requires logically deallocating the list cell that is being extracted. This in turn requires exhibiting both an empty pointed-by-thread assertion and an empty pointed-by-heap assertion for this cell. Yet, neither of these assertions is easy to obtain.

Let us discuss the pointed-by-thread assertion first. The difficulty is that “push” and “pop” are *invisible readers* [Alistarh et al. 2018]: these operations read the top of the stack (that is, the address of a list cell) without synchronization. Such a read normally requires updating a pointed-by-thread assertion for the cell whose address is thus obtained. However, here, we do not wish to record that this cell is pointed to by the current thread. Fortunately, these reads occur inside protected sections.
Hence, we use `LOADINSIDE`, which updates an “inside” assertion instead of a pointed-by-thread assertion. This allows the stack’s invariant to keep an *empty* pointed-by-thread assertion, at all times, for every list cell. This in turn allows a successful “pop” operation to extract this empty pointed-by-thread assertion out of the invariant. Maintaining empty pointed-by-thread assertions for locations that are acquired only inside protected sections is a typical idiom.

Next, let us discuss the pointed-by-heap assertion. Here, the difficulty is that a list cell $\ell$ may be pointed to by a new cell $\ell'$ that has just been allocated by an ongoing “push” operation. This scenario was discussed earlier (§3.2). Hence, each ongoing “push” holds an assertion $\ell \leftarrow_{\rho} \{+\ell'\}$, where $\ell$ is the list cell that “pop” is attempting to extract and $\ell'$ is the new list cell that “push” has allocated. Now, how can “pop” obtain the assertion $\ell \leftarrow \emptyset$ that is required to allow logical deallocation? We answer this question via an original technique that we dub *logical deallocation by proxy*: the thread that successfully pops the list cell $\ell$ also takes care of logically deallocating the predecessor cells $\ell'$ that have been allocated by ongoing “push” operations.<fnref n="18" /> The logical deallocation of these locations is made possible by the protected section in “push”. This approach has a somewhat strange consequence: in the proof of “push”, it may be the case that the cell $\ell'$ has been logically deallocated by another thread, yet “push” still needs to access this cell. Fortunately, IrisFit allows this: for example, the proof of “push” makes use of the rule `STOREDEAD`. More details can be found in the first author’s dissertation [Moine 2024, §12.5].

# 12 Related Work

## 12.1 Polling Points

A stop-the-world event may be viewed as an asynchronous interruption: a thread that emits such an event stops the execution of all other threads. Such an interruption can be implemented using hardware interrupts, but this scheme can be expensive and non-portable [Feeley 1993]. Another approach is to let the compiler insert explicit tests for interruptions into the code. These tests appear in the literature under various names, including *polling points* [Feeley 1993], *GC points* [Agesen 1998], *yield points* [Lin et al. 2015], and *safe points* [Sivaramakrishnan et al. 2020]. Let us refer to them collectively as *safe points*. Safe points are typically inserted by the compiler in such a way that no computation can run forever without encountering a safe point. When a thread encounters a safe point, it tests whether some other thread has requested garbage collection. If so, it pauses and passes control to the runtime system. Once all threads have paused in this way, the runtime system performs a global garbage collection phase.

Safe points are used in the Jalapeño/Jikes RVM [Alpern et al. 1999, 2005], in the .NET CLR [Warren 2016], in Go [The Go Authors 2019], and in OCaml 5 [Sivaramakrishnan et al. 2020], among other examples. The existence of safe points is not revealed to the programmer, who is not expected to know about their existence and is given no means of controlling their placement. As an experimental feature, the OCaml 5 compiler does offer a `@poll error` attribute [Jaffer 2021; Leroy et al. 2025]. This attribute is placed on a function definition. An attempt by the compiler to insert a safe point into a function that carries this attribute causes a compile-time error. This lets the programmer check that a function body does not contain any safe point, therefore is (de facto) a protected section. At this time, there is not a clear consensus whether this feature is useful and corresponds to the needs of expert programmers.

Safe points, as described above, and polling points, as proposed in this paper, are two related yet distinct concepts. Indeed, in our view, safe points play two distinct roles. On the one hand, they are points where a thread *must* stop and allow garbage collection to take place. On the other hand, they

<footnote n="18">¹⁸These ongoing “push” operations will fail, because the top list cell that they have observed has been replaced with another cell. No ABA problem arises because memory locations are not recycled (§4.2.1).</footnote>
dictate where garbage *can* take place: indeed, the GC cannot run unless every thread has reached a safe point. Because of this dual role, safe points do *not* enjoy a monotonicity property. When a safe point is inserted in a program, the set of possible behaviors of this program is neither shrunk nor enlarged; it is transformed into an incomparable set. We believe that our design, where polling points and protected sections are separate concepts, is better behaved. In particular, it enjoys several monotonicity properties. Inserting a new polling point shrinks the set of possible behaviors of the program.<fnref n="19" /> Creating or enlarging a protected section shrinks the family of programs that is implicitly described by a source program.

In our approach, the user explicitly inserts enough protected sections to (verifiably) obtain the desired worst-case heap space complexity, then lets the compiler implicitly insert enough polling points to guarantee liveness, without endangering the program’s space complexity. This is expressed by Theorem 8.2.

## 12.2 Protected Sections

In the production systems that we are aware of, the concept that seems closest to our protected sections appears in the .NET runtime system, where it was introduced in 2015, with performance in mind [Lander 2015]. The API of the GC module [Microsoft 2024] provides a method TryStartNoGCRegion(Int64) and a method EndNoGCRegion(). A “NoGC region” is not quite a protected section in our sense, though, as allocation is permitted inside a “NoGC region”. The integer parameter of the method TryStartNoGCRegion is a request for a certain amount of free heap space: garbage collection takes place at this point so as to guarantee that this much free space exists. Allocation requests within the “NoGC region” are then served out of this pre-allocated free space. However, if the runtime system runs out of free space while some thread is inside a “NoGC region”, then garbage collection will take place.

Feeley [1993, §1.2.1] discusses why “critical sections”—sections in which the GC must not run—may be needed for safety reasons. He takes the example of a store instruction that stores a 64-bit pointer into memory and that is decomposed into two 32-bit stores. In between the two stores, the memory is in an inconsistent state and must not be read by the GC.

To the best of our knowledge, our paper is the first where a notion of protected section is introduced for complexity reasons, that is, with the aim of guaranteeing tighter worst-case heap space complexity bounds.

## 12.3 Reasoning about Space without a GC

Hofmann [1999, 2003] introduces space credits in the setting of an affine type system for the λ-calculus. Hofmann [2000] and Aspinall and Hofmann [2002] adapt the idea to LFPL, a first-order functional programming language without GC and with explicit destructive pattern matching. There, a value of type ◊ exists at runtime and can be understood as a pointer to a free block in the heap. Subsequent work aims at automating space complexity analyses. In particular, Hofmann and Jost [2003] propose an affine type system where types carry space credits. Hofmann and Jost [2006]; Hofmann and Rodriguez [2009, 2013] analyze a variant of Java where garbage collection has been replaced with explicit deallocation. RaML [Hoffmann et al. 2012a,b, 2017] analyzes a fragment of OCaml, also without GC and with explicit destructive pattern matching. Niu and Hoffmann [2018] present a type-based amortized space analysis for a pure, first-order programming language where destructive pattern matching can be applied to shared objects, an unusual feature. Their system performs significant over-approximations: when a data structure becomes shared, the logic charges

<footnote n="19">¹⁹In our setting, inserting a new polling point does not create a new opportunity for the GC to run, because the GC is always enabled anyway.</footnote>
the cost of creating a copy of this data structure. As far as we understand, this analysis can be used to reason in a sound yet very conservative way about a programming language with GC. *Kahn and Hoffmann* [2021] present a system that is equipped with more flexible typing rules than its predecessors and therefore can derive tighter resource consumption bounds. *Hoffmann and Jost* [2022] offer a survey of two decades of work on automated amortized resource analysis (AARA).

Following the ideas of LFPL, Lorenzen et al. [2023] introduce a calculus with “reuse” credits. Explicit destructive pattern matching produces reuse credits, which can be used to satisfy a new allocation. Because the system allows fragmentation, reuse credits cannot be joined. The goal of Lorenzen et al. [2023] is to statically detect fully in-place functions—that is, functions that do not need to allocate new memory. This includes, for example, functions that reuse the heap space occupied by their arguments.

Chin et al. [2005, 2008] present a type system that automatically keeps track of data structure sizes. The type system incorporates an alias analysis, which distinguishes between shared and unique objects and allows unique objects to be explicitly deallocated. Shared objects can never be logically deallocated. Specifications indicate how much memory a method may need (a high-water mark) and how much memory it releases, in terms of the sizes of the arguments and results.

Compared with type systems, program logics offer weaker automation but greater expressiveness. Aspinall et al. [2007] propose a VDM-style program logic, where postconditions depend not only on the pre-state, post-state, and return value, but also on a cost. Atkey [2011] proposes an extension of Separation Logic with an abstract notion of resource, such as time or space, and introduces an assertion that denotes the ownership of a certain amount of resources.

All of the work cited above concerns languages with explicit memory deallocation, where there is no need to reason about unreachableity. Reasoning about unreachableity in the setting of a static analysis or program logic is a central challenge.

## 12.4 Reasoning about Space with a GC

Hur et al. [2011] propose a Separation Logic for the combination of a low-level language with explicit deallocation and a high-level language with a GC. They are interested in verifying just safety, not space complexity.

Madiot and Pottier [2022] and Moine et al. [2023] propose Separation Logics that allow reasoning about space in the presence of a GC.

The logic presented by Madiot and Pottier [2022] concerns a low-level language where roots are explicitly marked as such inside the heap via so-called “stack cells”. Programming in this artificial language is impractical because local variables must be manually registered and unregistered as stack cells. Madiot and Pottier’s language and program logic technically support concurrency, but the paper does not provide any case study.

The logic presented in our previous paper [Moine et al. 2023] concerns a high-level language, where the roots and the call stack are implicit, but is restricted to a sequential setting. This paper also introduces support for closures. The logic relies on a distinction between *visible roots*—the roots of the term under focus—and *invisible roots*—the roots of the evaluation context. The logic keeps track of invisible roots using a *Stackable* assertion, and introduces the idea that *Stackable* assertions must be “forcibly framed out” at applications of the *BIND* rule. We re-use this idea in our own *BIND* rule (§6.4), but replace *Stackable* assertions with pointed-by-thread assertions, which are better suited to a concurrent setting. In so doing, we remove the distinction between visible roots and invisible roots, which does not seem to make sense in a concurrent setting; our pointed-by-thread assertions keep track of all (ordinary) roots. In contrast, Moine et al. [2023] do not keep track of visible roots via an *invisible assertion*: indeed, in their setting, it suffices to inspect the term
under focus to determine the set of visible roots. This allows them to offer a standard LOAD rule,
whereas our LOAD rule updates a pointed-by-thread assertion for the value that is loaded (§6.2).

Our mechanization [Moine 2025] includes an encoding of our previous logic for sequential
programs [Moine et al. 2023] into IrisFit. This encoding demonstrates that IrisFit can be used to
reason about sequential programs with no overhead.

12.5 Space-Related Results for Compilers

Paraskevopoulou and Appel [2019] prove that, in the presence of a GC, closure conversion is safe
for space: that is, it does not change the space consumption of a program. They view closure
conversion as a transformation from a CPS-style λ-calculus into itself. This calculus is equipped
with two different environment-based big-step operational semantics. The “source” semantics
implicitly constructs a closure for each function definition by capturing the relevant part of the
environment and storing it in the heap. The “target” semantics performs no such construction:
it requires every function to be closed. In either semantics, the roots are defined as the locations
that occur in the environment. Up to the stylistic difference between a substitution-based seman-
tics and an environment-based semantics, this definition is equivalent to the “free variable rule”
(FVR) [Morrisett et al. 1995].

Besson et al. [2019] prove that (an enhanced version of) CompCert [Leroy 2024] preserves
memory consumption when compiling C programs.

In a sequential setting, Gómez-Londoño et al. [2020] prove that the CakeML compiler respects a cost model that is defined at the level of the intermediate language DataLang, which serves as the target of closure conversion. Our cost model is analogous to theirs. Our work and theirs are complementary: whereas they prove that the CakeML compiler respects the DataLang cost model, we show how to establish space complexity bounds about source programs, based on a similar cost model. One could in principle adapt IrisFit to DataLang. Then, one would be able to use IrisFit to establish a space complexity bound about a source CakeML program, to compile this program down to machine code using the CakeML compiler, and to obtain a machine-checked space complexity guarantee about the compiled code.

12.6 Safe Memory Reclamation Schemes

Manual memory management can be so difficult in a concurrent setting that programmers often
rely on semi-automatic *safe memory reclamation* (SMR) schemes. Two main families exist, namely
hazard pointers [Michael 2004a; Michael et al. 2023] and read-copy-update (RCU) [McKenney
2004; McKenney et al. 2023]. The two families offer roughly similar APIs. First, the user declares
*hazardous* locations for a delimited scope. While it is marked hazardous, a location is not deallocated.
Second, the user can *retire* a location to indicate that this location is no longer needed. The SMR
implementation deallocates a retired location once it is not marked hazardous by any thread.

Hazard pointers operates selectively: the user manually marks and unmarks pointers as hazardous. On the contrary, RCU declares *every* non-retired pointer hazardous inside a certain section of the code. RCU seems close to our concept of a protected section. Indeed, RCU delays the deallocation of a retired pointer until every RCU section that mentions this pointer terminates. Yet, there is not a perfect analogy between RCU sections and protected sections. Indeed, garbage collection provides a strong guarantee: *no dangling pointer can exist*. SMR schemes, on the contrary, can create dangling pointers, which client data structures often tolerate. For example, with RCU, a location that is mentioned in the code, but is not read or written, does not need to be protected. For example, in the “push” operation of Treiber’s stack (Figure 1), the address of the first cell of the internal list (named h in the code) is loaded from the heap and is a root throughout a certain section of the code, but is never dereferenced. Hence, “push” *can* tolerate the deallocation of this cell by a
successful concurrent pop operation, and “push” does *not* need an RCU section [Jung et al. 2023, mechanization]. On the contrary, the “pop” operation does need a RCU section. Indeed, the address of the first cell of the internal list (again named h in the code) is dereferenced twice: once during the call to the function `is_null` and once by the CAS instruction.

Automatic memory management, based on garbage collection, and manual memory management, based on a safe memory reclamation scheme, can cohabit. For example, SnowFlake [Parkinson et al. 2017], an extension of the GC-based system .NET CLR, lets the user allocate objects in a *manual heap* where memory must be manually deallocated via a variant of hazard pointers. The main motivation for such a hybrid scheme is efficiency: manual memory management in concurrent lock-free data structures can reduce the number of stop-the-world GC pauses.

Equipping SMR schemes with abstract Separation Logic specifications and verifying them has long been a challenge. Treiber’s stack has been the first data structure based on hazard pointers to be verified. This task was tackled several times using different variants of Concurrent Separation Logic [Parkinson et al. 2007; Fu et al. 2010]. Tofan et al. [2011] verify Treiber’s stack both with hazard pointers and with garbage collection (though without a heap space complexity analysis). They show that a large part of the main invariant can be shared between the two proofs. Gotsman et al. [2013] provide the first general framework for verifying programs using SMR schemes in Separation Logic, making use of temporal logic reasoning. Jung et al. [2023] provide a more abstract framework, where temporal reasoning is replaced with ownership arguments. Their work unveils a close relationship between RCU and garbage collection. Indeed, RCU allows accessing any location that was *not* retired when the current RCU section was entered. (There is a loose analogy with our liveness-based cancellable invariants: to access such an invariant, one must eliminate the case where *l* has been logically deallocated.) To prove that a location is *not* retired at a certain point in time, Jung et al. [2023] express the topology of data structures using pointed-by-heap assertions, which they borrow from our prior paper [Moine et al. 2023]. Like us, when retiring a location, they require the predecessors of this location to have been previously retired.

Outside the Separation Logic world, Meyer and Wolff [2019] propose an API for SMR schemes, in the form of an observer automaton, inspired by the temporal reasoning of Gotsman et al. [2013]. Meyer and Wolff [2019] make use of the observer automaton to de-correlate the verification of lock-free data structures from the SMR implementation, allowing them to develop an automatic linearizability checker.

## 13 Conclusion

We have presented LambdaFit, a language with shared-memory concurrency and tracing garbage collection. In particular, LambdaFit is equipped with protected sections, a new, realistic construct that programmers can and sometimes must exploit to ensure that fine-grained concurrent data structures have the desired worst-case heap space complexity. We believe that protected sections could be a useful part of a concurrent programmer’s toolbox, and that they should be considered for inclusion in high-level languages.

Furthermore, we have presented IrisFit, a Concurrent Separation Logic with space credits, which allows expressing and verifying worst-case heap space bounds about LambdaFit programs. IrisFit features pointed-by-heap and pointed-by-thread assertions, which offer a compositional means of keeping track of the various ways through which a memory block is reachable. These assertions can be used to prove that a block is unreachable, or more accurately, that by the time the garbage collector is allowed to run, this block will be unreachable. IrisFit provides special treatment of temporary roots within protected sections and is thereby able to take advantage of protected sections to establish stronger worst-case heap space bounds.
All of our results are mechanized in the Coq proof assistant using the Iris library [Jung et al. 2018b] and its dedicated Proof Mode [Krebbers et al. 2018]. Our definitions and proofs are available in electronic form [Moine 2025]. Discounting blank lines and comments, the definition of LambdaFit and of its oblivious semantics occupy roughly 2800LOC; the construction of IrisFit, including the reasoning rules and the core soundness theorem, represent 9200LOC; the definition of the default semantics of LambdaFit and the proof of the safety and liveness theorems take up 4500LOC; and the verification of the case studies represents 6400LOC. In addition to these numbers, we re-use about 3700LOC of proofs from Madiot and Pottier [2022] and from our own previous work [Moine et al. 2023]. We provide tactics that facilitate reasoning with IrisFit and achieve a basic level of automation thanks to the Diaframe library [Mulder et al. 2022].

# 14 Future Work

We now propose avenues for future work on LambdaFit and IrisFit.

*More Liberal Protected Sections.* LambdaFit forbids function calls inside protected sections. This is a simple way of ensuring that a protected section is exited in a bounded number of steps. One might wish to relax this restriction and tolerate calls to “small” functions (that is, functions whose execution requires a bounded number of steps) inside protected sections. The obligation of proving that every protected section terminates in bounded time would then have to be delegated to the user of IrisFit, perhaps via a variation on time credits [Charguéraud and Pottier 2019]. One could relax this restriction even further by requiring only that every protected section terminates (without a statically known bound). The proof obligation would again be delegated to the user of IrisFit. This would allow traversing a data structure of unbounded size inside a protected section. Harris’s list [Harris 2001; Michael 2002] is an example where this is required. Indeed, the *search* function searches for an element in a linked list. As long as this function is running, the location of at least one internal list cell is a root. Hence, in order to respect the principle that “an internal cell may be a root only inside a protected section”, the whole *search* loop should be wrapped inside a protected section.

If the restrictions that bear on protected sections are relaxed, then the polling point insertion strategy must be adapted accordingly. Our current polling point insertion strategy, *addpp*, inserts a polling point in front of each function call. This is a simple way of ensuring that every execution path must, in a bounded number of steps, reach a polling point. However, polling points must not be inserted inside protected sections. So, if a function call appears inside a protected section, then it must not be preceded by a polling point.

*Additional Case Studies.* We would like to apply IrisFit to more ambitious case studies. This includes larger examples as well as subtler concurrent examples, including multi-CAS algorithms such as RDCSS [Harris et al. 2002], Harris’s list [2001], or its variant due to Michael [2002]. As explained in the previous paragraph, Harris’s list would require unbounded protected sections. Additionally, Harris’s list features *lazy deletion*, in which a node is first marked as deleted, before an attempt is made to physically unlink it from the structure. If this attempt fails, another function call may perform this unlinking operation. It is presently unclear to us what the specification of Harris’s list delete function would be and whether protected sections would allow this function to be verified.

*Immutable Data Structures.* We would like to determine whether immutable data structures could be specified and verified in a more pleasant and lightweight manner. At present, IrisFit offers no special support for immutable data structures: every memory block is considered mutable by default, and it is up to the user to exploit the logical tools offered by Iris, such as invariants, to indicate that
a memory block is immutable. In this paper, we have done so in the special case of closures: we
have been able to describe the behavior of a closure via a *persistent* predicate, while still allowing
for its deallocation. We would like to investigate whether this approach can be extended to all
immutable data structures.

*IrisFit as a Foundation for Type Systems or Static Analyses.* We would like to draw upon our experience with IrisFit to investigate automated static analyses of the worst-case heap space complexity of a program in the presence of garbage collection. As far as we know, relatively few such analyses have been presented in the literature. A brief review of those that we know of is given by Madiot and Pottier [2022, §7]. None of them is justified by a machine-checked argument. It would be interesting to justify existing analyses by reduction to the reasoning rules of IrisFit or to draw inspiration from these rules to design new analyses.

Acknowledgments

We wish to thank the anonymous reviewers, whose insights and perseverance have significantly
helped improve the quality and presentation of this paper.

References

Ole Agesen. 1998. *GC Points in a Threaded Environment*. Technical Report SMLI TR-98-70. Sun Microsystems, Inc. https://dl.acm.org/doi/10.5555/974974

Dan Alistarh, William Leiserson, Alexander Matveev, and Nir Shavit. 2018. ThreadScan: Automatic and Scalable Memory Reclamation. *ACM Trans. Parallel Comput.* 4, 4, Article 18 (May 2018). https://doi.org/10.1145/3201897

Bowen Alpern, C. Richard Attanasio, John J. Barton, Anthony Cocchi, Susan Flynn Hummel, Derek Lieber, Ton Ngo, Mark F. Mergen, Janice C. Shepherd, and Stephen E. Smith. 1999. Implementing Jalapeño in Java. In *Object-Oriented Programming Systems, Languages & Applications (OOPSLA)*. 314–324. https://doi.org/10.1145/320384.320418

Bowen Alpern, Steve Augart, Stephen M. Blackburn, Maria A. Butrico, Anthony Cocchi, Perry Cheng, Julian Dolby, Stephen J. Fink, David Grove, Michael Hind, Kathryn S. McKinley, Mark F. Mergen, J. Eliot B. Moss, Ton Anh Ngo, Vivek Sarkar, and Martin Trapp. 2005. The Jikes Research Virtual Machine project: Building an open-source research community. *IBM Syst. J.* 44, 2 (2005), 399–418. https://doi.org/10.1147/sj.442.0399

Andrew W. Appel. 1992. *Compiling with Continuations*. Cambridge University Press. http://www.cambridge.org/9780521033114

David Aspinall, Lennart Beringer, Martin Hofmann, Hans-Wolfgang Loidl, and Alberto Momigliano. 2007. A program logic for resources. *Theoretical Computer Science* 389, 3 (2007), 411–445. https://doi.org/10.1016/j.tcs.2007.09.003

David Aspinall and Martin Hofmann. 2002. Another Type System for In-Place Update. In *European Symposium on Programming (ESOP) (Lecture Notes in Computer Science, Vol. 2305)*. Springer, 36–52. https://homepages.inf.ed.ac.uk/da/papers/readonly/readonly.pdf

Robert Atkey. 2011. Amortised Resource Analysis with Separation Logic. *Logical Methods in Computer Science* 7, 2:17 (2011), 1–33. https://lmcs.episciences.org/685/pdf

Yves Bertot and Pierre Castéran. 2004. *Interactive Theorem Proving and Program Development – Coq’Art: The Calculus of Inductive Constructions*. Springer. https://www.labri.fr/perso/casteran/CoqArt/coqartF.pdf

Frédéric Besson, Sandrine Blazy, and Pierre Wilke. 2019. CompCertS: a Memory-Aware Verified C Compiler Using a Pointer as Integer Semantics. *Journal of Automated Reasoning* 63, 2 (2019), 369–392. https://doi.org/10.1007/s10817-018-9496-y

Lars Birkedal and Aleš Bizjak. 2023. Lecture notes on Iris: Higher-order concurrent separation logic. (2023). https://iris-project.org/tutorial-pdfs/iris-lecture-notes.pdf Unpublished.

Lars Birkedal, Thomas Dinsdale-Young, Armaël Guéneau, Guilhem Jaber, Kasper Svendsen, and Nikos Tzevelekos. 2021. Theorems for free from separation logic specifications. *Proceedings of the ACM on Programming Languages* 5, ICFP (2021), 1–29. https://doi.org/10.1145/3473586

Wayne D. Blizard. 1990. Negative membership. *Notre Dame Journal of Formal Logic* 31, 3 (1990), 346–368. https://doi.org/10.1305/ndjfl/1093635499

Robert D. Blumofe, Christopher F. Joerg, Bradley C. Kuszmaul, Charles E. Leiserson, Keith H. Randall, and Yuli Zhou. 1996. Cilk: An Efficient Multithreaded Runtime System. *J. Parallel Distributed Comput.* 37, 1 (1996), 55–69. https://doi.org/10.1006/jpdc.1996.0107

Richard Bornat, Cristiano Calcagno, Peter O'Hearn, and Matthew Parkinson. 2005. Permission accounting in separation logic. In *Principles of Programming Languages (POPL)*. 259–270. http://www.cs.ucl.ac.uk/staff/p.ohearn/papers/permissions_
paper.pdf

John Boyland. 2003. Checking Interference with Fractional Permissions. In *Static Analysis Symposium (SAS) (Lecture Notes in Computer Science, Vol. 2694)*. Springer, 55–72. https://doi.org/10.1007/3-540-44898-5_4

Stephen Brookes and Peter W. O'Hearn. 2016. Concurrent separation logic. *SIGLOG News* 3, 3 (2016), 47–65. http://siglog.hosting.acm.org/wp-content/uploads/2016/07/siglog_news_9.pdf

Quentin Carbonneaux, Jan Hoffmann, and Zhong Shao. 2015. Compositional certified resource bounds. In *Programming Language Design and Implementation (PLDI)*. 467–478. https://www.cs.yale.edu/homes/hoffmann/papers/amort_imp15.pdf

Arthur Charguéraud and François Pottier. 2019. Verifying the Correctness and Amortized Complexity of a Union-Find Implementation in Separation Logic with Time Credits. *Journal of Automated Reasoning* 62, 3 (March 2019), 331–365. http://cambium.inria.fr/~fpottier/publis/chargueraud-pottier-uf-sltc.pdf

Philippe Charles, Christian Grothoff, Vijay Saraswat, Christopher Donawa, Allan Kielstra, Kemal Ebcioğlu, Christoph von Praun, and Vivek Sarkar. 2005. X10: an object-oriented approach to non-uniform cluster computing. In *Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA)*. 519–538. https://doi.org/10.1145/1094811.1094852

Wei-Ngan Chin, Huu Hai Nguyen, Corneliu Popeea, and Shengchao Qin. 2008. Analysing memory resource bounds for low-level programs. In *International Symposium on Memory Management*. 151–160. https://www7.in.tum.de/~popeea/research/memory.ismm08.pdf

Wei-Ngan Chin, Huu Hai Nguyen, Shengchao Qin, and Martin C. Rinard. 2005. Memory Usage Verification for OO Programs. In *Static Analysis Symposium (SAS) (Lecture Notes in Computer Science, Vol. 3672)*. Springer, 70–86. https://doi.org/10.1007/115476627

William R. Cook. 2009. On understanding data abstraction, revisited. In *Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA)*. 557–572. http://www.cs.utexas.edu/~wcook/Drafts/2009/essay.pdf

Karl Crary and Stephanie Weirich. 2000. Resource bound certification. In *Principles of Programming Languages (POPL)*. 184–198. http://www.cs.cornell.edu/talc/papers/resource_bound/res.pdf

Pedro da Rocha Pinto, Thomas Dinsdale-Young, and Philippa Gardner. 2014. TaDA: A Logic for Time and Data Abstraction. In *European Conference on Object-Oriented Programming (ECOOP) (Lecture Notes in Computer Science, Vol. 8586)*, Richard E. Jones (Ed.). Springer, 207–231. https://vtss.doc.ic.ac.uk/publications/daRochaPinto2014TaDA.pdf

Marc Feeley. 1993. Polling Efficiently on Stock Hardware. In *Functional programming languages and computer architecture (FPCA)*. 179–190. https://doi.org/10.1145/165180.165205

Matthias Felleisen and Robert Hieb. 1992. The Revised Report on the Syntactic Theories of Sequential Control and State. *Theoretical Computer Science* 103, 2 (1992), 235–271. https://www2.ccs.neu.edu/racket/pubs/tcs92-fh.pdf

Jean-Christophe Filliátre. 2011. Deductive software verification. *Software Tools for Technology Transfer* 13, 5 (2011), 397–403. https://doi.org/10.1007/s10009-011-0211-0

Ming Fu, Yong Li, Xinyu Feng, Zhong Shao, and Yu Zhang. 2010. Reasoning about Optimistic Concurrency Using a Program Logic for History. In *International Conference on Concurrency Theory (CONCUR) (Lecture Notes in Computer Science, Vol. 6269)*. Springer, 388–402. https://doi.org/10.1007/978-3-642-15375-4_27

Alejandro Gómez-Londoño and Magnus O. Myreen. 2021. A flat reachability-based measure for CakeML's cost semantics. In *Implementation of Functional Languages (IFL)*. 1–9. https://doi.org/10.1145/3544885.3544887

Alejandro Gómez-Londoño, Johannes Åman Pohjola, Hira Taqdees Syeda, Magnus O. Myreen, and Yong Kiam Tan. 2020. Do you have space for dessert? A verified space cost semantics for CakeML programs. *Proceedings of the ACM on Programming Languages* 4, OOPSLA (2020), 204:1–204:29. https://doi.org/10.1145/3428272

Alexey Gotsman, Noam Rinetzky, and Hongseok Yang. 2013. Verifying Concurrent Memory Reclamation Algorithms with Grace. In *European Symposium on Programming (ESOP) (Lecture Notes in Computer Science, Vol. 7792)*. Springer, 249–269. https://software.imdea.org/~gotsman/papers/recycling-esop13.pdf

Theodore Hailperin. 1986. Formalization of Boole's Logic. In *Boole's Logic and Probability: Studies in Logic and the Foundations of Mathematics*, Vol. 85. Elsevier, 135–172. https://www.sciencedirect.com/science/article/pii/S0049237X08702477

Timothy L. Harris. 2001. A Pragmatic Implementation of Non-blocking Linked-Lists. In *Proceedings of the 15th International Conference on Distributed Computing (DISC '01)*. Springer-Verlag, Berlin, Heidelberg, 300–314. https://doi.org/10.1007/3-540-45414-4_21

Timothy L. Harris, Keir Fraser, and Ian A. Pratt. 2002. A Practical Multi-word Compare-and-Swap Operation. In *Distributed Computing, Dahlia Malkhi (Ed.)*. Springer Berlin Heidelberg, Berlin, Heidelberg, 265–279. https://www.cl.cam.ac.uk/research/srg/netos/papers/2002-casn.pdf

Guanhua He, Shengchao Qin, Chenguang Luo, and Wei-Ngan Chin. 2009. Memory Usage Verification Using Hip/Sleek. In *Automated Technology for Verification and Analysis (ATVA) (Lecture Notes in Computer Science, Vol. 5799)*. Springer, 166–181. https://dro.dur.ac.uk/6241/

Maurice Herlihy and Nir Shavit. 2012. *The Art of Multiprocessor Programming, Revised Reprint* (1st ed.). Morgan Kaufmann Publishers Inc., San Francisco, CA, USA.
Maurice P. Herlihy and Jeannette M. Wing. 1990. Linearizability: a correctness condition for concurrent objects. *ACM Transactions on Programming Languages and Systems* 12, 3 (July 1990), 463–492. https://doi.org/10.1145/78969.78972

Jan Hoffmann, Klaus Aehlig, and Martin Hofmann. 2012a. Multivariate amortized resource analysis. *ACM Transactions on Programming Languages and Systems* 34, 3 (2012), 14:1–14:62. https://www.cs.cmu.edu/~janh/assets/pdf/HoffmannAH10.pdf

Jan Hoffmann, Klaus Aehlig, and Martin Hofmann. 2012b. Resource Aware ML. In *Computer Aided Verification (CAV) (Lecture Notes in Computer Science, Vol. 7358)*. Springer, 781–786. http://dx.doi.org/10.1007/978-3-642-31424-7_64

Jan Hoffmann, Ankush Das, and Shu-Chun Weng. 2017. Towards automatic resource bound analysis for OCaml. In *Principles of Programming Languages (POPL)*. 359–373. http://www.cs.cmu.edu/~janh/papers/HoffmannDW17.pdf

Jan Hoffmann and Steffen Jost. 2022. Two decades of automatic amortized resource analysis. *Mathematical Structures in Computer Science* 32, 6 (2022), 729–759. https://doi.org/10.1017/S0960129521000487

Martin Hofmann. 1999. Linear Types and Non-Size-Increasing Polynomial Time Computation. In *Logic in Computer Science (LICS)*. 464–473. https://doi.org/10.1109/LICS.1999.782641

Martin Hofmann. 2000. A type system for bounded space and functional in-place update. *Nordic Journal of Computing* 7, 4 (2000), 258–289. http://www.dcs.ed.ac.uk/home/mxh/nordic.ps.gz

Martin Hofmann. 2003. Linear types and non-size-increasing polynomial time computation. *Information and Computation* 183, 1 (2003), 57–85. https://doi.org/10.1016/S0890-5401(03)00009-9

Martin Hofmann and Steffen Jost. 2003. Static prediction of heap space usage for first-order functional programs. In *Principles of Programming Languages (POPL)*. 185–197. http://www2.tcs.ifi.lmu.de/~jost/research/POPL_2003_Jost_Hofmann.pdf

Martin Hofmann and Steffen Jost. 2006. Type-Based Amortised Heap-Space Analysis. In *European Symposium on Programming (ESOP) (Lecture Notes in Computer Science, Vol. 3924)*. Springer, 22–37. https://www2.tcs.ifi.lmu.de/~jost/research/hofmann_jost_esop06_postfinal.pdf

Martin Hofmann and Dulma Rodriguez. 2009. Efficient Type-Checking for Amortised Heap-Space Analysis. In *Computer Science Logic (Lecture Notes in Computer Science, Vol. 5771)*. Springer, 317–331. https://doi.org/10.1007/978-3-642-04027-6_24

Martin Hofmann and Dulma Rodriguez. 2013. Automatic Type Inference for Amortised Heap-Space Analysis. In *European Symposium on Programming (ESOP) (Lecture Notes in Computer Science, Vol. 7792)*. Springer, 593–613. https://doi.org/10.1007/978-3-642-37036-6_32

Chung-Kil Hur, Derek Dreyer, and Viktor Vafeiadis. 2011. Separation Logic in the Presence of Garbage Collection. In *Logic in Computer Science (LICS)*. 247–256. http://people.mpi-sws.org/~dreyer/papers/gcsl/paper.pdf

Sadiq Jaffer. 2021. OCaml Compiler Pull Request 10462: Add [@poll error] attribute. https://github.com/ocaml/ocaml/pull/10462.

Richard E. Jones and Rafael Dueire Lins. 1996. *Garbage collection – algorithms for automatic dynamic memory management*. Wiley.

Jaehwang Jung, Janggun Lee, Jaemin Choi, Jaewoo Kim, Sunho Park, and Jeehoon Kang. 2023. Modular Verification of Safe Memory Reclamation in Concurrent Separation Logic. *Proceedings of the ACM on Programming Languages* 7, OOPSLA2 (2023), 828–856. https://doi.org/10.1145/3622827

Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer. 2018a. RustBelt: Securing the Foundations of the Rust Programming Language. *Proceedings of the ACM on Programming Languages* 2, POPL (2018), 66:1–66:34. https://people.mpi-sws.org/~dreyer/papers/rustbelt/paper.pdf

Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Aleš Bizjak, Lars Birkedal, and Derek Dreyer. 2018b. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. *Journal of Functional Programming* 28 (2018), e20. https://people.mpi-sws.org/~dreyer/papers/iris-ground-up/paper.pdf

Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, and Derek Dreyer. 2015. Iris: monoids and invariants as an orthogonal basis for concurrent reasoning. In *Principles of Programming Languages (POPL)*. 637–650. http://plv.mpi-sws.org/iris/paper.pdf

David M. Kahn and Jan Hoffmann. 2021. Automatic amortized resource analysis with the quantum physicist's method. *Proceedings of the ACM on Programming Languages* 5, ICFP (2021), 1–29. https://doi.org/10.1145/3473581

Jan-Oliver Kaiser, Hoang-Hai Dang, Derek Dreyer, Ori Lahav, and Viktor Vafeiadis. 2017. Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris. In *European Conference on Object-Oriented Programming (ECOOP)*. 17:1–17:29. https://people.mpi-sws.org/~dreyer/papers/iris-weak/paper.pdf

Ioannis T. Kassios and Eleftherios Kritikos. 2013. A Discipline for Program Verification Based on Backpointers and Its Use in Observational Disjointness. In *European Symposium on Programming (ESOP) (Lecture Notes in Computer Science, Vol. 7792)*. Springer, 149–168. https://doi.org/10.1007/978-3-642-37036-6_10

Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung, Joseph Tassarotti, Jan-Oliver Kaiser, Amin Timany, Arthur Charguéraud, and Derek Dreyer. 2018. MoSeL: a general, extensible modal framework for interactive proofs in separation logic. *Proceedings of the ACM on Programming Languages* 2, ICFP (2018), 77:1–77:30. https://doi.org/10.1145/3236772
Rich Lander. 2015. Announcing .NET Framework 4.6. https://devblogs.microsoft.com/dotnet/announcing-net-framework-4-6/.

Peter J. Landin. 1964. The Mechanical Evaluation of Expressions. Computer Journal 6, 4 (Jan. 1964), 308–320.

Jonathan K. Lee and Jens Palsberg. 2010. Featherweight X10: a core calculus for async-finish parallelism. In Principles and Practice of Parallel Programming (PPoPP). 25–36. https://doi.org/10.1145/1693453.1693459

Xavier Leroy. 2024. The CompCert C compiler. http://compcert.org/.

Xavier Leroy, Damien Doligez, Alain Frisch, Jacques Garrigue, Didier Rémy, and Jérôme Vouillon. 2025. The OCaml language (language extensions; attributes). https://ocaml.org/manual/5.3/attributes.html.

Yi Lin, Kunshan Wang, Stephen M. Blackburn, Antony L. Hosking, and Michael Norrish. 2015. Stop and go: understanding yieldpoint behavior. In Symposium on Memory Management (ISMM). 70–80. https://doi.org/10.1145/2754169.2754187

Daniel Loeb. 1992. Sets with a negative number of elements. Advances in Mathematics 91, 1 (1992), 64–74. https://www.sciencedirect.com/science/article/pii/0001870892900119

Anton Lorenzen, Daan Leijen, and Wouter Swierstra. 2023. FP²: Fully in-Place Functional Programming. Proceedings of the ACM on Programming Languages 7, ICFP (Aug. 2023), 275–304. https://doi.org/10.1145/3607840

Anil Madhavapeddy and Yaron Minsky. 2022. Real World OCaml: Functional programming for the masses (2 ed.). Cambridge University Press. https://realworlddocaml.org/

Jean-Marie Madiot and François Pottier. 2022. A Separation Logic for Heap Space under Garbage Collection. Proceedings of the ACM on Programming Languages 6, POPL (Jan. 2022), 718–747. http://cambium.inria.fr/~fpottier/publis/madiot-pottier-diamonds-2022.pdf

Simon Marlow, Tim Harris, Roshan P. James, and Simon Peyton Jones. 2008. Parallel generational-copying garbage collection with a block-structured heap. In Proceedings of the 7th International Symposium on Memory Management (Tucson, AZ, USA) (ISM). Association for Computing Machinery, New York, NY, USA, 11–20. doi:10.1145/1375634.1375637

Paul McKenney, Michael Wong, Maged M. Michael, Andrew Hunter, Daisy Hollman, JF Bastien, Hans Boehm, David Goldblatt, Frank Birbacher, Erik Rigtorp, Tomasz Kamiński, Olivier Giroux, David Vernet, and Timur Doumler. 2023. Read-Copy Update (RCU). P2545R4 https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2023/p2545r4.pdf.

Paul E. McKenney. 2004. Exploiting deferred destruction: an analysis of read-copy-update techniques in operating system kernels. Ph. D. Dissertation. Oregon Health & Science University. http://www.rdrop.com/~paulmck/RCU/RCUdissertation.2004.07.14e1.pdf

Roland Meyer and Sebastian Wolff. 2019. Decoupling lock-free data structures from memory reclamation for static analysis. Proc. ACM Program. Lang. 3, POPL, Article 58 (Jan 2019), 31 pages. https://doi.org/10.1145/3290371

Maged M. Michael. 2002. High performance dynamic lock-free hash tables and list-based sets. In Proceedings of the Fourteenth Annual ACM Symposium on Parallel Algorithms and Architectures (Winnipeg, Manitoba, Canada) (SPAA). Association for Computing Machinery, New York, NY, USA, 73–82. doi:10.1145/564870.564881

Maged M. Michael. 2004a. Hazard Pointers: Safe Memory Reclamation for Lock-Free Objects. IEEE Transactions on Parallel and Distributed Systems 15, 6 (2004), 491–504. https://doi.org/10.1109/TPDS.2004.8

Maged M. Michael. 2004b. RC23089: ABA Prevention Using Single-Word Instructions. Technical Report. https://dominoweb.draco.res.ibm.com/4813d7c4e4c6b1a085256e2b00539e0f.html

Maged M. Michael, Michael Wong, Paul McKenney, Andrew Hunter, Daisy Hollman, JF Bastien, Hans Boehm, David Goldblatt, Frank Birbacher, and Mathias Stearn. 2023. Hazard Pointers for C++26. P2530R3 https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2023/p2530r3.pdf.

Microsoft. 2024. Documentation of the GC class of the .NET 8.0 framework. https://learn.microsoft.com/en-us/dotnet/api/system.gc?view=net-8.0

Alexandre Moine. 2024. Formal Verification of Heap Space Bounds under Garbage Collection. Ph. D. Dissertation. Université Paris Cité. https://cambium.inria.fr/~amoine/phd.html

Alexandre Moine. 2025. Will it Fit? Verifying Heap Space Bounds for Concurrent Programs under Garbage Collection with Separation Logic (Artifact). https://github.com/nobrakal/irisfit Permanent snapshot: https://archive.softwareheritage.org/swh:1:snp:20f90f6c746ee641b3d8473340f68eae48c6bdd2:origin=github.com/nobrakal/irisfit.

Alexandre Moine, Arthur Charguéraud, and François Pottier. 2023. A High-Level Separation Logic for Heap Space under Garbage Collection. Proceedings of the ACM on Programming Languages 7, POPL (Jan. 2023), 718–747. https://doi.org/10.1145/3571218

J. Gregory Morrisett, Matthias Felleisen, and Robert Harper. 1995. Abstract Models of Memory Management. In Functional Programming Languages and Computer Architecture (FPCA). 66–77. https://www.cs.cmu.edu/~rwh/papers/gc/fPCA95.pdf

Ike Mulder, Robbert Krebbers, and Herman Guевers. 2022. Diaframe: automated verification of fine-grained concurrent programs in Iris. In Programming Language Design and Implementation (PLDI). 809–824. https://doi.org/10.1145/3519939.3523432

Glen Mével, Jacques-Henri Jourdan, and François Pottier. 2019. Time credits and time receipts in Iris. In European Symposium on Programming (ESOP) (Lecture Notes in Computer Science, Vol. 11423). Springer, 1–27. http://cambium.inria.fr/~fpottier/
publis/mevel-jourdan-pottier-time-in-iris-2019.pdf

Yue Niu and Jan Hoffmann. 2018. Automatic Space Bound Analysis for Functional Programs with Garbage Collection. In *Logic for Programming Artificial Intelligence and Reasoning (LPAR) (EPiC Series in Computing, Vol. 57)*. 543–563. https://easychair.org/publications/paper/dcnD

Peter W. O'Hearn. 2019. Separation logic. *Commun. ACM* 62, 2 (2019), 86–95. https://doi.org/10.1145/3211968

Zoe Paraskevopoulou and Andrew W. Appel. 2019. Closure conversion is safe for space. *Proceedings of the ACM on Programming Languages* 3, ICFP (2019), 83:1–83:29. https://doi.org/10.1145/3341687

Matthew J. Parkinson, Richard Bornat, and Peter W. O'Hearn. 2007. Modular verification of a non-blocking stack. In *Principles of Programming Languages (POPL)*. 297–302. https://doi.org/10.1145/1190216.1190261

Matthew J. Parkinson, Dimitrios Vytiniotis, Kapil Vaswani, Manuel Costa, Pantazis Deligiannis, Dylan McDermott, Aaron Blankstein, and Jonathan Balkind. 2017. Project Snowflake: non-blocking safe manual memory management in .NET. *Proceedings of the ACM on Programming Languages* 1, OOPSLA (2017), 95:1–95:25. https://doi.org/10.1145/3141879

Azalea Raad, Josh Berdine, Hoang-Hai Dang, Derek Dreyer, Peter W. O'Hearn, and Jules Villard. 2020. Local Reasoning About the Presence of Bugs: Incorrectness Separation Logic. In *Computer Aided Verification (CAV) (Lecture Notes in Computer Science, Vol. 12225)*. Springer, 225–252. https://plv.mpi-sws.org/ISL/

John C. Reynolds. 1975. *User-defined Types and Procedural Data Structures as Complementary Approaches to Data Abstraction*. Technical Report 1278. Carnegie Mellon University. http://repository.cmu.edu/compsci/1278/

John C. Reynolds. 2002. Separation Logic: A Logic for Shared Mutable Data Structures. In *Logic in Computer Science (LICS)*. 55–74. http://www.cs.cmu.edu/~jcr/seplogic.pdf

K. C. Sivaramakrishnan, Stephen Dolan, Leo White, Sadiq Jaffer, Tom Kelly, Anmol Sahoo, Sudha Parimala, Atul Dhiman, and Anil Madhavapeddy. 2020. Retrofitting Parallelism onto OCaml. *Proceedings of the ACM on Programming Languages* 4, ICFP (Aug. 2020), 113:1–113:30. https://doi.org/10.1145/3408995

Simon Spies, Lennard Gäher, Joseph Tassarotti, Ralf Jung, Robbert Krebbers, Lars Birkedal, and Derek Dreyer. 2022. Later credits: resourceful reasoning for the later modality. *Proceedings of the ACM on Programming Languages* 6, ICFP (2022), 283–311. https://doi.org/10.1145/3547631

The Go Authors. 2019. Goroutine preemption. https://go.dev/src/runtime/preempt.go.

Bogdan Tofan, Gerhard Schellhorn, and Wolfgang Reif. 2011. Formal Verification of a Lock-Free Stack with Hazard Pointers. In *Theoretical Aspects of Computing (ICTAC) (Lecture Notes in Computer Science, Vol. 6916)*. Springer, 239–255. https://opus.bibliothek.uni-augsburg.de/opus4/frontdoor/index/index/docId/55403

R. Kent Treiber. 1986. Systems programming: Coping with parallelism. https://dominoweb.draco.res.ibm.com/reports/rj5118.pdf

Simon Friis Vindum and Lars Birkedal. 2021. Contextual refinement of the Michael-Scott queue. In *Certified Programs and Proofs (CPP)*. 76–90. https://cs.au.dk/~birke/papers/2021-ms-queue-final.pdf

Matt Warren. 2016. GC Pauses and Safe Points. https://mattwarren.org/2016/08/08/GC-Pauses-and-Safe-Points/.

Hassler Whitney. 1933. Characteristic Functions and the Algebra of Logic. *Annals of Mathematics* 34, 3 (1933), 405–414. http://www.jstor.org/stable/1968168