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

摘要

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