Busy-waiting is an important, low-level synchronization pattern that is used to
implement higher-level abstractions for synchronization. Its termination
depends on cooperation by other threads as well as a fair thread scheduler.

We present a general approach for modularly verifying busy-waiting concurrent programs based on higher-order separation logic.
The approach combines two strands of prior work.
First, the Jacobs and Piessens (2011) higher-order-programming perspective for verifying concurrent modules.
Second, the Reinhard and Jacobs (2021) ghost signals approach to verify busy-waiting.
Based on the latter, we extend the programming language with call permissions, obligations and signals as well as expect permissions.
Call permissions prevent infinite recursion while the other auxiliary constructs enable the sound generation of call permissions to fuel a program's busy-waiting loops.
The resulting language has no infinite fair executions.
Previously, these extensions were used to verify classical specifications for synchronization constructs where the module creates and discharges obligations.
Such specifications, however, fix particular client patterns and would in general require “obligation transfer” to handle more intricate wait dependencies.
This precludes clients from performing lock handoffs, an important mechanism to control (un)fairness in the design of locks.
Our contribution—inspired by D’Osualdo, Sutherland, Farzan and Gardner (2021)'s TaDA Live—is to require the client to create and discharge obligations as necessary to satisfy the module's liveness requirements.
However, instead of building these liveness requirements into the logic, we express them by having the module's operations take auxiliary code as arguments whose job it is to generate the call permissions the module needs for its busy-waiting.

With this parameterized setup we recover or even surpass the expressiveness of the first-order approach taken by TaDA Live while being more amenable to mechanization in tools that support higher-order separation logic.
In the paper we present specifications and proofs in Iris, a community standard for higher-order concurrent separation logic.
We validated our approach by developing a (non-foundational) machine-checked proof of a cohort lock—to the best of our knowledge the first of its kind—using an encoding of our approach in the program verifier for C and .
This fair lock is implemented on top of another fair lock module and involves lock handoff, thus exercising the asserted contributions.

§ INTRODUCTION

We use the program in Figure <ref> both as introduction to busy-waiting and motivating example for “lock handoffs”.
First, the program performs busy-waiting.

Thread-oblivious locks allow the acquiring and releasing thread to be different.
In this example the lock is passed between the left and middle thread.
We use OCaml inspired syntax: ! and := to dereference and assign a reference respectively.
The passing is synchronized by busy-waiting for the flag f to be cleared.
If the left thread acquires the lock before the right, the latter will have to wait until both the left and middle thread are done with their critical sections.

Specifically the middle thread's while loop does not make progress, even though it is continuously able to run, until the flag it dereferences (with “!”) is cleared (with the assignment operator “:=”).
Moreover, in the fine-grained concurrent setting we consider, there are no blocking primitives.
This means the acquire calls must also internally busy-wait.
Second, it performs a lock handoff by passing the logical ownership of the lock between the left and middle thread.
Busy-waiting and lock handoffs complicate proving termination as we will explain before elaborating on the sketched solution shown in Figure <ref>.

To begin with, termination is a liveness property <cit.> and is therefore impossible to prove directly for many powerful, well-established safety logics including their tool support.
Therefore, a common strategy is to transform termination into a safety property in order to reuse these efforts.
We will consider programs instrumented with “fuel” <cit.> i.e. some (trans-) finite resource that is consumed such that infinite executions inevitably run out of fuel and get stuck.
In turn, proving that the program cannot run out of fuel—a safety property—proves that the program terminates and therefore allows us to strengthen partial to total correctness.

The client explains to the acquire operations why their waiting is justified.

It has been shown that obligations-based reasoning enables modular reasoning about blocking dependencies between threads <cit.>.
In short, obligations are held by threads and assigned levels.
A thread may only block or wait on an obligation whose level is lower than those of all its held obligations.
Obligations can be associated with primitive blocking actions on e.g. channels and locks to prove deadlock-freedom.
Moreover, they can be associated with busy-waiting patterns <cit.> where they are used to soundly generate fuel to prove termination; thus addressing the first key difficulty, bringing us to the main difficulty and contribution of this paper.
Namely, this line of work enforces—via obligations—that whenever a thread acquires a lock, that it will be that same thread which eventually releases the lock.
This allows the lock module to keep full control of the termination argument.
Obligation creation and fulfillment are handled inside acquire and release respectively.
The client only has to know that a matching release in the same thread fulfills the acquired obligation.
This allows the modular verification of termination for “well-behaved” clients.
But it also means the lock handoff in Figure <ref> cannot be proven because the left thread would be stuck with the obligation it received when it acquired the lock.

If the lock cannot prescribe a fixed usage, then the client needs to explain instead why acquire is allowed to expect the lock to be unlocked eventually.
The auxiliary pseudocode in Figure <ref> (shown in blue) does just that.
Each thread expresses what they expect to happen before they can make progress.
Crucially, acquire is parametric in the client's argument as to why the module will eventually observe the lock to be unlocked.
As first approximation /*expect*/ can be thought of as simple logging operation.
In that case we could, for any trace of the program, determine if all expectations at that point are justified.
In Sections <ref> and <ref>, we will explain how we use the aforementioned work on obligations-based reasoning to formalize this intuitive reading of the passed auxiliary code and prove the program of Figures <ref> and <ref>.

Although the program in Figure <ref> is contrived, the need to verify the correct passing of lock ownership between threads is not.
It is commonly used to control the trade-off between fairness and increased throughput <cit.>.
Take WebKit's WTF::Lock which was initially conceived as an unfair lock <cit.> but a later patch uses the ability to handoff locks to avoid starvation <cit.>.
Similarly Linux' optimized mutexes and readers-writers semaphore use handoffs for the same purpose <cit.>.
On the other hand, lock handoffs are also used to increase unfairness in order to optimize for throughput.
Lock cohorting <cit.> is a design pattern to implement locks optimized for systems with non-uniform memory access from simpler locks.
Threads of the same cohort are allowed to hand each other the cohort lock to improve throughput, locking out threads of other cohorts in the process.
The unfairness is mitigated by a threshold that forces a full release.

We present the programming language we consider and its extensions to turn termination into a safety property while preserving modularity in Section <ref>.
Section <ref> applies our higher-order-programming approach to modular termination verification to the program of Figure <ref>.
Section <ref> reviews prior work on logically atomic triples <cit.> before presenting our approach for total correctness logically atomic triples (cf. <cit.>) and their interpretation in Section <ref>.
Our case studies in Section <ref> validate that our proposed specification approach achieves expressiveness, abstraction and compositionality by applying it to modularly verify a cohort lock implementation: a fair lock module that uses lock handoffs, built on top of another fair lock module.
Finally, we discuss related work in Section <ref> before concluding in Section <ref>.

§ A TERMINATING LANGUAGE:

modifies and extends  <cit.>, a language in the ML tradition with a higher-order heap, eager evaluation and unstructured concurrency (fork).
This section progressively introduces the main changes one by one starting with obligations.
In the end we prove that does not admit infinite fair executions, making it a terminating language under any fair scheduler.

§.§ Obligations & signals

To prove progress properties like deadlock-freedom and termination
[With primitive waiting, deadlock-freedom is already a safety property. Termination will be transformed into a safety property in the next section via fuel.]
, we must prove that threads do not wait indefinitely.
Therefore, proofs of these properties commonly associate waiting actions with knowledge about matching obligations, e.g. matching blocking receives on a channel with sends, or ensuring that lock acquisition is always paired with a release.
We reify the knowledge that a certain obligation exists as a signal, with: an identity to talk about specific obligations, a level taken from a well-founded set of levels $\Levdom$ to rule out cyclic dependencies, and a status boolean—$\myfalse$ for unset and $\mytrue$ for set.
Consequently, an obligation is simply the requirement to eventually set a signal.
Each thread of the program tracks its set of obligations: a set of signal identifiers.
Obligations can be considered obligatory because a thread gets stuck if it tries to finish while that set is non-empty.
Therefore a safe thread must fulfill all its obligations.

The state of is therefore extended with $\istate.\textsc{Signals}$ to keep track of signals and $\istate.\textsc{Obligations}$ to keep track of the set of obligations for each thread.
We use the notation $\istate : \textsc{Obligations}(\theta) \cup \{s\}$ to specify the state
[The program heap of memory locations is $\istate.\textsc{Heap}$.]
$\istate$ where $s$ is added to the set of obligations for thread $\theta$.
Similarly for other state manipulating actions which may also be chained with multiple colons.
The head step relation (see Appendix <ref>, cf. <cit.>) $(\expr,\istate) \hstepi[]{\theta} (\expr', \istate', \mathit{threads})$ denotes that in state $\istate$ expression $\expr$ can step to expression $\expr'$ with new state $\istate'$ and forked threads $\mathit{threads}$.
We write $\nil$ if no threads were spawned.
Equipped with this notation we describe the behavior of CreateSignal and SetSignal <cit.>.

s ∉.Signals
(CreateSignal(),) []θ (s, : Signals[s ←(,𝑓𝑎𝑙𝑠𝑒)] : Obligations(θ)∪s, )

CreateSignal л creates the signal at the specified level $\lev$, initialized to $\myfalse$ and equipped with an identity, which it returns.
Additionally, it creates the obligation to set the signal of that identity and adds it to the creating thread's set of obligations.

.Signals(s) = (,_)
(SetSignal(s),) []θ ((),: Signals[s ←(,𝑡𝑟𝑢𝑒)] : Obligations(θ)∖s, )

SetSignal s simply sets the signal i.e. its state to $\mytrue$, getting stuck if the signal does not exist.
Like other obligations-based systems, does not allow the transfer of obligations but it features a modified fork statement that allows the transfer of obligations from parent to child <cit.>.

𝑠𝑖𝑔𝑠 set of signals

θ' = { θ' ∈|θ' ∉.Obligations }

