Дониёр
Ботиров.

Асинхронные баги не случайны. Случаен лишь порядок выполнения, который выбирает операционная система, — поэтому ошибка всплывает раз в триста прогонов и не воспроизводится. unflake отбирает этот выбор у ОС: время, таймеры и порядок готовых колбэков становятся значениями из сида. Один сид — один и тот же прогон, побайтово. Найденный баг сжимается до минимального расписания и повторяется на любой машине.

Написать выбор лидера, который работает в хороший день, может кто угодно. Трудный день — тот, когда сеть разделилась, два узла считают себя главными, сообщение четырёхсекундной давности пришло дважды, а вернувшийся из мёртвых узел принёс устаревший лог. bulwark — реализация Raft на TypeScript, которую держит детерминированная симуляция: разделения, падения и перестановки сообщений задаются сидом, пять свойств безопасности из статьи проверяются после каждого перехода состояния, а каждая история клиентских операций — на линеаризуемость. Главное в репозитории — музей багов: каждый из семи экспонатов выключает ровно одно правило Raft и требует, чтобы харнесс поймал его с сидом и с именем свойства. Один экспонат — баг, который харнесс нашёл в самой реализации.

Каждая база данных заявляет уровни изоляции. Почти никто не может показать, что его уровень на самом деле допускает. Фраза «у нас snapshot isolation» — это два утверждения сразу: что ничего слабее не случается и что это действительно SI, а не что-то более строгое под тем же именем. Ни одно не проверяется чтением кода — это свойства исполнений, а не текста. adya ловит исполнения и допрашивает их: с одной стороны MVCC-движок с четырьмя уровнями изоляции, где serializable сделан алгоритмом Кэхилла — тем самым, что стоит в PostgreSQL; с другой — проверка, которая строит из наблюдаемой истории граф зависимостей, ищет в нём циклы и называет найденное именами из диссертации Адьи: G0, G1a, G1b, G1c, G-single, G2-item. Каждый уровень проверяется в обе стороны: он не производит того, что обязан предотвращать, и производит то, что предотвращает следующий. Ни одной стороне не доверяют отдельно — они уличают друг друга.

Этот репозиторий существует из-за одной фразы в разделе ограничений unflake: сотни сидов — очень хороший фаззинг, но не теорема. Выборка расписаний находит баги и никогда не доказывает их отсутствие; доказать — значит обойти все достижимые состояния, а это экспонента. Поэтому содержательная часть model checker — не поиск, а то, что позволяет не искать: симметрия (шесть взаимозаменяемых процессов дают 15 625 назначений, но всего 210 мультимножеств) и частично-упорядоченное сокращение. Ключевая проблема в том, что сломанное сокращение отвечает ровно то же, что и рабочее, — «нарушений не найдено». Поэтому полный перебор оставлен рядом, медленный и неспособный ошибиться, и каждая спецификация обязана дать в обоих совпадающий вердикт. Живость проверяется под слабой справедливостью: спинлок ловится контрпримером, алгоритм Петерсона проходит.