Software Engineering and Formal Methods - 21st International Conference, SEFM 2023, Eindhoven, The Netherlands, November 6-10, 2023, Proceedings
Software Engineering and Formal Methods - 21st International Conference, SEFM 2023, Eindhoven, The Netherlands, November 6-10, 2023, Proceedings
复制标题
软件工程和形式化方法 - 第 21 届国际会议，SEFM 2023，荷兰埃因霍温，2023 年 11 月 6-10 日，会议记录
DOI：
10.1007/978-3-031-47115-5_17
复制
发表时间：
2023
期刊：
影响因子：
--
通讯作者：
Semenyuk M
中科院分区：
文献类型：
--
作者：
Semenyuk M
读取-复制更新（RCU）是一种密钥无锁同步机制，在Linux内核中广泛使用。RCU的一个用途是在诸如C/C++等不支持垃圾收集的语言中进行安全内存回收。然而，RCU的正确性很难验证，即使假设顺序一致（SC）的内存。在本文中，我们开发和验证的RCU实现RC 11（C11弱内存模型的限制版本，其中包括放松和释放获取访问），增加了验证的挑战。我们的证明技术是基于所有权的概念，我们用它来系统地跟踪每个线程的读/写能力，每个内存位置。在我们的证明中，我们扩展了最近的Owicki-Gries逻辑的RC 11，我们联合收割机与我们的所有权模型，以显示正确性。我们所有的证明都是在Isabelle/HOL定理证明器中实现的。
Read-Copy Update (RCU) is a key lock-free synchronisation mechanism that is used extensively in the Linux kernel. One use of RCU is safe memory reclamation in languages such as C/C++ that do not support garbage collection. Correctness of RCU is, however, difficult to verify, even when assuming sequentially consistent (SC) memory. In this paper, we develop and verify an RCU implementation under RC11 (a restricted version of C11 weak memory model, which includes relaxed and release-acquire accesses), increasing the verification challenge. Our proof technique is based on a notion of ownership, which we use to systematically track each thread’s read/write capabilities to each memory location. In our proof, we extend a recent Owicki-Gries logic for RC11, which we combine with our ownership model to show correctness. All our proofs have been mechanised in the Isabelle/HOL theorem prover.