Хабрахабр

Инженерный подход к разработке ПО

Как сформулировать и проверить их свойства? Как проверить идеи, архитектуру и алгоритмы без написания кода? Требования и спецификации — пережиток прошлого? Что такое model-checkers и model-finders?

Меня зовут Васил Дядов, сейчас я работаю программистом в Яндексе, до этого работал в Intel, ещё раньше разрабатывал RTL-код (register transfer level) на Verilog/VHDL для ASIC/FPGA. Привет. Давно увлекаюсь темой надёжности софта и аппаратуры, математикой, инструментами и методами, применяемыми для разработки ПО и логики с гарантированными, заранее определёнными свойствами.

В последнее время он незаслуженно обойдён вниманием, несмотря на революционные изменения в подходе и инструментах поддержки. Это первая моя статья из цикла, призванного привлечь внимание разработчиков и менеджеров к инженерному подходу к разработке ПО.

Так что в ней будет минимум пространных рассуждений и максимум конкретики. Не буду лукавить: основная задача статьи — возбудить интерес.

В первой я опишу, что подразумеваю под инженерным подходом, во второй покажу пример использования подхода в рамках простой задачи (близкой к области микросервисной архитертуры). В статье две части.

Я всегда открыт для обсуждения вопросов, связанных с разработкой ПО, и буду рад пообщаться с читателями (координаты для связи есть в моём профиле).

Часть 1. Инженерный подход к разработке

Покажу на примере возведения моста: Что это такое?

  • Этап 1 — это сбор требований к мосту: тип моста, грузоподъёмность и т. д.
  • Этап 2 — уточнение требований и расчёт конструкций (спецификация).
  • Этап 3 — собственно само строительство на основе инженерных расчётов (спецификаций).

Никто не делает прототипов мостов, чтобы уточнить требования и спеки. Конечно, это упрощённая аналогия. Но в целом, думаю, аналогия ясна. В мост нельзя добавить параметризации, чтобы он становился то арочным, то подвесным.

Если требования и зафиксированы, то расплывчато, неполно и неформально. В разработке ПО этапы 1 и 2 часто отсутствуют либо очень слабо выражены. Лишь единицы детализируют требования и разрабатывают чёткие спецификации.

И это большое заблуждение. Многие считают, что это трата времени, пережиток прошлого, особенно если выбран agile-подход к разработке (особенно с короткими итерациями).

Почему?

Для начала разберёмся, что такое требование и спецификация и в чём их существенное отличие, которое даже многим профессионалам не всегда очевидно.

Что такое требования?

Например, так: «Все экземпляры программы должны одинаково обрабатывать входные запросы». Если кратко, требования — это формулирование свойств продукта в терминах предметной области.

Как только в требования просачиваются термины «синхронизация состояний», Raft, Paxos, «логарифмическая сложность по времени» — то начинают смешиваться требования и спецификация. В требованиях не используются термины области реализации.

Важно понимать это и чётко отделять одно от другого.

Почему?

  1. Требования должны быть понятны потребителям ПО, поэтому должны быть из предметной области, для которой разрабатывается ПО (часто к формулировке требований и постановке задачи на разработку ПО приходится привлекать экспертов, далеких от разработки).

  2. Нужно разделять требования и спецификации, чтобы иметь возможность 1) выделить основные метрики продукта, по которым потребитель будет оценивать наше ПО, и 2) ясно понимать, какие свойства продукта важны для пользователя, а какие нет. Свойства ПО, которые видит потребитель, оцениваются по метрикам предметной области.

Причём то, что кажется важным с точки зрения разработки ПО, может быть неважным с точки зрения для пользователя. А иначе может получиться так: разработчики, не укладываясь в срок, пожертвуют важными свойствами и уделят много времени и внимания неважным.

Разработчики обычно стараются оптимизировать время выполнения операции, например поиска информации в базе данных, а для пользователя важно время отклика системы. Классический пример такого несоответствия приведён в разнообразной литературе о разработке пользовательского интерфейса и в статьях (например: System Response Time and User Satisfaction: An Experimental Study of Browser-based Applications, Computer latency: 1977–2017). И если поиск идёт медленно, но пользователь начинает видеть выдаваемые результаты как можно быстрее, то ему кажется, что такое ПО работает лучше, чем то, которое ищет быстро, но сначала аккумулирует результаты и в конце выдаёт их все.

Для серверного режима важна максимальная пропускная способность системы, т. е. Именно поэтому планировщики ресурсов ОС различаются для серверного и десктопного режимов работы. А для пользователя важна задержка отклика системы. оптимизация времени и памяти, чтобы эффективно использовать сервер. Чем быстрее система реагирует на действия, тем более шустрой она кажется, даже если работает медленнее.

И, наконец, самая важная причина:

Задачи из предметной области мы начинаем формулировать и решать в области разработки ПО. Если требования и спеки смешиваются — значит, мы не полностью понимаем задачи, для которых разрабатываем ПО. В итоге получается сильно связанный код, который тяжело поддерживать. Поэтому логика предметной области просачивается и запутывает логику кода.

