Programs for multiprocessor machines commonly perform busy-waiting for synchronization. We propose a separation logic using so-called ghost signals to modularly verify termination of such programs under fair scheduling. Intuitively spoken, ghost signals lift the runtime concept of wait-notify synchronization to the verification level and allow a thread to busy-wait for an event $X$ while another thread promises to trigger $X$.
Recommended citation for TR: Tobias Reinhard and Bart Jacobs. Ghost Signals: Verifying Termination of Busy-Waiting (Technical Report) 2020. https://people.cs.kuleuven.be/~tobias.reinhard/ghostSignals–TR.pdf