...

PENELOPE: Weaving Threads to Expose Atomicity Violations

https://github.com/sorfrancesco/Penelope 

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

1. Мониторинг. Выполняем программу на входных данных, наблюдаем за ходом выполнения. Записываем операции чтения/записи в (потенциально) общие переменные, получение/снятие блокировок, создание потоков и барьеры.
2. Предсказание. Конструируем иные запуски, чтобы они содержали как минимум один из подозрительных шаблонов. Подозрительными считаем такие шаблоны:
   1. RWR
   2. WRW
   3. RWW
   4. WWR
   5. WWW
3. Изменение расписания. ВЫполняем программу на 1 процессоре, путем переплетения потоков на 1 процессоре. Если успешно выполняется - всё ок, если нет - рапортуем о баге. Если не можем составить расписание для запуска, то просто отбрасываем его.

CTrigger: Exposing Atomicity Violation Bugs from Their Hiding Places

Рассматривают все ошибки в виде предшествующих, настоящих и удаленных доступов. Предшествующий и настоящий - на одном потоке, а удаленный на другом, который потенциально может вклиниться между ними.

...

Вводят понятие окон:

1. Локальное - между предшествующим и настоящим доступом (с учетом границ синхронизации)
2. Удаленное - дистанция удаленного доступа до начала предшествующего или конца удаленного доступа

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

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

...

Всего вставляют 2 прерывания на итерацию. Умеют сохранять состояния, что позволяет не воспроизводить заново всю итерацию, а продолжить с какого-то места.

Delay-Bounding

Просто формальное описание планировщиков (очень формальное). Приведены 2 примера, но на практике по моему применяется round-robin. Никакой конкретики и реализации. Рассматриваются только чужие реализации.