На мой взгляд, это одна из самых полезных книг для разработчиков ПО. Об этом хорошо написал Michael Jackson в книге Problem Frames: Analysing & Structuring Software Development Problems. Супербыстрая программа, которая потребляет мало ресурсов системы, но не решает задач пользователей, — это плохая программа. Она учит в первую очередь анализировать проблемы пользователей, которые и должно решать хорошее ПО. Крутая, но плохая.

Что есть спецификация?

Вот тут появляются понятия сложности, синхронизации и т. д. Спецификация — это формулирование свойств ПО в терминах области разработки ПО.

Такой подход зачастую наиболее эффективен. Спецификации могут быть организованы иерархически: от абстрактных к конкретным, по которым можно писать код. Поэтому мы можем отыскать проблемы на ранних стадиях жизненного цикла ПО и существенно уменьшить затраты на исправление ошибок. В абстрактных спецификациях легко отражается архитектура — можно увидеть основные свойства, найти архитектурные ошибки и т. д.

Особенно стоить отметить пользу и важность спецификаций на протоколы и интерфейсы между компонентами системы, что позволит избежать вот таких ситуаций:

В чём отличие от обычного подхода к разработке?

Спецификации проверяем на нужные свойства, которые идут из требований. При инженерном подходе мы заранее проектируем ПО с требуемыми характеристиками в соответствии со спецификациями.

Я сделал сравнение в виде таблички (весьма субъективной):

А не за водопадную ли модель разработки тут идёт агитация?

Инженерия ПО, включая даже формальные спеки и моделирования, отлично сочетается с agile-подходом.

Есть мнение, что инженерный подход к разработке несовместим с быстрой итерационной разработкой ПО (так утверждается во многих статьях, вот пример).

Инженерный подход с успехом применяется во многих проектах, в том числе в проектах с короткими итерациями. Но это не так.

Раньше из-за слабо развитых средств и инструментов поддержки инженерный подход действительно был тесно связан с водопадной моделью.

Но сейчас всё кардинально поменялось.

теперь можно быстро проверять огромные пространства состояний системы на наличие нужных нам свойств и отсутствие ненужных, верифицировать промышленные объёмы кода и т. д. Благодаря прорывным успехам в области моделирования, SAT/SMT-солверов и др.

Появились первоклассные промышленные инструменты типа Alloy, TLA+/TLC, Atelier B, PRISM, которые перевели задачу формализации и проверки спецификаций из академической/математической, требующей высокой квалификации и огромных усилий, в задачу push-button, доступную большинству программистов.

Модели отлично разрабатываются итерационно, от абстрактных к конкретным. Спецификации сейчас можно разрабатывать итеративно и инкрементально. Время моделирования даже крупных систем исчисляется минутами и часами.

Требования легко уточнять итеративно, особенно с современными подходами и инструментами.
И уточнение требований, спецификаций, рефакторинг моделей, написание кода и его рефакторинг легко могут идти параллельно — в рамках одной итерации.

В общем, инженерный подход сейчас совсем не равен водопадной модели, это уже две независимые вещи.

Инженерный подход легко сочетается с любой методологией организации разработки.

У него есть отличный пример, как за 10 минут формально специфицировать логику пользовательского интерфейса программы и проверить некоторые её свойства. В блоге Hillel Wayne показано, как просто работать с формальными спецификациями и моделями.

Не буду вдаваться в детали и переводить статью целиком, просто покажу саму спецификацию на языке Alloy:

Спецификация UI

open util/ordering[Time]
sig Time { state: one State
}
abstract sig State
abstract sig Login extends State {}
abstract sig Reports extends Login {} one sig Logout extends State {}
one sig Students, Summary, Standards extends Reports {}
one sig Answers extends Login {} pred transition[t: Time, start: State, end: State] { t.state in start t.next.state in end
} pred logout[t: Time] { transition[t, Login, Logout] }
pred login[t: Time] { transition[t, Logout, Summary] }
pred students[t: Time] { transition[t, Reports, Students] }
pred summary[t: Time] { transition[t, Reports, Summary] }
pred standards[t: Time] { transition[t, Reports, Standards] }
pred answers[t: Time] { transition[t, Students, Answers] }
pred close_answers[t: Time] { transition[t, Answers, Students] } fact Trace { first.state = Summary all t: Time - last | logout[t] or login[t] or students[t] or summary[t] or standards[t] or answers[t] or close_answers[t]
}

Здесь описан небольшой автомат, реализующий абстрактную логику UI в виде состояний и переходов между ними. Как видно, спецификация краткая и понятная.

Свойства для проверки тоже легко задаются:

check {all t: Time | t.state = Answers implies t.prev.state = Students} for 7

Спецификация похожа на небольшую программу.

К её разработке, уточнению и рефакторингу можно применять те же подходы, что и к разработке программ на любых языках программирования.

С такими спецификациями можно легко работать в стиле agile.

Зачем нужны такие спецификации и что с ними делать — покажу далее.

Формализация спецификаций

Как вы уже догадались, вышеприведённая спецификация является формальной, так как выполнена в рамках формализма — языка Alloy, который позволяет описывать объекты и взаимосвязи между ними в рамках реляционной логики первого порядка.

