Как найти состояние гонки (race condition) в кодеМодель на Quint

Как работает модель Quint: идея вместо угадывания сценариев

Название Quint легко спутать с тестовым движком QUnit, но это другая программа: сравнение с тестами и TLA+. Чем Quint отличается от TLA+ и Alloy, разобрано в сравнении трёх языков. Обычный тест — это один сценарий, который вы придумали заранее: нажали, подождали, проверили результат. Бага, о котором вы не подумали, в таком сценарии нет. Модель устроена иначе. Вы описываете состояния системы и разрешённые действия, а программа сама пробует все порядки действий в маленьком мире и показывает первый, где правило нарушилось.

Одна модель описывает одну область логики, например жизнь записи встречи или права доступа участника, и занимает от пары десятков до пары сотен строк. Дальше несколько историй: что именно нашла модель и почему это не нашёл тест.

Как это устроено по шагам. Сначала вы выбираете маленький мир: например, один админ, один бот и одна сессия. Затем описываете, что в этом мире может произойти: вход, выход, падение процесса, новое сообщение. Программа пробует все порядки этих событий и после каждого шага проверяет правила. Такой перебор называется проверкой моделей. Если правило нарушилось, вы получаете точную цепочку шагов, которую можно повторить руками.

Мир нарочно маленький. Перебор всех порядков быстро растёт вместе с размером мира, поэтому две-три сущности и пять-шесть действий обычно дают результат за секунды. Для гонок этого хватает: чтобы два действия пересеклись, нужны всего два участника.

Какие ошибки находит модель Quint: примеры

Главная ценность модели в находках, которые никто не искал. Ниже две самые показательные и список остальных. У всех одна форма, это гонка: два действия, каждое по отдельности правильное, вместе дают потерю или путаницу.

Разберём первую историю подробно. Допустим, у человека в системе есть сессия в Telegram, и админ может её завершить. Одновременно бот может использовать эту сессию для отправки сообщения. Код сначала проверил, что сессия живая, затем пошёл отправлять. Между проверкой и отправкой админ успел выйти. В итоге сообщение ушло от имени человека, который уже закрыл доступ.

Ни один тест такого не ловил, потому что каждый шаг по отдельности работает правильно. Ошибка живёт только в порядке «проверка, выход, отправка», и модель нашла этот порядок сама.

Админ выходит из учётной записи, а в это же время бот входит по старой сессии. Код проверил права один раз, в начале, и дальше доверял результату.

Вторая история о потере данных. Система расшифровки ведёт запись встречи и в какой-то момент должен отметить, что запись идёт. Если процесс падает между началом записи и этой отметкой, после перезапуска система не знает, что запись была. Файл остался, а записи в базе нет. Пользователь видит пустое место там, где должна быть встреча.

Лечение простое: ставить отметку до начала записи, а не после. Но чтобы заметить проблему, нужно представить падение именно в этой щели, и модель делает это без усилий, потому что падение для неё одно из обычных действий.

Запись встречи шла, процесс упал, а отметки «запись идёт» нигде не осталось. После перезапуска система считает, что записи не было, и данные теряются без следа.

Как читать список выше. В каждой строке слева название класса ошибки, справа пример. «Пункт в двух карточках» и «потерянная отметка» относятся к задачам встречи, «удаление непустого» и «ключи шире прав» к административной части, «сообщение постороннему» и «чужая цитата» к переписке.

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

Пара моделей: как есть и как надо

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

Слева путь к красной комнате, то есть к нарушению, открыт. Справа на этом пути стоит преграда, и правило держится.

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

Третья строка о правках. Каждое отличие правой модели от левой помечено номером вида П1, П2 и подписью «было: …». По этим меткам можно пройти от требования к конкретному месту в коде и понять, что именно надо исправить.

Модель на каждый домен

У каждого ограниченного контекста свои правила: их записывают как MUST в карточке агрегата. Формальная модель делает эти правила проверяемыми, а агент на контекст работает внутри их границ.

Что стоит за каждым примером. «Встреча» — правило о том, что люди из прошлой записи не попадают в следующую, даже если ссылка на встречу та же. «Приватное» — приватная запись не может оказаться в общем хранилище ни при каком порядке действий. «Участник» — один Telegram-аккаунт соответствует одной записи участника, и при слиянии история сохраняется. «Вакансия» — статус по вакансии принадлежит конкретной паре «кандидат и вакансия», а не кандидату вообще.

Проверка проверок

