Published in , 2021
We propose a separation logic using so-called ghost signals to modularly verify termination of busy-waiting 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: Tobias Reinhard and Bart Jacobs. Ghost Signals: Verifying Termination of Busy-Waiting. 2021. https://drive.google.com/file/d/1oCCyINFeHxo4HPIadRTCj1u6i2kQPZB_/view