Эффективное построение переупорядочиваний множества операций с памятью в многопоточной программе

Аннотация

Данная работа посвящена различным методам построения всевозможных линейных порядков для частично упорядоченных множеств. Сложность задачи заключается в том, что даже для множества небольшого размера, построение и проверка на какой-либо признак его всевозможных линейных порядков может приводить к необходимости перебора огромного количества вариантов. Частным случаем этой общей задачи является построение всевозможных переупорядочений для операций с памятью в многопоточных программах с учётом модели памяти. Цель этой работы — это сокращение пространства перебора в этом случае. В качестве важного практического примера рассматриваются модели памяти, позволяющие буферизацию загрузок. При этом оказывается возможным установить классы эквивалентности над перестановками операций. Это в свою очередь имеет большое значение для верификации памяти в многопоточных системах. На сегодняшний день для такого рода верификации применяются литмус-тесты, которые имеют свои ограничения. В данной работе предложен алгоритм, который учитывает классы эквивалентности при переупорядочиваниях операций с памятью, что позволяет существенно сократить как количество необходимых перестановок, так и время, затраченное на их перебор. Результаты исследования позволяют эффективно обобщить концепцию литмус-тестов на произвольные частично упорядоченные множества и существенно расширить их применимость.