[Pre-Print] Ghost Signals: Verifying Termination of Busy-Waiting

Published in arxiv.org, 2020

Recommended citation: Tobias Reinhard and Bart Jacobs. Ghost Signals: Verifying Termination of Busy-Waiting. 2020. https://arxiv.org/abs/2010.11762
[Bibtex]

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$.

Paper
Technical Report (Full formalization and proofs.)

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
[Bibtex]