ECOOP 2020
Sun 15 - Tue 17 November 2020 Online Conference
co-located with SPLASH 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 events by abrupt program termination and 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.