Как обойти все исполнения программы?

Question

[floppapa]

В стандарте C++ говорится, что наличие гонки данных при исполнении программы означает неопределённое поведение.
Поэтому необходимо писать программы так, чтобы ни в одном из возможных исполнений не могло быть гонки данных.

Но как найти (хотя бы просто обойти) все возможные исполнения C++ программы для заданных входных данных?
Существует ли для этого какой-нибудь алгоритм?

Я как-то даже придумать ничего не могу.
Главная проблема - это то, что чтение может возвращать значение записи в эту же переменную, выполненную в другом потоке в далёком будущем.
Иначе говоря, когда мы глядим на чтение какой-то переменной и пытаемся понять, какое значение может быть прочитано, то мы не можем этого сделать, потому что не знаем, какие записи в эту переменную могут произойти в других потоках в будущем.
Более того, то, какие записи произойдут в других потоках в будущем, легко может зависеть от того, какое значение возвратит текущее чтение, - в итоге получается какой-то замкнутый круг.

Answer 1

[mayton2019]

Посмотри ключик
-fsanitize=thread

и еще посмотри PVS Studio. Вроде у них был статический анализ таких ситуаций но я точно не уверен.
Надо искать инфу.

Comments

[floppapa]

по поводу -fsanitize=thread это, как я понимаю, включение ThreadSanitizer.
ThreadSanitizer добавляет к программе функционал, отлавливающий гонки данных в рантайме. Соответсвенно тут проверяются только те исполнения программы, которое произошли в рантайме, тут не проверяются все возможные исполнения.
А я хотел бы проверить все возможные исполнения программы на отсутсвие гонок данных заранее - т.е. чтобы готовая программа гарантировано была без гонок данных.

[mayton2019]

floppapa, я вообще тебя наверное удивлю. Но на софт пишут обычно тесты. Всякие там.
Модульные. E-2-E. И у тебя впереди много шансов поймать WARNING: ThreadSanitizer.

А если ты тестов не делаешь то ты - плохой поросёнок. И софт твой будет плохой независимо
от наличия теоретического доказательства гонок.

[floppapa]

Попробуй перечитать вопрос ещё раз.
Спрашивается как обойти все возможные исполнения C++ программы.
Какие ты там тесты пишешь - вообще не интересует.

[mayton2019]

Спрашивается как обойти все возможные исполнения C++ программы.

Тестами!

[floppapa]

Это не работает: ни модульные, ни сквозные тесты не могут перебрать все возможные исполнения многопоточной программы.
Самое простое: во время исполнения программы процессор(ы) может переключаться между потоками в разном порядке, и мы даже этого не можем контролировать в тестах.
А при этом модель памяти C++ - менее строгая, чем переключение процессора между потоками, и разрешает ещё больше возможных исполнений в зависимости от факторов, которые мы не можем контролировать в тестах.

[mayton2019]

floppapa, я сколько ни программировал свою мультипоточку у меня условия гонок никогда не возникало.
Голодания потоков были. Было просто некорректное исполнение. Была неоптимальность в реализации
локов.

Если это твой собственный код (ты - сам писал) то такие точки отследить не очень сложно. Это
обычно разделяемые области памяти. И ты из знаешь поскольку ты - писал код.

Санитайзеры и статик-чекеры кода - обычно идут для чужого кода или для очень-очень большого
проекта где работают десятки людей и трудно держать все под контролем.

Но в принципе хорошее правило написали ниже - накрывай все разделяемые куски кода и данных мьютексами и это концептуально решает проблему. Вопрос перформанса можно обсудить.
Дополнительно - работа с атомиками как ускорение некоторых операций. Тоже обсуждается с кодом
вместе.

И помним о "проблеме останова". В общем случае глядя на код мы не можем доказать какое-то
свойство программы. Только запуск программы является доказательством ее (прогаммы) правоты.

[floppapa]