Если грамотно подходить к разработке, то на этапе формализации, отладки и моделирования спецификаций можно выявить и исправить наиболее критичные и дорогие (при обнаружении на заключительных этапах) ошибки и проблемы в ПО.

Отладка спецификаций позволяет выявить и исправить основные (или даже все) архитектурные проблемы ПО на ранних этапах, зачастую даже до кодирования.

Чтобы не утомлять читателя лишними словами, перейдём к простому примеру.

Часть 2. Пример использования Alloy

Чтобы показать возможности Alloy, я приведу пример создания и отладки спецификации вычислительных графов: структуры, описывающей один из способов обработки данных в системах, основанных на микросервисах и др.

Пример можно рассматривать как начало разработки архитектуры верхнего уровня для вычислительной системы для обработки больших потоков данных на основе микросервисов, где каждый микросервис — это узел в сети, который принимает данные, выполняет над ними какую-то операцию и передаёт их дальше.

Представленный подход к обработке данных на основе вычислительных графов применим для широкого класса задач.

Тут мы проанализируем основные свойства, которыми должны обладать вычислительные графы, чтобы на основе графов можно было делать работоспособные системы.

Отношения

Традиционно в математике бинарным отношением называется множество пар $\big\{x,y\big\}$, где $x \in X$ и $y \in Y$.

В Alloy принята такая запись: X->Y.

Описание отношений и их свойств поместим в отдельный модуль (который очень близок к стандартному util/relation):

Модуль relation.als

module relation -- Мультипликаторы:
-- set A - множество элементов из A, может быть пустым
-- one A - множество ровно из одного элемента из A
-- lone A - один элемент из A или пустое множество
-- some A - один и больше элементов из A -- Универсумы:
-- univ - множество всех элементов во всех множествах модели,
-- можно считать объединением всех сигнатур
-- iden - множество пар {A0, A0}, где первый и второй элемент
-- пары один и тот же и из univ
-- iden = {a : univ, b: univ | a=b}
-- то есть это отношение идентичности
-- none - пустое множество -- Операции:
-- логические: and, or, => (импликация), != (не равно), not
-- над множествами:
-- & - пересечение
-- A->B - множество кортежей с элементами из соотв.
-- множеств
-- X<:Y - выбор из кортежей в Y тех, которые начинаются с
-- кортежей из X
-- A in B - множество A содержится в B
-- ~A - перевернуть все кортежи в A
-- A + B - объединение
-- no A - A пустое, эквивалент A = none
-- ^A - транзитивное замыкание бинарного отношения A,
-- минимальное бинарное отношение B такое, что:
-- A in B,
-- {E0, E1}, {E1, E2} in B => {E0, E2} in B
-- A.B - оператор JOIN, работает след. образом:
-- {A0, B0} in A, {B0, C0, D0} in B, тогда
-- {A0, C0, D0} in A.B -- Кванторы:
-- all X : Y | .... - всеобщности
-- some X : Y | .... - существования -- применение предикатов:
-- pred[a: A, b:B] {...} есть две синтаксические формы
-- применения: pred[a, b] и a.pred[b]
-- вторая форма сделана для мимикрии под некоторые
-- ООП-языки, где методы определяются как
-- method(self : Object, args ...) pred valid [rel : univ->univ, dom : set univ, cod : set univ] { rel.univ in dom and rel.univ in cod
}
fun domain [rel : univ->univ] : set (rel.univ) { rel.univ }
fun codomain [rel : univ->univ] : set (univ.rel) { univ.rel }
pred total [rel: univ->univ, dom: set univ] { all x: dom | some x.rel
}
pred partial [rel: univ->univ, dom: set univ] { all x: dom | lone x.rel
}
pred functional [rel: univ->univ, dom: set univ] { all x: dom | one x.rel
}
pred surjective [rel: univ->univ, cod: set univ] { all x: cod | some rel.x
}
pred injective [rel: univ->univ, cod: set univ] { all x: cod | lone rel.x
}
pred bijective [rel: univ->univ, cod: set univ] { all x: cod | one rel.x
}
pred bijection [rel: univ->univ, dom, cod: set univ] { rel.functional[dom] and rel.bijective[cod]
}
pred reflexive [rel: univ->univ, s: set univ] { s<:iden in rel
}
pred irreflexive [rel: univ->univ] {no iden & rel}
pred symmetric [rel: univ->univ] {~rel in rel}
pred antisymmetric [rel: univ->univ] {~rel & rel in iden}
pred transitive [rel: univ->univ] {rel.rel in rel}
pred acyclic [rel: univ->univ, s: set univ] { all x: s | x not in x.^rel
}
pred complete[rel: univ->univ, s: univ] { all x,y:s | (x!=y => x->y in (rel + ~rel))
}
pred preorder [rel: univ->univ, s: set univ] { rel.reflexive[s] and rel.transitive
}
pred equality [rel: univ->univ, s: set univ] { rel.preorder[s] and rel.symmetric
}
pred partial_order [rel: univ->univ, s: set univ] { rel.preorder[s] and rel.antisymmetric
}
pred total_order [rel: univ->univ, s: set univ] { rel.partial_order[s] and rel.complete[s]
}

