tgoop.com/cpp_lects_rus/183
Last Update:
Опубликовали нашу с Ильёй Андреевым https://www.tgoop.com/BruceGliff очередную статью. Её тематика хорошо продолжает тему прошлого поста (может мне для snippy и системной верификации завести тег?). Генератор llvm-snippy принципиально однопоточный, он никак не учитывает возможных эффектов многопоточного true sharing. А что если развить идею и из нескольких сниппетов, каждый из которых исполняется на отдельном ядре, сделать поверх некий граф возможных общих обращений в память, смоделировать мьютексы, смоделировать CAS-циклы и т.п. Возможно ли тогда по этому графу понять корректность многопоточного кода с учётом возможных переупорядочений операций и с учётом слабой модели памяти?
Нечто подобное делают давно известные литмус-тесты, но они маленькие и короткие. Можно ли как-то решить проблему комбинаторного взрыва при росте числа верифицируемых операций? Собственно об этом статья.
http://sitito.cs.msu.ru/index.php/SITITO/article/view/1068
Фактически, как вы догадываетесь, мы сделали LLVM-based инструмент, теория для которого изложена в этой статье. Сам инструмент пока в опен-сорсе не появился и в ближайшее время вряд ли мне удастся согласовать его появление, т.к. такого рода программы продаются и стоят дорого (см. например breker от brekersystems.com). Но в статье мы постарались достаточно подробно описать основные алгоритмы.
PDF надеюсь скоро доедет до сайта.
P. S. установочная статья по llvm-snippy тоже в процессе подготовки.
#publications
BY C++ and other lectures
Share with your friend now:
tgoop.com/cpp_lects_rus/183