Извиняюсь за задержку с ответом, не сразу заметил.
TLA+ (и PlusCal, как более удобная и привычная программистам обёртка) — это в основном описание взаимодействующих автоматов. Хотя можно и много других вещей выразить в TLA+, но если цель ещё и моделировать, то практически только разновидности автоматов.
Alloy удобен для анализа структур, отношения между элементами которых описываются в реляционной логике первого порядка. Очень близко к описанию отношений между объектами (не в смысле ООП или подобного, а в смысле отражения объектов реального мира) в реляционных БД.
Частично Alloy и TLA+ пересекаются по классу тех систем, что можно ими описать. То есть, можно автоматы и в Alloy моделировать, если явно ввести моменты времени, порядок над ними и отношения между моментами времени и другими структурами системы. Но это будет неудобно и с существенными ограничениями. Ровно как в TLA+ можно описать варианты возможных структур и делать поиск по пространству возможных конфигураций этих структур, но это неудобно и весьма ограниченно.
В целом, первая моя статья описывает весьма характерную задачу для Alloy, а вторая статья — для TLA+
На мой взгляд, это была бы отличная статья для начинающих.
Некоторые тонкие моменты, возможно, я могу потом раскрыть в комментариях или других статьях (по поводу machine-closed спек, некоторые ньюансы временнОй логики, liveness и пр).
Можно конечно и в Alloy моделировать автоматы и их взаимодействие.
Я даже где-то выкладывал (или собирался выложить) Alloy модуль для работы с NDFA (non-determ. finite automata).
Так как и TLA+/TLC и Alloy делают поиск в пространстве состояний (по-разному, конечно), то понятно, что их области применения частично перекрываются.
Но, если посмотреть с точки зрения удобства использования формализмов для классов задач, то, на мой взгяд, Alloy удобен для исследования/моделирования структур, логики и операций над структурами и отношениями, а TLA+ для моделирования динамики в системах.
В других инструментах используются так называемые SAT-solver-ы, которые находят подстановку для логической формулы, при которой формула становится истинной. При этом саму формулу генерируют на основе описания, аналогичного примеру из статьи. То есть все отличия подобных инструментов лишь в обвязке вокруг сольвера, некоторые рисуют диаграммы, другие представляют всё в виде текста. Но ни один из них, естественно, никакие алгоритмы не проверяет. Все они проверяют (при помощи сольвера) можно ли подобрать состояние (а не алгоритм или его ветвь), при котором вылезут противоречия. Поэтому предполагать, что там как-то участвует алгоритм — неправильно, потому что это усложняет (до бесконечности, то есть делает недостижимым) моделирование. Без понимания сути придётся осваивать инструмент методом тыка, примерно как осваивают магию — вот такое заклинание действует вот так, а если изменить в заклинании одно слово — оно перестанет действовать. Почему перестанет? Потому что магия!
В начале статьи я немного уделил внимание тому, как работает TLC. Там принцип совершенно другой — это просто явный перебор пространства состояний.
В целом, одна из лучших связок инструментов на практике — это Alloy и TLA+/TLC. Alloy — для исследований структур и операций над ними, а TLA+/TLC — для проверки протоколов, интерфейсов взаимодействия, распределённых/параллельных алгоритмов и пр., всего того, что можно моделировать множеством недетерминированных конечных автоматов.
Если будет достаточный интерес читателей, то я могу в следующих статьях подробно расписать, что под капотом у этих инструментов и как они работают внутри. Но у меня сложилось ощущение, что подкапотная логика не так интересна читателям, как примеры использования.
Тут тяжело всё хорошо и подробно расписать и при этом уложиться в разумный объём статьи.
В предыдущей статье (про Alloy) многие написали, что пример слишком абстрактный и хорошо бы что-нибудь из реальных примеров. Поэтому в этой статье я расписал реальный пример применения TLA+/TLC. Акцент постарался сделать именно на опыте применения TLA+/TLC.
Можно было бы больше уделить внимания особенностям самого TLA+/TLC, но тогда пришлось бы серьёзно сокращать другие части статьи, иначе объём был бы слишком большой, что многих читателей могло бы отпугнуть.
Этот цикл статей изначально задумывался не как обучающий (для тех, кому интереснее будет глубже познакомиться, приведено много ссылок на обучающие и другие материалы), а как ознакомительный, для демонстрации использования современных инструментов в разных прикладных задачах, чтобы показать в первую очередь лёгкость применения современных средств анализа, моделирования и верификации алгоритмов и ПО.
Это инструмент, помогающий работать в рамках формализма b-method, который позволяет итеративно и последовательно разрабатывать ПО от абстрактной модели к конкретному коду.
То есть, не сначала пишем код, потом спеки на свойства и пытаемся доказать соответствие одного другому, а сначала высокоуровневая модель, которая потом итеративно и через верификацию уточняется вплоть до кода (на C, Ada и тд).
Такой подход называется correct by construction. Есть довольно много вариантов такого подхода, и у всех них отличительная черта то, что весь процесс разработки закрыт формальной верификацией, от начальных спек до готового кода.
Если удастся это "скрещивание" надёжно убрать за абстракции DSL, и эти абстракции будут обладать хорошими с точки зрения верификации свойствами, то можно задачу верификации и упростить.
Рон Преслер и про DLS'и тоже писал :) Как один из способов расширения класса программ, которые можно верифицировать.
Есть другой подход — correct by construction. Сделать формализм, в рамках которого создать с нужными свойствами программу, а затем синтезировать нужные программные и аппаратные блоки из этого формализма. Пример такого подхода — b-method (AtelierB), например.
Ну, фундаментально все инструменты имеют ограничения.
И вообще, многие задачи в области computer science неразрешимы.
Тут нужно просто понимать, какие классы задач какими способами и какими инструментами решать.
Alloy, даже со всеми своими ограничениями, для своего класса задач (моделирование структур и операций над ними, как пример подкласса) очень хороший инструмент.
Если Alloy не хватает (упёрлись в ограничения логики первого порядка), можно взять Higher-Order Alloy (https://aleksandarmilicevic.github.io/hola/). Там возможна квантификация по высшим структурам.
И для того, чтобы на примерах показать какие классы задач какими инструментами и как решаются и был задуман мной этот цикл статей.
О! Оккам. Считаю, что он слишком сильно опередил своё время и поэтому не смог получить (вместе с транспьютерами) заслуженной оценки и распространения. Хотя идеологичеки (и даже синтаксически :) ) сильно повлиял на многие языки.
Что касается спецификации/верификации, то разбиение системы на небольшие модули (как программные так и аппаратные) с точки зрения свойств системы в целом, в общем случае задачу не облегчает.
Так как сложность верификации системы в целом определяется в первую очередь сложностью свойств, которые могут (и часто будут) и не декомпозироваться по модулям.
Хорошо это расписано у Рона Преслера: https://pron.github.io/posts/correctness-and-complexity
Начиная от того, что предикаты из спек перекладываются на assert'ы в коде и в тестах + (если используете property-based testing) по модели можно шейпить пространство состояний, проверяемое тестами (делать тесты более специфичными и направленными) и заканчивая методами, которые через итеративный процесс позволяют от абстрактных спек перейти к коду через последовательность уточняющих шагов со строгим доказательством сохранения более абстрактных в уточнённых (например, b-method и AtelierB, как инструмент для него).
Ещё можно использовать DSL, специально спроектированные для конкретных задач, которые позволят и модели получить и провести кодогенерацию из одного источника.
Арсенал на самом деле довольно большой, в каждой конкретной задаче, исходя из требуемой степени надёжности соответствия кода спекам, можно подобрать удобный подход и инструментарий.
Уже в процессе. :)
Там будет прямо из реальной практики пример применения TLA+.
Должно неплохо получиться: с одной стороны реальное применение на реальной задаче (ошибка в алгоритме, которая не ловилась на тестах, но было интуитивное ощущение, что она там есть, и она там действительно была :) ), с другой — небольшая модель, которая будет понятна всем даже без всяких "сколемизаций" :)
Правда процесс не быстрый :( Сейчас основной работы много :(
Некоторые говорят, что мало написал про внутреннюю кухню и математику стоящую за Alloy.
Вам показалось сложным пояснение про ограничения Alloy.
На самом деле, показанная ситуация с ограничением логики Alloy на практике нечасто встречается.
И этим инструментом (Alloy) можно вполне успешно и эффективно пользоваться даже не зная, что такое "сколемизация". Просто зная, что некоторые подкванторные выражения он не может анализировать и нужно либо их переформулировать в более простом виде, либо изменить условия (ослабить, например, как в примере в статье)
Теоретически никто не запрещает в property-based тестах генерировать не случайные состояния, а вообще все (в пределах заданных ограничений), но из-за комбинаторного взрыва это может быть очень медленно. Если TLC тупо брутфорсит все пространство состояний — это ведь ничем не лучше, или там все-таки есть какие-то оптимизации?
В принципе, можно и тестами перебирать все состояния.
Но задавшись вопросами оптимизации этого процесса, сначала (в случае explicit state model checker'а) вы придёте к идее абстракции, чтобы уменьшить комбинаторный взрыв, потом к идее о том, что нужно состояния перебирать эффективно, учитывая симметрию (это, например, когда у нас есть две модельных переменных x и y, принимающие значения из одного множества S, и в логике учитывается только случай x == y и x != y, тогда мы эффективно можем считать что S состоит всего из двух элементов, так как остальные варианты значения пар {x, y} приведут нас либо к трассам изоморфным всего двум трассам для x==y и x!=y), потом вы захотите проверять не только safety свойства, но и liveness и тд.
И таким образом, постепенно придёте к идеям и реализациям, которые лежат в основе TLC (и похожих инструментов).
Ну и если зададитесь более удобным (и надёжным с точки зрения математики) формализмом, то придёте к идее чего-то подобного TLA+.
Кроме того, для TLA+ есть ещё TLAPS, который позволяет формально доказывать! свойства TLA+ формул. Со всей математической строгостью.
То есть, то что невозможно нормально проверить (не всё, конечно, но довольно многое) с помощью TLC (получается комбинаторный взрыв), можно доказать с помощью TLAPS.
То есть вы можете перейти от model-checking к формальному доказательству в тех случаях, где TLC не хватило оставаясь в рамках одного формализма и даже одного набора инструментов (TLA toolbox IDE + TLC + TLAPS).
Кроме того, TLC из коробки сразу предлагает возможность запуска на кластере машин и тд.
В общем, тут вопрос в удобстве и уровнях абстракции. А TLAPS вообще никак не сымитировать тестами, даже самыми навороченными property-based.
Кроме того, property-based тестирование, на мой взгляд не предлагает удобного уровня абстракции, оно весьма низкоуровневое и там нужно прилагать усилия, чтобы использовать его на высоких уровнях абстракции. И тут же встаёт проблема надёжного перехода к более низким уровням, то что в TLA+ решается за счёт обычной импликации TLA+ формул (которую можно закрыть TLAPS абсолютно надёжно), в property-based тестировании опять же надёжно не сделать.
Ну или, например, взять B-method (AtelierB), там можно надёжно спуститься от самых высоких уровней абстракции вплоть до кодогенерации надёжно и доказуемо закрыв процесс уточнения моделей. На основе property-based тестов такого не достичь.
Тут всё зависит от того, что вам нужно, какие сроки, бюджеты, срок жизни проекта и тд.
Серьёзно закрывать всё формальными методами — это весьма дорого, хотя иногда может дать серьёзный выигрыш (см. OpenCOM RTOS) по объёмам разработки и отладки.
Alloy — да, за счет использования SAT-солвера может проверить пространство состояний гораздо быстрее, но как вы сами показали в статье далеко не все модели можно им проверить в принципе.
Alloy — это уникальный инструмент, который, когда понимаешь как он работает и как его использовать, становится очень полезным для быстрого прототипирования архитектур и их свойств. Сделать набросок конфигураций какой-либо системы и посмотреть, как она может меняться под воздействием каких-либо операций, какие варианты развития возможны — это очень быстро и просто при определённом навыке.
Да, у него есть ограничения, и на сколемизацию, и на рекурсию в формулах и на порядок отношений. Но эти все ограничения позволяют ему быть крайне эффективным в своём классе задач (всё что можно выразить в реляционной логике первого порядка с операторами замыкания и join, а это очень широкий класс задач).
И в реальности, по моему опыту (весьма небольшому, нужно признать) в ограничения Alloy я почти никогда не упирался. А если и упирался где-то, то зачастую весьма просто их обходил, переписав отношения или ослабив некоторые условия в системе.
Кроме того, сейчас идёт усиленные подвижки в сообществе Alloy в сторону SMT солверов, что ещё больше расширит класс задач, где можно использовать Alloy. Есть определённое развитие в сторону Higher-Order Alloy, там тоже интересные результаты.
Питон тоже умеет очень даже декларативно и коротко:
Да, часть предикатов он может коротко. Но если потребуется выражать чуть более сложные свойства, содержащие транзитивные замыкания, например, то тут уже становится далеко не так красиво и совсем неэффективно.
Я не совсем точно выразился, контр-примеры искать конечно можно для safety свойств, но крайне неэффективно в общем случае, а про liveness свойства можно забыть, так как никакие тесты не позволят нормально проверить все трассы которые удовлетворяют или не удовлетворяют определённым LTL формулам. Ну либо вы уже среду тестирования превратите в model-checker :) И это уже будет model-checker с опцией тестирования :) Прямо как TLC (у него есть режим тестирования на рандомных цепочках трасс состояний) :)
Вот пример теста, который проверяет кучу инвариантов для протокола смены лидера (в частности, упрощенно, что если он начался, то в итоге закончится и все запросы выполненные хотя бы на одной ноде окажутся в очереди на выполнение всеми нодами): https://github.com/hyperledger/indy-plenum/blob/master/plenum/test/consensus/test_sim_view_change.py#L9 Причем проверяет это непосредственно для продакшн-кода на большом количестве конфигураций, а за счет инъекции всех внешних зависимостей (в частности времени, шедулера и сетевого стека) тест работает повторяемо и достаточно быстро. Багов в начальной имплементации кстати этот тест наловил прилично.
Ну это уже явное движение в сторону explicit state model checkers, как я уже и писал, можно в эту сторону дойти до функционального аналога TLC, но с особенностями в виде потери возможности уточнения моделей и возможности верификации (TLAPS), так как для этих возможностей нужен уже соотв. формализм (с определённым математическими свойствами, этот формализм, в принципе можно получить из целевого языка (питона, например), если его ограничить до определённой степени, но боюсь, там от питона только часть синтаксиса останется, семантика уже будет совершенно другая)
Только вы не подумайте, что я агитирую за Alloy/TLA+ в противовес тестированию и в частности property-based тестированию. Совсем нет. Наоборот model-checkers и model-finders могут дать огромный буст тестированию при правильном применении. И уж тем более они не заменяют тестирование.
Alloy, и возможно TLC, могут эффективнее перебирать пространства состояний (но при этом Alloy довольно ограничен в том, какие свойства в принципе поддаются проверке)
Не только эффективнее, но и могут делать то, что тестами сделать невозможно (TLAPS, как уже писал выше). Или оператор транзитивного замыкания отношений в Alloy (SAT солверы его вычисляют мгновенно, а у тестов будет комбинаторный взрыв и время улетит в бесконечность)
Кроме того, что Alloy, что TLA+ — это формализмы со специально разработанными свойствами, что тоже даёт определённые бонусы.
Alloy и TLA+ заточены под быстрое прототипирование высокоуровневых моделей (но при этом те же генераторы состояний и тесты инвариантов придется дублировать и для продакшн кода)
Да, в основном высокоуровневые спеки и прототипы особенно критичных частей системы и общей архитектуры компонент.
И да, в тесты придётся переносить часть инвариантов и предикатов и тесты будут всё-равно нужны.
Но, прототипирование и проверка свойств прототипов на Alloy и TLA+ просто несопоставимо быстрее, чем если это делать, например на питоне (даже без учёта написания тестов, просто описать модель в коде питона будет на порядок — два медленнее).
Возможно, если поискать различные DSL и фреймворки, задача прототипирования и станет чуть проще, но, думаю, к Alloy/TLA+ всё равно будет тяжело приблизиться.
И ещё такой момент, когда возникает "пощупать" какую-либо архитектурную идею, то на формальных спеках это можно сделать очень быстро и эффективно (ну и соответственно быстро найти фундаментальные проблемы), чем пытаться проверить её на уже готовом пуле кода и тестов.
В общем, я все это не к тому, что "TLA не нужен" — мне этот подход очень даже понравился, в каком-то смысле есть ощущение, что это как бы следующая ступенька над обычными спецификациями и генеративными тестами по их мотивам, но просто ощущения скорее всего будет недостаточно, чтобы "продать" эту идею менеджменту, при том, что мы уже используем property-based тестирование.
Круто, что используете property-based тестирование! Реально весьма мало кто использует хотя-бы нормальное тестирование с хорошим покрытием.
Во-первых — спасибо за статью, много нового узнал.
Пожалуйста! Рад, что статья оказалась полезной.
А во-вторых — пока читал не отпускала мысль: это очень похоже на property based testing, даже у Hillel Wayne в блоге оно неоднократно упоминается.
Да, во многом сходство есть. Но есть и фундаментальное различие: property testing — это те же самые тесты, пусть и направленные (засчёт шейпинга случайных данных по precondition предикатам), но всё-таки тесты. То есть они пространство состояний покрывают не сплошным покрытием, а выборочным.
Alloy же, при поиске моделей, просматривает все состояния вплоть до заданного предела.
TLС тоже просматривает (в основном режиме работы) все состояния порождаемые TLA+ формулой.
Ну и собственно, это в основном и отличает их от тестов.
Например, те пространства, которые доступны Alloy, недоступны тестам.
Так вот, вопрос: даст ли какие-то преимущества использование Alloy/TLA+ по сравнению с написанием хорошо изолированной бизнес-логики, покрытой property based тестами?
Тут в одном вопросе на самом деле несколько тем затронуто:
Выразительность: Alloy и TLA+ напрямую с тестами тяжело сравнивать, так как выразительные свойства Alloy и TLA+ намного лучше, так как там мы пишем декларативно и на высоком уровне абстракции.
Например, в тестах мне явно нужно писать функцию сортировки или функцию проверки того, что массив отсортирован, в Alloy (и в TLA+ тоже, только синтаксис немного другой) я пишу предикат, где описываю нужное мне свойство: pred sorted [s: seq Obj] { all disj x,y: s.elems | x < y => s.idxOf[x] < s.idxOf[y]}
Зачастую выразить свойства объектов намного проще декларативно в логике, чем описывать в каком-либо языке программирования процедуру вычисления этого свойства.
То есть, абстрактные описания на Alloy и TLA+ получаются существенно короче, чем если то же самое описывать, например, на питоне.
TLA+ и Alloy предназначены для разных вещей, которые тестами тяжело либо невозможно сделать.
Например, на базе тестов нельзя нормально искать контр-примеры к конфигурации какой-либо системы. Alloy же позволяет не только это, а ещё, например, поиск конфигураций с учётом классов эквивалентности (редукция симметрии), как такого эффекта достичь с помощью тестов — сразу не могу придумать.
TLA+ позволяет довольно просто описать несколько взаимодействующих процессов системы и промоделировать их на наличие гонок, дедлоков и пр. Частично этого можно достичь тестами, но TLC просматривает все возможные состояния, причём делает это весьма эффективно и может запускаться на кластере машин. Тестами такое сложно сделать, ну и покрытия такого сложно достичь.
Кроме того, TLA+/TLC позволяет проверить систему не только на safety свойства, но ещё и на liveness, то есть то что система у нас не только не делает плохих вещей, но и то что она обязательно делает что-то хорошее и полезное. Проверка liveness свойств с помощью тестов — тоже что-то такое, на что у меня воображения не хватает, так как там нужно проверять темпоральные формулы по трассам переходов системы в пространстве состояний.
То есть, с помощью model-finders/model-checkers решается существенно другой класс задач, чем тестами (даже направленными, фаззингом и др.). Что совсем не исключает тестов, а напротив, эти инструменты серьёзно усиливают тесты.
Понятно, что скорее всего на Alloy прототип можно набросать быстрее, чем даже на каком-нибудь питоне, но потом все равно придется писать реализацию, проверять на соответствие прототипу (глазами?) и крыть теми же тестами с проверками инвариантов — и разве генерация тест кейсов не даст те же плюшки, что и Alloy?
В статье есть хороший пример того, что сделать тестами весьма сложно — проверка свойств операций. Инварианты для нужных мне свойств операций я разрабатывал с помощью модели и поиска контр-примеров. Как примерно то же самое делать с тестами, да ещё и более менее эффективно — я не знаю.
Реализацию конечно придётся писать, и тесты на реализацию тоже. Но на модели можно обкатать все нужные свойства, предикаты и инварианты и уже на их базе разрабатывать направленные тесты.
Ну и ещё есть класс вещей, которые тестам практически не доступны: это распределённые системы, параллельное и асинхронные системы, в общем любой класс систем с существенным недетерминизмом в логике управления (когда много потоков управления с асинхронным недетерминированными событиями и реакциями на них).
Зато такой класс систем вполне успешно можно разрабатывать с применением model-checkers/model-finders, закрывая ими сложные недетерминированные места в логике, а последовательную логику можно и тестами закрыть.
Или там есть еще какие-то неочевидные преимущества?
Почему неочевидные?
Преимущества как раз хорошо очевидны:
На спеках с помощью Alloy/TLA+ и др мы отлаживаем архитектуру и самые базовые абстрактные вещи, отлаживаем синхронизационный скелет системы и основные сложные моменты. Это даёт нам шанс избежать дорогостоящих архитектурных, синхронизационных и др. ошибок, которые тестами тяжело, либо практически невозможно (ошибки в распределённых и параллельных системах) потом поймать стабильно на тестах и отладить.
На основе спек мы получаем множество предикатов, инвариантов и прочего, которые закладываем в код и тесты. Тесты в этом случае можно сделать намного более направленными и специфичными.
Намного проще становится делать серьёзный рефакторинг, который затрагивает архитектуру и базис системы. Мы всегда новый функционал можем проверить на спеках на совместимость с уже существующим. Что позволяет опять же избегать дорогостоящих ошибок.
о хотя бы переход от модели к логической формуле конкретно для вашего инструмента вы могли бы показать? Ведь вам понятен (надеюсь) инструмент, вы даже утверждаете, что понятна стоящая за ним математика, так почему нельзя по простому показать это банальное отображение модели на формулу с последующим указанием на суть перебора значений для полученной формулы?
Цель была другая совсем. Хотел привести именно пример использования инструмента, а не расписывать внутренности и математику.
Когда машину показывают среднестатистическому покупателю, ему же рассказывают про то как её клёво использовать, как она быстро ездит и как удобно ею рулить, а не про принципы двигателей внутреннего сгорания и как программировать микроконтроллеры в управляющей электронике, правильно?
Так же и эта статья призвана показать использование инструмента, а не математику и эвристики SAT-солверов (кстати, SAT только на первый взгляд простые, а на самом деле там огромное количество ньюансов, начиная от эвристик по выбору порядка переменных при построении BDD на основе формулы до эвристик по оптимизации формулы и тд.), то в ней и не уделялось внимание подкапотному пространству.
Если увижу, что многим людям интереснее про математику и внутренности тулов, то может напишу статьи и про это.
Насчёт DHT — лично мне очень понравилась Kademlia, показалась наиболее понятной и простой в реализации (ну и судя по количеству проектов на её вариациях, видимо у многих такое же мнение).
Извиняюсь за задержку с ответом, не сразу заметил.
TLA+ (и PlusCal, как более удобная и привычная программистам обёртка) — это в основном описание взаимодействующих автоматов. Хотя можно и много других вещей выразить в TLA+, но если цель ещё и моделировать, то практически только разновидности автоматов.
Alloy удобен для анализа структур, отношения между элементами которых описываются в реляционной логике первого порядка. Очень близко к описанию отношений между объектами (не в смысле ООП или подобного, а в смысле отражения объектов реального мира) в реляционных БД.
Частично Alloy и TLA+ пересекаются по классу тех систем, что можно ими описать. То есть, можно автоматы и в Alloy моделировать, если явно ввести моменты времени, порядок над ними и отношения между моментами времени и другими структурами системы. Но это будет неудобно и с существенными ограничениями. Ровно как в TLA+ можно описать варианты возможных структур и делать поиск по пространству возможных конфигураций этих структур, но это неудобно и весьма ограниченно.
В целом, первая моя статья описывает весьма характерную задачу для Alloy, а вторая статья — для TLA+
На мой взгляд, это была бы отличная статья для начинающих.
Некоторые тонкие моменты, возможно, я могу потом раскрыть в комментариях или других статьях (по поводу machine-closed спек, некоторые ньюансы временнОй логики, liveness и пр).
Было бы здорово, если бы вы написали статью именно как туториал для начинающих, по свежим следам, так сказать.
Мне сложнее писать туториалы для начинающих, так как уже тяжело вспоминать (да и не вспомню многого), как начанал работать с TLA+.
Можно конечно и в Alloy моделировать автоматы и их взаимодействие.
Я даже где-то выкладывал (или собирался выложить) Alloy модуль для работы с NDFA (non-determ. finite automata).
Так как и TLA+/TLC и Alloy делают поиск в пространстве состояний (по-разному, конечно), то понятно, что их области применения частично перекрываются.
Но, если посмотреть с точки зрения удобства использования формализмов для классов задач, то, на мой взгяд, Alloy удобен для исследования/моделирования структур, логики и операций над структурами и отношениями, а TLA+ для моделирования динамики в системах.
Они хорошо взаимодополняют друг-друга.
В начале статьи я немного уделил внимание тому, как работает TLC. Там принцип совершенно другой — это просто явный перебор пространства состояний.
В целом, одна из лучших связок инструментов на практике — это Alloy и TLA+/TLC. Alloy — для исследований структур и операций над ними, а TLA+/TLC — для проверки протоколов, интерфейсов взаимодействия, распределённых/параллельных алгоритмов и пр., всего того, что можно моделировать множеством недетерминированных конечных автоматов.
Если будет достаточный интерес читателей, то я могу в следующих статьях подробно расписать, что под капотом у этих инструментов и как они работают внутри. Но у меня сложилось ощущение, что подкапотная логика не так интересна читателям, как примеры использования.
Тут тяжело всё хорошо и подробно расписать и при этом уложиться в разумный объём статьи.
В предыдущей статье (про Alloy) многие написали, что пример слишком абстрактный и хорошо бы что-нибудь из реальных примеров. Поэтому в этой статье я расписал реальный пример применения TLA+/TLC. Акцент постарался сделать именно на опыте применения TLA+/TLC.
Можно было бы больше уделить внимания особенностям самого TLA+/TLC, но тогда пришлось бы серьёзно сокращать другие части статьи, иначе объём был бы слишком большой, что многих читателей могло бы отпугнуть.
Этот цикл статей изначально задумывался не как обучающий (для тех, кому интереснее будет глубже познакомиться, приведено много ссылок на обучающие и другие материалы), а как ознакомительный, для демонстрации использования современных инструментов в разных прикладных задачах, чтобы показать в первую очередь лёгкость применения современных средств анализа, моделирования и верификации алгоритмов и ПО.
Как уже вам успел ответить пользователь alygin, процесс довольно прост:
Во многом похоже на обычную отладку программ, когда просматриваете back-trace при нарушении какого-либо assert'a.
Насколько я понял, имеются в виду моделируемые процессы?
Да, конечно:
Будет запущено моделирование 3-х потоков event_processor с соответствующими названиями.
Описание ошибки выглядит довольно просто: выводится свойство, которое было нарушено и трасса, которая привела к нарушению свойства.
Вот пример, как это выглядит в IDE:
Я же прямо пример привел: AtelierB
Это инструмент, помогающий работать в рамках формализма b-method, который позволяет итеративно и последовательно разрабатывать ПО от абстрактной модели к конкретному коду.
То есть, не сначала пишем код, потом спеки на свойства и пытаемся доказать соответствие одного другому, а сначала высокоуровневая модель, которая потом итеративно и через верификацию уточняется вплоть до кода (на C, Ada и тд).
Такой подход называется correct by construction. Есть довольно много вариантов такого подхода, и у всех них отличительная черта то, что весь процесс разработки закрыт формальной верификацией, от начальных спек до готового кода.
Если удастся это "скрещивание" надёжно убрать за абстракции DSL, и эти абстракции будут обладать хорошими с точки зрения верификации свойствами, то можно задачу верификации и упростить.
Рон Преслер и про DLS'и тоже писал :) Как один из способов расширения класса программ, которые можно верифицировать.
Есть другой подход — correct by construction. Сделать формализм, в рамках которого создать с нужными свойствами программу, а затем синтезировать нужные программные и аппаратные блоки из этого формализма. Пример такого подхода — b-method (AtelierB), например.
Ну, фундаментально все инструменты имеют ограничения.
И вообще, многие задачи в области computer science неразрешимы.
Тут нужно просто понимать, какие классы задач какими способами и какими инструментами решать.
Alloy, даже со всеми своими ограничениями, для своего класса задач (моделирование структур и операций над ними, как пример подкласса) очень хороший инструмент.
Если Alloy не хватает (упёрлись в ограничения логики первого порядка), можно взять Higher-Order Alloy (https://aleksandarmilicevic.github.io/hola/). Там возможна квантификация по высшим структурам.
И для того, чтобы на примерах показать какие классы задач какими инструментами и как решаются и был задуман мной этот цикл статей.
О! Оккам. Считаю, что он слишком сильно опередил своё время и поэтому не смог получить (вместе с транспьютерами) заслуженной оценки и распространения. Хотя идеологичеки (и даже синтаксически :) ) сильно повлиял на многие языки.
Что касается спецификации/верификации, то разбиение системы на небольшие модули (как программные так и аппаратные) с точки зрения свойств системы в целом, в общем случае задачу не облегчает.
Так как сложность верификации системы в целом определяется в первую очередь сложностью свойств, которые могут (и часто будут) и не декомпозироваться по модулям.
Хорошо это расписано у Рона Преслера: https://pron.github.io/posts/correctness-and-complexity
На самом деле идей много.
Начиная от того, что предикаты из спек перекладываются на assert'ы в коде и в тестах + (если используете property-based testing) по модели можно шейпить пространство состояний, проверяемое тестами (делать тесты более специфичными и направленными) и заканчивая методами, которые через итеративный процесс позволяют от абстрактных спек перейти к коду через последовательность уточняющих шагов со строгим доказательством сохранения более абстрактных в уточнённых (например, b-method и AtelierB, как инструмент для него).
Ещё можно использовать DSL, специально спроектированные для конкретных задач, которые позволят и модели получить и провести кодогенерацию из одного источника.
Арсенал на самом деле довольно большой, в каждой конкретной задаче, исходя из требуемой степени надёжности соответствия кода спекам, можно подобрать удобный подход и инструментарий.
Уже в процессе. :)
Там будет прямо из реальной практики пример применения TLA+.
Должно неплохо получиться: с одной стороны реальное применение на реальной задаче (ошибка в алгоритме, которая не ловилась на тестах, но было интуитивное ощущение, что она там есть, и она там действительно была :) ), с другой — небольшая модель, которая будет понятна всем даже без всяких "сколемизаций" :)
Правда процесс не быстрый :( Сейчас основной работы много :(
Ну тут всем не угодишь :)
Некоторые говорят, что мало написал про внутреннюю кухню и математику стоящую за Alloy.
Вам показалось сложным пояснение про ограничения Alloy.
На самом деле, показанная ситуация с ограничением логики Alloy на практике нечасто встречается.
И этим инструментом (Alloy) можно вполне успешно и эффективно пользоваться даже не зная, что такое "сколемизация". Просто зная, что некоторые подкванторные выражения он не может анализировать и нужно либо их переформулировать в более простом виде, либо изменить условия (ослабить, например, как в примере в статье)
В принципе, можно и тестами перебирать все состояния.
Но задавшись вопросами оптимизации этого процесса, сначала (в случае explicit state model checker'а) вы придёте к идее абстракции, чтобы уменьшить комбинаторный взрыв, потом к идее о том, что нужно состояния перебирать эффективно, учитывая симметрию (это, например, когда у нас есть две модельных переменных x и y, принимающие значения из одного множества S, и в логике учитывается только случай x == y и x != y, тогда мы эффективно можем считать что S состоит всего из двух элементов, так как остальные варианты значения пар {x, y} приведут нас либо к трассам изоморфным всего двум трассам для x==y и x!=y), потом вы захотите проверять не только safety свойства, но и liveness и тд.
И таким образом, постепенно придёте к идеям и реализациям, которые лежат в основе TLC (и похожих инструментов).
Ну и если зададитесь более удобным (и надёжным с точки зрения математики) формализмом, то придёте к идее чего-то подобного TLA+.
Кроме того, для TLA+ есть ещё TLAPS, который позволяет формально доказывать! свойства TLA+ формул. Со всей математической строгостью.
То есть, то что невозможно нормально проверить (не всё, конечно, но довольно многое) с помощью TLC (получается комбинаторный взрыв), можно доказать с помощью TLAPS.
То есть вы можете перейти от model-checking к формальному доказательству в тех случаях, где TLC не хватило оставаясь в рамках одного формализма и даже одного набора инструментов (TLA toolbox IDE + TLC + TLAPS).
Кроме того, TLC из коробки сразу предлагает возможность запуска на кластере машин и тд.
В общем, тут вопрос в удобстве и уровнях абстракции. А TLAPS вообще никак не сымитировать тестами, даже самыми навороченными property-based.
Кроме того, property-based тестирование, на мой взгляд не предлагает удобного уровня абстракции, оно весьма низкоуровневое и там нужно прилагать усилия, чтобы использовать его на высоких уровнях абстракции. И тут же встаёт проблема надёжного перехода к более низким уровням, то что в TLA+ решается за счёт обычной импликации TLA+ формул (которую можно закрыть TLAPS абсолютно надёжно), в property-based тестировании опять же надёжно не сделать.
Ну или, например, взять B-method (AtelierB), там можно надёжно спуститься от самых высоких уровней абстракции вплоть до кодогенерации надёжно и доказуемо закрыв процесс уточнения моделей. На основе property-based тестов такого не достичь.
Тут всё зависит от того, что вам нужно, какие сроки, бюджеты, срок жизни проекта и тд.
Серьёзно закрывать всё формальными методами — это весьма дорого, хотя иногда может дать серьёзный выигрыш (см. OpenCOM RTOS) по объёмам разработки и отладки.
Alloy — это уникальный инструмент, который, когда понимаешь как он работает и как его использовать, становится очень полезным для быстрого прототипирования архитектур и их свойств. Сделать набросок конфигураций какой-либо системы и посмотреть, как она может меняться под воздействием каких-либо операций, какие варианты развития возможны — это очень быстро и просто при определённом навыке.
Да, у него есть ограничения, и на сколемизацию, и на рекурсию в формулах и на порядок отношений. Но эти все ограничения позволяют ему быть крайне эффективным в своём классе задач (всё что можно выразить в реляционной логике первого порядка с операторами замыкания и join, а это очень широкий класс задач).
И в реальности, по моему опыту (весьма небольшому, нужно признать) в ограничения Alloy я почти никогда не упирался. А если и упирался где-то, то зачастую весьма просто их обходил, переписав отношения или ослабив некоторые условия в системе.
Кроме того, сейчас идёт усиленные подвижки в сообществе Alloy в сторону SMT солверов, что ещё больше расширит класс задач, где можно использовать Alloy. Есть определённое развитие в сторону Higher-Order Alloy, там тоже интересные результаты.
Да, часть предикатов он может коротко. Но если потребуется выражать чуть более сложные свойства, содержащие транзитивные замыкания, например, то тут уже становится далеко не так красиво и совсем неэффективно.
Я не совсем точно выразился, контр-примеры искать конечно можно для safety свойств, но крайне неэффективно в общем случае, а про liveness свойства можно забыть, так как никакие тесты не позволят нормально проверить все трассы которые удовлетворяют или не удовлетворяют определённым LTL формулам. Ну либо вы уже среду тестирования превратите в model-checker :) И это уже будет model-checker с опцией тестирования :) Прямо как TLC (у него есть режим тестирования на рандомных цепочках трасс состояний) :)
Ну это уже явное движение в сторону explicit state model checkers, как я уже и писал, можно в эту сторону дойти до функционального аналога TLC, но с особенностями в виде потери возможности уточнения моделей и возможности верификации (TLAPS), так как для этих возможностей нужен уже соотв. формализм (с определённым математическими свойствами, этот формализм, в принципе можно получить из целевого языка (питона, например), если его ограничить до определённой степени, но боюсь, там от питона только часть синтаксиса останется, семантика уже будет совершенно другая)
Только вы не подумайте, что я агитирую за Alloy/TLA+ в противовес тестированию и в частности property-based тестированию. Совсем нет. Наоборот model-checkers и model-finders могут дать огромный буст тестированию при правильном применении. И уж тем более они не заменяют тестирование.
Не только эффективнее, но и могут делать то, что тестами сделать невозможно (TLAPS, как уже писал выше). Или оператор транзитивного замыкания отношений в Alloy (SAT солверы его вычисляют мгновенно, а у тестов будет комбинаторный взрыв и время улетит в бесконечность)
Кроме того, что Alloy, что TLA+ — это формализмы со специально разработанными свойствами, что тоже даёт определённые бонусы.
Да, в основном высокоуровневые спеки и прототипы особенно критичных частей системы и общей архитектуры компонент.
И да, в тесты придётся переносить часть инвариантов и предикатов и тесты будут всё-равно нужны.
Но, прототипирование и проверка свойств прототипов на Alloy и TLA+ просто несопоставимо быстрее, чем если это делать, например на питоне (даже без учёта написания тестов, просто описать модель в коде питона будет на порядок — два медленнее).
Возможно, если поискать различные DSL и фреймворки, задача прототипирования и станет чуть проще, но, думаю, к Alloy/TLA+ всё равно будет тяжело приблизиться.
И ещё такой момент, когда возникает "пощупать" какую-либо архитектурную идею, то на формальных спеках это можно сделать очень быстро и эффективно (ну и соответственно быстро найти фундаментальные проблемы), чем пытаться проверить её на уже готовом пуле кода и тестов.
Круто, что используете property-based тестирование! Реально весьма мало кто использует хотя-бы нормальное тестирование с хорошим покрытием.
Пожалуйста! Рад, что статья оказалась полезной.
Да, во многом сходство есть. Но есть и фундаментальное различие: property testing — это те же самые тесты, пусть и направленные (засчёт шейпинга случайных данных по precondition предикатам), но всё-таки тесты. То есть они пространство состояний покрывают не сплошным покрытием, а выборочным.
Alloy же, при поиске моделей, просматривает все состояния вплоть до заданного предела.
TLС тоже просматривает (в основном режиме работы) все состояния порождаемые TLA+ формулой.
Ну и собственно, это в основном и отличает их от тестов.
Например, те пространства, которые доступны Alloy, недоступны тестам.
Тут в одном вопросе на самом деле несколько тем затронуто:
Например, в тестах мне явно нужно писать функцию сортировки или функцию проверки того, что массив отсортирован, в Alloy (и в TLA+ тоже, только синтаксис немного другой) я пишу предикат, где описываю нужное мне свойство: pred sorted [s: seq Obj] { all disj x,y: s.elems | x < y => s.idxOf[x] < s.idxOf[y]}
Зачастую выразить свойства объектов намного проще декларативно в логике, чем описывать в каком-либо языке программирования процедуру вычисления этого свойства.
То есть, абстрактные описания на Alloy и TLA+ получаются существенно короче, чем если то же самое описывать, например, на питоне.
Например, на базе тестов нельзя нормально искать контр-примеры к конфигурации какой-либо системы. Alloy же позволяет не только это, а ещё, например, поиск конфигураций с учётом классов эквивалентности (редукция симметрии), как такого эффекта достичь с помощью тестов — сразу не могу придумать.
TLA+ позволяет довольно просто описать несколько взаимодействующих процессов системы и промоделировать их на наличие гонок, дедлоков и пр. Частично этого можно достичь тестами, но TLC просматривает все возможные состояния, причём делает это весьма эффективно и может запускаться на кластере машин. Тестами такое сложно сделать, ну и покрытия такого сложно достичь.
Кроме того, TLA+/TLC позволяет проверить систему не только на safety свойства, но ещё и на liveness, то есть то что система у нас не только не делает плохих вещей, но и то что она обязательно делает что-то хорошее и полезное. Проверка liveness свойств с помощью тестов — тоже что-то такое, на что у меня воображения не хватает, так как там нужно проверять темпоральные формулы по трассам переходов системы в пространстве состояний.
То есть, с помощью model-finders/model-checkers решается существенно другой класс задач, чем тестами (даже направленными, фаззингом и др.). Что совсем не исключает тестов, а напротив, эти инструменты серьёзно усиливают тесты.
В статье есть хороший пример того, что сделать тестами весьма сложно — проверка свойств операций. Инварианты для нужных мне свойств операций я разрабатывал с помощью модели и поиска контр-примеров. Как примерно то же самое делать с тестами, да ещё и более менее эффективно — я не знаю.
Реализацию конечно придётся писать, и тесты на реализацию тоже. Но на модели можно обкатать все нужные свойства, предикаты и инварианты и уже на их базе разрабатывать направленные тесты.
Ну и ещё есть класс вещей, которые тестам практически не доступны: это распределённые системы, параллельное и асинхронные системы, в общем любой класс систем с существенным недетерминизмом в логике управления (когда много потоков управления с асинхронным недетерминированными событиями и реакциями на них).
Зато такой класс систем вполне успешно можно разрабатывать с применением model-checkers/model-finders, закрывая ими сложные недетерминированные места в логике, а последовательную логику можно и тестами закрыть.
Почему неочевидные?
Преимущества как раз хорошо очевидны:
На спеках с помощью Alloy/TLA+ и др мы отлаживаем архитектуру и самые базовые абстрактные вещи, отлаживаем синхронизационный скелет системы и основные сложные моменты. Это даёт нам шанс избежать дорогостоящих архитектурных, синхронизационных и др. ошибок, которые тестами тяжело, либо практически невозможно (ошибки в распределённых и параллельных системах) потом поймать стабильно на тестах и отладить.
На основе спек мы получаем множество предикатов, инвариантов и прочего, которые закладываем в код и тесты. Тесты в этом случае можно сделать намного более направленными и специфичными.
Намного проще становится делать серьёзный рефакторинг, который затрагивает архитектуру и базис системы. Мы всегда новый функционал можем проверить на спеках на совместимость с уже существующим. Что позволяет опять же избегать дорогостоящих ошибок.
Цель была другая совсем. Хотел привести именно пример использования инструмента, а не расписывать внутренности и математику.
Когда машину показывают среднестатистическому покупателю, ему же рассказывают про то как её клёво использовать, как она быстро ездит и как удобно ею рулить, а не про принципы двигателей внутреннего сгорания и как программировать микроконтроллеры в управляющей электронике, правильно?
Так же и эта статья призвана показать использование инструмента, а не математику и эвристики SAT-солверов (кстати, SAT только на первый взгляд простые, а на самом деле там огромное количество ньюансов, начиная от эвристик по выбору порядка переменных при построении BDD на основе формулы до эвристик по оптимизации формулы и тд.), то в ней и не уделялось внимание подкапотному пространству.
Если увижу, что многим людям интереснее про математику и внутренности тулов, то может напишу статьи и про это.
Интересные идеи по ссылке.
Насчёт DHT — лично мне очень понравилась Kademlia, показалась наиболее понятной и простой в реализации (ну и судя по количеству проектов на её вариациях, видимо у многих такое же мнение).