nis2/project-tasks/p01-remix.md

P01. Remix: спецификации разной гранулярности для проверки распределённых систем

• Версия и дата проверки: 1.1, 07.09.2026.
• Статус: готово к назначению.

Статья и исходные материалы

• Основная статья: Lingzhi Ouyang и соавт. — Multi-Grained Specifications for Distributed System Model Checking and Verification. EuroSys 2025, DOI 10.1145/3689031.3696069.
• Кратко о статье: Авторы проверяют ZooKeeper с помощью TLA+ и рассматривают конфликт между точностью модели и размером пространства состояний. Remix позволяет сочетать детальные спецификации целевых модулей с более грубыми спецификациями остальной системы и проверять соответствие модели коду. Подход помог обнаружить шесть серьёзных ошибок. В проекте сравниваются разные гранулярности спецификаций на сокращённых сценариях ZooKeeper.
• Почему результат актуален: работа 2025 года проверяет развивающуюся производственную систему; исправления шести найденных ошибок были приняты в ZooKeeper. Локальный демонстрационный путь использует Java 11, Python 3 и Maven и не требует кластера или специализированного оборудования.
• Артефакты и данные: Lingzhi-Ouyang/Remix под Apache-2.0, с ZooKeeper 3.9.1, TLC, генерацией модельных трасс, проверкой соответствия и детерминированным воспроизведением; комитет EuroSys присвоил артефакту знаки Available и Functional. Зафиксированные ревизии: Lingzhi-Ouyang/Remix@81869f1accc1 (Apache-2.0).
• Что уже предоставляет артефакт: Готовы ZooKeeper, смешанная спецификация generator/MSPEC_2.tla, генерация и преобразование трасс, их проигрывание и отчёт matchReport. Скрипты и демонстрационные трассы разрешено использовать как основу; они не заменяют новый сценарий и независимую проверку команды. Проверенные исходные материалы: демонстрационные трассы, конфигурация TLC.

Обязательный результат

• Проверяемый вопрос или утверждение: смешанная гранулярность спецификации уменьшает стоимость model checking относительно полностью детальной модели и обнаруживает расхождения, которые теряются в полностью грубой модели.
• Технический результат: Подготовить грубую, детальную и смешанную спецификации и общий воспроизводимый конвейер: генерация трасс в TLC, преобразование в формат проигрывателя, запуск на малой конфигурации ZooKeeper и автоматический отчёт о совпадениях и расхождениях. Готовый конвейер можно повторно использовать; все варианты должны включать новый сценарий и одинаковые ограничения поиска.
• Обязательное приращение команды: Добавить сценарий ZooKeeper, отсутствующий в демонстрационных трассах закреплённой версии, и включить его в сравнение гранулярностей. Для хотя бы одного совпадения или расхождения самостоятельно сопоставить события модели с журналами и состоянием реализации; итогового matchReport без этого разбора недостаточно.
• Эксперимент: Сравнить три гранулярности по числу состояний, времени проверки и расхождениям на 2–3 сценариях, включая отсутствующий в демонстрации. Хотя бы одно совпадение или расхождение независимо подтвердить по событиям и состоянию ZooKeeper, объяснив их соответствие модели; обнаружение неизвестной ошибки не требуется.
• Границы выводов: сравнение относится к выбранным сценариям ZooKeeper и ограничениям поиска TLC; оно не доказывает полноту спецификаций и не оценивает все возможные ошибки реализации.
• Ресурсный профиль: Локально, Linux, CPU, 8–16 ГБ памяти. При дорогой генерации уменьшить число событий и конфигурацию ZooKeeper, сохранив три гранулярности, новый сценарий и независимую проверку соответствия. Демонстрационные трассы подходят для проверки конвейера.

Содержательные направления

• спецификации трёх гранулярностей и конфигурации TLC.
• новый сценарий и воспроизведение трасс ZooKeeper.
• независимая проверка соответствия и сравнительный анализ.

Возможное продолжение

Детализировать один дополнительный модуль или изменение ZooKeeper, внести контролируемое расхождение между моделью и кодом либо исследовать границу, после которой дополнительная детализация перестаёт окупаться.

История уточнений

Дата	Версия	Основание	Изменение обязательного результата
07.09.2026	1.1	Статический просмотр закреплённого артефакта: готовые сценарии частично покрывают задание.	Добавлены новый сценарий и независимая проверка соответствия реализации; сокращённый путь сохраняет их.