A well-established approach to proving progress properties such as deadlock-freedom and termination is to associate obligations with threads. For example, in most existing work the proof rule for lock acquisition prescribes a standard usage protocol by burdening the acquiring thread with an obligation to release the lock. The fact that the obligation creation is hardcoded into the acquire operation, however, rules out non-standard clients e.g. where the release happens in a different thread. We overcome this limitation by instead having the blocking operations take the obligation creation operations required for the specific client scenario as arguments. We dub this simple instance of higher-order programming with auxiliary code Sassy. To illustrate Sassy, we extend HeapLang, a simple, higher-order, concurrent programming language with erasable code and state. The resulting language gets stuck if no progress is made. Consequently, we can apply standard safety separation logic to compositionally reason about termination in a fine-grained concurrent setting. We validated Sassy by developing (non-foundational) machine-checked proofs of representative locks -- an unfair Spinlock (competitive succession), a fair Ticketlock (direct handoff succession) and the hierarchically constructed Cohortlock that is starvation-free if the underlying locks are starvation-free -- against our specifications using an encoding of the approach in the VeriFast program verifier for C and Java.

翻译：证明死锁自由性和终止性等进展性质的一种成熟方法是将义务与线程相关联。例如，在现有大多数工作中，锁获取的证明规则通过让获取线程承担释放锁的义务来规定标准的使用协议。然而，由于义务创建被硬编码到获取操作中，这排除了非标准客户端（例如在不同线程中执行释放操作的情况）。我们通过让阻塞操作将特定客户端场景所需的义务创建操作作为参数来克服这一限制。我们将这种带有辅助代码的高阶编程的简单实例称为Sassy。为说明Sassy，我们扩展了HeapLang——一种简单、高阶、并发的编程语言，使其包含可擦除代码和状态。所得语言在未取得进展时会陷入阻塞。因此，我们可以应用标准的安全分离逻辑来组合推理细粒度并发环境中的终止性。我们通过在VeriFast程序验证器（针对C和Java）中对方法进行编码，针对代表性锁开发了（非基础性的）机器验证证明来验证Sassy：非公平的自旋锁（竞争式继承）、公平的票据锁（直接移交继承）以及分层构建的队列锁（若底层锁无饥饿性则该锁也无饥饿性）。