30 lines
5.3 KiB
Markdown
30 lines
5.3 KiB
Markdown
|
# P01. Remix: спецификации разной гранулярности для проверки распределённых систем
|
|||
|
|
|
|||
|
|
- **Версия и дата проверки:** 1.0, 05.09.2026.
|
|||
|
|
- **Статус:** готово к назначению.
|
|||
|
|
|
|||
|
|
## Статья и исходные материалы
|
|||
|
|
|
|||
|
|
- **Основная статья:** Lingzhi Ouyang и соавт. — [Multi-Grained Specifications for Distributed System Model Checking and Verification](https://tianyin.github.io/pub/mspec.pdf). EuroSys 2025, DOI `10.1145/3689031.3696069`.
|
|||
|
|
- **Кратко о статье:** Авторы проверяют ZooKeeper с помощью TLA+ и рассматривают конфликт между точностью модели и размером пространства состояний. Remix позволяет сочетать детальные спецификации целевых модулей с более грубыми спецификациями остальной системы и проверять соответствие модели коду. Подход помог обнаружить шесть серьёзных ошибок. В проекте сравниваются разные гранулярности спецификаций на сокращённых сценариях ZooKeeper.
|
|||
|
|
- **Почему результат актуален:** работа 2025 года проверяет развивающуюся производственную систему; исправления шести найденных ошибок были приняты в ZooKeeper. Локальный демонстрационный путь использует Java 11, Python 3 и Maven и не требует кластера или специализированного оборудования.
|
|||
|
|
- **Артефакты и данные:** [Lingzhi-Ouyang/Remix](https://github.com/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, внести контролируемое расхождение между моделью и кодом либо исследовать границу, после которой дополнительная детализация перестаёт окупаться.
|