操作系统作为计算机软件系统的核心部分,其正确性与可靠性等的保证一直以来都是学术界和工业界努力的方向,而操作系统中出现的大量问题都和并发技术的实现有关。随着并发系统规模的增大,非阻塞算法成为并发技术中的一个研究热点。非阻塞算法在硬件提供的特定原子操作的基础上实现并发算法,保证一个线程的延迟或失败不会影响其他线程。这种同步方法天然地避免了传统互斥锁固有的死锁、锁护航、优先级倒置等问题,同时具有良好的可伸缩性以及在高并发下显著的性能。与此同时,其实现也更加复杂,这给其正确性和安全性的验证带来了挑战。目前针对非阻塞算法的实现已有大量研究,其中的关键问题是在没有自动垃圾回收机制(Garbage Collection,GC)的环境中,如何安全地回收这些数据结构对象中删除掉的动态节点所占用的内存。本文针对其中的两种内存回收方案进行研究,其中简单而高效的一个方案是Michael提出的风险指针(Hazard Pointers),另一个是已经被引入到Linux内核中的非阻塞同步机制——RCU(ReadCopy-Update)。本文将分析这两类内存回收方案,使用CIVL(the Concurrency Intermediate Verification Language)验证框架对其进行形式化建模,提取内存管理方面的性质,并验证其正确性和安全性。使用形式化方法对非阻塞算法的两种典型内存回收方案进行建模与验证分析,为今后基于非阻塞算法的系统开发等工作打下了基础,也为其他并发技术的分析与研究起到了促进作用。