Ghost Signals: Verifying Termination of Busy-Waiting (Extended Version)

TL;DR

This paper introduces a novel separation logic framework for verifying the termination of busy-waiting loops in multiprocessor programs, using ghost signals and well-founded orders to ensure correctness under fair scheduling.

Contribution

It presents the first modular verification method for busy-waiting termination using ghost signals and formal obligations, extending verification capabilities to arbitrary data structures and conditions.

Findings

First separation logic for busy-waiting termination verification

Allows modular proofs with ghost signals and obligations

Applicable to arbitrary data structures and conditions

Abstract

Programs for multiprocessor machines commonly perform busy waiting for synchronization. We propose the first separation logic for modularly verifying termination of such programs under fair scheduling. Our logic requires the proof author to associate a ghost signal with each busy-waiting loop and allows such loops to iterate while their corresponding signal $s$ is not set. The proof author further has to define a well-founded order on signals and to prove that if the looping thread holds an obligation to set a signal $s^\prime$, then $s^\prime$ is ordered above $s$. By using conventional shared state invariants to associate the state of ghost signals with the state of data structures, programs busy-waiting for arbitrary conditions over arbitrary data structures can be verified.