  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.
