基于内存回收方案的非阻塞算法的形式化分析

本文是计算机论文，本文主要针对两类内存回收方案进行研究，并使用形式化验证工具CIVL对其进行形式化建模并分析其安全性和可靠性。其中一个是Michael提出的风险指针，它通过维护一个保存了存在访问风险的指针引用的数组来检测安全的内存回收时机。对该方案的形式化分析基于先进先出的队列结构，从队列的基本结构、内存管理、风险指针的应用以及队列的操作四个方面进行建模；并将正确性和与内存相关的性质使用同一形式化语言进行描述。RCU方案则在那些读、写操作强度不对称，对读操作的性能要求较高的场景中具有非常大的优势。RCU方案的核心内容是宽限期机制，在对该方案的形式化分析中利用了CPU的状态信息来检测宽限期的结束，即当宽限期开启后，若CPU发生一次上下文切换则意味着该CPU上的读线程一定已经执行结束。本文将针对基于多CPU核心的经典RCU方案进行形式化建模与验证。宽限期的界定是经典RCU方案的核心内容，读线程需要在执行完成后提供一个信号以确定宽限期的结束。由于读端临界区不允许被抢占，这样，当一个读线程结束时，它所在的CPU必定会进行一次上下文切换，或者陷入内核态的程序由内核态转为用户态，或者本CPU进入空闲状态。

第1章绪论

作为计算机重要的组成部分，同时也是关键的核心软件系统，操作系统的行为更是需要进行严格、精确的定义和验证。操作系统中出现的大量问题都和并发技术的实现有密切的关系。随着并发系统规模的增大，非阻塞算法成为并发技术中的一个研究热点。非阻塞算法通过特定的原子操作实现并发算法，保证一个线程的延迟或失败不会影响其他线程。这种同步方法天然地避免了传统互斥锁固有的问题，同时具有良好的可伸缩性以及在高并发下显著的性能。同时其实现也更加复杂，这给其正确性和安全性的验证带来了挑战。非阻塞算法实现的关键问题是在没有GC机制的环境中，如何安全地回收这些数据结构对象中删除掉的动态节点所占用的内存。无论是出现内存泄露，还是不安全的回收引起的非法访问等问题，都存在致命隐患。例如美国航天局(NASA)的勇气号火星车，由于其存储系统模块存在着一个边界错误[6][20]，该错误在密集测试与审查中并未检测出，然而却在非常小概率的情况下触发，进而导致整个系统瘫痪。随着互联网的飞速发展，软件和程序已经变得越来越复杂。一旦出现故障，修复起来将是牵一发而动全身，有限的知识和人力无法应对这种复杂的局面，于是诞生了软件工程理论[7]，它提供了一套针对软件开发过程中各个周期的工程化方法以保证软件质量。与此同时，人们也提出了另一种理论来指导软硬件开发实践，通过严谨的数学技术来描述和验证系统，检验其产生的形式化模型的性质，以提高软硬件设计的可靠性，即形式化方法（FormalMethods）[9][10]。目前，利用严格的形式化方法被公认为是能够保证系统正确性和安全性的可靠手段。

第2章预备知识

2.1非阻塞算法

非阻塞算法通常应用在没有GC机制的环境中，在这种情况下，由于需要一个有效的手段安全地回收这些对象中删除掉的动态节点所占用的内存，该方法在实践中难以广泛应用。在没有GC机制的环境中，动态创建的非阻塞数据结构的对象无法被自动销毁，此时将会产生内存泄漏问题。另一方面，对于非阻塞算法而言，由于在删除一个节点时可能还有其他并发的线程占用该节点，所以不能立即回收节点所占内存，否则后续将会出现非法访问内存问题。在传统基于互斥锁的同步方法中，访问共享节点前加锁，这保证了此时只有该线程独占指向该节点的指针，因此能够安全回收内存。而在非阻塞算法中，很难确认其他线程是否持有某个节点的引用。这种情况下，对于内存的访问是无法预测的，因此导致了内存回收上的困难。关于非阻塞算法中的内存回收问题在很多论文中已有研究，例如基于引用计数的方案[28]，基于静止期的方案[29]，以及一些依赖特别的硬件支持[30]或需要满足特殊形式算法[31]的内存回收机制等等。这些解决方案可以大致分为两类：基于时间点的和基于指针的。基于时间点的解决方案通过要求线程等待一段时间，在这段时间过后的一个时间点，所有线程都不再持有共享数据节点的引用，此时可以将其安全地释放。然而，遵循规范的开发流程也难以保证软件完全不出现错误，尤其是软件测试[8]阶段，一般来说很难提供完备的测试用例。特别在安全攸关系统中更是无法容忍。

2.2内存回收问题

这类解决方案中并发的读写操作是以非阻塞方式执行的，但等待安全回收时间点的阶段是阻塞的。基于指针的方案则保存着并发操作中具有访问风险的节点指针，以此来标记不能立刻回收的节点内存，直到记录清除以后，就可以回收这些节点的内存了。基于指针的实现是非阻塞的，但由于需要记录具有风险的指针，因此会带来额外的开销，以及算法上的复杂性。形式化方法的思路是利用严格定义的数学概念和语言，用自动化或半自动化的工具对程序进行分析和验证，主要包括定理证明[32]和模型检验[33]。定理证明技术将软件系统以及系统性质的刻画都使用逻辑方法进行规约，依据选定的逻辑体系中的推导规则等进行推理证明，验证性质公式是否满足。定理证明技术能够对系统有较精确的描述，其对使用者的数学背景知识以及逻辑功底有很高的要求，并且在一些关键的推导路径中需要人工的辅助才能完成，因此自动化程度受到一定限制。还有一种半形式化的技术，即等价性验证[41]，它与前两者不同，验证的是设计是否一致。这种技术中一般采用符号和增量的方法，而且由于和硬件电路紧密结合，所以电路验证的一些传统方法也大量应用此种方法，比如ATPG技术等。非阻塞算法是并发数据结构技术中的一个热点，它能保证某个线程的失败或任意延迟不会影响其他线程取得进展，保证整个程序的持续前进。这大大提高了并发性能，与此同时其实现也更加复杂。本章将对非阻塞算法相关的预备知识，其中的关键问题，以及形式化方法的相关技术进行简单介绍，使读者有一个整体性的认识。

