Robustness against Relaxed Memory Models (R2M2)

点击翻译按钮获取中文摘要

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.