Многое из этого модуля нам не понадобится, оно приведено в качестве примера того, как можно даже сложные свойства отношений легко и лаконично выражать Alloy.

Графы

Теперь на основе отношений определим основные свойства графов.

Модуль для описания графов близок к стандартному utils/graph, но, в отличие от модуля отношений, в данный модуль вошли только необходимые нам предикаты и функции:

Модуль graph.als

module graph[node]
open relation -- функция получения всех узлов графа
fun nodes[r: node->node]: set node { r.domain+ r.codomain
} -- граф связан, то есть из любой вершины
-- можно добраться до любой другой по рёбрам
-- без учёта направленности
pred connected[r: node->node] { all n1,n2 : r.nodes | n1 in n2.*(r + ~r)
} -- граф ацикличный и направленный
pred dag [r: node->node] { r.acyclic[r.nodes]
} -- получить все корневые вершины
-- корневая вершина та, в которую нет
-- никаких входящих путей
fun roots [r: node->node] : set node { let ns = r.nodes | -- ns - все узлы графа ns - ns.^r -- из всех узлов убираем те, -- в которые есть какой-либо -- входящий путь
} -- получить все листья
-- лист - конечный узел, из которого
-- нет исходящих путей
fun leaves [r: node->node] : set node { let ns = r.nodes | -- ns - все узлы графа ns - ns.^~r -- из всех узлов убираем те, -- из которых есть какой-либо -- исходящий путь
}

Вычислительный граф

Вычислительный граф — это абстракция, описывающая вычисления в системе в виде графа.

Основные характеристики:

  • (1) есть исток — узел, куда передаются входные данные, над которыми и выполняются вычисления;
  • (2) есть сток — узел, куда поступает результат вычислений, который отправляется дальше вовне;
  • (3) есть вычислительные узлы — они принимают данные, вычисляют и передают данные дальше;
  • (4) сток один, исток — тоже;
  • (5) у вычислительного узла может быть множество входящих и исходящих дуг. Типы данных и синхронизацию пока не рассматриваем. Для простоты считаем, что данные, пришедшие по входящей дуге, обрабатываются и передаются на все исходящие дуги;
  • (6) граф направленный, между любой парой узлов — максимум одна дуга, двух дуг в противоположных направлениях быть не может.

На данном этапе мы рассматриваем в основном топологию.

Теперь опишем вычислительный граф, который удовлетворяет вышеприведённым свойствам, на Alloy:

Модуль compgraph.als

module compgraph[node] open graph[node]
open relation pred valid [edges: node->node, source : one node, -- свойство 1 drain : one node -- свойство 2
] { edges.antisymmetric and edges.irreflexive -- свойство 6 graph/roots[edges] = source -- свойство 1 и 4 graph/leaves[edges] = drain -- свойство 2 и 4
}

Посмотрим на пару примеров вычислительных графов:

open compgraph[node] as cg -- cg - это псевдоним enum node {n0, n1, n2, n3, n4}
-- зададим узлы как перечисление, чтобы было более наглядно run cg/valid -- ещё дополнительно указываем модуль cg, так как -- предикат valid есть в двух модулях: relation и compgraph

Примеры графов можно увидеть на следующем рисунке:

Примеры вычислительных графов

Можем заметить, что некоторые графы не совсем подходят для вычислений (есть подозрительные циклы).

Подумав над свойствами вычислительных графов по отношению к обрабатываемым данным, мы придём к идее консистентности.

Консистентность вычислительного графа

Под консистентностью тут понимаются свойства графа по отношению к потоку данных, которые обрабатываются в графе.

Это фундаментальное свойство вычислительного графа по отношению к абстрактным данным. Результаты обработки данных не должны теряться. То есть все результаты должны попадать либо в сток, либо в другие вычислительные узлы.

Мы можем классифицировать узлы по возможности потери данных: Понятно, что потерять данные можно только после получения.

  • активный узел — до него есть путь от истока, т. е. сюда могут прийти данные для вычислений;
  • неактивный узел — до него нет пути от истока;
  • безопасный узел — от него все пути ведут в сток, т. е. нет опасности подключения к узлу исходящего ребра от активного узла, переданные в него данные не потеряются.

е. Граф консистентен, если в нём не теряются результаты вычислений и все вычислительные процессы конечны, т. мы получим результат за конечное время (все вычисления в графе останавливаются за конечное время, и мы можем считать результат из стока).

Консистентности можно достичь, добавив ещё несколько свойств к свойствам вычислительного графа:

  • (7) нет циклов (для простоты описания). В реальных графах могут быть циклы при условиях, которые исключают бесконечную циркуляцию данных по путям цикла, но тут считаем граф ациклическим;
  • (8) все пути из активных узлов должны вести к стоку, т. е. нет потерь данных.

И можно ослабить свойство единственности корня и равенства его истоку, так как мы ввели понятие неактивного узла.

То есть все узлы, которые являются корнями, кроме истока, это просто неактивные узлы.

  • (9) могут быть дополнительные корневые узлы, являющиеся неактивными узлами.

