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. 2020. A Separation Logic to Verify Termination of Busy-Waiting for Abrupt Program Exit. Accepted at Formal Techniques for Java-like Programs. 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.