TLA+ не может проверить всё: чего не выразить формально
What TLA+ can and can't check
После заявления Бориса Черни о том, что Opus нашёл race conditions с помощью TLA+, в сети вспыхнул ажиотаж вокруг формальной верификации. Хиллел Уэйн, многолетний пропагандист TLA+, предупреждает: метод хорош для инвариантов и лайвнес-свойств, но бессилен там, где нужно выразить достижимость, гиперсвойства или свойства над множеством поведений. Он разбирает, какие ограничения заложены в саму логику TLA+ и почему это важно для проверки агентного кода.
TLA+ properties are implicitly quantified over all behaviors. … Any property TLA+ can check of the system must be a property that is true for every individual behavior. What does that leave out? A lot more than you'd expect!
- sourdecor
Я узнал о Quint[0] благодаря этому комментарию[1] на HN. Quint — это «исполняемый язык спецификаций [который работает в JavaScript] с восхитительным инструментарием, основанным на темпоральной логике действий (TLA)». По-моему, это круто, и всем, кто интересуется TLA+, стоит с ним ознакомиться.
- singron
Обожаю это. Отличное чтиво, если вы пытаетесь применить TLA+ для чего-нибудь.
С другой стороны, ещё одна вещь, в которой TLA+ не силён, — это моделирование атомиков и, в частности, слабой модели памяти или чего угодно, что не является последовательно консистентным. Если вы транслируете свой алгоритм в pcal, он будет выполняться так, как будто он последовательно консистентен. Если вам нужно смоделировать не-последовательную консистентность, то это придётся прописать в TLA+ явной логикой, что, вероятно, слишком сложно и чревато ошибками, чтобы делать это вручную. Модели памяти C/C++/Rust допускают кучу всяких безумств. Представляю, что нужно добавить кэши чтения и буферы отложенной записи для каждой переменной с инструкциями сброса кэша в нужных местах, но, может, есть и более элегантный способ.
Если вы используете rust, то у miri и loom есть анализаторы, которые могут проверить некоторое не-последовательно-консистентное поведение (причём loom вообще не реализует последовательную консистентность).
- adamddev1
Отличная статья. Люди продолжают говорить «мы можем просто написать тесты» или, в последнее время, «мы можем использовать формальную верификацию», думая, что это достаточные меры защиты, которые можно применить, а затем переложить всю реализацию на LLM. Но факт в том, что вероятностные угадывающие машины их не спасут. Людям никуда не деться от необходимости действительно понимать то, что они создают.
- rrook
Мне кажется, часть проблемы — это недостаток наших языков программирования. Обычно языки позволяют выражать частичные графы, что делает задачу верификации технически сложной. Моё мнение: язык, который предоставляет только семантику замкнутых графов, мог бы помочь сократить разрыв между моделью и реализацией, пусть даже и не абсолютно.
- metabagel
Обожаю встроенные сноски!