И (правда, избыточное, оно следует из других) свойство:

  • (10) все активные узлы безопасны.

Теперь уточним спецификацию вычислительного графа:

Модуль compgraph.als

module compgraph[node] open graph[node] pred active[edges : node->node, source: node, n : node
] { -- n находится в множестве узлов, -- достижимых от истока n in source.^edges
} pred safe[edges : node->node, drain : node, n : node
] { -- если есть ещё листья, кроме drain, -- то не один путь из n -- не должен вести в эти узлы -- и n не должно быть одним из -- этих узлов no n.*edges & (leaves[edges] - drain) -- одно из свойств безопасных узлов, что -- можно подать туда данные из активных узлов -- и данные не будут теряться, -- таким образом, должен быть путь до drain drain in n.*edges
} pred valid [edges: node->node, source : one node, -- свойство 1 drain : one node -- свойство 2
] { edges.connected -- так как мы ослабили ограничения -- на корни и вершины (теперь и -- тех и тех может быть не по одной), -- то граф может быть не графом, а -- лесом, поэтому нужно дополнительное -- условие connected edges.dag -- свойство 6 и 8 source in edges.roots -- свойство 1, 4 и 9 drain in edges.leaves -- свойство 2, 4 и 8 all n : edges.roots - source | not active[edges, source, n] -- свойство 9 all n : edges.nodes | -- 10 свойство active[edges, source, n] => safe[edges, drain, n]
}

Для экономии времени и места картинки с уточнёнными вычислительными графами приводить не буду.

Операции над вычислительным графом

Для работы с вычислительными графами нам нужны операции.

Сначала подумаем, как граф будет жить в системе и что из этого может следовать.

В простейшем случае жизнь графа состоит из шести этапов:

  1. создание графа;
  2. проверка валидности графа;
  3. запуск данных в граф;
  4. работа графа;
  5. прекращение подачи данных;
  6. уничтожение графа.

Сценарий простой и для большинства задач подойдёт. Изменение работающего графа не подразумевается. Не надо заботиться о консистентности графа по отношению к данным во время работы: после создания граф валидируется и далее не меняется.

А если мы хотим менять функциональность сервиса во время работы? А если нам нужен сервис, который будет работать долго и сумеет адаптироваться к меняющейся нагрузке?

Это серьёзно усложняет задачу.

Подумаем о том, как менять граф во время работы, чтобы изменения не нарушали его консистентность.

Предположим, у нас уже есть валидный и работающий граф.

Сначала подумаем, какие операции нам минимально необходимы:

  • добавление нового узла и дуги (граф задаётся дугами, поэтому добавить новый узел без связей не получится);
  • добавление дуги;
  • удаление дуги;
  • удаление узла и связанных с ним дуг.

Новый узел при добавлении очевидно считается неактивным.

Основные свойства определяются дугами, поэтому рассмотрим добавление дуги между узлами.

Соединять узлы мы можем несколькими вариантами:

  1. неактивный -> неактивный;
  2. неактивный -> активный;
  3. активный -> неактивный;
  4. активный -> активный.

Первый и последний вариант тривиальны, а второй и третий уже интереснее.

Ведь в противном случае должна быть дуга к какому-то неактивному узлу, а оттуда — путь к данному неактивному, а это противоречит определению активного/неактивного узла. Очевидно, что при подключении неактивного узла к активному ничего плохого не произойдёт: активные узлы безопасны относительно данных, циклов не получится.

Остался самый интересный вариант, третий: активный -> неактивный.

Такое подключение будет безопасным, только если:

  • неактивный узел безопасен;
  • не образуется циклов.

Опишем операции в виде предикатов над графами, которые связывают граф до и после операции.

Если читатель знаком с Прологом, то вот в Alloy примерно так же идёт работа с данными. Можно попробовать описать в виде функций, но в Alloy тяжело задавать функции по созданию сложных структур данных, так как язык чисто декларативный.

Операция добавления дуги

pred connect[ old_edges : node->node, new_edges : node->node, source : one node, drain : one node, from : one node, to : one node
] { -- ребра ещё не было from->to not in old_edges -- from недостижим из to, -- чтобы не возникло цикла from not in to.*old_edges -- to должен быть узлом графа, -- иначе граф может стать -- лесом to in (old_edges.nodes - source) -- подключение к to должно быть -- безопасно, то есть передаваемые -- данные в to не потеряются safe[old_edges, drain, to] -- новый граф определяется рёбрами, -- берём все старые рёбра и добавляем -- новое ребро new_edges = old_edges + from->to
}

Предикат connect покрывает все случаи добавления узла с ребром или только ребра к графу.

Давайте проверим, что connect сохраняет валидность графа:

open compgraph[node] as cg sig node {} check { -- для всех возможных наборов рёбер r1, r2 all r1, r2 : node->node | -- для всех возможных узлов source, drain, from, to all source, drain, from, to : node { -- r1 является валидным вычислительным графом с -- source/drain истоком/стоком -- и r2 является графом r1 с добавленным операцией -- connect ребром from->to (cg/valid[r1, source, drain] and connect[r1, r2, source, drain, from, to]) -- это влечёт то, что r2 + source/drain -- также является валидным вычислительным -- графом implies cg/valid[r2, source, drain] -- то есть операция connect сохраняет валидность -- вычислительного графа }
} for 8

