Верификация конкурентных структур данных на C++

Реализация конкурентных структур данных — достаточно сложная задача, но не менее сложная задача — проверка корректности реализованной конкурентной структуры данных.

Выполнить такую проверку очень сложно из-за недетерминизма конкурентных вычислений и, как следствие, огромного количества возможных исполнений.

Тем не менее возможно значительно увеличить уверенность в корректности реализации благодаря технике model checking. Расскажем про реализованный в команде VK инструмент для проверки корректности конкурентных структур данных, покажем его работу на практических примерах и познакомим слушателей с алгоритмами, использующимися для верификации конкурентного кода.