A Separation Logic to Verify Termination of Busy-Waiting for Abrupt Program Exit: Technical Report

Research output: Working paperResearch

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.
Original languageEnglish
Publication statusPublished - Jul 2020

Bibliographical note

22 pages, 14 figures, Technical report (replacement: corrected citation in conclusion)

    Research areas

  • cs.LO, cs.PL, F.3.1; D.2.4

See relations at Aarhus University Citationformats

ID: 193242591