A separation logic to verify termination of busy-waiting for abrupt program exit
Tobias Reinhard, Amin Timany, Bart Jacobs · 2020
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.