Существующие техники можно разбить на 3 категории гарантий покрытия:
Грубо говоря, все техники применяют отношение частичного порядка. То есть, в каждом алгоритме есть последовательность операций, которая должна произойти раньше другой. При этом, в разные потоки не имеют между собой никаких связей. Во всех случаях мы ищем паттерны вида "чтение и запись в одну переменную" в разных потоках и моделируем расписание таким образом, чтобы эти паттерны были в разных порядках. Если ничего плохого не произошло, то значит всё нормально.
Притом, 1 категория просто получает данные и алгоритм, который нужно к ним применить, находит баг - всё плохо, не находит, то считаем программу корректной. Очевидно, что данный подход не дает гарантии, что на других данных всё не сломается (вдруг есть к примеру, какой-либо if, который всё разрушит).
Методы 2 категории, же действуют иным образом. Они ищут все паттерны. И генерируют множество перестановок. Очевидно, что на каких-то данных расписание будет отличаться от запланированного, тогда даем этому расписанию другие данные чтобы всё было хорошо. При таком подходе, нужно учитывать, что при новых входных данных, нужно задать новое множество линеаризуемых результатов (например, так работает CHESS).
http://fsl.cs.illinois.edu/index.php/JPredictor
Выделяют 2 вида зависимостей
Используется подход нарезанной трассы. Такой подход предполагает проверку какого-то определенного поля объекта, что существенно сокращает количество возможных перестановок.
На вход имеем некоторый алгоритм. Запускаем его и строит трассу.
Сперва записываем:
Строим законченную трассу на уровне байткода, то есть добавляем в нынешнюю трассу:
Режем трассу для каждого определенного свойства, с учетом зависимостей
Как режем трассу:
Для чего строим трассу? Потому что каждый поток делаем линейным. То есть, нам плевать, что где-то есть if конструкция, мы просто верим, что если изначально получилось что-то вроде if then, то при како-то перестановке на каких-либо данных получим аналогичное (скорее моя догадка, в статьях ничего не сказано по этому поводу).
На основе векторных часов записываем всё это в множество, в котором учитываем зависимости и атомарные блоки.
Строим всевозможные трассы и смотрим есть ли где-то гонки или неделимость атомарных блоков.
На самом деле jPredictor не строит всевозможные трассы.
Гонки проверяются по условию, чтобы в двух потоках были операции чтения/запись не защищенные замком. Если такое есть - гонка.
Атомарность проверяются попарно, сопоставляя с 11 паттернами.
На вход получает программу и входной вектор. Запускает и ищет пары событий (w,r) - null WR пара:
Для каждой такой пары находим множество всех выполнений и используют SMT solvers (Что это?) для поиска конкретного расписания, которое приводит к ошибке.
Запускаем найденное решение.
https://github.com/sorfrancesco/Penelope
Считаем, что нам известны результаты последовательного выполнения. На вход получаем какой-то алгоритм и входные данные. Начинаем работу. Работа разбита на 3 этапа:
Рассматривают все ошибки в виде предшествующих, настоящих и удаленных доступов. Предшествующий и настоящий - на одном потоке, а удаленный на другом, который потенциально может вклиниться между ними.
Вводят понятие окон:
Рассматривают все такие потенциальные ошибки в многопоточной среде (ставят где-то задержки и прочее) с учетом метрики.
Для всех операций делает обертки, которые находятся с помощью профайлера. Эти обертки помогает планировщику планировать.
Сам планировщик работает в 3 этапа
Справедливый планировщик дает меньший приоритет потокам, которые передали управление.
Всего вставляют 2 прерывания на итерацию. Умеют сохранять состояния, что позволяет не воспроизводить заново всю итерацию, а продолжить с какого-то места.
Просто формальное описание планировщиков (очень формальное). Приведены 2 примера, но на практике по моему применяется round-robin. Никакой конкретики и реализации. Рассматриваются только чужие реализации.