A Separation Logic to Verify Termination of Busy-Waiting for Abrupt Program Exit
Logic in Computer Science
2020-10-19 v2 Programming Languages
Abstract
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.
Cite
@article{arxiv.2010.07800,
title = {A Separation Logic to Verify Termination of Busy-Waiting for Abrupt Program Exit},
author = {Tobias Reinhard and Amin Timany and Bart Jacobs},
journal= {arXiv preprint arXiv:2010.07800},
year = {2020}
}
Comments
7 pages, 11 figures, accepted at FTfJP 2020, corresponding technical report: arXiv:2007.10215