#atomics

На днях решил наконец-то твердо разобраться в Модели памяти C++ (до этого лишь всякие доклады по теме смотрел, но там как в мозг втекало, так через некоторое время и вытекало).

В процессе задумался: а все эти happens before, synchronizes with и более сложные отношения между операциями — их ведь можно было бы визуализировать!

Погуглил, а, оказывается, такой инструмент уже существует: CppMem. Но печаль: его не прогнать на плюсовом коде; и даже на произвольном сишном коде его не прогнать. Он умеет лишь в свой ограниченный синтаксис. И это понятно: CppMem был создан лишь для демонстрации папиры Mathematizing C++ Concurrency. Пилить полноценный такой инструмент — раньше, чем допилишь, наверное, сам выпилишься.

А знаете ли вы какие-либо другие инструменты для статического анализа корректности атомарных операций? Как думаете, будет ли когда-либо написан полноценный инструмент для этого, или нам в этом плане до конца веков остается полагаться лишь на нейронку в своей голове?