C++ and other lectures

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

🔥60👍22❤5🤮3🤔1😢1

www.tgoop.com/cpp_lects_rus/183

12.6K viewsedited  Jun 23, 2024 at 16:42

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