В ядре Redox дедлоки теперь ловятся на этапе компиляции — через систему типов

В ядре Redox появились упорядоченные блокировки: каждому типу блокировки присвоен свой токен, а комбинации, способные привести к дедлоку, отвергаются компилятором. Часть найденных таким образом дедлоков уже исправлена.

Почему дедлок не ловится обычными средствами

Взаимная блокировка возникает, когда два участка кода берут ресурсы в разном порядке: первый держит A и ждёт B, второй держит B и ждёт A. По отдельности оба участка написаны правильно, поэтому ни компилятор, ни линтер, ни обзор кода не имеют оснований возразить. Программа просто перестаёт отвечать.

Как это решается типами

Идея в том, чтобы запретить саму возможность написать опасную последовательность. Каждому типу блокировки соответствует свой токен — обычный тип Rust со своим значением. Тип блокировки хранит токены всех блокировок, уже удерживаемых в этом вызове, и требует, чтобы новая блокировка бралась строго по возрастанию.

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

Авторы прямо пишут, что крейт ordered_locks не удалось использовать напрямую из-за зависимостей, но идеи и реализация открыты для использования.

Что это дало сразу

Часть потенциальных дедлоков в ядре была найдена и исправлена по результатам. Авторы оценивают это так: многопоточность Redox стала надёжнее.

Отдельно отмечу: месяцем позже, в марте 2026, в ядре появилось ещё и обнаружение дедлоков во время работы — по счётчику спин-блокировок. Статическая проверка ловит нарушения порядка, динамическая — зависания, вызванные причинами вне блокировок. Механизмы дополняют друг друга.

Почему это интересно за пределами Redox

Приём «токены блокировок в типах» известен в сообществе seL4 и в некоторых системах реального времени. Здесь он применён в микроядре, написанном на Rust, и в ядре обычной операционной системы. Это показательный пример того, что даёт система типов: не «запретить небезопасный код», а выразить правило порядка так, чтобы нарушение нельзя было написать.

Сравнение с обычной практикой показательно. В Си и в Rust без такого механизма порядок захвата блокировок соблюдается по соглашению и проверяется обзором кода или линтером — то есть может быть нарушен и пойман поздно, при отладке на реальной нагрузке.

Оригинал

Коммит Implement ordered locks in kernel от 22 сентября 2025 года в репозитории redox-os/kernel; сводка «This Month in Redox — September 2025», раздел «Deadlock Prevention and Detection at Compile-Time»