(fork(e,𝑠𝑖𝑔𝑠), ) []θ (, : Obligations(θ) ∖𝑠𝑖𝑔𝑠 : Obligations[θ' 𝑠𝑖𝑔𝑠], (e;AssertNoObs))

In the code snippets we simply show parallel bars with sets of obligations hanging off them to indicate the transferred obligations.

The signals' levels are crucial to rule out cyclic dependencies.
We will illustrate this point via a primitive Await operation with the following semantics (cf. <cit.>).
Await s gets stuck if the signal s does not exist and returns immediately if s exists and is set.
Otherwise, the level of s must be less than the levels of all signals for which the Await-executing thread holds obligations.
In that case Await evaluates to itself.
Note that we use Await to introduce obligations and signals; it is not part of proper.

$\color{black} \emptyset$     $\color{black} \small \set{\texttt{s}}$

Obligations and signals prevent missing and circular dependencies.
$\signalexists{s}{0}$ can be freely shared between threads so its presence in both threads' pre- and postcondition is elided.
The parallel bars are for presentation purposes; the underlying program code is shown as a comment.
For simplicity this example defines $\Levdom$ as $\nat$.

Figure <ref> shows a separation logic proof outline for a simple program using Await.
$\color{myspecs} \obligations{O}[\theta]$ is a separation logic resource that tracks thread $\theta$'s obligations to set the signals whose identifiers are in the set $O$.
This resource will be reused in the rest of the paper.
We omit the thread identifier if the resource is owned by the corresponding thread and
write $\lev \prec O$ to say that level $\lev$ is less than all levels associated to the signals in set $O$:

\[
\lev \prec O \leftrightarrow \forall s \in O, \lev'.\, (\lev', \myfalse) = \istate.\textsc{Signals}(s) \rightarrow \lev < \lev'
\]

Because Await and SetSignal do not care about the signal state for their safety, we describe the knowledge that a signal has been created with the $\color{myspecs} \signalexists{s}{\lev}$ resource.
It simply expresses that a signal exists without mentioning its state and can be freely duplicated.
If the right thread in Figure <ref> was missing, the left thread would have to hold the obligation and would get stuck at the execution of Await.
Moreover, causing a deadlock by introducing a second signal and Await such that the left thread waited on the right and vice versa would also clearly violate the runtime checks outlined above.
This is due to the well-founded set of levels making it impossible to pick two levels $\lev_1$ and $\lev_2)$ for these signals such that $\lev_1 < \lev_2 \land \lev_2 < \lev_1$.
Obligations clearly rule out deadlocks via the Await primitive.

§.§ Call permissions

If primitive blocking operations were the only source of non-termination in , termination would follow from deadlock-freedom.
To the contrary, features (recursive) functions, including the ability to pass them to other functions as well as storing them in the higher-order heap.
Therefore, it is easy to cause non-termination via infinite recursion.

To rule out this possibility while still allowing large classes of programs,  is instrumented with a flexible notion of fuel: call permissions.
A program is equipped with a stock of call permissions <cit.>: a global, arbitrarily large but finite, multiset of call permissions.
A call permission is associated with an element in the well-founded universe of degrees $\Degdom$.
The stock of call permissions is itself well-founded with respect to “lowering” i.e. the replacement of a call permission of some degree $\degree$ by arbitrarily (but finitely) many call permissions of lower degree <cit.>.

0 ≤n
(lowertontimesin, ) []θ (, : CallPerms∖⊎[n ·], )

, like , does not feature iteration constructs except recursion
[For presentation purposes we sometimes use while loops, which can easily be encoded as recursive functions.]
Consequently, removing a call permission at every function application guarantees termination.
The definition of is parameterized by this well-founded set of degrees $\Degdom$.
We assume for convenience the presence of a minimum degree $\degree[0] \in \Degdom$ to which every other degree can be lowered.
Therefore it suffices to show that at every function application a call permission at degree $\degree[0]$ is removed.

[0] ∈.CallPerms
((()= )(), ) θ
((()= ) , : CallPerms∖[0], )

In examples we will omit the uninteresting lowering of the smallest available call permissions to degree $\degree[0]$ just before function application to save space.
Furthermore, we simplify the presentation of this and the following section by picking a concrete set of degrees: $\Degdom \eqdef \mathbb{N}$ ordered by $<$.
Section <ref> will explain a more general and, importantly, modular approach to picking this set of degrees $\Degdom$.
In general we use bold to display degrees.
That is in the following we denote the natural number $n$ used as degree as $\degree[n]$.
Ownership of one call permission at degree $\degree[n]$ is expressed as the separation logic resource $\color{myspecs}\callp{\degree[n]}$.

Call permissions as modular “fuel”.
For simplicity natural numbers are used as degrees.
Increased modularity can be achieved by abstracting over the natural numbers with constants.
See <cit.> for more advanced uses.

To demonstrate the contribution of call permission degrees to the modularity of fuel-based termination reasoning, consider the two functions in Figure <ref>.
Recall that our choice of $\Degdom \eqdef \nat$ is naive and will be improved in Section <ref>.
Given a hardware primitive beep the function n_beeps simply evokes that primitive $n$ times.
Clearly, $n$ function applications suffice explaining the precondition of n_beeps (cf. classic decreases clause for while loops).
alarm calls this helper function.
By picking $\color{myspecs} \callp{\degree[1]}$ as alarm's precondition, its spec does not reveal or even bound how often alarm will beep.
For example the alarm module could evolve to choose an arbitrary other natural number or even pick $n$ randomly without changing its precondition.

§.§ Atomic blocks and traditional auxiliary code

Before explaining how to connect fuel-based termination reasoning with the obligations-based deadlock prevention to support busy-waiting we must explain the atomic blocks that we are going to use.