第3章总体架构和验证框架..............................................................9
3.1总体架构..........................................................................................................9
3.2验证框架........................................................................................................10
3.3本章小结........................................................................................................17
第4章风险指针形式化分析............................................................19
4.1风险指针方案................................................................................................19
4.2形式化建模....................................................................................................20
4.3性质的提取....................................................................................................27
4.4验证与分析....................................................................................................31
第5章基于多核的RCU机制形式化分析.....................................33
5.1RCU机制......................................................................................................33
5.2总体设计........................................................................................................34
5.3形式化建模....................................................................................................36

第5章基于多核的RCU机制形式化分析

5.1RCU机制

RCU机制同风险指针方案一样要解决在并发情况下安全回收已删除节点内存的问题，其经典实现是让读者在访问被RCU方案保护的数据结构时不允许被抢占。在这样的环境中，所有线程将运行到完成所有操作，或自愿放弃所拥有的CPU资源时，这样可以方便为更新端提供一个信号用于确定在此之前开始的读者已经执行结束。更新端等待其他读者完成的时间段称为宽限期。宽限期的确定是RCU方案的核心机制。RCU方案将更新端和读端的同步过程拆分为“删除”和“回收”两个阶段，如图5.1所示：图中下方从左至右是更新线程执行的三个阶段，上方每一个矩形框代表一个读线程。当更新线程执行完删除操作后，开始等待持有已删除节点引用的读线程。如果不等待其完成，将来使用该引用访问的时候就会发生不可预料的后果。宽限期机制确定了安全回收的时机，解决了有关内存管理的问题；订阅发布机制则提供了两个原语用于保证数据被修改的同时也能安全地访问，避免编译器或CPU对程序代码重排序造成的安全问题；保存最近更新数据对象的多个版本有利于数据对象的安全更新，尽管存在数据不一致或旧数据的情况，但这在大量的实际应用场景中都不是问题，一个经典的例子是路由表的更新。RCU方案可以看作是读写锁的改进版本，但不同的是读写锁允许多个读操作并发执行，而不允许读操作和写操作或多个写操作并发执行。表5.1列举了二者的主要特点。从表中可以看出，与读写锁相比，RCU方案不仅允许读者和写者同时操作，而且RCU方案保护的读者还可以安全地升级为写者，并且不会引起死锁。这是由于RCU的读端原语通常不允许阻塞，而在读写锁中进行这种升级则会带来死锁的问题。

5.2总体设计

经典RCU方案的实现是不允许读端临界区的代码在执行期间被本CPU上的其他线程抢占，所以对于单CPU核心的环境，更新端执行完成时不会存在读端线程持有已删除节点的引用，即在此之前开始执行的读线程都已结束，可以立即回收。因此，应用在单CPU核心上的RCU方案实现退化为各线程互斥进行，显然其正确性及安全性可以满足，本文不对此进行验证。对于多CPU核心的环境，多个线程同时执行，更新端线程执行结束需要经过宽限期的阶段，等待每一个CPU上的读操作结束，才能完成已删除节点的回收。根据经典RCU方案的三个基本机制以及5.2节的总体设计，RCU方案的形式化建模主要从CPU建模、宽限期建模、内存回收建模、RCU原语建模以及验证场景建模五个方面来介绍：CPU模型为方便分配多个线程的CPU以及静止状态的记录；宽限期模型描述了对每一个CPU静止状态的记录和宽限期结束的检测过程；内存回收模型是当宽限期结束时描述如何进行已删除节点的回收；RCU原语模型将应用于读端和更新端代码中；验证场景模型则提供了应用RCU方案的一种具体的并发场景。图5.3为RCU方案的建模整体框架图。关于内存结构以及内存操作的建模与第4章中风险指针方案对应的建模方式相同，此处不再赘述。

第6章总结与展望

因此，对该方案的建模从CPU状态建模、RCU原语建模和验证场景建模三个方面介绍，同时针对程序的正确性和内存安全性相关的性质进行形式化描述。根据验证结果及分析可以得出，在所有可能的并发执行情况下，风险指针方案和RCU方案的形式化模型均满足提取的相应性质。本文的主要工作是对非阻塞算法中的内存回收问题进行研究，并对其中两种有效的解决方案进行形式化分析。下一步工作可以从以下几个方面继续研究：在风险指针的形式化分析中，为降低模型复杂度，将其应用在先进先出的队列结构中，主要有出队和入队两个基本操作，该队列依赖于链表实现，而链表有着更普遍的数据操作方式，因此接下来可以将风险指针应用在单链表或双链表中，进一步分析验证风险指针方案的应用情况；RCU方案的宽限期机制是该方案的重点内容，为了及时回收内存，不仅依靠CPU的状态信息，还需要其他信息如系统中断等尽快完成静止态的检测，接下来可以考虑更复杂的情况以验证RCU方案的有效性；在Linux内核中，RCU方案的多核实现采用了分层的实现，通过树的结构将静止态信息高效地整合，对于宽限期的嵌套带来极大的便利，下一步工作可以将此结构添加到RCU方案的形式化模型中。
参考文献（略）