Результат

Executing "Check check$1 for 8" Sig this/node scope <= 8 Sig this/node in [[node$0], [node$1], [node$2], [node$3], [node$4], [node$5], [node$6], [node$7]] Generating facts... Simplifying the bounds... Solver=sat4j Bitwidth=4 MaxSeq=7 SkolemDepth=4 Symmetry=20 Generating CNF... Generating the solution... 8374 vars. 168 primary vars. 22725 clauses. 108ms. No counterexample found. Assertion may be valid. 26904ms

Это большое пространство, "168 primary vars" говорит о том, что оно размером $2^{168}$ возможных значений основных переменных. Alloy не смог найти контрпример во всём пространстве конфигураций графов с количеством узлов до восьми включительно. И это заняло на среднем ноутбуке меньше 30 секунд!

То есть мы можем быть вполне уверены, что операция connect сохраняет валидность любых вычислительных графов.

Теперь обратная операция, удаление дуги:

Удаление дуги

pred disconnect[ old_edges : node->node, new_edges : node->node, source : one node, drain : one node, from : one node, to : one node
] { -- рёбра есть в старом графе from->to in old_edges -- при удалении ребра from -- должен остаться безопасным safe[new_edges, drain, from] -- граф должен оставаться связанным new_edges.connected -- удаляем ребро new_edges = old_edges - from->to
}

Пробуем:

open compgraph[node] as cg
sig node {}
check { all r1, r2 : node->node | all source, drain, from, to : node { (cg/valid[r1, source, drain] and disconnect[r1, r2, source, drain, from, to]) implies cg/valid[r2, source, drain] }
} for 8

Найдены контрпримеры! Ого! Парочку из них можно увидеть на следующем рисунке:

Контрпримеры для disconnect

Там, где есть r1, но нет параллельной ей r2, эта r2 и была удалена операцией. Дуги, помеченные как r1, — это дуги графа до операции disconnect, r2 — после неё.

Видно, что причина контрпримеров — это удаление единственной дуги from->to, в случае когда source (он же from) перестаёт быть связанной вершиной графа.

Поправляем операцию disconnect:

исправленная операция удаления дуги

pred disconnect[ old_edges : node->node, new_edges : node->node, source : one node, drain : one node, from : one node, to : one node
] { from->to in old_edges ( safe[new_edges, drain, from] or (from not in new_edges.nodes and from != source)) new_edges.connected new_edges = old_edges - from >to
}

Результат проверки

Executing "Check check$2 for 8" Sig this/node scope <= 8 Sig this/node in [[node$0], [node$1], [node$2], [node$3], [node$4], [node$5], [node$6], [node$7]] Generating facts... Simplifying the bounds... Solver=sat4j Bitwidth=4 MaxSeq=7 SkolemDepth=4 Symmetry=20 Generating CNF... Generating the solution... 8505 vars. 168 primary vars. 24808 clauses. 207ms. No counterexample found. Assertion may be valid. 18369ms.

Таким образом мы определили две основные операции, которые сохраняют свойства валидности вычислительного графа.

Полнота операций

У нас есть множество валидных графов, а достаточны ли наши операции для построения любого валидного графа из любого валидного?

И она окажется в тупике и придётся останавливать и перезапускать всю систему? Не окажется ли так, что мы не сможем поменять топологию работающей системы нужным образом?

Давайте проверим:

-- для любых двух валидных графов
-- есть последовательность промежуточных валидных графов,
-- такая, что два следующих друг за другом графа
-- приводятся друг к другу за одну операцию
check { all r1,r2: node->node | all source,drain: node | some intermediate : seq node->node { cg/valid[r1, source, drain] and cg/valid[r2, source, drain] => intermediate.first = r1 and intermediate.last = r2 and all i : intermediate.inds - intermediate.lastIdx { let from = intermediate[i] | let to = intermediate[i+1] | some n1, n2 : node | connect[from,to, source, drain, n1, n2] or disconnect[from, to, source, drain, n1, n2] } }
} for 3

И вот тут мы получаем:

Executing "Check check$3" Sig this/node scope <= 3 Sig this/node in [[node$0], [node$1], [node$2]] Generating facts... Simplifying the bounds... Solver=sat4j Bitwidth=4 MaxSeq=4 SkolemDepth=4 Symmetry=20 Generating CNF... Generating the solution...
A type error has occured: (see the stacktrace)
Analysis cannot be performed since it requires higher-order
quantification that could not be skolemized.

Что это значит?

Мы столкнулись с ограничением Alloy: квантификация может быть только первого порядка либо должна сводиться к первому порядку.

А здесь не получилось сделать сколемизацию квантора «some intermediate…», так как подкванторная переменная должна пробегать по структуре высшего порядка — последовательности графов.

И к первому порядку такую конструкцию не свести.

Иногда (но не так часто, как хотелось бы) можно переформулировать предикат так, чтобы он свёлся к первому порядку.

