Некоторые из самых опасных дефектов систем можно обнаружить ещё до написания кода, если рассматривать само проектирование как систему, пригодную для анализа. Этой теме посвящено выступление Hillel Wayne, в котором он объясняет, как принципы формальных методов помогают исследовать будущие системы и выявлять проблемы отказоустойчивости, параллелизма и отказов до того, как они превратятся в эксплуатационные ошибки.
Wayne начинает с упрощённого примера того, что он называет «исполнителем задачи»: система проверяет, выполнена ли задача, затем помечает её как выполненную и после этого выполняет задачу. Последовательность кажется логичной, но нарушается при возникновении отказа во время выполнения. После того как задача была зарегистрирована как выполненная, может произойти повторная попытка, и фактически задача не будет выполнена. Если перенести регистрацию выполнения на момент после самой операции, возникает другая проблема: два параллельных исполнителя могут выполнить одну и ту же задачу дважды, прежде чем кто-либо из них зарегистрирует её завершение.
Это не только теоретическая проблема: в выступлении она связана с такими примерами, как системы отправки посылок, которые могут отправить заказ дважды, системы планирования, способные забронировать одно и то же время для двух человек, и механизмы установки приложений, которые при повторении запроса могут перейти к разрушительному поведению.
Начните с определения того, что означает «правильно»
Wayne предлагает формулировать требования к системе в виде бинарных свойств: они либо истинны, либо ложны. Например, задача не должна выполняться более одного раза — это свойство безопасности, предотвращающее нежелательное событие, — а задача должна выполняться хотя бы один раз — это свойство живучести, гарантирующее наступление требуемого события.
В выступлении подчёркивается, что свойства не равны по силе. Система, способная обрабатывать 10 000 запросов в секунду, автоматически удовлетворяет свойству обработки двух запросов в секунду, но обратное неверно. Поэтому выполнение сильного свойства может свидетельствовать о корректности набора более слабых свойств, тогда как нарушение более слабого свойства помогает сузить область поиска причины сбоя. Wayne связывает эту идею с пирамидой тестирования: многочисленные модульные тесты могут быть полезнее для диагностики ошибки, чем ограниченное число сквозных тестов.
Упрощённая модель выявляет основную проблему
Вместо представления системы во всех деталях Wayne призывает строить абстрактную модель, включающую минимально необходимое состояние: текущий этап алгоритма, отметку о том, помечена ли задача как выполненная, и число её выполнений. Это позволяет исследовать возможные состояния и пути, по которым может двигаться система, включая состояния отказа и повторных попыток.
В формальных методах такую модель и свойства можно кодировать с помощью логических формул, а затем проверять инструментами вроде проверяющих моделей и SMT-решателей. Однако практическая идея выступления не требует непосредственного использования этих инструментов: инженер может применять тот же образ мышления, отслеживая состояния и возможные переходы.
Фактор «противника» в параллелизме и отказах
Wayne предлагает рассматривать каждый источник недетерминизма — например, пользовательский ввод, параллелизм, случайность, тайм-ауты и отключения серверов — как «противника», который всегда выбирает наихудший возможный исход. Если система может повторять попытку бесконечно, этот противник будет выбирать отказ каждый раз, показывая, что свойство живучести не гарантировано, даже если успех теоретически возможен.
Он также объясняет, что наличие двух параллельных исполнителей требует представлять одни переменные как локальные для каждого процесса, а другие — как общие для системы и внешнего мира. Исследование различных порядков выполнения позволяет прийти к состоянию, в котором задача выполняется дважды, даже если каждый исполнитель по отдельности кажется корректным.
Предположения — часть проектирования
Корректность системы зависит не только от её свойств, но и от предположений о среде, в которой она работает. Одно проектное решение может требовать сильного предположения о том, что процесс вообще никогда не завершается с ошибкой, тогда как другое способно работать, если отказ происходит ограниченное число раз. Wayne отмечает, что перестановка шагов может ослабить предположения о живучести, но увеличить требования к безопасности, например необходимость гарантировать, что в каждый момент времени существует только один исполнитель.
Ситуация также меняется при изменении рабочей среды. Зависимость от строгой согласованности базы данных с последующим переходом к eventual consistency может сделать ранее истинные свойства негарантированными, даже если код системы не изменился. Поэтому предположения о поставщике услуг или базе данных не следует считать внешними деталями: это непосредственные условия корректности проектирования.
Что меняется на практике?
Практическая ценность метода заключается не в замене тестирования и не в призыве использовать формальные инструменты в каждом проекте, а в том, чтобы сделать вопросы проектирования более строгими: каковы возможные состояния? Каков наихудший порядок событий? Что мы действительно контролируем? Какие предположения команда не может гарантировать? Чем сильнее требуемое свойство или менее предсказуема среда, тем более сложного проектирования требует система — либо тем сильнее нужно ослабить требуемое свойство, например заменить условие «обработать все сообщения» на «обработать сообщения или отправить их в очередь недоставленных сообщений».
Wayne представляет эти идеи как инструменты мышления, заимствованные из формальных методов, а не как готовую замену инженерному суждению. Открытым вопросом в каждой системе остаётся точность используемой модели и предположений: если какое-либо состояние упущено или команда предположила поведение, которое среда не гарантирует, анализ может доказать корректность модели, не похожей на реальную систему.