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

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

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.

Ghost Signals: Verifying Termination of Busy-Waiting (Extended Version)

Programs for multiprocessor machines commonly perform busy waiting for synchronization. We propose the first separation logic for modularly verifying termination of such programs under fair scheduling. Our logic requires the proof author to associate a ghost signal with each busy-waiting loop and allows such loops to iterate while their corresponding signal $s$ is not set. The proof author further has to define a well-founded order on signals and to prove that if the looping thread holds an obligation to set a signal $s^\prime$, then $s^\prime$ is ordered above $s$. By using conventional share…

关键软件的半自动化模块化形式验证：活性和完备性阈值

Semi-Automated Modular Formal Verification of Critical Software: Liveness and Completeness Thresholds

本论文提出两项贡献：一是用于公平调度下忙等待程序终止性验证的分离逻辑，二是将有界内存安全证明简化为有界证明的完备性阈值概念，并刻画了数组遍历程序的阈值。

TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs

We present TaDA Live, a concurrent separation logic for reasoning compositionally about the termination of blocking fine-grained concurrent programs. The crucial challenge is how to deal with abstract atomic blocking: that is, abstract atomic operations that have blocking behaviour arising from busy-waiting patterns as found in, for example, fine-grained spin locks. Our fundamental innovation is with the design of abstract specifications that capture this blocking behaviour as liveness assumptions on the environment. We design a logic that can reason about the termination of clients which use …