Существующие техники можно разбить на 3 категории гарантий покрытия:

1. Никаких гарантий покрытия: Эвристические техники, основанные на философии использования эвристик для достижения чередований, которые наиболее часто содержат баги и тестирование их как можно больше (с ограничениями по времени и пространству). Особенно успешны в нахождении ошибок, но не могут предоставить какую-либо полезную информацию тестировщику о том, что было упущено в тестировании, то есть не могут предоставить никаких гарантий покрытия
2. Гарантии покрытия над пространством чередований: Техники поиска приоритетов получают более ориентированный на покрытие подход, чем техники категории 1 за счет использования идей вроде ограничения упреждения, ограничения контекста, ограничения глубины и ограничения задержек для поиска с приоритетами всех прерываний программы. Эти приоритеты позволяют нам дать количественную оценку какая часть пространства чередований протестирована, свойства, которое техники категории 1 не дают. Техники поиска приоритетов очень полезны в поиске багов. Например, Chess - отличный инструмент, основанный на ограничении контекста поиска приоритизации. Тем не менее, эти техники все основаны на фиксированых (предопределенных) множествах вводом и следовательно, если баг не может быть открыт на данном множестве вводов, он будет упущен. Более того гарантии покрытия даются только нам пространством программных чередований.
3. Гарантии покрытия над пространствами чередований и входных данных (Подозреваю, что это можно даже не смотреть, так как сейчас не учитываем входные данные)

Представители 1 категории.

F. Chen, T. Serbanuta, and G. Roşu. JPredictor: A Predictive Runtime Analysis Tool for Java. In ICSE, pages 221–230,2008.

Используется подход нарезанной трассы. Такой подход предполагает проверку какого-то определенного поля объекта, что существенно сокращает количество возможных перестановок.
На вход имеем некоторый алгоритм. Запускает его (тут не понял, зачем именно) и строит трассу.
Сперва записываем:

1. начало метода
2. true-переход условных операторов
3. доступ к переменным
4. Вызов методов (притом учитываем какая именно реализация вызывается)

Строим законченную трассу на уровне байткода, то есть добавляем в нынешнюю трассу:

1. Точки возврата из метода
2. Состояния до прыжков
3. Имена полей к которым обращаются объекты
4. Начала потоков
5. События снятия/условия блокировок

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

Строим всевозможные трассы и смотрим есть ли где-то гонки или неделимость атомарных блоков.
На самом деле jPredictor не строит всевозможные трассы.

Гонки проверяются по условию, чтобы в двух потоках были операции чтения/запись не защищенные замком. Если такое есть - гонка.

Атомарность проверяются попарно, сопоставляя с 11 паттернами.

A. Farzan, P. Madhusudan, N. Razavi, and F. Sorrentino. Predicting Null-Pointer Dereferences in Concurrent Programs. In FSE, pages 47:1–47:11, 2012.

На вход получает программу и входной вектор. Запускает и ищет пары событий (w,r) - null WR пара:

• w - запись null в переменную x
• r - чтение непустой переменной x
• w,r независимы, то есть для них есть пересстановка

Для каждой такой пары находим множество всех выполнений и используют SMT solvers (Что это?) для поиска конкретного расписания, которое приводит к ошибке.

Запускаем найденное решение.

Представители 2 категории.