Зелёный результат может означать «всё правильно», а может означать «проверка ничего не проверяла». Поэтому проверяют сами проверки: модель ломает нарочно сам автор или агент (например, убирает одно условие) и смотрят, заметит ли правило поломку. Если не заметило, правило бесполезно.

Столбики показывают, какая доля правил в текущем коде нарушается. Чем длиннее столбик, тем больше правил модель поймала на реальном коде. «Участники 2 из 2» означает, что обе проверки нашли проблему. «Приватность 1 из 4» означает, что в основном код держится, но одна дыра есть.

Это не оценка качества кода. Столбик зависит от того, какие правила были выбраны, и показывает скорее, где модель принесла больше пользы.

Испорченная копия модели должна нарушить правило. Если она проходит сквозь правило и ничего не срабатывает, значит правило ничего не проверяет.

После каждой правки модели автоматически запускается проверка. Если правило нарушено, агент получает цепочку шагов и сразу исправляет модель или код.

Что значит каждая строка. «Шапка как контракт» — в начале файла перечислены правила, ожидаемые нарушения и ситуации, которые обязаны случиться. «Испорченная копия» — проверка, что правило вообще способно сработать. «Обязательные ситуации» — защита от правил вида «если А, то Б», где А ни разу не наступило. «Тупики» — случаи, когда программа молча отбрасывает прогон, и результат «ок» получается сам собой.

Последние две строки о людях и агентах. «Желание отдельно» значит, что намерение человека записывается в модель независимо от проверяемого поля, иначе правило сверяет поле с самим собой. «Автопроверка» (по сути хук) значит, что агент не может забыть запустить модель: запуск происходит после каждой правки сам.

Граница с человеком

Модель проверяет всё, что можно записать конечным списком условий: пропала ли запись, смешались ли участники, есть ли выход из тупика. Понятность подписей, удобство и общее ощущение от экрана так не описать, их оценивает человек на макете.

Список слева описывает всё, что можно сформулировать как «всегда» или «никогда»: запись не исчезает, участники не смешиваются, опасное действие требует подтверждения. Такие правила модель проверяет полностью.

Список справа содержит то, для чего конечного перечня признаков не существует. Подпись понятна читателю или нет, решает читатель. Поэтому в таблице требований заранее отмечают строки «нужна сверка с человеком» и не пытаются их формализовать.

Слабые места проверки моделей

У метода есть пределы, и о них лучше знать до начала работы. Модель сама по себе не следит за кодом, не проверяет «рано или поздно» и видит только тот мир, который в неё положили.

Нет связи с кодом: модель написана руками, и никто не заставляет её меняться вместе с кодом. Через месяц она может описывать то, чего уже нет. Лекарство: хранить в шапке коммит, с которого снята модель, и обновлять вместе с кодом. Более сильное лекарство — прогонять трассы модели через настоящий обработчик, но этого шага пока нет. Похожая задача, держать желаемое, код и замер в согласии, разобрана в статье про петлю сверки спек.

Нет проверки «рано или поздно»: что баг в итоге дойдёт до команды, проверяется только косвенно. Маленький мир: баг, которому нужно пять сущностей одновременно, можно пропустить. Пустые зелёные: правило держится только потому, что нужной функции в коде ещё нет, и зелёный цвет здесь обманывает.

С чего начать с Quint: первая модель за вечер

Порядок на первый вечер. Откройте список исправленных багов и выберите тот, где причина в порядке или времени событий. Выпишите участников и действия, которые к нему привели. Опишите их в модели, запустите и дождитесь, пока программа сама найдёт цепочку. Затем добавьте исправление под переключателем и убедитесь, что правило держится. Наконец, сломайте модель нарочно и проверьте, что правило это замечает.

Не нужно сразу моделировать продукт целиком. Возьмите один недавний баг, который пришлось чинить дважды или который нашёл пользователь. Опишите в модели его участников и два-три действия, запустите перебор и убедитесь, что программа находит этот баг без подсказки. Потом исправьте и убедитесь, что правило держится.

Как начать вместе с агентом

1. Поставить Quint. Агент установит его сам через npm.

Поставь себе Quint и убедись, что он запускается.

2. Сначала требования, не код. Так агент сначала описывает мир, а правит код потом.

Не меняй код. Сделай требования на Quint для [область].
Для каждого правила покажи две версии: как сейчас и как должно быть.

3. Проверить результат.

4. Логику и экран — отдельно. Агент по умолчанию их путает: правила экрана пишет как логику, а в логике пропускает случаи.

Сделай два списка требований.
1. Логика: только «всегда» и «никогда», проверяем моделью на Quint.
2. Экран: понятность и удобство, их я проверю сам на макете.

Частые вопросы