Robustness against Relaxed Memory Models (R2M2)

出于性能原因，现代多处理器实现了宽松的内存模型，允许程序外顺序和非存储原子执行。虽然没有数据竞争的程序对这些松弛不敏感，但它们给底层并发库的开发带来了严重的问题。在顺序一致性下正常工作的例程在宽松内存模型上运行时会出现不良影响。例如，如果程序顺序稍微放松，互斥锁算法就会失败。我们说这些程序对于处理器支持的松弛不是健壮的。为了增强健壮性，程序员必须在控制硬件的代码中添加安全网指令——即使对专家来说，这也是一项困难的任务。随着多处理器的广泛使用，并发库在日常编程中变得越来越重要，并且健壮性开始成为一个关键问题。我们建议开发算法来检查和增强程序对放松记忆模型的鲁棒性。假设一个内存模型和给定一个程序，我们的过程决定放松行为是否与顺序一致性语义一致。如果情况并非如此，它们就会合成增强鲁棒性的安全网指令。当内置于编译器中时，我们的算法对程序员隐藏了宽松的内存模型，并提供了顺序一致性的假象。由于问题中的两个无界性来源，检查鲁棒性是具有挑战性的。首先，为了确保分析独立于体系结构参数（如写缓冲区的大小），我们不能假设程序的顺序松弛有一个界限。其次，使用类似的论据，我们不能假设一个库的客户机数量有一个界限~尽管这个数字在实际的处理器中是有限的。该项目力求对鲁棒性分析的理论和实践贡献。从理论的角度来看，我们的目标是开发一种鲁棒性的可计算性和复杂性结果的证明方法。其思想是将松弛计算的组合推理与语言理论方法相结合。发展这样一个普遍的理论是完全合理的。未来的处理器将采用新的内存模型，我们在这里开发的技术应该延续到这些架构中。实际上，我们的第二个目标是在实践中应用证明方法。我们针对具有高度宽松内存模型的流行POWER处理器解决健壮性问题。此外，我们还研究了在未知环境中工作的并发库的鲁棒性。总而言之，我们项目的中心目标如下：研究违反鲁棒性的计算的组合性质。在此基础上，发展语言理论技术来确定鲁棒性。应用该方法对POWER处理器进行鲁棒性检查。扩展该方法以检查并发库的健壮性。

For performance reasons, modern multiprocessors implement relaxed memory models that admit out~of~program~order and non~store atomic executions. While data race free programs are not sensitive to these relaxations, they pose a serious problem to the development of the underlying concurrency libraries. Routines that work correctly under sequential consistency show undesirable effects when run on relaxed memory models. Mutex algorithms, for example, fail if the program~order is relaxed slightly. We say that these programs are not robust against the relaxations that the processor supports. To enforce robustness, the programmer has to add safety net instructions to the code that control the hardware ~ a task that has proven to be difficult, even for experts. With the widespread use of multiprocessors, concurrency libraries become increasingly important in everyday programming and robustness is starting to be a key concern.We propose to develop algorithms that check and enforce robustness of programsagainst relaxed memory models. Assuming a memory model and given a program, ourprocedures decide whether the relaxed behaviour coincides with the sequential consistency semantics. If this is not the case, they synthesize safety net instructions that enforce robustness. When built into a compiler, our algorithms thus hide the relaxed memory model from the programmer and provide the illusion of sequential consistency.Checking robustness is challenging due to two sources of unboundedness in the problem. First, to ensure the analysis is independent from architectural parameters (like the size of write buffers), we cannot assume a bound on the program~order relaxations. Second, and with a similar argument, we cannot assume a bound on the number of clients to a library ~ although this number is finite in actual processors.The project strives for theoretical as well as practical contributions to robustness analysis. From a theoretical point of view, our goal is to develop a proof method for computability and complexity results about robustness. The idea is to combine combinatorial reasoning about relaxed computations with language~theoretic methods. Developing such a general theory is well justified. Future processor generations will come with new memory models, and the techniques we develop here should carry over to these architectures. Indeed, our second goal is to apply the proof method in practice. We address robustness against the popular POWER processors that have a highly relaxed memory model. Moreover, we study robustness for concurrency libraries that act in an unknown environment.To sum up, the central goals of our project are the following.1. Investigate combinatorial properties of computations that violate robustness.2. Based on this, develop language~theoretic techniques to decide robustness.3. Apply the method to check robustness against POWER processors.4. Extend the method to check robustness of concurrency libraries.