Илья Кокорин, Кирилл Гарманов — Верификация конкурентных структур данных на C++

Подробнее о конференции C++ Russia: https://jrg.su/nbdpQS — — Скачать презентацию с сайта — https://jrg.su/FQt5eG Реализация конкурентных структур данных — достаточно сложная задача, но не менее сложная задача — проверка корректности реализованной конкурентной структуры данных. Выполнить такую проверку очень сложно из-за недетерминизма конкурентных вычислений и как следствие, огромного количества возможных исполнений. Тем не менее возможно значительно увеличить уверенность в корректности реализации благодаря технике model checking. Расскажем про реализованный в команде VK инструмент для проверки корректности конкурентных структур данных, покажем его работу на практических примерах и познакомим слушателей с алгоритмами, использующимися для верификации конкурентного кода.