Verifying Concurrent Memory Reclamation Algorithms with Grace
Verifying Concurrent Memory Reclamation Algorithms with Grace
复制标题
优雅地验证并发内存回收算法
DOI：
--
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
Hongseok Yang
中科院分区：
文献类型：
--
作者：
Alexey Gotsman;N. Rinetzky;Hongseok Yang
内存管理是现代并发算法中最复杂的方面之一，为它提出的各种技术-如危险指针，读取-复制-更新和基于时期的回收-已被证明是非常具有挑战性的形式化推理。在本文中，我们表明，不同的内存回收技术实际上依赖于相同的隐式同步模式，没有清楚地反映在代码中，但仅在用于论证其正确性的断言的形式。该模式基于宽限期的关键概念，在此期间，线程可以访问某些共享内存单元，而不必担心它们被释放。我们提出了一个模块化的推理方法，动机的模式，以统一的方式处理所有上述三个内存回收技术。通过阐明其基本核心，我们的方法实现了干净和简单的证明，甚至可以扩展到算法的实际实现，而不会显着增加证明的复杂性。我们形式化的方法使用分离逻辑和时序逻辑的组合，并使用它来验证实例的三种方法来内存回收。
Memory management is one of the most complex aspects of modern concurrent algorithms, and various techniques proposed for it--such as hazard pointers, read-copy-update and epoch-based reclamation--have proved very challenging for formal reasoning. In this paper, we show that different memory reclamation techniques actually rely on the same implicit synchronisation pattern, not clearly reflected in the code, but only in the form of assertions used to argue its correctness. The pattern is based on the key concept of a grace period, during which a thread can access certain shared memory cells without fear that they get deallocated. We propose a modular reasoning method, motivated by the pattern, that handles all three of the above memory reclamation techniques in a uniform way. By explicating their fundamental core, our method achieves clean and simple proofs, scaling even to realistic implementations of the algorithms without a significant increase in proof complexity. We formalise the method using a combination of separation logic and temporal logic and use it to verify example instantiations of the three approaches to memory reclamation.