...
Атомарность проверяются попарно, сопоставляя с 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 категории.