(AtomicBlock(e), ) []θ (v, ', )

The big step relation $\Downarrow$ supports a subset of .
One notable exclusion is fork.
Termination of atomic blocks follows from the big-step relation itself.
Its definition directly mirrors the small-step semantics of .
Both are given in Appendix <ref>.
We use ⟨e⟩ as shorthand for $\langkw{AtomicBlock}(e)$.

To make full use of atomic blocks we need auxiliary
[We use the term “auxiliary” to avoid any confusion with the concept of “ghost” in Iris.]
versions of most operations.
Later we establish that safe programs always terminate (Theorem <ref>), therefore the auxiliary code is guaranteed not to diverge either.
As a result, safe auxiliary code can be erased without observable differences to the behavior of the program.

§.§ Expect permissions

Call permissions allow us to modularly ensure the termination of the non-blocking parts of the program.
Moreover, the obligations and signals introduced support reasoning about primitive blocking constructs.
So far this would enable proving termination given that the only sources of blocking are primitive (e.g. Await) and integrated into the obligations reasoning (cf. <cit.>).

lacks primitive blocking constructs like Await.
Instead, busy-waiting loops can be implemented via recursion e.g. by repeatedly testing a signal.
Yet, it is unknown how many iterations need to be performed.
Consequently, it is impossible to have enough fuel for all fair executions.
To handle this situation expect permissions (renamed from <cit.>'s wait permissions) are required to connect the two systems.

Recall that LowerS allows replacing a call permission at degree $\degree[n]$ into arbitrarily but finitely many call permissions at $\degree[m]$ ($\degree[m] < \degree[n]$).
The reason this lowering cannot be used to fuel a busy-waiting loop is that we do not know how often the loop will have to be executed before the expected value is read.
Worse still, it is unknown whether such an upper bound even exists in the case of unsound dependencies.
Obligations allow us to rule out the latter situation but not the former.
The solution <cit.>: a call permission at $\degree[n]$ can be turned into an expect permission fixed to a call permissions of lower degree ($\degree[m]$) and tied to a specific signal (s).
A thread observing the signal s unset is allowed to produce a call permission of degree $\degree[m]$ if the level of s is lower than the associated levels of all obligations held by that thread.
This allows threads to tie their progress to the setting of that signal, justified by the necessary presence of a thread holding the matching obligation.

$\color{black} \emptyset$     $\color{black} \small \set{\texttt{s}}$

Busy-waiting equivalent of Await. Code shown in  blue is auxiliary code that is to be erased.

The program shown in Figure <ref> assumes that Await is no longer available.
Instead, we give the dereference operator ! the ability to read a signal's state in this section.
It returns the signal's state, true once set and false otherwise.
The representation of signals in the logic changes accordingly: $\color{myspecs}\signal{s}{\lev}{b}$, where $b$ tracks the signals state unset ($\myfalse$) or set ($\mytrue$) and $\lev$ indicates the level.
An expect permission for signal s such that /*expect s*/ produces call permissions at degree $\degree[m]$ is written $\color{myspecs} \waitp{\degree[m]}{s}$.
Ignoring the ghost code and proof outline in Figure <ref>, shown in blue and orange respectively, it employs a simple busy-waiting loop—encoded as the recursive function busy_wait—in the left thread to await the signal being set by the right thread.
The program has two function applications:

* the recursive call inside busy_wait and

* the initial invocation of busy_wait.

An initial call permission of degree $\degree[2]$ is lowered to two call permissions of degree $\degree[1]$ one of which justifies the call to busy_wait (recall that we elide the trivial lowering from $\degree[1]$ to $\degree[0]$).
The other call permission is used to create an expect permission for signal s: as long as s is unset, /*expect s*/ can be used to generate call permissions of degree $\degree[0]$.
This expect permission is then used inside busy_wait to justify the recursive call to retry (busy-wait).
The atomic block is used to conditionally call /*expect*/ if the signal is not set yet.

Generating call permissions is only sound if self-fueling loops are prevented.
We adopt the same approach as <cit.> and track threads' “phases”.

τ= .Phase(θ)

𝑠𝑖𝑔𝑠 set of signals

θ' = { θ' ∈|θ' ∉.Obligations }
(fork(e,𝑠𝑖𝑔𝑠), ) []θ (, : Obligations(θ) ∖𝑠𝑖𝑔𝑠 : Obligations[θ' 𝑠𝑖𝑔𝑠]

: Phase[θ←τ.Forker; θ' ←τ.Forkee], (e;AssertNoObs))

The initial thread starts at phase $\epsilon$.
At each fork, “$\mathrm{Forker}$” and “$\mathrm{Forkee}$” are appended to the forking and forked threads' phases respectively.
Call permissions generated by /*expect*/ are labeled by the /*expect*/ing thread's phase.
Correspondingly, the call permission at degree $\degree[0]$ consumed at function application is subject to a phase-compatibility check: the call permission consumed must be labeled by the current thread's phase or that of an ancestor (we use $\sqsubseteq$ for that relation).
When multiple call permissions are available, a call permission of maximal phase is consumed.

τ' = .Phase(θ)

τ= max_⊑{ τ|(τ,[0]) ∈.CallPerms τ⊑τ' }

[τ][0] ∈.CallPerms
((()= )(), ) []θ
((()= ) , : CallPerms∖[τ][0], )

s ∈.Signals

τ' = σ.Phase(θ)

τ= max_⊑{ τ|(τ,) ∈.CallPerms τ⊑τ' }

[τ] ∈.CallPerms

CreateExpectPerm(s,,), []θ (),: CallPerms∖[τ] : ExpectPerms ∪(s,(τ',),)

τ' = σ.Phase(θ)

.Signals(s) = (, 𝑓𝑎𝑙𝑠𝑒)

(s,[τ]) ∈.ExpectPerms
(Expect(s,), ) []θ (, : CallPermissions ⊎[τ'],)

To avoid clutter in the example programs, the phases of the call permissions consumed by the various commands are not specified as operands to the commands; instead, these commands consume appropriate call permissions with maximal phases.
Still, we can use proof rules for these commands where any appropriate call permission is consumed.
This does mean the Iris view of the stock of permissions available to the program diverges from the stock of permissions available in the operational semantics; however, the former can always be obtained from the latter by weakening.

In general the ability to share call permissions is useful to verify non-blocking algorithms <cit.>.
However, this paper does not make use of this ability.
Therefore, we omit all mentions of thread phases with the exception of the soundness proof (Section <ref>).
Moreover, in the examples of this paper there will only ever be one expect permission matching the signal, obviating the need to specify the desired generated degree.
We therefore omit the second argument of /*expect*/ since it is clear from context.

Returning to the problem of verifying busy-waiting programs, two important aspects are still missing.
For one obligations and signal are still taken to be primitive, essentially allowing us to wait on boolean conditions but nothing else.
This will be addressed in the next subsection.
Moreover, the program in Figure <ref> is not modular, the busy-waiting loop is hard-coded to wait on signal s, justified in turn by a fixed expect permission for exactly that signal.

§.§ Busy-waiting for arbitrary conditions

Obligations and signals must be erasable from programs without changes in observable behavior.
Therefore, busy-waiting loops must not wait on them in the real code.
Moreover, signals are essentially glorified booleans and in general we wish to wait on complex conditions.
We therefore turn signals into auxiliary code but tie their state to the (complex) condition being waited for via regular invariants (cf. <cit.>).
The simultaneous manipulation of the real condition and its signal counterpart is achieved with atomic blocks.

$\color{myghostcode} \emptyset$     $\color{myghostcode} \small \set{\texttt{s}}$

Simple busy-waiting.

The differences between Figures <ref> and <ref> are quite simple.
Obligations and signals are turned into auxiliary code that may not influence the outcome of the erased program (provided that the instrumented program is safe).
Instead of waiting on a built-in signal, the left thread now busy-waits until the reference f holds the value 42.
Again, the right thread makes this expectation come true eventually, this time by setting f := 42.
An invariant is used to tie together the state of the signal and the condition the program actually waits on.

The regular code does not interact with the auxiliary code meaning that the latter can be safely erased together with the auxiliary state of call permissions, obligations and signals.

§.§ Soundness

To conclude this presentation of we must show that it does not admit infinite fair executions.
Moreover, to complete the transformation of termination from a liveness to a safety property we have to establish that safe programs terminate i.e. reduce to a value.
Due to the setup's similarity, the proof is very similar to that of <cit.>.

A program does not have infinite fair executions.

Consider the program order graph of any infinite fair execution, where the nodes are labeled by the executed command, the global state, and the time point—$n$th machine step, where $n \in [0,\infty)$—when it occurred: $(c,\istate,n)$.
Each node points to the next step of the same thread, and if the current step (executed command) is a fork, additionally to the first step of the forkee.
The resulting graph forms a directed tree.

Recall that the global state keeps track of the threads' phases ($\istate.\textsc{Phase}$), describing each thread's ancestry.
Expect permissions and call permissions are only available to threads if they are phase-compatible i.e. the expect/call permission's phase must be an ancestor ($\sqsubseteq$) of the thread's current phase (see Section <ref>).
This allows us to define the “path fuel” available at each node.
The path fuel available is the multiset union of all phase-compatible call permission and an over-approximation of call permissions generated in the future as long as no signal is /*expect*/ed infinitely often on the path.

\begin{align*}
& \mathit{PF}(c,\istate,m) \eqdef [ (\tau,\degree) \mid (\tau,\degree) \in \istate.\textsc{CallPerms} \land \tau \sqsubseteq \tau'] \uplus{} \\
& \qquad
\biguplus_{(\tau,(\degree,s)) \in W}
\left. \begin{cases}
[(n - m) \cdot (\tau',\degree)] & \text{if $s$ is last \lstinline{/*expect*/}ed at machine step $n$} \\
\emptyset & \text{otherwise i.e.\ $s$ is \lstinline{/*expect*/}ed infinitely often}
\end{cases} \right. \\
& \qquad
\textrm{where} \\
& \qquad\qquad
\tau' ~\text{is the phase of the execution step's thread and} \\
& \qquad\qquad
W \eqdef \{ (\tau,(\degree, s)) \mid (\tau,(\degree,s)) \in \istate.\textsc{ExpectPerms} \land \tau \sqsubseteq \tau' \}
\end{align*}

We use this measure as the more significant element of the lexicographic ordered tuple of path fuel and syntactic size.
The latter decreases as each path step in the absence of function application, 's only source of non-termination.
Crucially, function applications are only possible as long as there are call permissions available.
Given the absence of signals that are /*expect*/ed infinitely often on the path, the path fuel over-approximates the stock of call permissions available to all paths starting at that node.
The path fuel is finite and decreasing.
At every function application a call permission of degree $\degree[0]$ is removed and the generation of call permissions is limited if no signal is waited for infinitely often on the path.
While signals and wait permissions allow the generation of new call permissions, creating an expect permission requires giving up a call permission of higher degree, causing the path fuel to decrease despite over-approximating the number of possibly generated call permissions using that signal and the new expect permission.
By Kőnig's lemma the infinite graph corresponding to the assumed infinite fair execution must have an infinite path.
However, this path must run out of path fuel and get stuck eventually, a contradiction.

It remains to show that no signal is /*expect*/ed infinitely often.
Once a signal is created, the corresponding obligation is associated to a thread.
Transfer of obligations is only possible at forks.
Hence, for each signal there exists a path carrying that signal's obligation until it is fulfilled.
At that point the signal cannot be /*expect*/ed anymore.
Accordingly, a signal which is /*expect*/ed infinitely often must never be fulfilled.
Let be the set of signals /*expect*/ed infinitely often and $\smin \in \Sinf$ a signal of minimal level.
This choice is justified by the fact that the universe of levels is well-founded.
The path carrying 's obligation must only wait for signals that are not /*expect*/ed infinitely often and therefore end.
If the path ends with the obligation unfulfilled, the program gets stuck stopping execution: a contradiction.
Otherwise, we arrive at another contradiction: must have been set and therefore $\smin \not\in \Sinf$.

A safe programs reduces to a value.

By Theorem <ref> we know that programs must either reduce to a value or get stuck.
If a programs is proven safe it cannot get stuck.

§ MODULAR VERIFICATION OF BUSY-WAITING

We can now revisit the program of Figure <ref> performing a simple lock handoff.
For this example it does not matter whether a lock is fair or unfair so we will consider arguably the simplest lock implementation: a .
A is a thin wrapper around a reference to a boolean.
Atomically changing the value from false to true with a compare-and-set (CAS) instruction acquires the lock.
Lock acquisition busy-waits (“spins”, hence the name) on this transition from false to true.
Its implementation is shown in Figure <ref>.

let spinlock_create () = ref false

let spinlock_release x = x := false

let spinlock_acquire x =
let b = ref false in
while not !b do
b := CAS x false true

Implementation of the module.

The is interesting because the module is completely unfair.
Consider a translation of the specification approach for primitive blocking.
Each acquire gives the acquiring thread an obligation to release the lock again.
For a fair lock this enforced usage pattern does ensure eventual termination of any single call to acquire.
It does not, however, work for unfair locks in general and s in particular because it can suffer from unlimited “barging”.
There is no bias in favor of earlier attempts to acquire the lock, a call to may thus starve.
Therefore, the termination argument must be entirely made by the client.

To show how, we ignore the issue of modularity at first and inline the definitions of and in Figure <ref>.
The auxiliary code justifies why each thread is allowed to wait inside its busy-waiting loop.
Since we have global knowledge we can specify all but one dependency statically.
Clearly, $\theta_2$ has to wait for the flag to be cleared.
We know $\theta_1$ will do so and associate this action with /*s_1*/.
If $\theta_3$ needs to wait, it does so because it expects the lock to be released.
Using our global knowledge it is clear that $\theta_1$ must have acquired the lock and that $\theta_2$ will release it.
We associate /*s_2*/ with this action, which $\theta_3$ can /*expect*/.
Clearly, s_1 $<$ s_2 must hold.
It remains to show that $\theta_1$'s expectation that the lock will be eventually released if it is locked.
We avoid circular waiting by having $\theta_3$ create the necessary signal precisely when it acquires the lock, storing it at location /*l*/.
At that point $\theta_3$ no longer needs to wait on /*s_2*/.
This allows us to pick the level of /*!l*/ $<$ /*s_1*/ $<$ /*s_2*/.

While this solution is thread-modular—$\theta_3$ need not know who will set /*s_2*/—it is not procedure-modular since we had to inline the module's definitions.

Consider this modified loop body of :

b := /*⟨let b' = */ CAS x false true /*in (if b' then α () else β ()); b'⟩*/

Here, and are auxiliary code passed to by the client.
's responsibility is to generate call permissions when the expected state is not reached i.e. justifies (busy) waiting
[In Modern Greek, $\beta$ is pronounced as ipa: [v], which is close enough to the w in “waiting” to serve as mnemonic because we use to justify waiting.]
$\theta_3$'s dynamic allocation of a signal at the point of acquire moreover demonstrates the need to execute auxiliary code at the linearization point together with the atomic update (more on that in Sections <ref> and <ref>).
Hence, spinlock_acquire x /*α   β*/ has two auxiliary parameters
[We use $\aalpha$ to evoke the atomic update that it accompanies.]
and .
We will always fully apply functions.
When only one piece of auxiliary code is passed it will be , otherwise and in that order.
Figure <ref> re-establishes the abstraction boundary of the module using and to pass in the necessary auxiliary code to justify the threads' expectation as before.

$\color{myghostcode} \set{\mathtt{s_1}}$     $\color{myghostcode} \set{\mathtt{s_2}}$     $\color{myghostcode} \emptyset$

Motivating example of Figure <ref> assuming the use of the module (Figure <ref>) with all function calls inlined.
The constructs of Section <ref> allow us to demonstrate termination.
The annotations adorning the parallel composition bars indicate how the obligations held by the main thread are distributed among the child threads.

Recover procedure modularity by paramterizing the module's functions with and .
must be executed at the tomic update from unlocked to locked.
While can be used by the module to ait (wait) on the client.
spinlock_acquire takes both and , in that order, while spinlock_release only takes because it does not need to wait.

Passing auxiliary code subsumes the lock budget approach where a maximum number of acquisitions $B$ is determined up front, therefore guaranteeing that at most $B-1$ may overtake a call to acquire.
That is to say, the budget approach can be easily implemented outside the module.
Moreover, it applies to situations where no appropriate budget can be picked.

At this point we have covered the main thrust of the paper.
It remains to show that we can prove safety in a modular way.
These details will vary between logics.
The presented approach has been conceived with higher-order concurrent separation logics in mind.
In the following we will discuss specifications and proofs in the Iris
<cit.> logic.
Moral equivalents of these specifications, adapted to the program verification tool for C and  <cit.>, have been mechanized and applied to our case studies (see Section <ref>).

§ LOGICALLY ATOMIC TRIPLES

\begin{align*}
& \overbrace{\langle \vec{x}. P \rangle \spac \textcolor{black}{e} \spac \langle \vec{v}. Q \rangle_\mask}^{\text{Logically atomic triple}} \eqdef{} \\
& \forall \Phi.\, \overbrace{\langle \vec{x}. P \mid \vec{v}. Q \vs \Phi \rangle_{\top\setminus\mask}}^{\atomicupdate} \wand \wpre {\textcolor{black}{e}} {\Phi} \\
& \overbrace{\langle \vec{x}. P \mid \vec{v}. Q \vs \Phi \rangle_{\mask}}^{\atomicupdate} \proves \pvs[\mask][\emptyset] \exists \vec{x}.\, P \ast \left( \overbrace{\left( P \vsW[\emptyset][\mask] \langle \vec{x}. P \mid \vec{v}. Q \vs \Phi \rangle_{\mask} \right)}^{\vsabort} \land \overbrace{\left(\forall \vec{v}.\, Q \vsW[\emptyset][\mask] \Phi \right)}^{\vscommit} \right) \\
\end{align*}

Logically atomic triples <cit.>. Presentation adapted from <cit.>.

Logically atomic triples <cit.> (cf. <cit.>'s atomic triples) of the form $\langle \vec{x}.\, P \rangle\, e\, \langle \vec{v}.\, Q \rangle$ state that “$e$ atomically updates $P$ to $Q$” (or $e$ diverges).
We call $P$ the atomic precondition and $Q$ the atomic postcondition.
Unlike in classic Hoare triples, $e$ does not own $P$ directly which would forbid concurrent access to it.
The resources behind $P$ must be able to change during $e$'s execution while still allowing, and forcing, it do perform the atomic update (or diverge).
Iris encodes this by proving the weakest precondition of $e$ given an atomic update resource (see “” in Figure <ref>) parameterized by a universally quantified postcondition: $\forall \Phi.\, \langle \vec{x}.\, P \mid \vec{v} Q \vs \Phi \rangle_{\mask} \wand \wpre e {\Phi}$.
This resource can be used to access $P$ at any step.
After obtaining $\exists \vec{x}.\, P$ one must either

* either perform the atomic update from $P$ to $Q$.
Witnessing $Q$ allows performing which is the only way to obtain $\Phi$. Otherwise

* one must “abort” the atomic update by giving $P$ back.
In return one receives the back ().

A lock acquire can be specified as $\color{myspecs} \langle b.\, L(x,b) \rangle\, {\color{black} {\small\texttt{acquire}}}\, \langle L(x,true) \ast b = false \rangle $.
The extra binder tells us which variables in $P$ (here $\color{myspecs} L(x,b)$) are existentially quantified over i.e. are allowed to change during $e$ (e.g. acquire).

It has been shown <cit.> that proving logical atomicity for a module implies linearizability <cit.>.
Linearizability allows reasoning about a module's operations with respect to their (atomic) pre- and postconditions.
This is exemplified by the ability to open and close invariants not just around atomic operations but logically atomic operations in Iris.

Unfortunately, logically atomic triples do not work as presented for blocking programs.
For example during acquire, while the lock is held, $\color{myspecs} \exists b.\, L(x,b)$ will need to be accessed repeatedly, possibly without bound.
While provides the required for retrying (in a recursive loop, possibly busy-waiting)
that (recursive) call also requires a call permission.
In Section <ref> the call permissions necessary for waiting were generated via .
The next section explains how we integrate and with logically atomic triples to obtain total correctness logically atomic triples suitable for .

§ MODULAR SPECIFICATIONS

In this section we introduce our specification approach for blocking modules: total correctness logically atomic triples.
As precursor, we revisit the subject of degrees and levels.
A modular—and therefore composable—choice of degrees and levels hides important implementation details, enabling proof reuse and library evolution.
The method presented in Section <ref> lays the foundation to scaling the total correctness logically atomic triples (Section <ref>) to advanced synchronization primitives.
Importantly, we will be able to prove our fair lock specification for a , implemented against a module of the same specification (Section <ref>).

§.§ Determination of degrees and levels

To verify a program written in , we must instantiate the universe of degrees $\Degdom$.
In prior sections we fixed $\nat$ as this universe.
While simplifying the presentation it severely limits the modularity of possible specifications.
For a concrete program without abstraction boundaries (and corresponding specifications) a suitable universe of degrees can be determined by inspecting the program text.
Modular proofs of libraries and clients permit non-automated verification efforts to scale.
To this end we adopt the following convention.
Each module picks a well-founded, non-empty, local set of degrees with one element designated as top.
This set is opaque to its clients, including the top element which has to be treated symbolically.
Moreover, each module is parameterized by a strict-order preserving embedding of the local module degrees into the universe of degrees.
Each use of the local degrees by the module is therefore wrapped by this embedding.
By convention, we require a call permission of (embedded) degree top in the precondition of public module operations.
Consequently, modules importing other modules define their local set of degrees with respect to the opaque local degrees of their dependencies, supplying each dependency with the appropriate embedding into the constructed local set of degrees.
This process applies to the entire (acyclic) dependency graph.
The root of this graph, the top-level program, applies the same method to obtain the universe of degrees.

Recall the Alarm module of Section <ref> (see Figure <ref>), consisting of the module-internal function n_beeps and the public operation alarm.
Applying this approach to it, yields the following specification of alarm:

\begin{align*}
& \exists \degree[Alarm].\forall(\degembedding{\degree[Alarm]} : \degree[Alarm] \embedsinto \Degdom). \\
& \qquad
\{ \callp{\degembedding{\degree[Alarm]}(\degree[\top_{\mathbf{Alarm}}])} \}\,
\{ \TRUE \}
\end{align*}

Internally, the Alarm module picks $\degree[Alarm] \eqdef \set{\degree[0],1}$ as its well-founded set of degrees with $\degree[0]$ preceding $1$.
A simple program that only imports alarm can therefore construct the universe degrees like this: $\Degdom \eqdef \degree[Alarm] \plusprec \set{()}$.
Where $A \plusprec B$ is notation for constructing the disjoint union of two well-founded sets $A,B$ such that every element in the embedding of $A$ precedes every element in the embedding of $B$, for example:

\begin{align*}
& \degembedding{A} : A \embedsinto A \plusprec B \eqdef \lambda x.  \mathsf{inl}\, x \\
& \degembedding{B} : B \embedsinto A \plusprec B \eqdef \lambda x.\mathsf{inr}\, x \\
& \text{such that} \\
& \qquad \forall x, y.\, \mathsf{inl}\, x < \mathsf{inr}\, y \\
& \qquad \forall x, y.\, \mathsf{inl}\, x < \mathsf{inl}\, y ~\text{if}~ x <_A y \\
& \qquad \forall x, y.\, \mathsf{inr}\, x < \mathsf{inr}\, y ~\text{if}~ x <_B y \\
\end{align*}

Blocking modules apply the same strategy to levels: they pick local sets of levels and are parametric in strict-order preserving embeddings.

\begin{align*}
& \exists \degree[M],\levset{M}.\forall (\degembedding{\degree[M]} : \degree[M] \embedsinto \Degdom), (\levembedding{M} : \levset{M} \embedsinto \Levdom). \ldots
\end{align*}

§.§ Total correctness logically atomic triples

Section <ref> explained how to program using and to verify the termination of a busy-waiting program in a modular way.
was used to run auxiliary code at the linearization point while was used to justify the waiting while the expected condition—the lock being unlocked—did not hold.
Concretely, “justifying” expresses itself as the generation of call permissions.
For that example all generated call permissions were at degree $\degree[0]$.
In general, modules require the passed to generate call permissions of higher degree in order to call other modules while busy-waiting.
As outlined above, (blocking) modules define a local set of module degrees with a top element.
Having generate call permissions at degree top necessarily suffices to fuel a blocking module's busy-waiting loop.

This section explains, step by step, how we integrate and into the definition of logically atomic triples, thus arriving at our total correctness logically atomic triples.
We will use green color to emphasize additions over the most recent predecessor.
First consider the addition of $\eventually$
[The $\eventually$ notation is borrowed and adapted from <cit.>'s usage of it in their abstract atomic triples.]
in $\setlength\fboxsep{1pt} \langle \vec{x} \, \colorbox{greenbg}{$\eventually\, X$}.\, P \rangle \spac \textcolor{black}{e} \spac \langle \vec{v}. Q \rangle_{\mask}$.
It expresses that eventually, $\vec{x}$ will be in the set $X$.
For example we specify the simple—unfair—'s acquire like this:

\[
\color{myspecs} \langle b \eventually\, \set{\myfalse}\!.\, L(x,b) \rangle\, {\color{black}{\texttt{acquire}}~x}\, \langle L(x,\mytrue) \ast b = \myfalse \rangle
\]

This says, that the lock state is allowed to flip between unlocked and locked repeatedly but eventually, acquire will observe it to be unlocked.
To show where and fit in, we unfold the definition, highlighting our additions over the logically atomic triple definition in Figure <ref>:

\begin{align*}
& \setlength\fboxsep{1pt}
\forall \Phi, \colorbox{greenbg}{$\aalpha, \abeta.\, \callp{\degembedding{M}(\degree[\top_\mdegset])}$} \ast \langle \vec{x} \colorbox{greenbg}{$\overset{\abeta}{\eventually}\, X$} \underset{{\colorbox{greenbg}{\aalpha}}}{|} \vec{v}.\, Q \vs \Phi \rangle_{\top\setminus\mask} \wand \wpre {e\, \colorbox{greenbg}{$\aalpha\, \abeta$}} \Phi \\
& \setlength\fboxsep{1pt}
\langle \vec{x} \colorbox{greenbg}{$\overset{\abeta}{\eventually} X$}.\, P \underset{{\colorbox{greenbg}{\aalpha}}}{\mid} \vec{v}. Q \vs \Phi \rangle_{\mask} \proves \pvs[\mask][\emptyset] \exists \vec{x}.\, P \ast{} \\
& \setlength\fboxsep{1pt}
\qquad \bigl((\colorbox{greenbg}{$\vec{x}\, \not\in X \wand \textlog{wp}^{\Downarrow}_{\emptyset} \spac \abeta \spac \{\callp{\degembedding{M}(\degree[\top_\mdegset])}$} \ast{} \vsabort\colorbox{greenbg}{$\vphantom{{\textlog{wp}_{\emptyset}^{\Downarrow}}}\}$}) \land{} \bigr.\\
& \setlength\fboxsep{1pt}
\qquad \,\, (\colorbox{greenbg}{$\vec{x} \in X \wand \textlog{wp}^{\Downarrow}_{\emptyset} \spac \aalpha \spac \{$}\vscommit \colorbox{greenbg}{$\vphantom{\textlog{wp}^{\Downarrow}_{\emptyset}}\}$})\bigl.\bigr) \\
\end{align*}

We use $\textlog{wp}^{\Downarrow}$ to reason about and because they will be executed together with non-auxiliary instructions in an atomic block.
This specialized weakest precondition (see Figures <ref> and <ref> in the appendix) says that from the expression and state, the big-step relation steps to a value and modified state such that the postcondition is satisfied.
's specification matches the intuitive reading given above: if the module is not in a target state ($\color{black} \vec{x} \not\in X$) it must generate a call permission at degree $\degree[\top_\mdegset]$ and allow recovering the atomic update resource again ($\callp{\degree[\top_\mdegset]} \ast \vsabort$).
Remember that, by convention, a module $M$ (to which $e$ belongs) picks a local set of call permission degrees $\degree[M]$ with a designated top element $\top_{\degree[M]}$.
Specifically, our total correctness logically atomic triples are implicitly defined in such a context and must hold for every client-defined strict-order preserving embedding $\degembedding{M}$:
\exists \degree[M]. \forall (\degembedding{\degree[M]} : \degree[M] \embedsinto \Degdom).
\langle \vec{x} \, \eventually\, X.\, P \rangle
\spac \textcolor{black}{e} \spac
\langle \vec{v}. Q \rangle_{\mask}$.
In the following we omit showing the explicit application of $\degembedding{M}$ since it is systematically applied to all occurrences of degrees in the module implementation and proof.
is a simple wrapper around , allowing us to, for example, create obligations when the atomic update is performed in a target state (see the right thread in Figure <ref>).
This specification does not pass ownership of the thread's obligations-tracking resource ($\obligations{O}$) to the operation.
The module may therefore not perform any waiting that is not justified by .

To allow the module to perform encapsulated blocking, i.e. blocking that is not visible to the module's client (via ), we need to pass the obligations-tracking resource to the operation.
Additionally, a lower bound on the levels of all held obligations must be given in order for the module to be able to call blocking operations internally.
We extend the notation $\lev \prec O$ to apply to sets of levels on the left side as well ($\levset{M} \prec O$).
We add the modules choice of levels to our total correctness logically atomic triples:
$ \setlength\fboxsep{1pt}
\exists \degree[M], \colorbox{greenbg}{$\levset{M}$}.
\forall (\degembedding{\degree[M]} : \degree[M] \embedsinto \Degdom),
\colorbox{greenbg}{$(\levembedding{M} : \levset{M} \embedsinto \Levdom)$}.
\langle \vec{x} \, \eventually\, X.\, P \rangle
\spac \textcolor{black}{e} \spac
\langle \vec{v}. Q \rangle_{\mask}^{\colorbox{greenbg}{$\levset{M}$}}$.
is passed the tracked obligations $\obligations{O}$, but has to return them unmodified.
Ownership of the tracked obligations is returned to the client via at the linearization point.

\begin{align*}
& \setlength\fboxsep{1pt}
\forall \Phi,\aalpha,\abeta,\colorbox{greenbg}{$O$}.\, \colorbox{greenbg}{$\obligations{O} \ast \levembedding{M}(\lev) \prec O \ast{}$} \callp{\degree[\top_\mdegset]} \ast \langle \vec{x} \overset{\abeta}{\eventually}\, X \underset{\aalpha}{|} \vec{v}.\, Q \vs \Phi \rangle_{\top\setminus\mask}^{\colorbox{greenbg}{$\lev;O$}} \wand \wpre {e\, \aalpha\, \abeta} \Phi \\
& \setlength\fboxsep{1pt}
\langle \vec{x} \overset{\abeta}{\eventually} X.\, P \underset{\aalpha}{\mid} \vec{v}. Q \vs \Phi \rangle^{\colorbox{greenbg}{$\lev;O$}}_{\mask} \proves \pvs[\mask][\emptyset] \exists \vec{x}.\, P \ast{} \\
& \setlength\fboxsep{1pt}
\qquad \bigl( (\colorbox{greenbg}{$\obligations{O}$} \ast \vec{x} \not\in X \wand \bswpre \abeta [\mask] {\colorbox{greenbg}{$\obligations{O}$} \ast \callp{\degree[\top_\mdegset]} \ast \vsabort}) \land{} \\
& \setlength\fboxsep{1pt}
\qquad \,\, (\colorbox{greenbg}{$\obligations{O} \ast \vec{x} \in X$} \wand \bswpre \aalpha [\emptyset] {\vscommit}) \bigl.\bigr) \\
\end{align*}

The explicit application of level embeddings, like those of the degree embeddings, will be elided.

Some proofs, e.g. the proof in Section <ref>, benefit from the ability to wait internally.
That is, they need to justify busy-waiting by calling while holding module-created obligations before the linearization point.
For that purpose we allow the set of tracked obligations to change while calling , provided that the lower bound remains true.

\begin{align*}
& \setlength\fboxsep{1pt}
\forall \Phi,\aalpha,\abeta,O.\, \obligations{O} \ast \lev \prec O \ast \callp{\degree[\top_\mdegset]} \ast \langle \vec{x} \overset{\abeta}{\eventually}\, X \underset{\aalpha}{|} \vec{v}.\, Q \vs \Phi \rangle_{\top\setminus\mask}^{\lev;O} \wand \wpre {e\, \aalpha\, \abeta} \Phi \\
& \setlength\fboxsep{1pt}
\langle \vec{x} \overset{\abeta}{\eventually} X.\, P \underset{\aalpha}{\mid} \vec{v}. Q \vs \Phi \rangle^{\lev;O}_{\mask} \proves \pvs[\mask][\emptyset] \exists \vec{x}.\, P \ast{} \\
& \setlength\fboxsep{1pt}
\qquad \bigl( (\forall \colorbox{greenbg}{$O'$}.\, \obligations{\colorbox{greenbg}{$O'$}} \ast \colorbox{greenbg}{$\lev \prec O'$} \ast \vec{x} \not\in X \wand \bswpre \abeta [\mask] {\obligations{\colorbox{greenbg}{$O'$}} \ast \callp{\degree[\top_\mdegset]} \ast \vsabort}) \land{} \\
& \setlength\fboxsep{1pt}
\qquad \,\, (\obligations{O} \ast \vec{x} \in X \wand \bswpre \aalpha [\emptyset] {\vscommit}) \bigl.\bigr) \\
\end{align*}

So far these specification apply to unfair modules i.e. has to produce a call permission whenever called while the target state has not been reached.
This places a heavy burden on the client, even when locks are always released by the same thread that acquired it by e.g. having to keep track of a maximum number of locking operations or leveraging specific client situations (cf. Figure <ref>).
By contrast, a fair blocking module can support the client in its job to create call permissions.
In particular, fair modules will provide call permissions to at each new round of waiting.
For fair locks specifically, a new round starts whenever the lock is acquired.
For example the 's acquire in Section <ref> knows that there are a fixed amount of tickets preceding its own ticket.
Therefore it is willing to help with that many rounds of waiting by providing call permissions when the owner changes.
The expression $r$ dangling off of $\eventually[r]$ evaluates to a natural number indicating the current round.
We associate to this round number a linear
[Linear in the sense that it is required in pre- and postconditions and can therefore not be “lost”. The logic is still affine.]
resource $R$ which is indexed by the round.
This allows to keep track of the round, associating specific resources to each if it has been called during that round already.
The cooperation between client and module necessitates a multi-step process to determine the appropriate degrees in order to remain modular.
First, the client has to define a well-founded set of degrees $\degree[B]$ with designated top and bottom elements $\top_\bdegset$ and $\bot_\bdegset$, respectively.
Second, the module defines its module degrees $\mdegset$ in terms of $\bdegset$, providing a strict-order preserving embedding of type $\bdegset \embedsinto \mdegset$.
Note that previously all embeddings were defined by the client.
Third, as before, the client embeds $\mdegset$ into the universe of degrees:

\forall \colorbox{greenbg}{$\degree[B]$}. \exists \degree[M],
\colorbox{greenbg}{$(\degembedding{B} : \bdegset \embedsinto \mdegset)$}, \lev.
\forall (\degembedding{\degree[M]} : \degree[M] \embedsinto \Degdom),
(\levembedding{M} : \lev \embedsinto \Levdom).
\langle \vec{x} \, \eventually[\colorbox{greenbg}{$r$}]\, X.\, P \rangle
\spac \textcolor{black}{e} \spac
\langle \vec{v}. Q \rangle_{\mask}^{\lev}$.

\begin{align*}
& \setlength\fboxsep{1pt}
\forall \Phi,\aalpha,\abeta,O,\colorbox{greenbg}{$R$}.\, \colorbox{greenbg}{$R(\mynone)$} \ast  \obligations{O} \ast \lev \prec O \ast \callp{\degree[\top_\mdegset]} \ast \langle \vec{x} \overset{\abeta}{\eventually[\colorbox{greenbg}{$r$}]}\, X \underset{\aalpha}{|} \vec{v}.\, Q \vs \Phi \rangle_{\top\setminus\mask}^{\lev;O} \wand \wpre {e\, \aalpha\, \abeta} \Phi \\
& \setlength\fboxsep{1pt}
\langle \vec{x} \overset{\abeta}{\eventually[\colorbox{greenbg}{$r$}]} X.\, P \underset{\aalpha}{\mid} \vec{v}. Q \vs \Phi \rangle^{\lev;O}_{\mask} \proves \pvs[\mask][\emptyset] \exists \vec{x}.\, P \ast{} \\
& \setlength\fboxsep{1pt}
\qquad \bigl( (\forall O'.\, \colorbox{greenbg}{$(\exists r_0. R(r) \ast (r_0 = r \lor \callp{\degree[\top_\bdegset]}))$} \ast \obligations{O'} \ast \lev \prec O' \ast \vec{x} \not\in X \wand{}\\
& \setlength\fboxsep{1pt}
\qquad \qquad
\bswpre \abeta [\mask] {\colorbox{greenbg}{$R(r)$} \ast \obligations{O'} \ast \colorbox{greenbg}{$\callp{\degree[\bot_\bdegset]}$} \ast \vsabort}) \land{} \\
& \setlength\fboxsep{1pt}
\qquad \,\, (\colorbox{greenbg}{$R(\_)$} \ast \obligations{O} \ast \vec{x} \in X \wand \bswpre \aalpha [\emptyset] {\vscommit}) \bigl.\bigr) \\
\end{align*}

An important change to note is the call permission's degree returned by , now at the degree $\bot_\bdegset$.
Nevertheless, because the module picks its module degrees after $\bdegset$, it can embed $\bdegset$ in such a way into its module degrees $\mdegset$ so that $\bot_\bdegset$ suffices to fuel the blocking module's busy-waiting loop.
At the same time, the module degrees $\mdegset$—and in particular $\top_\mdegset$—can be chosen in such a way that the module can provide with call permission at $\top_\bdegset$ for each new round.
For example, if $\ddegset$ was the set of degrees required to perform the busy-waiting loop's body, the following definition of $\mdegset$ would support compensating $n$ many rounds of waiting:
$\mdegset \eqdef \ddegset \plusprec \bdegset \plusprec ()$.
Concretely, this setup suffices to prove the 's waiting.

§ CASE STUDIES

The following case studies have been mechanized in the research prototype tool.
C and versions of both and have been implemented and verified and are available at <https://github.com/verifast/verifast/tree/master/examples/busywaiting/flexiblespecs/ticketlock-java>.

§.§ Unfair locks

Section <ref> serves as a small case study on the simple unfair lock module, the .

§.§ Fair locks

We give the shared specification of acquire and release for both and .
The specification of release looks like a regular logically atomic triple but is modified to apply , in order to run auxiliary code at the linearization point.

\begin{align*}
& \forall{\bdegset}.\exists \degree[\modid],\levset{\modid}.\forall \degembedding{\modid},\levembedding{\modid}.\\
& \qquad
\{ \TRUE \}
~ {\color{black}\small \texttt{create} ~ {\color{black} ()}} ~
\{ \lambda v.\, \islock^{\namesp}_{\gamma}(x) \} \\
& \qquad
\islock^{\namesp}_{\gamma}(x) \proves \\
& \qquad\qquad
\langle o,b \eventually[o] (\mathbb{N} \times \set{false}).\, L(x,o,b) \rangle
~ {\color{black}\small \texttt{acquire} ~ x} ~
\langle L(x,o,\mytrue) \ast b = \myfalse \rangle_{\namesp}^{\lev} \\
& \qquad\qquad
\langle L(x,o,\mytrue) \rangle
~ {\color{black}\small \texttt{release} ~ x} ~
\langle L(x,o + 1,\myfalse) \rangle_{\namesp} \\
\end{align*}

For , the definitions of $\islock$ and $L$ are given in Figure <ref>.

The is simple yet interesting.
It consists of two fields owner and next, initialized to zero.
During acquire (see Figure <ref>), the next field is atomically incremented with the fetch-and-add (FAA) instruction, returning the old value i.e. the ticket.
The lock is locked if the owner's value is less than the next ticket's value.
An acquire call successfully acquired the lock if the taken ticket is equal to the owner field, which is checked in a busy-waiting loop.
Releasing the lock increments the owner counter by one (see Figure <ref>).
For simplicity we use FAA for this operation too, but an increment in two steps is also possible because the owning thread is the only one allowed to mutate owner.

Implementation of module operations and proof outline for acquire. The proof outline also refers to definitions in Figure <ref>. alone will be used in the implementation. Its specification is given in Figure <ref>.

The is clearly fair, everyone waits for their turn.
More interestingly, the lock has two possible linearization points.
The first is inside the acquire code when the FAA of next returns the same value as owner.
The second occurs if the call to acquire has to busy-wait.
In that case the predecessor's release increments the owner field thus passing ownership directly.
To prove this instance of helping, we add the auxiliary field /*AUs*/ to store the s corresponding to the waiting thread's atomic updates.
Additionally, we add the auxiliary variable /*held*/ in order to hide the implementation detail of the that it is locked when the value of owner is less than the value of next.
Specifically, this allows us to hide the fact that releasing the while another thread is waiting passes the ownership directly without “actually” unlocking the lock by toggling the /*held*/ boolean within an atomic block.
This induces an artificial state change from unlocked to locked, allowing us to satisfy the atomic precondition of acquire for the next owner.
The owner field can be abstractly thought of as the blocking module's round as discussed at the end of Section <ref>.

The proof outline in Figure <ref> gives the most salient proof states.
Figure <ref> shows the definitions of predicates $L$ and $\mathit{is\_lock}$.

Proof of acquire
acquire is given a call permission at degree $\degree[\top_{\degree[FL]}]$, the linear resource $R$ used later to keep track of the rounds, the resource tracking the set of obligations with the lock-appropriate lower-bound, and the atomic update resource.
The first execution step is an atomic block wrapping the FAA that obtains the ticket.
In order to modify next we open $\mathit{is\_lock}^{\namesp}_{\gamma}$.
This lets us update next as required.
The remaining code of the atomic block is auxiliary code.
First, it computes the number of tickets ahead in line: /*diff*/.
It lowers the call permission $\callp{\degree[\top_{\degree[FL]}]}$ correspondingly, receiving the necessary call permissions (at degree $\degree[\top_{\degree[B]}]$) to fuel the rounds of waiting later on.
Then, it checks whether the linearization point is now i.e. when the obtained ticket immediately matches the owner.
In that case the client's is run immediately, storing the atomic updates' universally quantified predicate in the invariant at the corresponding position in the map of the big separating conjunction of $\mathit{is\_lock}^{\namesp}_{\gamma}$.
Otherwise, while the auxiliary code stores in /*AUs*/, the proof puts the matching atomic update resource in the module's invariant.
The atomic update resource is stored together with a later credit <cit.> to facilitate the helping by the matching release.
After the atomic block's single step, the invariant inside $\mathit{is\_lock}^{\namesp}_{\gamma}$ is closed again.

⟨(o,b) [o]  ℕ ×.  Ł(x,o,b) | (Ł(x,o,) ∗b = Φ)⟩_⊤∖^;O

\begin{align*}
& \color{black} \L(x,o,b) \eqdef x.\ownfld \xmapsto{\sfrac{1}{2}} o \ast x.\heldfld \xmapsto{\sfrac{1}{2}} b \\
& \lkAU(O,\aalpha,\abeta) \eqdef \theatomicupdate \\
& \color{black} \lockinv(x,\gammao,\gamman,\gammaM) \eqdef \exists o, n, b.\,  x.\ownfld \xmapsto{\sfrac{1}{2}} o \ast x.\nextfld \mapsto n \ast x.\heldfld \xmapsto{\sfrac{1}{2}} b \ast{} \\
& \color{black} \qquad (b \leftrightarrow o < n) \ast \textlog{mono}_\gammao(o) \ast \textlog{mono}_\gamman(n) \ast \textlog{GhostMapAuth}^{\gamma_\mapn}(\mapn) \ast \dom(\mapn) = [0,n) \lor{} \\
& \color{black} \qquad \Sep_{k \mapsto (\gamma,\Phi,O,\aalpha,\abeta) \in \mapn} \left(
\begin{array}{l}
(\lkAU(O,\aalpha,\abeta) \ast \laterCredit{1} \ast o < k) \lor (\Phi \ast o = k) \lor (\tok_\gamma \ast o \geq k)
\end{array} \right) \\
& \color{black} \islock^{\namesp}_{\gammao,\gamman,\gammaM}(x) \eqdef \knowInv{\namesp}{\lockinv(x,\gammao,\gamman,\gammaM)}
\end{align*}

Predicates $\mathit{is\_lock}$ and $L$ used in the proof of .

At this point, just before the busy-waiting while loop, we own: the token for the current ticket, the call permissions to supply to at round changes and a lower bound on the owner field.
The lower bound is justified by the $\textlog{mono}$ camera in the invariant, enforcing that the owner field increases monotonically.

For the while loop, we repeatedly open the module invariant.
Once the taken ticket and the owner field's value match, the loop terminates and we swap the token $\mathit{tok}_{M(t).0}$ for the universally quantified predicate required for the method's postcondition.
Otherwise, we use to justify busy-waiting for the lock to be unlocked.
Inside the loop we note the owner ticket last seen by us.
If the owner ticket and our last impression do not match, is supplied with a new call permission at degree $\degree[\top_{\degree[B]}]$.
At most ${\color{myghostcode}\small \texttt{diff}}$ many ownership changes (rounds) of the may be observed until the ticket must match the owner field.

Proof of release

The release proceeds similarly but additionally immediately applies the 's opening view shift in order to increment the owner field.
It executes its after setting /*held*/ to false, thus matching the atomic postcondition.
If a waiting thread exists, it additionally executes the next thread's atomic update by opening the matching stored atomic update resource (in $\mathit{is\_lock}^{\namesp}_{\gamma}$) and running the stored in the auxiliary field /*lk.AUs*/.
It then puts the universally quantified postcondition of the next owner's atomic update into the invariant in order to be able to close the module invariant again.

Specification of the alone API.

Lock cohorting <cit.> (Figure <ref>) is a design pattern to construct non-uniform memory access (NUMA) aware locks from NUMA unaware locks.
Specifically, s employ one top-level lock shared by all cohorts, plus a local lock per cohort.
To own a , both the local lock and the top-level lock must be owned.
The crux lies in the 's release procedure.
When there are many threads of the same cohort trying to access the same , it would be wasteful to pass the lock between cohorts because of cache misses.
The effect is even more pronounced on NUMA architectures.
Therefore, release queries the current owner's local lock to see if it is alone.
If it is not, and the threshold has not been reached yet, the local lock is released without releasing the top-level one.
That is the lock is passed between the current owner and the next thread in line locally.
Threads of other cohorts, on the other hand, are overtaken.
Starvation is prevented—if the underlying locks are starvation-free themselves—via the threshold that prevents one cohort from monopolizing the lock.

The local locks must support alone queries in order to determine when it is possible to handoff the lock.
alone makes an effort to check if other threads are waiting.
Its specification is shown in Figure <ref>.
Calls to alone are allowed to return true even if threads are waiting, but they must not return false if no threads are waiting.
Moreover, we do not consider cancellation and therefore alone must not return true if it has previously returned false for the same round (see alone's precondition in Figure <ref>).
We represent the knowledge that a lock owner is not alone and that ownership transfers immediately upon release, as is the case for , as follows (see NotAloneElim in Figure <ref>).
If $\texttt{alone}~x$ returns false while the $o$'th owner holds lock $x$, it produces a $\notalone(x, o)$ token that satisfies the law $L(x,o + 1,b) * \notalone(x, o) \vsW[\namesp] \FALSE$, i.e. if the $o$'th owner is not alone, then after the $o$'th owner releases the lock, the $o+1$'th owner immediately holds the lock and there is no intermediate machine state where the lock is not held.

. CC means current cohort.

We proved that this lock implementation satisfies total correctness per our fair lock specification, assuming only that the s used in turn satisfy our fair lock specification. We machine-checked our proof (albeit not foundationally) using the program verifier.

A core design decision of the proof is that |acquire| creates a
signal (which we call the acquire signal) during the
|ticketlock_acquire LL| call's linearization point (LP), but only if
|lk.passing[CC]| is false, and discharges it during
|ticketlock_acquire TL|'s LP. Similarly, |release| creates
a signal (the release signal) during the
|ticketlock_release TL| call's LP (again, if not passing) and discharges it during the |ticketlock_release LL| call's LP.
If the beta passed into |ticketlock_acquire LL| is executed, some other thread in the cohort holds |LL|, and either 1) has not yet acquired |TL|, 2) holds |TL|, or 3) has released |TL|. Correspondingly, this beta waits either for this thread's acquire signal, calls the client's beta, or waits for the thread's release signal.
If the beta passed into |ticketlock_acquire TL| is executed, some other cohort holds |TL|. At most |MAX| number of successive threads of that cohort own the lock, so at most |MAX| rounds of the client's beta have to be called.

§ RELATED WORK

Prior work on obligations and signals (the moral equivalent being also sometimes called capabilities or credits) has mostly addressed the safety property deadlock-freedom under primitive blocking <cit.>, or termination with primitive blocking <cit.>.
This line of work has proven the applicability of obligations to many kinds of primitive blocking, from locks to channels to monitors, whereas here we only show our approach for locks.
We believe the other use cases can be handled similarly.
Recent work <cit.>, adapted the system to busy-waiting i.e. without the assumption of primitive blocking but did not address the problem of one-size-must-fit-all specifications.
We adopt and extend this approach to handle lock handoffs and a higher-order programming language.

<cit.> present , an extension of the logic <cit.> to modularly reason about termination of busy-waiting programs.
Indeed, their paper is a major inspiration for this work.
Modules written in their While-like first-order language can be modularly reasoned about with their proof system.
The details of their proof system are quite different from ours although it also prominently features “obligations”.
For them, subjective obligations (subjective in the sense of <cit.>) are a logic level construct that distinguishes between the current thread's perspective and everyone else: the environment.
They too use a well-founded set of layers (our levels) to prevent circular dependencies and are thus able to express environment liveness assumptions and prove them correct.
While they do show that their system supports lock handoffs, they do not argue for its usefulness in the implementation of advanced locks.
They prove the implementation of a CLH lock <cit.>, exercising their fair specification, and a for their unfair specification.
Furthermore, multiple lock clients are shown, among them a blocking counter and lock-coupling sets.
We believe that the fair specifications of and our approach are equally powerful but our unfair specifications are stronger because we do not require a budget to be defined up front for an unfair lock.
This allows us to prove their “tricky client” <cit.> example although we also do not immediately see its usefulness.
Unlike its predecessor  <cit.>, which received tool support in  <cit.>, does not have tool support.
Conveniently, we inherit <cit.>'s tool support for obligations, signals, call permissions and wait permissions (renamed as expect permissions in this paper) as auxiliary code.
Hence, we obtained tool support by translating the presented specification approach into terms.
Finally, 's logic is first-order and requires stability checks, whereas we use higher-order logic that does not feature unstable assertions.

Although Iris <cit.> is fundamentally limited to safety properties due to its use of step-indexing, many approaches have been developed to work around this limitation.
Iris' mechanization in features a total weakest precondition that ensures safe termination by never generating laters.
This, however, rules out Löb induction and prohibits the use of higher-order resources that require the laters for soundness.
<cit.>'s Transfinite Iris switches the step-index from natural numbers to ordinals solving the biggest issue of a fuel-based approach at the logic level, obviating the need for auxiliary code.
They support termination-preserving refinement between two programs.
Additionally they prove that they can prove modular termination of single-threaded programs by proving termination-preserving refinement between an ordinal and the target program.
Currently, Transfinite Iris loses widely used reasoning rules due to its transfinite step-indexing.
Nevertheless, there are recent developments using it e.g. <cit.>.
More importantly, however, Transfinite Iris did not address concurrent programs under fair scheduling, and it is not clear to us how to reason about fair scheduling in the logic itself.
<cit.> support termination-preserving refinement for concurrent programs.
They only support stuttering for a fixed, finite, number of steps and do not support unbounded nondeterminism.
Trillium <cit.> considers a more general form of refinement between traces of a program and a model.
Fairis, an instantiation of Trillium for reasoning about concurrent programs under fair scheduling, allows them to reason about liveness properties, including termination.
They, foundationally, prove termination of a program of two threads decrementing a non-deterministically initialized counter.
The two threads share a boolean which they toggle back and forth, one thread only decrements the counter when the boolean is true, the other if it is false.
Thus far this line of refinement reasoning does not support abstract, modular specifications.

§ CONCLUSION AND FUTURE WORK

In this paper, we demonstrated modular programming for blocking modules in a concurrent, higher-order programming language that enforces termination through erasable obligations, signals, expect permissions and call permissions.
The key insight is to apply <cit.>'s higher-order programming perspective for specifying concurrent modules to the auxiliary code justifying termination.
This lets busy-waiting blocking modules depend on necessarily client-dependent termination arguments in a well-defined, procedure-modular manner.
Moreover, we illustrate how the logic can be used to reason about the resulting language and code.
Specifically, we show that the derived specification approach is modular and expressive.
In particular, we provide general and abstract specifications to unfair and fair lock modules and show that s and s implement them, respectively.
The modularity of these specifications is exemplified by a that relies and adheres to our fair specification.
The is able to encapsulate its internal use of lock handoffs, making use of the added flexibility that passing erasable code provides.
The (non-foundational) mechanization in accompanying this paper serves as validation of the presented approach.
To the best of our knowledge it includes the first mechanized proof of a .

We identify three key directions for future work.
First, in this paper we presented how Iris can be used to reason about programs.
The implementation and proof of the leveraged 's higher-order nature and Iris' ability to reason about helping.
Another key strength of Iris with respect to the verification of concurrent modules is its support for erasable prophecy variables to reason about future-dependent linearization points.
inherits support for prophecy variables but, as presented, cannot read them in erasable code.
One is therefore unable to reason about future-dependent linearization points in blocking modules.
To address this limitation, we plan to modify prophecy variables, allowing auxiliary code to read them.
We suspect that this might additionally allow attaching prophecy resolutions to logically atomic operations, not just atomic operations, a current limitation <cit.>.
Second, a natural next step would then be to integrate the presented work and this extension in a mechanization.
This would give foundational backing to our approach.
Third, we would like to integrate with other tools and their corresponding logics to prove the general applicability of the approach.
We believe that such integrations should be straightforward as long as the tool and logic support reasoning about (erasable) closures.

This research is partially funded by the Research Fund KU Leuven, and by the Flemish Research Programme Cybersecurity.

#1     #1#1#1     #1     #1     #1     #1#1          #1#1

[Alpern and Schneider(1985)]
authorpersonBowen Alpern and personFred B.
Schneider. year1985.
Defining Liveness.
journalInf. Process. Lett. volume21,
number4 (year1985), pages181–185.

[Birkedal et al(2021)]
authorpersonLars Birkedal, personThomas
Dinsdale-Young, personArmaël Guéneau,
personGuilhem Jaber, personKasper Svendsen, and
personNikos Tzevelekos. year2021.
Theorems for free from separation logic
journalProc. ACM Program. Lang.
volume5, numberICFP (year2021),

[Boström and Müller(2015)]
authorpersonPontus Boström and
personPeter Müller. year2015.
Modular Verification of Finite Blocking in
Non-terminating Programs. In booktitle29th European
Conference on Object-Oriented Programming, ECOOP 2015, July 5-10, 2015,
Prague, Czech Republic (seriesLIPIcs,
Vol. volume37), editorpersonJohn Tang
Boyland (Ed.). publisherSchloss Dagstuhl - Leibniz-Zentrum
für Informatik, pages639–663.

[Coupet-Grimal and Delobel(2006)]
authorpersonSolange Coupet-Grimal and
personWilliam Delobel. year2006.
An effective proof of the well-foundedness of the
multiset path ordering.
journalAppl. Algebra Eng. Commun. Comput.
volume17, number6 (year2006),

[da Rocha Pinto et al(2014)]
authorpersonPedro da Rocha Pinto,
personThomas Dinsdale-Young, and personPhilippa
Gardner. year2014.
TaDA: A Logic for Time and Data Abstraction. In
booktitleECOOP 2014 - Object-Oriented Programming - 28th
European Conference, Uppsala, Sweden, July 28 - August 1, 2014. Proceedings
(seriesLecture Notes in Computer Science,
Vol. volume8586), editorpersonRichard E.
Jones (Ed.). publisherSpringer, pages207–231.

[Dershowitz and Manna(1979)]
authorpersonNachum Dershowitz and
personZohar Manna. year1979.
Proving Termination with Multiset Orderings.
journalCommun. ACM volume22,
number8 (year1979), pages465–476.

[Dice et al(2012)]
authorpersonDavid Dice, personVirendra J.
Marathe, and personNir Shavit.
Lock cohorting: a general technique for designing
NUMA locks. In booktitleProceedings of the 17th ACM
SIGPLAN Symposium on Principles and Practice of Parallel Programming,
PPOPP 2012, New Orleans, LA, USA, February 25-29, 2012,
editorpersonJ. Ramanujam and
personP. Sadayappan (Eds.). publisherACM,

[Dice et al(2015)]
authorpersonDavid Dice, personVirendra J.
Marathe, and personNir Shavit.
Lock Cohorting: A General Technique for Designing
NUMA Locks.
journalACM Trans. Parallel Comput.
volume1, number2 (year2015),

[D'Osualdo et al(2021)]
authorpersonEmanuele D'Osualdo, personJulian
Sutherland, personAzadeh Farzan, and personPhilippa
Gardner. year2021.
TaDA Live: Compositional Reasoning for Termination
of Fine-grained Concurrent Programs.
journalACM Trans. Program. Lang. Syst.
volume43, number4 (year2021),

[Filliâtre et al(2016)]
authorpersonJean-Christophe Filliâtre,
personLéon Gondelman, and personAndrei
Paskevich. year2016.
The spirit of ghost code.
journalFormal Methods Syst. Des.
volume48, number3 (year2016),

authorpersonRobert W Floyd.
Assigning meanings to programs. In
booktitleProceedings of Symposia in Applied Mathematics,
Vol. volume19. pages19–32.

[Guéneau et al(2023)]
authorpersonArmaël Guéneau,
personJohannes Hostert, personSimon Spies,
personMichael Sammler, personLars Birkedal, and
personDerek Dreyer. year2023.
Melocoton: A Program Logic for Verified
Interoperability Between OCaml and C.
journalProc. ACM Program. Lang.
volume7, numberOOPSLA2, Article
articleno247 (dateoct year2023),
numpages29 pages.

[Guerraoui et al(2018)]
authorpersonRachid Guerraoui, personHugo
Guiroux, personRenaud Lachaize, personVivien
Quéma, and personVasileios Trigonakis.
Lock-Unlock: Is That All? A Pragmatic Analysis of
Locking in Software Systems.
journalACM Trans. Comput. Syst.
volume36, number1 (year2018),

[Herlihy and Wing(1990)]
authorpersonMaurice Herlihy and
personJeannette M. Wing. year1990.
Linearizability: A Correctness Condition for
Concurrent Objects.
journalACM Trans. Program. Lang. Syst.
volume12, number3 (year1990),

[Iris contributors(2022)]
authorpersonIris contributors.
titleThe Iris 4.0 Reference.

[Jacobs et al(2018)]
authorpersonBart Jacobs, personDragan
Bosnacki, and personRuurd Kuiper.
Modular Termination Verification of Single-Threaded
and Multithreaded Programs.
journalACM Trans. Program. Lang. Syst.
volume40, number3 (year2018),

[Jacobs and Piessens(2011)]
authorpersonBart Jacobs and personFrank
Piessens. year2011.
Expressive modular fine-grained concurrency
specification. In booktitleProceedings of the 38th ACM
SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL
2011, Austin, TX, USA, January 26-28, 2011,
editorpersonThomas Ball and personMooly
Sagiv (Eds.). publisherACM, pages271–282.

[Jung et al(2016)]
authorpersonRalf Jung, personRobbert
Krebbers, personLars Birkedal, and personDerek
Dreyer. year2016.
Higher-order ghost state. In
booktitleProceedings of the 21st ACM SIGPLAN
International Conference on Functional Programming, ICFP 2016, Nara, Japan,
September 18-22, 2016, editorpersonJacques
Garrigue, personGabriele Keller, and personEijiro
Sumii (Eds.). publisherACM, pages256–269.

[Jung et al(2018)]
authorpersonRalf Jung, personRobbert
Krebbers, personJacques-Henri Jourdan, personAles
Bizjak, personLars Birkedal, and personDerek
Dreyer. year2018.
Iris from the ground up: A modular foundation for
higher-order concurrent separation logic.
journalJ. Funct. Program.  volume28
(year2018), pagese20.

[Jung et al(2020)]
authorpersonRalf Jung, personRodolphe
Lepigre, personGaurav Parthasarathy, personMarianna
Rapoport, personAmin Timany, personDerek Dreyer,
and personBart Jacobs. year2020.
The future is ours: prophecy variables in
separation logic.
journalProc. ACM Program. Lang.
volume4, numberPOPL (year2020),

[Jung et al(2015)]
authorpersonRalf Jung, personDavid Swasey,
personFilip Sieczkowski, personKasper Svendsen,
personAaron Turon, personLars Birkedal, and
personDerek Dreyer. year2015.
Iris: Monoids and Invariants as an Orthogonal Basis
for Concurrent Reasoning. In booktitleProceedings of the
42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming
Languages, POPL 2015, Mumbai, India, January 15-17, 2015,
editorpersonSriram K. Rajamani and
personDavid Walker (Eds.). publisherACM,

authorpersonNaoki Kobayashi.
A New Type System for Deadlock-Free Processes. In
booktitleCONCUR 2006 - Concurrency Theory, 17th
International Conference, CONCUR 2006, Bonn, Germany, August 27-30, 2006,
Proceedings (seriesLecture Notes in Computer Science,
Vol. volume4137), editorpersonChristel
Baier and personHolger Hermanns (Eds.).
publisherSpringer, pages233–247.

[Leino et al(2010)]
authorpersonK. Rustan M. Leino, personPeter
Müller, and personJan Smans.
Deadlock-Free Channels and Locks. In
booktitleProgramming Languages and Systems, 19th European
Symposium on Programming, ESOP 2010, Held as Part of the Joint European
Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus,
March 20-28, 2010. Proceedings (seriesLecture Notes in
Computer Science, Vol. volume6012),
editorpersonAndrew D. Gordon (Ed.).
publisherSpringer, pages407–426.

[Ley-Wild and Nanevski(2013)]
authorpersonRuy Ley-Wild and
personAleksandar Nanevski. year2013.
Subjective auxiliary state for coarse-grained
concurrency. In booktitleThe 40th Annual ACM
SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL
'13, Rome, Italy - January 23 - 25, 2013,
editorpersonRoberto Giacobazzi and
personRadhia Cousot (Eds.). publisherACM,

authorpersonWaiman Long.
booktitlelocking/rwsem: Implement lock handoff to
prevent lock starvation.

[Magnusson et al(1994)]
authorpersonPeter S. Magnusson, personAnders
Landin, and personErik Hagersten.
Queue Locks on Cache Coherent Multiprocessors. In
booktitleProceedings of the 8th International Symposium on
Parallel Processing, Cancún, Mexico, April 1994,
editorpersonHoward Jay Siegel (Ed.).
publisherIEEE Computer Society, pages165–171.

[Morris and Jones(1984)]
authorpersonF. Lockwood Morris and
personCliff B. Jones. year1984.
An Early Program Proof by Alan Turing.
journalIEEE Ann. Hist. Comput.
volume6, number2 (year1984),

[Mulder and Krebbers(2023)]
authorpersonIke Mulder and personRobbert
Krebbers. year2023.
Proof Automation for Linearizability in Separation
journalProc. ACM Program. Lang.
volume7, numberOOPSLA1 (year2023),

[Owicki and Gries(1976)]
authorpersonSusan S. Owicki and
personDavid Gries. year1976.
Verifying Properties of Parallel Programs: An
Axiomatic Approach.
journalCommun. ACM volume19,
number5 (year1976), pages279–285.

authorpersonFilip Pizlo.
booktitleLocking in WebKit.

authorpersonFilip Pizlo.
booktitleWTF::Lock should be fair eventually.

[Reinhard and Jacobs(2021a)]
authorpersonTobias Reinhard and personBart
Jacobs. year2021a.
Ghost Signals: Verifying Termination of Busy
Waiting - Verifying Termination of Busy Waiting. In
booktitleComputer Aided Verification - 33rd International
Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part
II (seriesLecture Notes in Computer Science,
Vol. volume12760), editorpersonAlexandra
Silva and personK. Rustan M. Leino (Eds.).
publisherSpringer, pages27–50.

[Reinhard and Jacobs(2021b)]
authorpersonTobias Reinhard and personBart
Jacobs. year2021b.
titleGhost Signals: Verifying Termination of Busy-Waiting
(Technical Report).

[Spies et al(2021)]
authorpersonSimon Spies, personLennard
Gäher, personDaniel Gratzer, personJoseph
Tassarotti, personRobbert Krebbers, personDerek
Dreyer, and personLars Birkedal.
Transfinite Iris: resolving an existential dilemma
of step-indexed separation logic. In booktitlePLDI '21:
42nd ACM SIGPLAN International Conference on Programming Language Design
and Implementation, Virtual Event, Canada, June 20-25, 2021,
editorpersonStephen N. Freund and
personEran Yahav (Eds.). publisherACM,

[Spies et al(2022)]
authorpersonSimon Spies, personLennard
Gäher, personJoseph Tassarotti, personRalf
Jung, personRobbert Krebbers, personLars Birkedal,
and personDerek Dreyer. year2022.
Later credits: resourceful reasoning for the later
journalProc. ACM Program. Lang.
volume6, numberICFP (year2022),

[Tassarotti et al(2017)]
authorpersonJoseph Tassarotti, personRalf
Jung, and personRobert Harper.
A Higher-Order Logic for Concurrent
Termination-Preserving Refinement. In booktitleProgramming
Languages and Systems - 26th European Symposium on Programming, ESOP 2017,
Held as Part of the European Joint Conferences on Theory and Practice of
Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings
(seriesLecture Notes in Computer Science,
Vol. volume10201), editorpersonHongseok
Yang (Ed.). publisherSpringer, pages909–936.

[Timany et al(2024)]
authorpersonAmin Timany,
personSimon Oddershede Gregersen, personLéo
Stefanesco, personJonas Kastberg Hinrichsen,
personLéon Gondelman, personAbel Nieto, and
personLars Birkedal. year2024.
Trillium: Higher-Order Concurrent and Distributed
Separation Logic for Intensional Refinement.
journalProc. ACM Program. Lang.
numberPOPL (year2024).

authorpersonAlan Turing.
Checking a large routine. In
booktitleReport of a Conference on High Speed Automatic
Calculating Machines. pages67–69.

[Vogels et al(2015)]
authorpersonFrédéric Vogels,
personBart Jacobs, and personFrank Piessens.
Featherweight VeriFast.
journalLog. Methods Comput. Sci.
volume11, number3 (year2015).

[Wolf et al(2021)]
authorpersonFelix A. Wolf, personMalte
Schwerhoff, and personPeter Müller.
Concise Outlines for a Complex Logic: A Proof
Outline Checker for TaDA. In booktitleFormal Methods - 24th
International Symposium, FM 2021, Virtual Event, November 20-26, 2021,
Proceedings (seriesLecture Notes in Computer Science,
Vol. volume13047), editorpersonMarieke
Huisman, personCorina S. Pasareanu, and
personNaijun Zhan (Eds.). publisherSpringer,

authorpersonPeter Zijlstra.
booktitlelocking/mutex: Add lock handoff to avoid

* 's syntax is defined in Figure <ref>.

* 's state is defined in Figure <ref>.

* 's pure and boxed reduction rules are defined in Figure <ref>.

* 's impure reduction steps are shown in Figure <ref>.

* 's evaluation contexts are defined in Figure <ref>.

* 's extensions over are defined in Figure <ref>.

* 's big-step evaluation relation is defined in Figure <ref>.

The state interpretation to tie the state of Figure <ref> follow the general pattern of tying the physical state to the ghost state of Iris.
Iris' authoritative camera <cit.> is used to store the authoritative fragment in the state interpretation, allowing fragments to be given out.
The authoritative part in the state interpretation makes sure that at every step the ghost state matches the physical state.
Call permissions may slightly diverge between the ghost and physical state due to the automatic selection of call permissions by our auxiliary code, as discussed in Section <ref>.
The proof may pick “worse” call permissions to be consumed with respect to the path.
Therefore, the physical stock of call permissions may always be weakened to the Iris view of the stock.

, mostly identical to  <cit.>.
Auxiliary code added by is highlighted in blue.
Note the additional argument to fork, explained in Figure <ref>.

's state. This figure is adapted from <cit.>. The additions for auxiliary state are shown in blue.

HeapLang pure and boxed reduction rules. This figure is taken from <cit.>.

's impure head reduction rules. Taken from the Iris technical documentation <cit.>.

evaluation contexts. The let construct is added but not auxiliary code.
Auxiliary code added by is highlighted in blue.

Operations of that extend or modify .

Adapted from the Iris technical documentation <cit.>.

A big-step evaluation relation for a subset of . Importantly, fork is not supported. does not feature atomic blocks and does not feature this big-step relation.

\begin{align*}
\bswp \eqdef{}& \lambda \mask, \expr, \pred. \All \istate, n_s, \vec\obs, n_t. \stateinterp(\istate, n_s, \vec\obs, n_t) \vsW[\mask][\mask] {}\\
& \Exists \istate', v. \ulcorner \expr, \istate \Downarrow v, \istate' \urcorner \ast \stateinterp(\istate', n_s, \vec\obs, n_t) \ast \pred(v) {}\\
\bswpre\expr[\mask]{\Ret\val. \prop} \eqdef{}& \bswp(\mask,\expr,\Lam\val.\prop)
\end{align*}

Our weakest precondition for big-step evaluation.
Unlike Iris' general weakest precondition <cit.>, the big-step weakest precondition is specialized to and in particular a fixed state interpretation. Moreover, it directly uses the big-step evaluation relation defined on a subset of that notably excludes the fork command. Finally, never allows non-stuck computations.

[_1][_2] [_2]. [_2][_1]

$\lctx$ is a context
[]. (())[]. ()[].

Reasoning rules for $\textdom{wp}^{\Downarrow}$. Here, “context” really refers to a list of -specific context items (cf. <cit.>).