论文标题
幽灵信号：验证忙碌的终止（扩展版本）
Ghost Signals: Verifying Termination of Busy-Waiting (Extended Version)
论文作者
论文摘要
多处理器机器的程序通常会忙于等待同步。我们建议在公平计划下模块化验证此类程序的第一个分离逻辑。我们的逻辑要求证明作者将幽灵信号与每个忙碌的待循环相关联，并允许此循环进行迭代，同时未设置其相应的信号$ s $。证明作者还必须在信号上定义一个有充分的订单，并证明，如果循环线程有义务设置信号$ s^\ prime $，则$ s^\ prime $在$ s $以上订购。通过使用常规的共享状态不变性将幽灵信号状态与数据结构的状态相关联，可以验证忙于任意条件的程序，以任意数据结构为单位。
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 shared state invariants to associate the state of ghost signals with the state of data structures, programs busy-waiting for arbitrary conditions over arbitrary data structures can be verified.
