  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.
The latter uses 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.
  In the paper we present specifications and proofs in Iris. 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 VeriFast program verifier for C and Java. This fair lock
is implemented on top of another fair lock module and involves lock handoff,
thus exercising the asserted contributions.
