幽灵信号：验证忙等待的终止性（扩展版）
计算机科学中的逻辑
2021-05-19 v2 编程语言
摘要
多处理器机器的程序通常执行忙等待以进行同步。我们提出了首个用于在此类程序在公平调度下模块化验证终止性的分离逻辑。我们的逻辑要求证明作者为每个忙等待循环关联一个幽灵信号，并允许此类循环在其对应信号 未被置位时迭代。证明作者还需在信号上定义良基序，并证明若循环线程负有置位信号 的义务，则 序高于 。通过使用常规共享状态不变量将幽灵信号的状态与数据结构的状态相关联，可以验证针对任意数据结构上任意条件进行忙等待的程序。
引用
@article{arxiv.2010.11762,
title = {Ghost Signals: Verifying Termination of Busy-Waiting (Extended Version)},
author = {Tobias Reinhard and Bart Jacobs},
journal= {arXiv preprint arXiv:2010.11762},
year = {2021}
}
备注
68 pages; 42 figures; Simplified logic by removing permissions and updated soundness proof in appendix. Simplified the logic's presentation. Added case studies to appendix.; This is the extended version of a paper which is to be published at CAV21