Охота за 16-летней ошибкой SQLite с помощью TLA+: затронут ли dqlite?
Hunting a 16-year-old SQLite WAL bug with TLA+
Мы из команды dqlite в Canonical исследуем критическую ошибку в механизме WAL базы данных SQLite, существующую с 2010 года. Используя формальную верификацию с TLA+, мы смоделировали поведение системы, чтобы понять последовательность событий, приводящих к повреждению данных, и проверить, уязвим ли наш проект dqlite к этой проблеме.
Важным аспектом этой ошибки является не её реальное влияние, которое очень мало, а то, как долго она находилась в репозитории, как трудно было её найти и как сложно было воспроизвести.
- hackingonempty
TLA+ = формальный язык для моделирования программного обеспечения на уровне выше кода и оборудования на уровне выше схем, созданный Лесли Лемпортом (известным, среди прочего, векторными часами и Paxos).
- letFunny
Автор статьи здесь. Я удивлен, что пост был отправлен и попал на главную страницу! С радостью отвечу на любые вопросы
- mempko
Это просто супер, и я думаю, насколько эффективной была бы эта техника при генерации кода с помощью LLM. Пусть LLM генерирует и код, и модель TLA+. Используйте модель TLA+ как полигон для проверки кода (вместо написания тестов на исходном языке).
- romaaeterna
Мне не нравится заголовок. В статье на самом деле описывается процесс доказательства того, что в dqlite нет той же ошибки, что и в SQLite, с использованием спецификации TLA+. Исправление ошибки в SQLite было совершенно отдельным делом от того, что описано здесь.
- vatsachak
Нужно любить TLA+
Интересно, кто-нибудь работал над портированием его в Lean и созданием тактик для него?