...
Грубо говоря, все техники применяют отношение частичного порядка. То есть, в каждом алгоритме есть последовательность операций, которая должна произойти раньше другой. При этом, в разные потоки не имеют между собой никаких связей. Во всех случаях мы ищем паттерны вида "чтение и запись в одну переменную" в разных потоках и моделируем расписание таким образом, чтобы эти паттерны были в разных порядках. Если ничего плохого не произошло, то значит всё нормально.
Притом, 1 категория просто получает данные и алгоритм, который нужно к ним применить, находит баг - всё плохо, не находит, то считаем программу корректной. Очевидно, что данный подход не дает гарантии, что на других данных всё не сломается (вдруг есть к примеру, какой-либо if, который всё разрушит).
Методы 2 категории, же действуют иным образом. Они ищут все паттерны. И генерируют множество перестановок. Очевидно, что на каких-то данных расписание будет отличаться от запланированного, тогда даем этому расписанию другие данные чтобы всё было хорошо. При таком подходе, нужно учитывать, что при новых входных данных, нужно задать новое множество линеаризуемых результатов (например, так работает CHESS).
Представители 1 категории.
...