Я спрашивал про алгоритм, позволяющий обойти все исполнения C++ программы для заданных входных данных.
SPIN или другие формальные верификаторы это умеют?
Если да, то напишите, пожалуйста, как они это делают.
Ещё раз: я спрашиваю не про абстрактное "как писать многопоточные программы", а конкретно про алгоритмы обхода всех возможных исполнений C++ программы.
"Исполнение" программы, "гонка данных" - это всё термины из части стандарта C++, называемого моделью памяти C++.
Видно, что ты не знаком с моделью памяти C++, поэтому тебе и не понятно ни что именно я спрашиваю, ни почему это кому-то может быть интересным.
По этой же причине ты продолжаешь писать про юнит-тесты, про "только запуск программы является доказательством", и т.д., хотя любому разбирающемуся в модели памяти С++ (или C#, Java, железа) очевидно, что в таких случаях ничего из этого не работает.
Если хочешь, можешь попробовать посмотреть вот это видео - в нём эта тема объясняется на русском (хотя сразу предупреждаю: тема сложная, с первого раза её никто не понимает).
Я говорю про все возможные исполнения с точки зрения так называемой "модели памяти C++".
Обычно разработчики узнают про эту "модель памяти C++" когда сталкиваются с std::atomic (напр. из этой статьи ).
Правила модели памяти C++ - это более низкий уровень, чем объекты синхронизации.
И исполнение (execution) программы, и гонка данных (data race) - это всё понятия, взятые из модели памяти C++.
Для маленьких C++ программ все возможные исполнения можно найти, например, с помощью CppMem.
Это не работает: ни модульные, ни сквозные тесты не могут перебрать все возможные исполнения многопоточной программы.
Самое простое: во время исполнения программы процессор(ы) может переключаться между потоками в разном порядке, и мы даже этого не можем контролировать в тестах.
А при этом модель памяти C++ - менее строгая, чем переключение процессора между потоками, и разрешает ещё больше возможных исполнений в зависимости от факторов, которые мы не можем контролировать в тестах.
Я в курсе про Rust и про то, что в C++ программах не должно быть гонок данных.
Но в данном случае мой вопрос именно такой, каким я его задал: "Какие есть алгоритмы для обхода всех возможных исполнений C++ программы?"
Именно это меня интересует.
То, что обход возможных исполнений может содержать что-то похожее на проблему останова, я тоже в курсе.
Однако такая же проблема возникает и, например, в статическом анализе программ, и тем не менее там она решается/обходится разными способами.
Я хорошо знаком со всеми этими механизмами синхронизации.
В вопросе спрашивается про другое: про то, какие есть алгоритмы для обхода всех возможных исполнения C++ программы.
Именно на этот вопрос хотелось бы получить ответ.
по поводу -fsanitize=thread это, как я понимаю, включение ThreadSanitizer.
ThreadSanitizer добавляет к программе функционал, отлавливающий гонки данных в рантайме. Соответсвенно тут проверяются только те исполнения программы, которое произошли в рантайме, тут не проверяются все возможные исполнения.
А я хотел бы проверить все возможные исполнения программы на отсутсвие гонок данных заранее - т.е. чтобы готовая программа гарантировано была без гонок данных.
Написано
Войдите на сайт
Чтобы задать вопрос и получить на него квалифицированный ответ.
SPIN или другие формальные верификаторы это умеют?
Если да, то напишите, пожалуйста, как они это делают.