osukhoroslov/nis2
1
Fork 0
Code Issues Pull Requests Actions Packages Activity

Update project task cards to version 1.1

Browse Source
This commit is contained in:
osukhoroslov
2026-09-07 21:46:04 +03:00
parent 2bbfdac874
commit f8a5e00ab9
42 changed files with 264 additions and 103 deletions
Download Patch File Download Diff File Expand all files Collapse all files
project-tasks/p01-remix.md
+15 -7
View File
@@ -1,6 +1,6 @@
# P01. Remix: спецификации разной гранулярности для проверки распределённых систем
- **Версия и дата проверки:** 1.0, 05.09.2026.
- **Версия и дата проверки:** 1.1, 07.09.2026.
- **Статус:** готово к назначению.
## Статья и исходные материалы
@@ -9,21 +9,29 @@
- **Кратко о статье:** Авторы проверяют 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).
- **Что уже предоставляет артефакт:** Готовы ZooKeeper, смешанная спецификация `generator/MSPEC_2.tla`, генерация и преобразование трасс, их проигрывание и отчёт `matchReport`. Скрипты и демонстрационные трассы разрешено использовать как основу; они не заменяют новый сценарий и независимую проверку команды. Проверенные исходные материалы: [демонстрационные трассы](https://github.com/Lingzhi-Ouyang/Remix/tree/81869f1accc1/traces/demo), [конфигурация TLC](https://github.com/Lingzhi-Ouyang/Remix/blob/81869f1accc1/generator/Zab-simulate.ini).
## Обязательный результат
- **Проверяемый вопрос или утверждение:** смешанная гранулярность спецификации уменьшает стоимость model checking относительно полностью детальной модели и обнаруживает расхождения, которые теряются в полностью грубой модели.
- **Технический результат:** Собрать воспроизводимый конвейер для трёх вариантов спецификации: генерация трасс в TLC, преобразование в формат проигрывателя, запуск на малой конфигурации ZooKeeper и автоматический отчёт о совпадениях и расхождениях. Все варианты должны использовать общие сценарии и одинаковые ограничения поиска.
- **Эксперимент:** воспроизвести генерацию и проигрывание трасс для ZooKeeper, затем сравнить грубую, детальную и смешанную спецификации по числу состояний, времени проверки и найденным расхождениям на 2–3 сценариях.
- **Технический результат:** Подготовить грубую, детальную и смешанную спецификации и общий воспроизводимый конвейер: генерация трасс в TLC, преобразование в формат проигрывателя, запуск на малой конфигурации ZooKeeper и автоматический отчёт о совпадениях и расхождениях. Готовый конвейер можно повторно использовать; все варианты должны включать новый сценарий и одинаковые ограничения поиска.
- **Обязательное приращение команды:** Добавить сценарий ZooKeeper, отсутствующий в демонстрационных трассах закреплённой версии, и включить его в сравнение гранулярностей. Для хотя бы одного совпадения или расхождения самостоятельно сопоставить события модели с журналами и состоянием реализации; итогового `matchReport` без этого разбора недостаточно.
- **Эксперимент:** Сравнить три гранулярности по числу состояний, времени проверки и расхождениям на 2–3 сценариях, включая отсутствующий в демонстрации. Хотя бы одно совпадение или расхождение независимо подтвердить по событиям и состоянию ZooKeeper, объяснив их соответствие модели; обнаружение неизвестной ошибки не требуется.
- **Границы выводов:** сравнение относится к выбранным сценариям ZooKeeper и ограничениям поиска TLC; оно не доказывает полноту спецификаций и не оценивает все возможные ошибки реализации.
- **Ресурсный профиль:** локально, Linux, CPU, 8–16 ГБ памяти. Если полная генерация пространства состояний слишком долгая, использовать демонстрационные трассы и уменьшенную конфигурацию ZooKeeper, сохранив сравнение трёх вариантов спецификации и проверку соответствия.
- **Ресурсный профиль:** Локально, Linux, CPU, 8–16 ГБ памяти. При дорогой генерации уменьшить число событий и конфигурацию ZooKeeper, сохранив три гранулярности, новый сценарий и независимую проверку соответствия. Демонстрационные трассы подходят для проверки конвейера.
## Содержательные направления
- спецификации и конфигурации TLC.
- воспроизведение трасс и инструментирование ZooKeeper.
- сравнение гранулярностей, контролируемые расхождения и анализ результатов.
- спецификации трёх гранулярностей и конфигурации TLC.
- новый сценарий и воспроизведение трасс ZooKeeper.
- независимая проверка соответствия и сравнительный анализ.
## Возможное продолжение
Детализировать один дополнительный модуль или изменение ZooKeeper, внести контролируемое расхождение между моделью и кодом либо исследовать границу, после которой дополнительная детализация перестаёт окупаться.
## История уточнений
| Дата | Версия | Основание | Изменение обязательного результата |
|---|---|---|---|
| 07.09.2026 | 1.1 | Статический просмотр закреплённого артефакта: готовые сценарии частично покрывают задание. | Добавлены новый сценарий и независимая проверка соответствия реализации; сокращённый путь сохраняет их. |