5.3 KiB
5.3 KiB
P01. Remix: спецификации разной гранулярности для проверки распределённых систем
- Версия и дата проверки: 1.0, 05.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).
Обязательный результат
- Проверяемый вопрос или утверждение: смешанная гранулярность спецификации уменьшает стоимость model checking относительно полностью детальной модели и обнаруживает расхождения, которые теряются в полностью грубой модели.
- Технический результат: Собрать воспроизводимый конвейер для трёх вариантов спецификации: генерация трасс в TLC, преобразование в формат проигрывателя, запуск на малой конфигурации ZooKeeper и автоматический отчёт о совпадениях и расхождениях. Все варианты должны использовать общие сценарии и одинаковые ограничения поиска.
- Эксперимент: воспроизвести генерацию и проигрывание трасс для ZooKeeper, затем сравнить грубую, детальную и смешанную спецификации по числу состояний, времени проверки и найденным расхождениям на 2–3 сценариях.
- Границы выводов: сравнение относится к выбранным сценариям ZooKeeper и ограничениям поиска TLC; оно не доказывает полноту спецификаций и не оценивает все возможные ошибки реализации.
- Ресурсный профиль: локально, Linux, CPU, 8–16 ГБ памяти. Если полная генерация пространства состояний слишком долгая, использовать демонстрационные трассы и уменьшенную конфигурацию ZooKeeper, сохранив сравнение трёх вариантов спецификации и проверку соответствия.
Содержательные направления
- спецификации и конфигурации TLC.
- воспроизведение трасс и инструментирование ZooKeeper.
- сравнение гранулярностей, контролируемые расхождения и анализ результатов.
Возможное продолжение
Детализировать один дополнительный модуль или изменение ZooKeeper, внести контролируемое расхождение между моделью и кодом либо исследовать границу, после которой дополнительная детализация перестаёт окупаться.