C++ and other lectures

Опубликовали нашу с Ильёй Андреевым https://t.me/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