权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

Robustness against Relaxed Memory Models (R2M2)

针对宽松内存模型 (R2M2) 的鲁棒性

基本信息

批准号：
241337241
负责人：
Professor Dr. Roland Meyer
金额：
--
依托单位：
Institut für Theoretische Informatik
依托单位国家：
德国
项目类别：
Research Grants
财政年份：
2013
资助国家：
德国
起止时间：
2012-12-31 至 2016-12-31
项目状态：
已结题

来源：
https://gepris.dfg.de/gepris/projekt/241337241?language=en
关键词：
Robustness against Relaxed Memory Models

项目摘要

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.

出于性能方面的考虑，现代多处理器实现了宽松的内存模型，允许程序乱序和非存储原子执行。虽然无数据竞争的程序对这些放松不敏感，但它们对底层并发库的开发造成了严重的问题。在顺序一致性下正确工作的算法在宽松的内存模型上运行时会显示出不期望的效果。例如，如果程序的顺序稍微放松，互斥算法就会失败。我们说，这些程序对处理器支持的弛豫并不健壮。为了增强鲁棒性，程序员必须在控制硬件的代码中添加安全网指令，这是一项即使对专家来说也很困难的任务。随着多处理器的广泛使用，并发库在日常编程中变得越来越重要，鲁棒性开始成为一个关键问题，我们提出了开发算法，检查和执行程序的鲁棒性对宽松的内存模型。假设一个内存模型，并给出一个程序，我们的程序决定是否放松的行为符合顺序一致性语义。如果不是这种情况，它们会合成安全网指令，以增强鲁棒性。当内置到编译器中时，我们的算法因此隐藏了程序员放松的内存模型，并提供了顺序一致性的错觉。检查鲁棒性是具有挑战性的，由于两个来源的无界性的问题。首先，为了确保分析独立于架构参数（如写入缓冲区的大小），我们不能假设程序顺序松弛的界限。第二，与类似的论点，我们不能假设一个库的客户端的数量上的约束-虽然这个数字是有限的，在实际的处理器。从理论的角度来看，我们的目标是开发一个证明方法的可计算性和复杂性的结果的鲁棒性。其想法是将有关放松计算的联合收割机组合推理与语言理论方法结合起来。发展这样一个一般理论是很有道理的。未来几代处理器将带来新的内存模型，我们在这里开发的技术应该可以应用到这些架构中。事实上，我们的第二个目标是在实践中应用证明方法。我们解决鲁棒性对流行的POWER处理器，有一个高度宽松的内存模型。此外，我们还研究了并发库在未知环境下的鲁棒性。总而言之，我们项目的主要目标如下。研究违反鲁棒性的计算的组合特性。在此基础上，发展语言理论技术来判定鲁棒性.应用该方法检查针对POWER处理器的鲁棒性。扩展该方法以检查并发库的健壮性。