论文标题
分离逻辑，以验证忙碌的终止因突然计划退出的终止：技术报告
A Separation Logic to Verify Termination of Busy-Waiting for Abrupt Program Exit: Technical Report
论文作者
论文摘要
多处理器机器的程序通常会执行忙碌的同步。在本文中，我们迈出了证明终止此类计划的第一步。我们通过突然终止程序终止和（ii）忙于忙于忙碌的待招呼，以突然终止事件来近似（i）任意等待事件。 我们建议对程序进行模块化验证终止的分离逻辑（在公平的计划下），其中一些线程最终突然终止了程序，而其他繁忙等待的线程会发生这种情况。
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.
