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.

翻译：忙碌等待是一种重要的底层同步模式，用于实现更高级的同步抽象。其终止依赖于其他线程的协作以及公平的线程调度器。我们提出了一种基于高阶分离逻辑的通用方法，用于模块化验证忙碌等待的并发程序。该方法结合了先前两个方向的研究：一是Jacobs和Piessens（2011）提出的用于验证并发模块的高阶编程视角；二是Reinhard和Jacobs（2021）提出的用于验证忙碌等待的幽灵信号方法。后者采用经典规范描述同步构造，其中模块创建并解除义务。然而，此类规范固定了特定的客户端模式，通常需要“义务转移”来处理更复杂的等待依赖关系，这阻止了客户端执行锁移交——一种控制锁（非）公平性的重要机制。我们的贡献——受D'Osualdo、Sutherland、Farzan和Gardner（2021）的TaDA Live启发——要求客户端在必要时创建并解除义务，以满足模块的活性需求。但我们并非将这些活性需求内置于逻辑中，而是通过让模块的操作将辅助代码作为参数来表达，这些辅助代码负责生成模块在忙碌等待时所需的调用权限。在本文中，我们使用Iris逻辑给出了规范与证明。我们通过在VeriFast程序验证器（针对C和Java）中对我们的方法进行编码，开发了一个队列锁的（非基础性）机器校验证明（据我们所知，这是首个此类证明），从而验证了我们的方法。该公平锁构建在另一个公平锁模块之上，并涉及锁移交，从而实践了所提出的贡献。