A Separation Logic to Verify Termination of Busy-Waiting for Abrupt Program Exit
Published in FTfJP, 2020
Recommended citation: Tobias Reinhard, Amin Timany, and Bart Jacobs. A Separation Logic to Verify Termination of Busy-Waiting for Abrupt Program Exit. Accepted at Formal Techniques for Java-like Programs (2020). https://dl.acm.org/doi/10.1145/3427761.3428345
[Bibtex]
Programs for multiprocessor machines commonly perform busy-waiting for synchronisation. In this paper, we make a first step towards proving termination of such programs. We approximate (i) arbitrary waitable events by abrupt program termination and (ii) busy-waiting for events by busy-waiting to be abruptly terminated.
We propose a separation logic for modularly verifying termination (under fair scheduling) of programs where some threads eventually abruptly terminate the program, and other threads busy-wait for this to happen.
This paper’s accompanying technical report can be found here.
The slides of the presentation held at FTfJP 2020 can be found here.