5ⁿ → 4n+1: сколько на самом деле дают редукции в explicit-state model checking

5ⁿ → 4n+1: сколько на самом деле дают редукции в explicit-state model checking

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

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

Три результата, ради которых стоит читать дальше:

1. На модельной спецификации две редукции вместе превращают экспоненту 5ⁿ в линейную функцию 4n+1 — точно, а не приближённо. По отдельности ни одна из них этого не делает: симметрия даёт полином четвёртой степени, частичные порядки — экспоненту с основанием 2.

2. На семи из десяти спецификаций портфеля редукция даёт фактор 1,00× и при этом стоит от 2 до 3 % времени сверху. Отрицательный результат, который в публикациях обычно не показывают.

3. Направленный поиск по 100 000 сгенерированных спецификаций нашёл свидетелей необходимости условий C2 и C3 — и не нашёл ни одного для C1. Что это значит, разобрано в разделе 8.

---

1. Постановка задачи

Explicit-state model checker отвечает на вопрос «достижимо ли состояние, нарушающее инвариант» перебором всех достижимых состояний. В отличие от тестирования, отрицательный ответ здесь означает «невозможно», а не «не нашли» — и это единственная причина, по которой такой инструмент вообще нужен, потому что по стоимости он проигрывает тестированию на порядки.

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

Две редукции рассматриваются здесь.

Редукция по симметрии. Если процессы взаимозаменяемы, состояния, отличающиеся только перестановкой процессов, эквивалентны. Вместо всех назначений достаточно хранить канонического представителя класса. Идея независимо предложена в [Clarke, Filkorn, Jha, CAV’93] и [Emerson, Sistla, CAV’93].

Редукция частичных порядков (POR). Если два действия не касаются ничего общего, они коммутируют, и исследование обоих порядков не даёт ничего сверх исследования одного. Метод ample-множеств — [Peled, CAV’93]; родственные формулировки: persistent sets [Godefroid, 1996] и stubborn sets [Valmari, CAV’90]. Каноническое изложение условий C0–C3, которое используется ниже, — [Clarke, Grumberg, Peled, Model Checking, MIT Press].

Вопросы, на которые отвечает это исследование:

• Q1. Каков фактический выигрыш каждой редукции и их композиции как функция размера задачи?

• Q2. Какова накладная стоимость редукции в пересчёте на одно посещённое состояние?

• Q3. На каких формах спецификаций редукция не даёт ничего, и сколько это стоит?

• Q4. Необходимо ли каждое из условий C1, C2, C3, или какие-то из них можно снять без потери корректности?

Q4 — не риторический вопрос. Реализация с ослабленным условием ведёт себя неотличимо от корректной ровно до момента, когда она молча теряет контрпример: обе выводят «нарушений не найдено».

2. Объект исследования

Измерения проведены на pnueli — explicit-state model checker на TypeScript, MIT, коммит daee203, версия 0.2.0. Выбор обусловлен двумя свойствами, которых нет у промышленных инструментов: во-первых, реализация умещается в несколько сотен строк и допускает точечное вмешательство в алгоритм; во-вторых, в ней сохранён нередуцированный поиск, служащий эталоном истины.

Спецификация в этой модели объявляет для каждого действия множества читаемых и записываемых переменных, а также функцию канонизации для симметрии. Это осознанное решение, а не упрощение: восстановить множества reads/writes из замыкания статическим анализом невозможно, поэтому TLA+ требует объявлять множества симметрии, а SPIN получает отношение зависимости только потому, что Promela ограничивает, что может делать оператор. При явном объявлении редукция корректна относительно объявленного, а ошибка в объявлении становится ошибкой спецификации, а не молчаливой некорректностью инструмента.

Условия ample-множества в реализации:

• C0 — если что-то разрешено, ample-множество непусто. Иначе поиск изобретал бы несуществующие тупики.

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

• C2 — выбранные действия невидимы для проверяемого свойства, то есть не пишут ничего, что читает хоть один инвариант.

