非阻塞算法的形式化建模与分析

Formal modeling and analysis of non-blocking algorithm

目前针对非阻塞(Non-blocking)同步算法的实现已有大量研究,但在实践应用中受到阻碍。其中的关键问题是在没有自动垃圾回收机制(GC)的环境中,如何安全地回收这些数据结构对象中删除掉的动态节点所占用的内存。一个有效的解决方案是Michael提出的风险指针,同时,这种内存管理方法也提供了ABA问题的一个解决方案。将应用该内存回收方法于非阻塞同步算法中,使用CIVL验证框架对其进行形式化建模,并提取内存管理方面的性质进行验证。实验结果表明,应用了该内存回收算法的非阻塞模型不仅功能正确,同时也能够避免内存管理方面的问题。

At present,there are a lot of researches on the implementation of non-blocking synchronization algorithms,but they are hindered in practice.The key issue is how to safely reclaim the memory occupied by the dynamic nodes which have been deleted from the data structure objects in an environment without an automatic Garbage Collection(GC)mechanism.An effective solution is hazard pointer proposed by Michael.At the same time,this memory management method also provides a solution to the ABA problem.This memory reclamation method was applied to the non-blocking synchronization algorithm,and CIVL(Concurrency Intermediate Verification Language)verification framework was used to formally model it and verify the properties related to memory management.Experimental result shows that the non-blocking model applied with this memory reclamation algorithm is not only functionally correct,but also avoids memory management problems.