Она катастрофически замедляет моделирование, так как идёт через CEGIS — counter-example guided inductive synthesis. Хотя уже есть higher-order Alloy, но он пока экспериментальный, квантификация высших порядков у него имеет существенные ограничения по размеру моделей.

В данном случае нам придётся придумать альтернативный способ проверки, возможно ли достичь всех валидных графов.

Если ослабить условие и проверять не достижимость любого валидного из любого валидного, а возможность сделать шаг между двумя валидными, которые отличаются на одно ребро, то получим:

check { all edges, edges1 : node->node | all source,drain, from, to : node { (cg/valid[edges, source, drain] and cg/valid[edges1, source, drain] and edges1 = edges + from->to and edges1 != edges) => some n1, n2: node | connect[edges, edges1, source, drain, n1, n2] }
} for 7

Эта проверка уже работает, и мы видим результат:

результат проверки connect на полноту

Executing "Check check$3 for 7" Sig this/node scope <= 7 Sig this/node in [[node$0], [node$1], [node$2], [node$3], [node$4], [node$5], [node$6]] Generating facts... Simplifying the bounds... Solver=sat4j Bitwidth=4 MaxSeq=7 SkolemDepth=4 Symmetry=20 Generating CNF... Generating the solution... 6471 vars. 133 primary vars. 16634 clauses. 200ms. Counterexample found. Assertion is invalid. 116ms.

Найден контрпример!

контрпример

На этом шаге добавляется дуга from->to. Красные дуги — это дуги графа до шага, чёрные пунктирные — после шага.

Тут мы видим, что операция connect не позволяет добавить дугу от неактивной вершины к небезопасной (и, соответственно, неактивной).

Поправляем connect:

исправленная версия connect

pred connect[ old_edges : node->node, new_edges : node->node, source : one node, drain : one node, from : one node, to : one node
] { from->to not in old_edges from not in to.*old_edges to in (old_edges.nodes - source) -- вот тут поправили active[old_edges, source, from] => safe[old_edges, drain, to] -- учитываем безопасность to только для активной from, -- и, так как to теперь может быть отдельной вершиной, -- как и from, то нужно добавить условие -- сохранения связанности графа new_edges.connected -- это стало очевидным, так как старая проверка -- стала давать контрпримеры 🙂 new_edges = old_edges + from -> to
}

Проверяем снова:

результат

Executing "Check check$3 for 7" Sig this/node scope <= 7 Sig this/node in [[node$0], [node$1], [node$2], [node$3], [node$4], [node$5], [node$6]] Generating facts... Simplifying the bounds... Solver=sat4j Bitwidth=4 MaxSeq=7 SkolemDepth=4 Symmetry=20 Generating CNF... Generating the solution... 6513 vars. 133 primary vars. 16837 clauses. 125ms. No counterexample found. Assertion may be valid. 291ms.

Теперь всё нормально.

Там тоже будет контрпример, придётся внести правки: Точно так же проверяем обратный шаг для операции disconnect.

исправленная версия diconnect

pred disconnect[ old_edges : node->node, new_edges : node->node, source : one node, drain : one node, from : one node, to : one node
] { from->to in old_edges -- если удаляем исходящее ребро из активной вершины, -- то она должна оставаться безопасной active[old_edges, source, from] => safe[new_edges, drain, from] -- заметьте, что теперь не нужно анализировать на -- то, что вершина вышла из графа: -- (from not in new_edges.nodes and -- from != source) new_edges.connected new_edges = old_edges - from->to
}

Таким образом, мы доказали, что если один валидный граф достижим из другого валидного за конечное число шагов добавления/удаления по одной дуге, то мы всегда можем прийти с помощью наших операций от одного графа к другому.

Это означает, что, начав с минимального работающего валидного графа (например, source->drain), мы можем дойти до больших валидных графов с помощью операций connect/disconnect и всегда вернуться к начальному графу.

Этого свойства хватит для построения широкого класса вычислительных графов (есть основание предполагать, что всех интересных на практике вычислительных графов или же вообще всех, но это требует более серьёзного доказательства).

Что дальше?

Дальше можно развивать идею в направлении локальности операций, например.

В большой распределённой системе может быть очень неудобно при операциях над графом требовать наличия в узлах, которые участвуют в операции, знаний обо всём графе, чтобы определить отсутствие циклов и т. д.

То есть хорошо бы разработать операции со свойством локальности: им понадобится знание только об узлах, что участвуют в операции (признаки safe/active и пр.).

При небольших ограничениях на возможные топологии графа эта задача решаема.

Далее, хорошо бы проводить множество параллельных операций над графом одновременно.

Если мы локализовали операции, то распараллеливание — задача тоже вполне решаемая с помощью механизмов транзакций, локальных блокировок и т. д.

Либо можно изначально проектировать систему таким образом, чтобы операции были локальные и параллельные.

Ещё хорошо бы ввести типы входных и выходных из узлов данных, чтобы конструировать графы с учётом специфики узлов обработки.

В результате на выходе мы получим уже не игрушечную, а реальную рабочую спецификацию вычислительных графов и операций над ними, по которой можно разрабатывать реальную систему с нужными нам (заложенными в спецификации) свойствами.