• C3 — условие цикла: ample-множество, все преемники которого уже на стеке поиска, отвергается, и состояние раскрывается полностью.

Ключевой фрагмент — построение ample-множества:

for (const [process, candidate] of byProcess) {  // C2 — невидимо для каждого инварианта  if (candidate.some((e) => e.action.writes.some((w) => visibleVars.has(w)))) continue;  // C1 — ничто из другого процесса не зависит от выбранных действий  const clashes = spec.actions.some(    (other) =>      other.process !== process && candidate.some((e) => !independent(e.action, other)),  );  if (clashes) continue;  if (!best || candidate.length < best.length) best = candidate;}return best ?? enabled;   // C0

3. Методология

Среда. Apple M4 Max, 16 ядер, macOS 26.3.1, Node.js v25.8.1, vitest 2.1.8. Все замеры — медиана из 3–5 прогонов в одном процессе после прогрева JIT.

Измеряемая величина. Основная метрика — число различимых посещённых состояний. Она не зависит от машины, языка и реализации хеш-таблицы, и именно по ней редукции сравниваются в литературе. Время приводится дополнительно, для оценки накладных расходов.

Четыре режима. Спецификация workers(n) существует в двух вариантах — с объявленной функцией симметрии и без неё, — что даёт четыре комбинации:

Абляция. Для ответа на Q4 функция checkReduced воспроизведена с вынесенными во флаги условиями C1, C2, C3. Код совпадает с оригиналом построчно, за исключением трёх условных выражений. Это позволяет сравнивать вердикты «с условием» и «без условия» на одном и том же поиске.

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

Воспроизводимость. Генератор спецификаций в эксперименте 4 детерминирован: линейный конгруэнтный генератор с явным сидом, без обращений к Math.random и системному времени. Один и тот же сид даёт одну и ту же спецификацию на любой машине.

4. Эксперимент 1: выигрыш как функция размера

Спецификация workers(n): n взаимозаменяемых рабочих, каждый проходит четыре приватных шага, затем инкрементирует общий счётчик. Инвариант читает только счётчик. Это форма, на которой обе редукции имеют полный набор оснований для работы: приватные шаги независимы и невидимы, рабочие взаимозаменяемы.

Все четыре столбца имеют точные замкнутые формы, совпадающие с измерениями во всём диапазоне без единого исключения:

Это главный результат работы, и он интереснее, чем «редукции помогают».

Симметрия убирает измерение «кто именно». Состояние n рабочих, каждый в одной из пяти фаз, — это 5ⁿ назначений, но всего C(n+4, 4) мультимножеств. Экспонента заменяется полиномом четвёртой степени, где четвёрка — это число фаз минус один, а не что-то, связанное с n.

Частичные порядки убирают измерение «в каком порядке». Но не трогают идентичность процессов, поэтому остаются 2ⁿ комбинаций «этот рабочий уже дошёл до общего счётчика или ещё нет». Основание падает с 5 до 2 — экспонента остаётся экспонентой.

Композиция даёт линейность. И это не сумма эффектов и не произведение: каждая редукция снимает свой источник комбинаторики, и лишь после того, как сняты оба, остаётся 4n+1 — по сути «сколько рабочих прошло сколько шагов» в свёрнутом виде.

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

5. Эксперимент 2: стоимость редукции

Редукция не бесплатна. Канонизация по симметрии — сортировка на каждом состоянии; построение ample-множества — перебор действий с квадратичной проверкой независимости. Стоимость одного посещённого состояния:

Отношение устойчиво держится около 1,8–2,0× и не растёт с n. То есть редуцированный поиск платит примерно двойную цену за состояние — и это ровно та величина, с которой нужно сравнивать выигрыш из раздела 4. При факторе 11 837× двойная цена состояния несущественна; при факторе 1,0× она и есть весь итог.

6. Эксперимент 3: где редукция не даёт ничего

Портфель из десяти спецификаций репозитория: алгоритм Петерсона, спинлок, обедающие философы, рабочие и модель выборов лидера Raft.

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

Существеннее другое: редукция при этом стоит времени. На raft(5, term ≤ 2) — 782,8 мс против 761,3 мс, то есть +2,8 % при нулевом выигрыше; на philosophers(5) — 0,4 против 0,2 мс. Накладные расходы платятся на каждом состоянии независимо от того, удалось ли что-то сократить.

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

7. Эксперимент 4: необходимы ли условия

7.1. Абляция на портфеле репозитория

Каждая из четырнадцати спецификаций прогнана в пяти конфигурациях: все условия, без C1, без C2, без C3, без всех трёх. Сравнивается вердикт с эталоном полного перебора.

Крестиком помечено расхождение с истиной.

Результат отрицательный и в этом виде малополезный: снятие любого одного условия ни разу не изменило вердикт. Ломается только конфигурация, где сняты все три сразу — и там теряются шесть нарушений из четырнадцати, включая тупик у философов и нарушение Election Safety в модели Raft без правила «один голос на терм».

Отдельного внимания заслуживают строки philosophers(3) safe и write skew исправленный: при снятом C1 поиск посетил 3 состояния из 12 и 7 из 14 соответственно — и вердикт совпал с истиной. Совпадение вердикта не является свидетельством корректности: некорректный поиск, не наткнувшийся на нарушение, выглядит точно так же, как корректный, доказавший его отсутствие.

Вывод из 7.1 — не «условия избыточны», а «портфель их не нагружает». Портфель составлен из учебных задач, где либо всё разделяемо (и ample-множество вырождается в полное), либо всё приватно (и условия выполняются тривиально).

7.2. Направленный поиск свидетелей

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

Схема генератора: 2–3 процесса, у каждого одна приватная переменная и 1–2 общих; программа длиной 2–3 инструкции, циклическая; каждая инструкция объявляет свои reads/writes правдиво; инвариант читает случайное подмножество переменных с вероятностью density для каждой и нарушается, когда все читаемые им переменные подняты в единицу.

Приватная переменная — ключевой элемент конструкции: действие, пишущее только её, независимо от всех остальных процессов и проходит C1. Если при этом инвариант её читает, единственным препятствием остаётся C2. Именно этой формы не было в портфеле раздела 7.1.

Прогон: 20 000 сидов на каждое из пяти значений density, всего 100 000 спецификаций. Для каждой сравнивается вердикт полного перебора, вердикт базовой конфигурации (все условия) и вердикт конфигурации без одного условия.

Три наблюдения.

Базовая конфигурация не ошиблась ни разу на 100 000 спецификациях. Это самое сильное эмпирическое подтверждение корректности реализации, которое здесь получено: 100 000 независимых сравнений с эталоном без единого расхождения.

Число свидетелей для C2 монотонно растёт с плотностью инварианта — с 1 до 31. Так и должно быть: C2 — условие о видимости, и чем больше переменных наблюдает инвариант, тем чаще оно оказывается связывающим.

Число свидетелей для C3 монотонно падает — с 1 710 до 275. Причина обратная и столь же логичная: чем плотнее инвариант, тем чаще C2 отвергает кандидатов ещё до того, как редуцированное ample-множество вообще образуется, и тем реже возникает ситуация, в которой C3 мог бы иметь значение. Условия перекрывают друг друга, и измерять их по отдельности можно только так — разводя по разным режимам плотности.

Минимальный свидетель для C2. Сид 7266, density 0,8: два процесса, три переменные, программа длиной 3, инвариант читает v0 и v1. Полный перебор — 8 состояний, вердикт invariant. Тот же поиск со снятым C2 — 6 состояний, вердикт ok.

потерянный контрпример:  (начало)   pc=00 v=000  p0:0       pc=10 v=000  p0:1       pc=20 v=100  p1:0       pc=21 v=110

Механика ровно та, которую предсказывает теория: действие p0:1 независимо от всех действий процесса 1, но пишет наблюдаемую переменную v0. Без C2 поиск вправе зафиксироваться на процессе 0 и пройти «мимо» промежуточного состояния диаманта — того самого, в котором нарушение и наступает.

Минимальный свидетель для C3. Сид 87, density 0,2: два процесса, три переменные, программа длиной 2, инвариант читает v1. Полный перебор — 4 состояния, invariant; без C3 — 2 состояния, ok. Нарушение достижимо за один шаг от начального состояния, и редукция без условия цикла его не видит:

потерянный контрпример:  (начало)   pc=00 v=000  p1:0       pc=01 v=010

Для C1 свидетелей не найдено ни при одной плотности. Ноль на 100 000 спецификаций.

8. Обсуждение

Результат по C1 требует аккуратной формулировки, и соблазн сказать «C1 не нужно» здесь нужно подавить. Отсутствие свидетеля — не доказательство отсутствия. Более того, теоретически C1 необходимо, и известны конструкции, где его снятие разрушает корректность.

Правдоподобных объяснений два, и оба сводятся к тому, что в этой конкретной реализации C1 редко оказывается связывающим ограничением.

Во-первых, C1 здесь реализовано консервативно. Условие проверяется структурно — «существует ли вообще действие другого процесса, зависящее от кандидата», — вместо анализа того, какие действия действительно могут выполниться следующими. Это отвергает часть законных ample-множеств. Инструмент, ошибающийся в сторону меньшей редукции, теряет производительность, но не корректность; и он же оказывается труднее опровергаемым экспериментально.

Во-вторых, C1 и C2 в этой конструкции сильно перекрываются. Кандидат, проходящий C2, пишет только невидимые переменные; в сгенерированном семействе невидимая переменная почти всегда оказывается приватной, а приватность влечёт независимость, то есть C1 выполняется автоматически. Чтобы нагрузить C1 отдельно, нужна спецификация с общей, но не наблюдаемой переменной, которую генератор порождает редко. Это прямое направление для продолжения работы.

Итоговая формулировка честна ровно настолько, насколько позволяют данные: необходимость C2 и C3 подтверждена экспериментально и конструктивно — с минимальными свидетелями, которые воспроизводятся по сиду. Необходимость C1 не подтверждена и не опровергнута; поставленный эксперимент не обладает достаточной мощностью для этого вопроса.

Отдельно стоит отметить методологическую ценность самой связки. Разница между корректной и некорректной редукцией не наблюдаема изнутри редуцированного поиска: оба варианта выводят «нарушений не найдено». Единственный доступный внешний арбитр — нередуцированный перебор. Практика, при которой в инструменте сохраняется заведомо медленный, но не способный ошибаться поиск, и все спецификации, достаточно маленькие для обоих, прогоняются через оба, — представляется единственным способом обосновать доверие к редукции. 100 000 совпадений из 100 000 в разделе 7.2 — это ровно то, что даёт такая практика.

9. Ограничения исследования

Одна реализация. Все выводы получены на pnueli. Числа в разделах 4 и 5 отражают в том числе особенности этой реализации: строковые ключи состояний, канонизация сортировкой, отсутствие дискового хранилища. Асимптотика в разделе 4 от реализации не зависит, абсолютные времена — зависят полностью.

Замкнутые формы получены индукцией по данным. Совпадения 5ⁿ, C(n+4, 4), 2ⁿ+3n и 4n+1 проверены на n = 2…8 и не доказаны. Для первых двух вывод очевиден комбинаторно; для 2ⁿ+3n и 4n+1 — правдоподобен, но требует доказательства.

Одна форма спецификации в эксперименте 1. workers(n) сконструирована так, чтобы обе редукции работали в полную силу. Это верхняя оценка выигрыша, а не типичный случай; типичный случай — раздел 6, где фактор равен единице.

Проверяются только инварианты. Реализация поддерживает предикаты состояния и одну форму живости при слабой справедливости. Полная LTL, вложенные темпоральные операторы и сильная справедливость не рассматривались; условия C0–C3 в классической формулировке обосновываются через статтер-эквивалентность для LTL без оператора X, и вопрос, насколько C2 ослабляемо для чистой проверки инвариантов, здесь не решался.

Генератор покрывает узкое семейство. 2–3 процесса, 3–5 переменных, программы длиной 2–3, единственный инвариант фиксированного вида. Отрицательный результат по C1 — прежде всего утверждение об этом семействе.

Модель — не реализация. Всё сказанное относится к спецификациям. Доказательство свойства модели ничего не говорит о том, реализует ли код алгоритм; для этого существует другой инструмент — детерминированная симуляция, — и сопоставление двух подходов выходит за рамки этой работы.

10. Выводы

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

2. Редукция стоит примерно двойной цены за посещённое состояние и эта доля не зависит от размера задачи. При большом факторе она пренебрежима, при факторе 1,00× — является единственным итогом.

3. На семи спецификациях из десяти редукция не убирает ничего и добавляет 2–3 % времени. Включение POR по умолчанию не является бесплатной страховкой.

4. Условия C2 и C3 необходимы: построены минимальные воспроизводимые спецификации, на которых снятие каждого из них приводит к потере достижимого нарушения инварианта. Необходимость C1 экспериментально не подтверждена; данных для вывода недостаточно.

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

11. Воспроизведение

git clone https://github.com/BOTIROFF-D/pnueli && cd pnueligit checkout daee203npm install# эксперименты 1–3npx vitest run exp/ablation# эксперимент 4 (100 000 спецификаций, ~13 с)npx vitest run exp/witness

Файлы exp/ablation.test.ts и exp/witness.test.ts содержат копию checkReduced с вынесенными во флаги условиями и детерминированный генератор. Сиды 7266 и 87 воспроизводят минимальных свидетелей для C2 и C3.

12. Литература

1. Peled D. All from One, One for All: On Model Checking Using Representatives. CAV 1993. — метод ample-множеств.

2. Clarke E., Grumberg O., Peled D. Model Checking. MIT Press. — каноническое изложение условий C0–C3.

3. Godefroid P. Partial-Order Methods for the Verification of Concurrent Systems. LNCS 1032, 1996. — persistent sets.

4. Valmari A. A Stubborn Attack on State Explosion. CAV 1990. — stubborn sets.

5. Clarke E., Filkorn T., Jha S. Exploiting Symmetry in Temporal Logic Model Checking. CAV 1993.

6. Emerson E. A., Sistla A. P. Symmetry and Model Checking. CAV 1993.

7. Pnueli A. The Temporal Logic of Programs. FOCS 1977. — темпоральная логика в верификации программ; премия Тьюринга 1996.

8. Holzmann G. The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, 2003.

9. Lamport L. Specifying Systems: The TLA+ Language and Tools. Addison-Wesley, 2002.

10. Ongaro D., Ousterhout J. In Search of an Understandable Consensus Algorithm. USENIX ATC 2014. — модель выборов лидера в разделах 6 и 7.

Об авторе

Дониёр Ботиров (Doniyor Botirov) — основатель dbit.one, компании полного цикла разработки со штаб-квартирой в Нью-Йорке и офисом в Ташкенте. Компания занимается системами, для которых цена ошибки измеряется не в упавшем экране: финтех-продукты, онлайн-банкинг, платёжные и учётные контуры.

Инженерные стандарты компании опубликованы открыто, как и набор инструментов, на которых они держатся:

• pnueli — explicit-state model checker, объект этого исследования;

• unflake — детерминированная симуляция для поиска гонок, взаимоблокировок и потерянных повторов с воспроизведением по сиду;

• bulwark — реализация Raft, проверяемая сеяными разделениями сети и отказами узлов по пяти свойствам безопасности из оригинальной статьи;

• adya — MVCC-движок с четырьмя уровнями изоляции, включая SSI по Cahill, и проверкой историй на циклы зависимостей.

Все — TypeScript, MIT, без зависимостей.

Разбор того, почему зелёный прогон тестов означает «не нашли», а не «нет», и что закрывает эту разницу: Тесты не доказывают отсутствие бага.