PDF非阻塞数据结构的正确性证明
非阻塞同步在可伸缩性和实时响应方面可以产生惊人的效果，但代价是验证状态空间。
Mathieu Desnoyers，EfficiOS
您已决定使用非阻塞数据结构，现在需要确保其正确性。这该如何实现呢？
当多线程程序由于频繁获取互斥锁而速度过慢时，程序员的典型反应是质疑这种互斥是否真的必要。如果互斥锁仅保护对单个变量的访问，并且在每个站点都使用单条指令执行访问，则这种疑问会更加明显。移除同步可以提高性能，但这样做是否会在不损害程序正确性的前提下完成呢？
能否实现这一壮举——以及能否将其扩展到涉及更复杂数据结构的算法——取决于变量与程序其余部分的关系。它还取决于编译器、架构和操作系统的细节，以及本文通篇讨论的其他有趣方面。
非阻塞数据结构27 可用于线程之间的通信，而无需使用互斥或其他同步，否则会导致一个线程阻塞等待另一个线程。本文着眼于使非阻塞数据结构设计和实现变得棘手的原因，并调查了建模技术和验证工具，它们可以为这些算法的正确性提供有价值的反馈。
是什么使非阻塞数据结构编程变得棘手？
在编程非阻塞数据结构时，需要考虑许多方面，包括语言和架构内存模型、原子性、排序、线性化能力和性能。
内存模型
除非程序员提供显式的关键字或同步提示，否则 C、C++ 和 Java 等编程语言会假定单个线程执行变量访问，从而使多处理器系统上非同步并发数据访问的行为要么未定义，要么程序员对其了解不足。然而，随着多核和多处理器计算机变得普及，允许并发执行非常重要。在并发系统中提供一致性的常用方法之一是使用临界区和互斥来确保可串行化，5 这最终通过排除其他执行线程并发访问临界区来创建顺序代码区域。不幸的是，在许多情况下，尤其是在考虑扩展到多个核心时，这种方法不会产生最佳性能。然而，通过缩短临界区的持续时间来放宽顺序执行会增加复杂性。
人们通常使用volatileC 和 C++24 中的关键字来指示变量可以在其当前作用域之外被修改，从而禁用可能干扰程序正确性的优化。但是，此关键字仅告诉编译器假定变量可能在本地线程之外被修改，并且需要保留单个线程内 volatile 访问之间的顺序；它对阻止处理器重新排序没有任何作用。 的排序保证volatile关键字在不同语言之间，甚至在语言版本之间也差异很大：例如，volatileJava 中的关键字从 JDK 1.5 开始具有比 JDK 1.4 更严格的内存排序语义。15
原子性
非阻塞数据结构编程的另一个可能问题是，在处理器上原子执行的指令不足以确保其效果以原子方式对其他处理器可见。
未对齐的字大小内存访问就是一个很好的例子：许多架构将允许通过单条指令执行这些操作，但不能保证内存中的结果将以原子方式更新。
另一个例子是非原子读-修改-写操作。尽管某些架构最终可能会将 Ci++语句转换为单条指令，但编译器很可能选择分三条单独的指令执行此操作：从内存加载到寄存器；递增寄存器；将寄存器存储到内存。编译器可能会选择这样做，要么是因为指令集（例如，RISC）要求这样做，要么仅仅是因为寄存器压力过高。此外，例如，对于 Intel x86 指令集，旨在由许多并发运行的处理器以原子方式读取、修改和写入的变量必须具有 LOCK 前缀。23 除非使用特殊的双比较和交换或事务内存指令（如果架构支持），否则需要访问多个字对齐字大小数据结构的内存访问必须在多条指令中执行，因此是非原子的。
最后，允许编译器从内存中重新获取变量。因此，某人可能认为将始终在单次加载操作中执行的操作可能并非如此。
重新排序
出于性能原因，可以在多个级别执行重新排序。首先，许多处理器可以重新排序加载和存储。此外，处理器可以重新排序不具有相互依赖性的指令的执行。最后，只要保留程序顺序，编译器就可以重新排序表达式求值、语句和指令。不幸的是，这些重新排序没有考虑到并发执行的线程可能会假定其他线程执行的操作将从它们自己的角度按程序顺序出现。这就是为什么处理器提供内存屏障指令，而编译器提供编译器屏障。这些操作限制了指令和代码流中跨屏障的重新排序。
重要的是要理解，内存访问的原子性不一定提供排序。在某些架构（如 x86）中，用于指定原子操作的 LOCK 前缀意味着内存屏障。然而，许多其他架构（如 PowerPC、22 ARM2 和 MIPS28）使用 LL/SC（加载链接/存储条件）指令执行其原子操作，并且通常需要显式内存屏障指令来提供排序。
线性化能力
原子性和排序不一定足以确保整个非阻塞数据结构的表现方式与始终按顺序访问的数据结构相同。非阻塞操作通常包含线性化点20，以保证相对于该操作的顺序定义的正确性。线性化点是原子操作，它将执行必要的突变，以提供相对于数据结构的顺序规范的正确外部可观察效果，同时验证操作成功或失败。这确保当更新操作中止时，不会存在全局可见的不一致操作状态。这也确保整个数据结构的行为与按顺序使用数据结构所期望的行为相匹配。应该理解，根据线性化点进行推理存在一些局限性。例如，它不考虑方法调用与其线性化点执行之间的延迟。18,25
以下是线性化问题的一个很好的例子：假设您有一个队列，例如具有无等待入队/阻塞出队的并发队列 (http://lttng.org/urcu)。它在队列尾部入队节点，并从队列头部出队。它通过要求执行出队、拼接和迭代的线程在队列的非尾部节点中找到 NULL 下一个指针时忙等待，从而提供非阻塞（无等待）入队。出队操作一次出队一个节点，而拼接操作将源队列中的所有节点移动到目标队列中。为了说明入队和拼接操作，图 1、2、3、4、5 和 6 将队列节点表示为框。在这些框内，圆圈表示指向下一个节点的指针。灰色圆圈是 NULL 指针。实线箭头表示指针的目标，虚线箭头表示先前的指针目标。包含数字的圆圈表示更新存储在内存中的顺序。
图 1 显示了空队列。入队操作分两步执行，如图 2 和图 3 所示。第一步使用原子交换操作将尾部指针移动到下一个节点。它会导致一个瞬态状态，在此期间，并发执行出队、拼接或迭代的线程需要忙等待。通过将新节点的地址存储到最后一个节点的下一个指针中来完成入队。
执行另一个入队操作会在尾部添加一个新节点 B，因此您最终得到一个具有两个节点 A 和 B 的队列，从而导致图 4 中所示的源队列的初始状态。此图中显示的拼接操作将源队列中的所有节点移动到目标队列中。
请注意，当队列处于瞬态状态时，可能会发生任意数量的操作。例如，这将允许在第一个节点尚未完全入队时完成第二个节点的入队操作，如图 5 所示。当遇到此队列结构时，拼接和出队操作都需要忙等待，直到第一个入队完成。
如图 6 所示，处于瞬态状态的队列引发了对拼接操作进行有趣优化的可能性：当在非空队列中遇到第一个具有 NULL 下一个指针的节点时，可以简单地假设队列为空。毕竟，如果短时间后再次调用拼接操作，则它最终会获得队列内容。不幸的是，即使这种方法乍一看似乎很合适，但它会破坏队列的线性化能力。考虑以下场景：一个线程 X 正在入队节点 A，而另一个线程 Y 首先入队 B，然后执行拼接操作以获取整个队列。给定一个程序，它只有这两个线程，没有其他出队器线程，线程 Y 应该可以期望，如果它执行入队操作，然后执行拼接，则拼接永远不会遇到空队列，因为它必须包含先前入队添加的元素。然而，如果线程 X 在将第一个元素添加到队列时被抢占，则线程 Y 的拼接操作可能会遇到一个看似为空的队列，即使其顺序规范应该允许它假设队列包含至少一个节点。
性能考虑
使非阻塞数据结构编程变得困难的其他因素是与原子访问和内存屏障相关的吞吐量和可伸缩性考虑。根据数据结构的设计和使用，与执行一系列具有自身内存屏障的更昂贵的原子操作相比，持有锁并使用一系列常规非原子指令执行操作在性能方面可能更便宜。因此，性能考虑在很大程度上驱动了原子指令和屏障的仔细选择，以实现更高级别的操作，从而增加了复杂性。
非阻塞数据结构具有许多有趣的属性，例如可重入性和互斥死锁免疫性，以及在某些情况下，良好的可伸缩性和吞吐量。然而，高效地实现它们需要理解与中断和陷阱（在内核级别）、信号（在用户空间级别）、多线程、调度程序抢占和线程迁移的交互，以及低级编译器和处理器方面。
模型
正如上一节关于线性化能力的讨论所示，提供反例是说明非阻塞数据结构设计和实现中问题的好方法。非阻塞算法的设计者应尝试找到能够更深入地理解算法的表示形式，帮助他们考虑尽可能多的竞争场景。这些表示形式不仅可以增强设计者对线程之间详细交互的理解，还可以帮助向他人表达他们的想法。
这使我们想到了代码审查：鼓励许多人思考算法可能出错的不同方式，每个人都有自己的重点和专业知识，与仅让一个人从单一角度看待问题相比，可能会更清楚地了解问题。即使对于个人审查非阻塞算法，这也是一个有用的技巧：一遍又一遍地查看算法，在一天中的不同时刻，在各种上下文中，使用大量的模型来表示算法，将有助于从各个角度进行彻底的研究。
这要求以各种方式表示算法。图表是显示数据结构中各种对象之间关系、内存操作之间的依赖关系以及对象可以经历的各种状态转换的好方法。
上一节中介绍的具有无等待入队/阻塞出队的并发队列说明了如何使用图表来表示非阻塞数据结构。先前的工作提供了表示为图表的数据结构状态的示例：在 RCU（读取-复制-更新）链表和宽限期解释中；12 在 Cliff Click 的哈希表解释中显示哈希表可能处于的各种状态；8 以及在处理器级别显示指令依赖关系。10,11
许多优化编译器在内部使用模型来表示语句之间的依赖关系。它帮助它们移动语句并执行优化，而不会更改程序顺序所看到的行为。其中一些表示形式，仅举几个例子，是 DFG（数据流图），它表示语句之间的数据依赖关系（例如，内存访问或寄存器访问）；CFG（控制流图），它表示语句之间的控制依赖关系（例如，分支或循环）；以及这两者的方便组合 PDG（程序依赖图）。14 在 PDG 级别对算法进行建模对于验证可能很有用，正如将在测试部分中显示的那样。
将算法表示为编程语言中的语句序列是另一种表示形式，它允许以更顺序的方式思考代码。但是，不应假定代码是按顺序执行的。此表示形式仅仅是考虑可能执行的所有重新排序的起点。尽管这听起来可能很傻，但在计算机上、用铅笔和纸张、带或不带对每行可能重新排序的详尽注释编写代码，作为初始草稿，或从内存中重新复制都是与代码交互的不同方式，可以更好地理解代码以某种方式编写的原因。
呈现反例的一种便捷方法是通过两个或多个处理器或线程的并排执行序列来演示竞争场景。首先详细说明算法规范内有效的初始变量状态，然后检查算法的各个部分。这可以通过详细说明程序顺序中每个涉及的处理器或线程的执行序列来实现。然后，可以在编译器和处理器允许的约束范围内更改一个或两个语句的顺序。对于每个修改后的执行场景，应遵守算法正确性施加的所有不变量。如果有可能找到违反这些不变量的场景，则应将其视为错误。它可能是由算法设计问题、缺少内存屏障或对操作序列的原子性的不正确假设引起的。
对于较小的代码片段，移动到指令级范围来表示算法的关键部分可能是值得的。当考虑处理器执行的内存重新排序时，这尤其有用。它可以使编译器退出，并让审查者专注于指令和处理器语义——但代价是模型不够紧凑。
非阻塞算法的问题在于，仅考虑顺序等效的高级算法操作一个接一个地发生是不够的：在算法中的每条指令之后，都需要考虑如果其他处理器可能无限次地执行算法的任何并发操作会发生什么。此外，当没有编译器或处理器级内存屏障时，需要考虑架构规范内允许的每个重新排序。这迅速增加了要考虑的并发执行流的数量，这解释了为什么确保没有执行流会出错很困难。当面临大量要验证的状态时，测试部分中介绍的模型检查器可以非常有助于自动化繁琐且容易出错的验证。
在并发代码段中做出的每个假设都应带有偏见地重新审视。重要的是要确保这些假设在硬件内存模型、编程语言内存模型和更高级别的正确性约束（例如线性化能力）中都成立。对于做出的每个假设，都应尝试多次提出竞争条件，无论它多么牵强，都可能导致算法出错。
模型准确性
为了提出非阻塞算法的准确模型，需要考虑所有目标架构的内存模型。乍一看，非阻塞算法似乎应该专门绑定到单个架构，但是有一些方法可以对非阻塞算法进行建模，从而允许推理它们在大量架构中的正确性。
为了以跨多个架构可移植的方式对算法进行建模，您可以将算法视为在由一组架构可以执行的所有最坏重新排序可能性组成的模型上运行。可以在 Linux 内核 (https://linuxkernel.org.cn)、Userspace RCU 项目 (http://lttng.org/urcu) 和 Concurrency Kit (http://concurrencykit.org) 中找到针对一组架构的内存模型。
因此，算法模型应包含可能发生的最坏情况重新排序，方法是组合所有目标架构的特性。当然，这增加了要验证的状态空间，但好处是拥有一个适用于各种架构的算法模型。证明单个目标架构可能失败足以识别错误。
当以许多架构为目标时，在所有支持的架构下进行压力测试是强制性的，因为可能导致算法出错的某些特定重新排序特性可能仅特定于该组中的一个架构。
以具有较弱内存模型的架构为目标将增加模型状态空间的大小，因为可能会发生更多的重新排序。另一方面，如果涵盖了具有弱内存一致性模型的架构，那么其他具有更严格内存一致性模型的架构（在各方面都与先前验证的模型同等或更严格）将是给定的。
这演示了模型的局限性：它们的完整性不幸地受到它们如何准确地表示架构行为的限制。诸如 litmus 测试之类的技术可以帮助提高模型的准确性。这些将在形式方法部分中讨论。
测试
尽管在设计和实现非阻塞算法时采取了大量的谨慎措施，但始终存在处理器、编译器或操作系统的某些特性被忽视的可能性。因此，没有任何建模或审查可以取代良好的旧测试方法。此外，在移植到未预料到的架构时，测试在发现问题方面非常有效。
当测试非阻塞算法时，与通常的定义相比，测试覆盖率需要稍微调整。实际上，当测试简单的顺序算法时，覆盖大部分行和分支可能很好地表明测试已彻底执行。不幸的是，在测试可以并行执行的算法时，这还不够。测试覆盖率不仅必须检查每行代码和分支是否已执行，还必须检查每个代码和分支是否在其他线程的每个上下文中执行。
这意味着，如果错误是由小的竞争窗口引起的，其中两个指令序列在并发执行时出错，则可能需要很长时间才能在生产中触发错误。因此，适度的测试足以确保常见情况正常工作，但确保极端情况不会出错可能非常具有挑战性。
解决此问题的一种方法是压力测试。当错误条件需要一段时间才能重现时，专注于长时间反复触发竞争条件可以增加更快重现它的机会。可以控制的主要方面是竞争窗口的执行频率。因此，随着要进行压力测试的算法的运行时长度增加，花费在执行每个单独的竞争窗口上的时间比率会减少。
为了加速此过程，您可以使用所谓的“定向压力测试”。这需要根据对设计的理解，在进行压力测试时更改测试台的配置，以便更有可能频繁地命中极端情况。例如，为了压力测试哈希表，有意保持较低数量的存储桶，并使用具有相同键的数千个节点进行测试，这两种方法都可能生成长哈希链。即使经过数周的测试，在没有定向压力测试的情况下，也可能很难使用大型哈希表触发此极端情况。除了配置更改之外，一些工具还可以帮助自动化定向测试：CONCURRIT 可以帮助指定应通过测试运行强制执行的确定性执行顺序；6 Relacy 工具 (http://www.1024cores.net/home/relacy-race-detector) 允许控制线程之间原子操作的交错。
压力测试的另一个技巧是在算法中添加随机延迟，以便测试不同的执行时间。这可以使竞争窗口稍微变大，这可以帮助更快地发现问题。
在确定性多线程方面已经进行了相当多的研究，4,29 它包括使用调度程序确定性地固定临界区的顺序。关于正确性，目标是在运行之间获得可重复的结果，从而使错误在测试中更容易重现。尽管这在某些情况下会产生可接受的结果，但这种方法是否会扩展到细粒度锁定和更大的多处理器系统，同时具有较低的开销，仍有待观察。此方法的局限性包括它要求并发访问使用锁，这比 RCU 和非阻塞同步更昂贵；跟踪具有锁获取频率的模式所需的状态空间大小的增加；锁获取所需的额外通信开销；以及对源代码的小更改可能会显着更改锁访问模式的事实。
当可伸缩性、性能和实时响应很重要时，通过使用测试覆盖率的统计方法而不是在运行时固定锁获取的布局，压力测试可以产生比确定性多线程更好的结果。
模型检查
如果可以通过自动化方式来完成验证非阻塞算法的耗时工作，即手动提出基于并发线程对于线程的任何给定状态可以达到的所有状态的反例，并通过统计方式进行测试，那岂不是很好吗？幸运的是，在某种程度上，有一些方法可以实现这一点。
形式方法
模型检查执行完整的状态空间搜索，以验证给定模型的特定断言。3,7 尽管这种方法非常强大，但它有重要的局限性。首先，执行完整状态空间搜索所需的内存和时间量随着状态空间的大小而快速增长。因此，此方法仅适用于相对较小的模型。这就是为什么保持非阻塞算法在状态空间方面非常紧凑非常重要的原因：它允许更轻松地进行彻底的状态空间搜索。为了确保这一点，应以尽可能减小状态空间的方式设计非阻塞算法。
利用模型检查进行非阻塞算法的一种方法是将算法设计为小型构建块，这些构建块均不超过当前计算机的状态空间搜索能力。然后，每个算法都可以通过 API 提供内存排序保证，并且可以被将使用它的另一个非阻塞算法假定为正确。因此，可以通过在其接口处切割状态空间搜索，将非阻塞算法组合成非常复杂的算法。
模型检查的另一个局限性是，验证的准确性仅与模型和断言一样准确。如果模型与处理器可以执行的重新排序相比过于简单，则检查器不会捕获某些错误。此外，如果断言不能代表要验证的内容，则检查器可能永远不会发现本应捕获的错误。这是因为模型检查器的工作方式有点像预言机：当一切正常时，它们只会报告一切正常。只有当断言失败时，它们才会提供导致问题的详细事件序列。
限制建模错误风险的一种方法是将错误注入到模型中。如果假定给定的模型和断言应捕获一种类型的错误，则应创建一个稍微更改的模型来触发断言，只是为了确保它在有意添加错误时捕获错误。
可用于非阻塞算法的模型检查器包括 Spin，21 它允许在 Promela 中描述模型，并验证该模型上的 LTL（线性时序逻辑）断言。要验证的属性可以像代码中的断言一样简单，但 LTL 的真正强大之处在于它提供了时序运算符。然后，可以验证在达到另一个状态之前永远不会达到某个状态，对于所有可能的执行都是如此。
其他模型检查器专注于在指令级别重现架构行为。先前的文章报道了在各种架构上进行 litmus 测试的结果，以表征它们各自的行为并形式化它们的内存模型。1 作者随后创建了一个工具，该工具允许在验证器中运行 ARM 和 Power litmus 测试 (http://www.cl.cam.ac.uk/~pes20/ppcmem/)。30
关于非阻塞算法模型检查的重要问题是：应该对什么进行建模？在之前的研究中，我提出了一个用于编译器、内存和处理器重新排序的模型。10 其目的是允许在考虑到代码和指令级别的 PDG 依赖关系的模型中表达算法。根据所需的准确度级别、算法的复杂性以及可用于运行模型检查器的资源，可以在模型中包含或省略不同程度的细节。
基于执行的模型检查
通过执行要验证的程序来驱动模型检查器是另一种模型检查方法，称为 EMC（基于执行的模型检查）。13
与其遍历证明条件永远不为假所需的所有状态，不如使用已验证系统执行达到的状态来驱动验证，这可以显着限制要探索的状态数量，但代价是证明的完整性。因此，如果程序的执行导致已验证的条件失败，则会报告该条件失败。但是，不存在错误并不能保证程序的有效性，因为它可能包含其执行未达到的状态中的错误。
在 Linux 内核中实现的 lockdep 验证器9 中可以找到一个很好的 EMC 示例。也许其最重要的验证是通过构建遇到的锁依赖链图，并在锁使用可能触发死锁时报告错误来执行的。值得一提的是，lockdep 可以适用于验证任意应用程序中的锁定，因此任何程序员都可以掌握它。
EMC 可以直接在程序执行的同时执行，也可以基于程序执行的跟踪执行。此执行跟踪可以充当存储驱动脱机模型检查器的事件的容器。
通过数学证明进行形式验证
形式数学证明是验证算法不包含不需要的特征的另一种方法。其思想是从要证明的定理开始。这通常假定某些不变量始终为真。然后，通过基于编译器和处理器内存模型以及算法强制执行的排序约束的归纳来获得证明。可以在文献12,17 中找到形式数学证明的示例，其他作者也提出了关于算法进度和正确性的有趣证明。16,19,26
结论
当涉及到非阻塞算法和数据结构时，我们正在平衡不同的目标。一方面，编译器编写者和芯片设计者希望利用任何未指定行为允许的所有自由。另一方面，并行算法的设计者和开发人员希望在依赖关系排序方面具有精确定义的行为。
非阻塞同步在可伸缩性和实时响应方面可以产生惊人的效果，但其代价是验证状态空间。在具有各自内存模型的多个架构上验证算法也会增加状态空间大小。但是，一旦对最弱的排序约束进行建模，就可以添加符合这些约束的新架构，而无需额外的验证成本，只需进行测试以确保内存模型定义明确即可。
有多种方法可以提高对非阻塞算法的信心，包括定向压力测试、形式和基于执行的模型检查、数学证明和代码审查。鉴于要探索的状态空间随着非阻塞算法的复杂性而迅速增加，因此在设计小型算法时考虑到完整的状态空间验证有助于完整的状态空间验证。然后可以将这些算法组合成更复杂的算法。
随着编程语言对其并发性的感知不断提高，观察编译器级别和静态代码分析器对并发性进行建模和验证的持续进步将是一件有趣的事情。
致谢
感谢 Paul E. McKenney 在 RCU 和非阻塞同步方面的工作，感谢 David Miller 在 Linux 内核原子操作方面的工作，感谢 David Howells 在 Linux 内核原子操作和内存屏障方面的工作，以及感谢 Hugh Dickins 在类型安全内存方面的工作。 还要感谢 Linux 内核社区在非阻塞同步、内存模型和 lockdep 方面的工作和反馈，特别是 Lai Jiangshan、Ingo Molnar、Peter Zijlstra 和 Arjan van de Ven。 我感谢 Paul E. McKenney、Samy Bahra、Christian Babeux、Jeremie Galarneau 和 Michel R. Dagenais 审阅了本文。
法律声明
这项工作代表作者的观点，不一定代表 EfficiOS 的观点。 Linux 是 Linus Torvalds 的注册商标。 其他公司、产品和服务名称可能是其他公司的商标或服务标志。
参考文献
1. Alglave, J., Maranget, L., Sarkar, S., Sewell, P. 2011. Litmus: 针对硬件运行测试。载于第 17 届国际工具与算法构造与分析系统会议论文集: 41-44; http://dl.acm.org/citation.cfm?id=1987389.1987395.
2. ARM. 2010. ARM 架构参考手册; http://infocenter.arm.com/help/index.jsp?topic=/com.arm.doc.set.architecture/index.html.
3. Baier, C., Katoen, J. 2008. 模型检测原理。 剑桥：麻省理工学院出版社； http://books.google.ca/books?id=nDQiAQAAIAAJ.
4. Bergan, T., Anderson, O., Devietti, J., Ceze, L., Grossman, D. 2010. Coredet：用于确定性多线程执行的编译器和运行时系统。 SIGARCH 计算机体系结构新闻 38(1): 53-64; http://doi.acm.org/10.1145/ 1735970.1736029.
5. Bernstein, P., Shipman, D., Wong, W. 1979. 数据库并发控制中可串行化的形式化方面。 IEEE 软件工程汇刊 5(3): 203-216.
6. Burnim, J., Elmas, T., Necula, G., Sen, K. 2012. CONCURRIT：使用可编程状态空间探索测试并发程序。 载于第 4 届 Usenix 并行主题热点会议论文集: 16-16; http://dl.acm.org/citation.cfm?id=2342788.2342804.
7. Clarke, E., Grumberg, O., Peled, D. 1999. 模型检测。 剑桥：麻省理工学院出版社； http://books.google.ca/books?id=Nmc4wEaLXFEC.
8. Click, C. 2007. 无锁哈希表。 JavaOne 会议。
9. Corbet, J. 2006. 内核锁验证器。 LWN; http://lwn.net/Articles/185666/.
10. Desnoyers, M. 2009. 低影响操作系统跟踪。 博士论文。 蒙特利尔理工学院； http://www.lttng.org/pub/thesis/desnoyers-dissertation-2009-12.pdf.
11. Desnoyers, M., McKenney, P. E., Dagenais, M. R. 即将出版。 用于并行算法形式化验证的多核系统建模。 操作系统评论。
12. Desnoyers, M., McKenney, P. E., Stern, A. S., Dagenais, M. R., Walpole, J. 2012. 用户级读取-复制-更新的实现。 IEEE 并行与分布式系统汇刊 23(2): 375-382.
13. Drusinsky, D. 2011. 使用 UML 状态图进行建模和验证。 爱思唯尔科学出版社； http://books.google.ca/books?id=JMz-SWTfgiAC.
14. Ferrante, J., Ottenstein, K. J., Warren, J. D. 1987. 程序依赖图及其在优化中的应用。 编程语言与系统汇刊 9(3): 319-349; http://doi.acm.org/10.1145/24039.24041.
15. Gosling, J., Joy, B., Steele, G. L., Jr., Bracha, G., Buckley, A. 2013. Java 语言规范，Java SE 7 版。 培生教育出版社； http://books.google.ca/books?id=2RYN9exiTnYC.
16. Gotsman, A., Cook, B., Parkinson, M., Vafeiadis, V. 2009. 证明非阻塞算法不阻塞。 载于第 36 届 SIGPLAN-SIGACT 编程语言原理研讨会论文集: 16-28; http://doi.acm.org/10.1145/1480881.1480886.
17. Gotsman, A., Rinetzky, N., Yang, H. 2013. 使用 grace 验证并发内存回收算法。 载于欧洲编程研讨会。 意大利罗马：斯普林格出版社。
18. Haas, A., Kirsch, C. M., Lippautz, M., Payer, H. 2012. 您的并发 FIFO 队列有多 FIFO？ 载于放宽多核和众核可扩展性同步研讨会论文集。
19. Herlihy, M. 1991. 无等待同步。 编程语言与系统汇刊 13(1): 124-149; http://doi.acm.org/10.1145/114005.102808.
20. Herlihy, M. P., Wing, J. M. 1990. 线性化：并发对象的正确性条件。 编程语言与系统汇刊 12(3): 463-492; http://doi.acm.org/10.1145/78969.78972.
21. Holzmann, G. J. 1997. 模型检查器 Spin。 IEEE 软件工程汇刊 23(5): 279-295.
22. IBM. 2010. Power ISA 版本 2.06 修订版 B; http://www.power.org/resources/reading/.
23. Intel Corporation. 2011. Intel 64 和 IA-32 架构软件开发人员手册：指令集参考，A-Z; http://download.intel.com/products/processor/manual/325383.pdf.
24. 国际标准化组织。 2011. 编程语言 - C++，ISO/IEC 14882:2011。
25. Kirsch, C. M., Lippautz, M., Payer, H. 2012. 快速且可扩展的 k-fifo 队列。 奥地利萨尔茨堡萨尔茨堡大学。 技术报告 2012-04。
26. Michael, M. M. 2004. Hazard 指针：用于无锁对象的安全内存回收。 IEEE 并行与分布式系统汇刊 15(6): 491-504; http://ieeexplore.ieee.org/xpl/articleDetails.jsp?tp=&arnumber=1291819&queryText%3Dhazard+pointers.
27. Michael, M. M., Scott, M. L. 1996. 简单、快速和实用的非阻塞和阻塞并发队列算法。 载于第 15 届 分布式计算原理年度研讨会论文集: 267-275; http://doi.acm.org/10.1145/248052.248106.
28. MIPS Technologies Inc. 2012. 程序员 MIPS 架构，第二卷：MIPS64 指令集。
29. Olszewski, M., Ansel, J., Amarasinghe, S. 2009. Kendo：软件中高效的确定性多线程。 SIGPLAN 通知 44(3): 97-108; http://dl.acm.org/citation.cfm?id=1508256.
30. Sarkar, S., Sewell, P., Alglave, J., Maranget, L., Williams, D. 2011. 理解 Power 多处理器。 SIGPLAN 通知 46(6): 175-186; http://doi.acm.org/10.1145/1993316.1993520.
喜欢还是讨厌？ 告诉我们
Mathieu Desnoyers 是 EfficiOS 的总裁兼创始人。 他维护 LTTng 项目和 Userspace RCU 库。 他的研究兴趣在于性能分析工具、操作系统、可扩展性和实时性问题。 他拥有蒙特利尔理工学院计算机工程博士学位（2010 年）。
© 2013 1542-7730/13/0500 $10.00
最初发表于 Queue vol. 11, no. 5—
在 数字图书馆 中评论本文
更多相关文章
Adam Morrison - 多核程序中同步的扩展
为现代多核处理器设计软件提出了一个难题。 传统的软件设计中，线程操作共享数据，其可扩展性受到限制，因为对共享数据更新的同步会串行化线程并限制并行性。 另一种分布式软件设计，线程不共享可变数据，消除了同步并提供了更好的可扩展性。 但是，分布式设计使得实现共享数据结构自然提供的功能（例如动态负载均衡和强一致性保证）具有挑战性，并且并非适用于每个程序。 然而，通常共享可变数据结构的性能受到当今使用的同步方法的限制，无论是基于锁的还是无锁的。
Fabien Gaud, Baptiste Lepers, Justin Funston, Mohammad Dashti, Alexandra Fedorova, Vivien Quéma, Renaud Lachaize, Mark Roth - 现代 NUMA 系统上内存管理的挑战
现代服务器级系统通常构建为在单个系统中组合多个多核芯片。 每个芯片都有一个本地 DRAM（动态随机存取存储器）模块； 它们一起被称为一个节点。 节点通过高速互连连接，系统完全一致。 这意味着，程序员无需感知，内核可以向其节点的本地内存以及其他节点的内存发出请求。 主要区别在于远程请求将花费更长的时间，因为它们会受到更长的线路延迟的影响，并且可能必须跳转多个跃点才能遍历互连。
Spencer Rathbun - 使用 Promise 进行并行处理
在当今世界，有很多理由编写并发软件。 提高性能和增加吞吐量的愿望导致了许多不同的异步技术。 然而，所涉及的技术通常很复杂，并且是许多细微错误的原因，特别是当它们需要共享可变状态时。 如果不需要共享状态，那么这些问题可以通过称为 promise 的更好抽象来解决。 这些允许程序员将异步函数调用连接在一起，等待每个函数返回成功或失败，然后再运行链中的下一个适当的函数。
Davidlohr Bueso - 实用同步原语的可扩展性技术
在理想的世界中，应用程序有望在越来越大的系统上执行时自动扩展。 然而，在实践中，不仅这种扩展没有发生，而且常见的是在那些更大的系统上看到性能实际上恶化。
© 保留所有权利。