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

2020/07/24 by Reinhard, Tobias, Timany, Amin, Jacobs, Bart
#D.2.4 #F.3.1 #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Programming Languages (cs.PL)

paper · doi:10.48550/arxiv.2010.07800

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.

Related

• A Separation Logic to Verify Termination of Busy-Waiting for Abrupt Program Exit: Technical Report
• Ghost Signals: Verifying Termination of Busy-Waiting (Extended Version)
• Semi-Automated Modular Formal Verification of Critical Software: Liveness and Completeness Thresholds
• Modular termination verification with a higher-order concurrent separation logic (Intermediate report)
• Semantics and Termination of Simply-Moded Logic Programs with Dynamic Scheduling