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

TL;DR

This paper introduces a separation logic framework to verify the termination of busy-waiting programs on multiprocessor systems, focusing on scenarios where threads wait for or cause abrupt program termination.

Contribution

It presents a novel separation logic approach for modularly verifying termination of busy-waiting programs with abrupt termination behavior.

Findings

First formal verification method for busy-waiting termination

Handles arbitrary waitable events via abrupt termination approximation

Proves termination under fair scheduling assumptions

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.