Текущие проверки линеаризуемости алгоритмов, например с помощью lincheck, заключаются в случайном многопоточном исполнении кода и сравнеии результатов со всеми возможными последовательными исполнениями тех же операций. В ходе проверки даже самых простых студенческих lock-free алгоритмов выявилась полезность следующих функций:
Внедриться в JRE или байт-код и на основе понимания использования CAS явно влиять на планирование потоков