А сколько времени ушло на эту модель вычислительного графа?

На написание кода на Alloy и отладку спек ушло не более часа.

Намного больше времени заняли сопровождающий текст и подготовка иллюстраций.

Формализация спецификаций, их моделирование и отладка при небольшой практике занимают намного меньше времени, чем написание и отладка прототипного кода, даже на динамических языках программирования типа Python.

При работе со спецификациями доступны операции самого высокого уровня абстракции, что позволяет (как вы уже убедились) лаконично описывать сложные свойства системы.

Как поэкспериментировать с моделями графов?

Установите Alloy Analyzer, скопируйте файлы из репозитория на GitHub — и экспериментируйте.

А что нам даёт описание на Alloy?

Тут всё довольно очевидно:

  • промоделировав высокоуровневую архитектуру и её свойства, мы будем уверены, что нам не придётся кардинально менять систему из-за проблем в архитектуре;
  • предикаты, выражающие основные свойства системы, можно использовать, чтобы расставлять assert’ы в коде, писать статичные и динамические чекеры и т. д.;
  • мы можем на основе моделей сделать направленные тесты на краевые случаи (по мотивам найденных во время отладки контрпримеров);
  • При расширении функциональности системы мы можем сначала посмотреть, как новая функциональность работает со старой на моделях, а затем уже её реализовывать в коде, что позволяет развивать систему стабильно и предсказуемо. Например, при добавлении новых операций легко проверяется то, что они сохраняют консистентность вычислительного графа.

Заключение

Facebook, Google, Microsoft, Amazon уделяют много внимания и сил разработке надёжных систем и ПО. Сейчас разработка серьёзного ПО уже немыслима без грамотного инженерного подхода.

Сейчас технологии и мир меняются очень быстро, конкуренция высока, стоимость ошибок при разработке ПО для бизнеса измеряется в потере конкурентного преимущества и доли рынка.

Обычные agile-подходы во многих областях недостаточны для быстрой адаптации к рынку, нужна быстрая адаптация с минимумом ошибок.

Даже если хватит денег на исправление ошибок, потеря времени может стать фатальной для проекта: конкуренты займут рыночную нишу.

И тут на помощь придёт инженерный подход.

Во многих областях разработку ПО можно и нужно вести в рамках гибких методологий с применением инженерных методов.

Постараюсь сопроводить статьи примерами использования инструментов. В следующих статьях я собираюсь подробнее рассказать о требованиях и спецификациях, их плюсах, минусах, возможностях и ограничениях, о других весьма полезных инструментах (TLA+/TLC, B-method/Atelier B, Promela/SPIN).

Библиография

Книги для погружения в область

Список упорядочен по возрастанию сложности. Тут собраны книги, которые отличаются практическим подходом, минимумом сложной математики, максимумом объяснений и примеров.

  1. Michael Jackson Problem Frames: Analysing & Structuring Software Development Problems
    Хорошая книга об анализе проблем (не способов решения!), которые встают перед разработчиками ПО. Будет интересна тем, кто хочет грамотно анализировать задачи и составлять требования.
  2. Daniel Jackson Software Abstractions: Logic, Language, and Analysis
    Книга о model finder Alloy и его принципах. От читателя особой подготовки не требуется, но нужны внимание и вдумчивость. Поможет понимание реляционной алгебры (операции join, транзитивного замыкания отношений). Но это необязательно, в книге всё хорошо объяснено.
  3. Юрий Карпов. MODEL CHECKING. Верификация параллельных и распределённых программных систем
    Хорошая обзорная книга о моделировании. Доходчиво написана, рассмотрены все основные темы, приведено множество примеров. Никакой серьёзной подготовки от читателя не требуется, знания матлогики и дискретки в объёме стандартной вузовской программы более чем достаточно.

Примеры практического применения Alloy

  1. Pamela Zave. How to Make Chord Correct
    С помощью Alloy была составлена модель алгоритма DHT Chord, найдена ошибка (именно в алгоритме, так что все реализации содержали её), предложена исправленная версия алгоритма. Яркий пример того, как бывает полезно формально специфицировать и моделировать алгоритмы.
    1. Примеры спецификаций
      В репозитории много примеров спецификаций на Alloy, часть которых взята из промышленных задач.

Блоги

  1. Hillel Wayne
    Много интересного материала и примеров. Лёгкий стиль, простая подача. Рекомендую тем, кто начинает изучать моделирование.

Презентации

  1. Ю. Г. Карпов, И. В. Шошмина, А. Б. Беляев. Верификация параллельных и распределённых программных систем
    Интересная презентация, где хорошо объясняется, что такое моделирование и зачем оно нужно.

Alloy

  1. Alloy Analyzer + Higher-Order Alloy
    Инструменты для работы со спецификациями на языке Alloy.
  2. Online Tutorial
    Материал немного устарел, но может быть полезным для новичков.
  3. Tutorial Materials
    Обучающие материалы.
Теги
Показать больше

Похожие статьи

Добавить комментарий

Ваш e-mail не будет опубликован. Обязательные поля помечены *

Кнопка «Наверх»
Закрыть