发表机构
School of Computing, University of Kent（肯特大学计算学院）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
针对无锁算法重试循环验证难题，提出循环片段与同步点概念，实现有限操作语义，高效验证安全属性并修复释放后使用错误。
AI 中文摘要
无锁同步算法通常以可能失败的操作（如比较并交换（CAS））实现，这些操作被包裹在无界重试循环中。验证此类算法需要考虑任意多次失败的迭代，产生庞大的状态空间，并发线程的交错进一步加剧了这一问题。先前的工作丢弃了失败的迭代，认为它们在循环后的状态中不留下痕迹。然而，编译器和硬件会重排指令，且加载-存储重排可能跨越失败迭代的边界，引入微妙的并发错误。我们演示了这样一个错误，使得在先前验证过的读-复制-更新（一种在Linux内核中广泛采用的同步原语）变体中可能发生释放后使用，并提供了验证过的修复。我们发现无锁算法中的实际重试遵循一种常见模式。我们引入了循环片段，一种对无界重试循环的语义刻画，在许多实际情况下可语法识别，以及同步点，即在循环片段内限制指令重排和状态空间的操作。我们证明了SMRD——一种允许加载-存储重排的C11程序符号事件结构语义——在无界循环是片段式的程序中具有有限表示。我们进一步引入了一种有限操作语义，使得安全属性可以在有限步骤内得到验证。对于所演示的释放后使用错误，验证只需对程序进行单次遍历，时间复杂度与程序规模线性相关。我们提供了SMRD的参考实现，复现了该错误并验证了修复，并在Isabelle/HOL中机械化操作语义以及最小错误及其修复。
英文摘要
Lock-free synchronisation algorithms are often implemented with fallible operations, such as compare-and-swap (CAS), wrapped in unbounded retry loops. Verifying such algorithms requires considering arbitrarily many failing iterations, yielding large state spaces, compounded by the interleavings of concurrent threads. Prior work discarded failing iterations, arguing that they leave no trace in the post-loop state. Compilers and hardware reorder instructions, and load-store reorderings may cross the boundaries of failing iterations, introducing subtle concurrency bugs. We demonstrate one such bug, making use-after-free possible in a previously verified variant of Read-Copy-Update - a synchronisation primitive widely adopted in the Linux Kernel - and we provide and verify a fix. We find that practical retries in lock-free algorithms adhere to a common pattern. We introduce episodic loops, a semantic characterisation of unbounded retry loops which is syntactically recognisable in many practical cases, and synchronisation points, operations that bound both instruction reordering and state space within episodic loops. We show that SMRD - a symbolic event structure semantics for C11 programs which allows for load-store reordering - admits a finite representation in programs where unbounded loops are episodic. We further introduce a finitary operational semantics that allows safety properties to be verified in finitely many steps. For the use-after-free bug we demonstrate, verification takes a single pass over the program, linear in the program size. We provide a reference implementation of SMRD reproducing the bug and verifying the fix, and mechanise the operational semantics together with the minimal bug and its fix in Isabelle/HOL.
Comments115 pages (42 pages main text plus appendices), 19 figures, 2 tables. Reference implementation: https://github.com/christiankissig/mordor ; Isabelle/HOL mechanisation: https://github.com/christiankissig/isa-smrd-opsem
