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

作     者：杨兰兰 郭建 YANG Lanlan;GUO Jian

作者机构：华东师范大学软件工程学院上海200062 

出 版 物：《计算机应用》 (journal of Computer Applications)

年 卷 期：2020年第40卷第S2期

页      面：106-111页

学科分类：08[工学] 0812[工学-计算机科学与技术（可授工学、理学学位）] 081202[工学-计算机软件与理论] 

基　　金：国家自然科学基金重点项目(61532019)。 

主　　题：非阻塞算法 形式化建模 风险指针 ABA问题 CIVL验证框架 

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