Ещё раз: я спрашиваю не про абстрактное "как писать многопоточные программы", а конкретно про алгоритмы обхода всех возможных исполнений C++ программы.
"Исполнение" программы, "гонка данных" - это всё термины из части стандарта C++, называемого моделью памяти C++.
Видно, что ты не знаком с моделью памяти C++, поэтому тебе и не понятно ни что именно я спрашиваю, ни почему это кому-то может быть интересным.
По этой же причине ты продолжаешь писать про юнит-тесты, про "только запуск программы является доказательством", и т.д., хотя любому разбирающемуся в модели памяти С++ (или C#, Java, железа) очевидно, что в таких случаях ничего из этого не работает.
Если хочешь, можешь попробовать посмотреть вот это видео - в нём эта тема объясняется на русском (хотя сразу предупреждаю: тема сложная, с первого раза её никто не понимает).

[mayton2019]

Я не обещаю что я посмотрю это видео. Моя жизнь очень насыщенна другими задачами.

Я считаю что никакой модели памяти С++ не существует. Есть конкретное железо. x86_64 например.
И у него есть определенные свойства при чтении разделяемой памяти из разных потоков.
Вот это - существует и на это следует ориентироваться.

Я очень скептически отношусь к стандартам С++. Эти станарты очень богаты на UB и вообще С++
бьет рекорды среди языков по сложности поведения кода. Поэтому ты особо не упарывайся
С++ а больше думай о железе и о порядке захвата ресурсов. Это - важно.

Я очень прошу тебя приаттачить код. Потому что без кода мы занимаемся пустой болтовней.
Знаешь как средневековые богословы обсуждали ... "бог един или все таки это 3 человека" (отец-сын-дух).

Давай мы не будем богословами, а обсудим код. Иначе я буду тебя ругать за бесполезные посты перед
лицом хабра.

Answer 2

[maaGames]

Мьютексы, семафоры, критические секции. То есть добавь объекты синхронизации, чтобы гарантировать, что объекты изменяются упорядоченно и только одним потоком в единицу времени.

Comments

[floppapa]

Я хорошо знаком со всеми этими механизмами синхронизации.

В вопросе спрашивается про другое: про то, какие есть алгоритмы для обхода всех возможных исполнения C++ программы.
Именно на этот вопрос хотелось бы получить ответ.

[maaGames]

floppapa, Или не понимаю или не вижу смысла в вопросе. Если боишься, что будет race-condition - используешь объекты синхронизации.
Алгоритмов обхода нет, есть code coverage tool, которые проверяют, что каждая строчка кода была хоть раз выполнена. Для этого нужны горы тестов с разными входными данными. Если какие-то строки не выполнялись, то нужно написать дополнительные тесты, чтобы они покрыли этот участок кода... Но к race condition это отношения не имеет. Ведь один и тот же участок кода с одними и теми же данными может, в многопточной среде, выдавать разные результаты при неаккуратном обращении.
Не утверждаю, но лично я не верю, что можно написать комплексную многопоточную программу вообще без race condition, а значит, от объектов синхронизации не избавиться.

[floppapa]

Или не понимаю или не вижу смысла в вопросе.

Я говорю про все возможные исполнения с точки зрения так называемой "модели памяти C++".
Обычно разработчики узнают про эту "модель памяти C++" когда сталкиваются с std::atomic (напр. из этой статьи ).
Правила модели памяти C++ - это более низкий уровень, чем объекты синхронизации.
И исполнение (execution) программы, и гонка данных (data race) - это всё понятия, взятые из модели памяти C++.

Для маленьких C++ программ все возможные исполнения можно найти, например, с помощью CppMem.

[maaGames]

floppapa, Думаю, таких статических анализаторов не существует. std::atomic это очень частный случай использования всего одной единственной элементарной переменной. Даже две переменых через atomic уже не синхронизировать друг с другом. Анализатор, наверное, может тебе показать участок кода, к которому может быть обращение из разных потоков, но где ты, возможно, забыл сделать синхронизацию.
Если разрабатываешь программу с учётом race condition, то тебе не нужно ничего знать про модель памяти и прочие низкоуровневые дела, оставайся на уровне абстракции мьютексов и критических секций.

Answer 3

[Станислав Макаров]

т.е. чтобы готовая программа гарантировано была без гонок данных.

для этого лучше использовать язык программирования с отсутствием гонок данных, например Rust (без unsafe).
А так то что вы хотите от C++ - это к сожалению аналог проблемы останова.

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

Вот именно, что нужно программы ПИСАТЬ так, чтобы не было гонок, а не пытаться проверять непонятно как написанное.

Comments

[floppapa]

Я в курсе про Rust и про то, что в C++ программах не должно быть гонок данных.

Но в данном случае мой вопрос именно такой, каким я его задал: "Какие есть алгоритмы для обхода всех возможных исполнений C++ программы?"
Именно это меня интересует.

То, что обход возможных исполнений может содержать что-то похожее на проблему останова, я тоже в курсе.
Однако такая же проблема возникает и, например, в статическом анализе программ, и тем не менее там она решается/обходится разными способами.

Answer 4

[Сергей Соловьев]

Если хочешь упороться, то можно заюзать формальные верификаторы.
Например, SPIN.

Он использует свой язык, поэтому придется дублировать логику.
На так можно удостовериться в корректности.

Comments

[floppapa]

Я спрашивал про алгоритм, позволяющий обойти все исполнения C++ программы для заданных входных данных.
SPIN или другие формальные верификаторы это умеют?
Если да, то напишите, пожалуйста, как они это делают.