Efficient Reordering of Multiple Memory Operations in a Multithreaded Program - Ilya Andreev; Konstantin Vladimirov (Современные информационные технологии и IT-образование)
This paper is devoted to various methods of constructing all kinds of linear orders for partially ordered sets. The complexity of the problem lies in the fact that even for a set of small size, constructing and checking for any feature of its possible linear orders can lead to the need of enumeration of huge number of options. A special case of this general problem is the construction of all possible reorderings for memory operations in multithreaded programs, taking into account the memory model. The goal of this work is to reduce the search space in this case. An important practical example is the consideration of memory models that allow buffering of downloads. In this case, it becomes possible to establish equivalence classes over permutations of operations. This in turn is of great importance for memory verification in multithreaded systems. Today, litmus tests are used for this type of verification, which have their limitations. In this paper, an algorithm is proposed that takes into account equivalence classes when reordering memory operations, which can significantly reduce both the number of necessary permutations and the time spent on their enumeration. The results of the study allow us to effectively generalize the concept of litmus tests to arbitrary partially ordered sets and significantly expand their applicability.