Лекция
Привет, Вы узнаете о том , что такое живучесть, Разберем основные их виды и особенности использования. Еще будет много подробных примеров и описаний. Для того чтобы лучше понимать что такое живучесть, живучесть в системах связи, живучесть любой системы, survivability, живучесть в параллельных вычислениях, liveness, формы живости, различие между безопасностью и живостью, ограниченный обгон, живучесть в ооп, persistence, живучесть в программном обеспечении, устойчивость программ, robustness, живучесть в информатике, persistence computer science, постоянство в информатике, ортогональное сохранение, прозрачное сохранение, теорема об описании множества поведений , настоятельно рекомендую прочитать все из категории Информатика.
1 Понятие живучести системы (любой) - Survivability
2 Понятие живучести в системах связи
3 Понятие живучести параллельных вычислениях - Liveness
4 живучесть (persistence) в ООП
5. живучесть в программном обеспечении - Устойчивость (Robustness) -( надежность)
6 Живучесть ( Постоянство) в информатике - Persistence (computer science)
7 теорема об описании множества поведений с помощью свойства безопасности (safety) и свойства живучести (liveness)
Понятие Живучесть в широком смысле тесно связано с понятием живучести систем, в узких смыслах (часто одновременно) это в более узких областях таких как базы данных, ООП, параллельные вычисления, сети, в программном обеспечении , в инфомрматике и т.д. Ввиду того что разные англоязчные термины имеют одинаковы перевод живучесть - может возникнуть сложность идентифицации помощь в этом оказывает контекст.
Рассмотрим комплексно некторые понятия живучести в более узких смыслах.
В [ 5 ] под живучестью понимается “свойство системы связи сохранять и восстанавливать способность к выполнению основных функций в заданном объеме и в течение заданной наработки при изменении структуры системы и (пли) алгоритмов и условий ее функционирования вследствие неблагоприятных воздействий”. Живучесть характеризует устойчивость сети связи против действия причин, лежащих вне сети и приводящих к разрушениям или значительным повреждениям некоторых ее частей. Живучесть – свойство сети сохранять способность выполнять требуемые функции в условиях, создаваемых воздействием внешних дестабилизирующих факторов [ 6 ].
Живучесть — способность технического устройства, сооружения, средства или системы выполнять основные свои функции, несмотря на полученные повреждения, либо адаптируясь к новым условиям .
Например, под живучестью судна можно понимать его способность оставаться на плаву и не терять остойчивость в случае затопления одного или большего числа отсеков из-за полученного повреждения корпуса.
Живучесть системы городского электротранспорта определяется способностью не прерывать работу всей системы или значительного ее участка из-за планового ремонта, аварии, повреждения контактной сети и (или) рельсового пути. При возникающих затруднениях маршруты пускаются по обходным путям, укорачиваются за счет промежуточных разворотных колец или перенаправляются на запасную конечную станцию. Для троллейбусов также возможно применение систем автономного хода. В случаях, когда работа маршрута на участке невозможна в течение длительного времени (ремонт) — вводят временные маршруты электротранспорта и компенсирующие автобусные маршруты. В некоторых случаях, когда разветвленный участок соединен с основной сетью единственной линией (по мосту, например) — на этом участке стараются запроектировать собственное депо. При его отсутствии организуют временные площадки для ночного отстоя ПС. В случаях с трамваями, когда на заблокированном на длительный период участке нет разворотного кольца, применяют челноки — вагоны, сцепленные хвостами.
Живучесть ствола (лейнера) орудия определяется как количество выстрелов, которые может произвести орудие до выхода из строя или снижения кучности выстрелов до неприемлемого уровня.
В [ 4 ] под живучестью системы связи понимается “устойчивость системы связи к повреждению элементов стихийными факторами и преднамеренными воздействиями противника”. В [ 7 ] дано определение живучести применительно к системе военной связи: “Способность системы военной связи обеспечивать управление войсками или силами и оружием в условиях воздействия оружия противника”
"The capability of a system to fulfill its mission, in a timely manner, in the presence of threats such as attacks or large-scale natural disasters. Survivability is a subset of resilience."[ 1 ][ 2 ]
“The capability of a system to fulfill its mission, in a timely manner, in the presence of attacks, failures, or accidents.”
В компьютерных сетях используется т.н. протокол Stop and Wait . Доказательство его корректности состоит в доказательстве –
ГАРАНТИРОВАННОСТИ (safety) : пакеты доставляются строго по порядку и не происходит размножения пакетов (каждый пакет доставляется в единственном числе) –
и ЖИВУЧЕСТИ (liveness) : в конце концов, все пакеты доставляются (нет пропущенных пакетов).
Модели количественной оценки живучести и вероятности связности сети разрабатывались с середины прошлого века и затем получили многочисленное развитие. При определении вероятности связности сети предполагается, что в сети имеются избыточные (по сравнению с деревом) дуги, допускающие их разрыв. любые повреждения древовидной сети приводят к потере связности и живучесть становится равной нулю. Но анализ атак на сети показывает, что сети продолжают действовать, даже если они распались на фрагменты. Появилась потребность в развитии методов, моделей живучести сетей, учитывающих современные условия эксплуатации.
Структурная живучесть, выраженная через математическое ожидание числа погибших узлов, отображает топологию сети.
Функциональная живучесть, выраженная через математическое ожидание числа выживших соединений (межузловых потоков), является отображением характеристик потока в сети: распределения длин путей, общей и средней длины пути, средней нагрузки дуг, общего числа соединений.
Потоковая живучесть позволяет оценить нагрузку дуг как до, так и после атаки на избыточные дуги, установить необходимый запас пропускной способности на случай потери избыточных дуг.
На рисунке приведена классификация (дерево) свойств, определяющих живучесть ИТС (ИНФОРМАЦИОННО-ТЕЛЕКОММУНИКАЦИОННЫХ СЕТЕЙ) .
Рис Классификация (дерево) свойств, определяющих живучесть ИТС
Перечисленные выше свойства обусловливают соответствующие единичные показатели живучести ИТС.
Структурная живучесть — свойство системы сохранять выполнение своих функций хотя бы на минимально допустимом уровне в течение требуемого времени при пассивном противодействии повреждениям элементов системы.
Функциональная живучесть — свойство системы сохранять требуемый уровень работоспособности за счет принятого алгоритма управления маршрутизацией
обмена информацией между абонентами системы или се реконфигурации.
Техническая живучесть — свойство системы сохранять выполнение своих функций за счет восстановления работоспособности се элементов.
Элементная живучесть — свойство элементов ИТС, характеризующее их стойкость к воздействию ПФ и способность восстанавливать работоспособность
Разведзащищенность в данном случае также является одним из единичных свойств живучести ИТС.
Отметим, что набор свойств, представленных на рисунке, не является замкнутым, его можно расширить или сузить. Это определяется системой взглядов
(принципов) на обеспечение живучести ИТС.
В параллельных вычислительном процессе , живучесть относится к набору свойств параллельных систем , которые требуют систем к прогрессу макияжа , несмотря на то , что его одновременно исполняющим компоненты ( «процессы») , возможно , придется «по очереди» в критических секциях , части программы которые не могут быть одновременно управляет несколькими процессами. Живучесть гарантии являются важными свойствами в операционных системах и распределенных систем .
В более общем плане , а живучесть собственность гласит , что «что - то хорошее, в конечном счете произойдет», противопоставляя в собственность безопасности , которая гласит , что «что - то плохое не происходит». Если свойство безопасности нарушается всегда конечное исполнение , что показывает нарушение ( «плохое» событие , происходящее), но свойство живучести не может быть нарушено в конечном исполнении распределенной системы , так как «хорошее» событие все еще может произойти в некоторое время спустя. Возможные консистенции является примером свойства живучести. Все свойства могут быть выражены как пересечение свойств безопасности и живучести. В то время как нарушение данного свойства безопасности допускает конечное свидетельство, нарушение живучести свойств может быть труднее установить , как никакой конечный свидетель не может быть использован в качестве доказательства.
Некоторые формы живости признаются. Следующие из них определены в терминах системы с несколькими процессов , которая имеет критическую секцию, защищаемую некоторое взаимоисключение (мьютекс) устройство. Предполагается , что все процессы , чтобы правильно использовать семафор; прогресс определяется как отделка выполнения критической секции.
По словам Б. Alpern, тупиковый-свобода является безопасность собственности. Альперн предполагает , что состояния системы могут быть разделены между состояниями , в котором взаимоблокировка присутствует (красные) состояния и состояние , в котором нет взаимоблокировки не находится в месте (зеленых состояниях). Свойство , которое гласит , что система остается навсегда в зеленых состояниях (или, в качестве альтернативы, что система никогда не достигает красный состояния) является свойством безопасности. Если один не может различать зеленый и красные государства, однако, свойство , которое говорит , что в конечном итоге один из процессов в системе будет эволюционировать является свойством живучести.
различие между безопасностью и живостью может быть формально установлено через предикат , где относится ко времени. Пусть будет момент времени , начиная с которого оцениваются свойства живучести и безопасности. В приведенных ниже примерах, пусть будет процесс (или нить) , что один хочет , чтобы гарантировать , что это тупик бесплатно. 
Безопасность: 
Пример: означает « находится в состоянии взаимоблокировки в момент времени ».
Живучесть: 
Пример: средство « прекращает ожидания на время ».
Живучесть(C,L) в алгоритме Паксос — Если было предложено решение C, то рано или поздно вычислитель L примет какое-либо решение (при условии наличия достаточного количества работающих вычислителей).
Стоит также отметить, что различие между живучестью свойством ограниченной шунтировании и свойством безопасности ограниченного обгона является тонким. свобода Голодания с ограниченным обгоном подразумевает ограниченное шунтирование (т.е. даже если ограниченные перепускной классифицируются как свойство живучести, в действительности она представляет собой смесь свойства живучести и свойство безопасности). Bounded обгон означает, что после того, как процесс меченый объявляет интерес к выходу из критической секции, каждый другой процесс будет перегнать метку процессу ограниченного количество раз до того, как меченый процесс входит в критическую секцию. Об этом говорит сайт https://intellect.icu . Обратите внимание, что если меченый процесс никогда не получил разрешения на въезд в критической секции, ограниченный обгон может по-прежнему держать. Таким образом, ограниченная обгон, само по себе не является свойством живучести. В тупиковой системе, ограниченный обгон тривиально выполняется, так как ни один процесс не обгоняет другой, но ограниченные перепускные нет.
Многие приложения, вероятно, большинство, требуют сохранения объектов от одного сеанса до следующего. Среда должна обеспечивать механизм выполнения этого простым способом.
Объект часто содержит ссылки на другие объекты, тоже содержащие, в свою очередь, ссылки на объекты. Поэтому каждый объект может иметь большое количество зависимых объектов с возможно сложным графом зависимости (который может содержать циклы). Обычно не имеет смысла сохранять или восстанавливать объект без всех его прямых и непрямых зависимых объектов. Говорят, что механизм живучести поддерживает замыкание живучести (persistence closure), если он может автоматически сохранять зависимые объекты наряду с самим объектом.
Должен существовать механизм хранения, поддерживающий замыкание живучести. Он сохраняет объект вместе со всеми зависимыми объектами на внешних устройствах и восстанавливает их в течение того же или другого сеанса.
Для некоторых приложений простой поддержки живучести недостаточно; такие приложения нуждаются в полной поддержке баз данных (database support) . Понятие ОО-базы данных объясняется в одной из дальнейших лекций, где также исследуются другие вопросы живучести, такие как эволюция схемы, способность безопасного восстановления объектов, даже если изменились соответствующие классы.
Устойчивость - это способность ПО соответствующим образом реагировать на аварийные ситуации.
Устойчивость дополняет корректность. Корректность относится к поведению системы в случаях, определенных спецификацией; устойчивость характеризует то, что происходит за пределами этой спецификации.
Рис. 1.3. Устойчивость против корректности
Как видно из определения, устойчивость по своей природе более нечеткое понятие, чем корректность. Невозможно сказать, как в случае с корректностью, что в аварийных ситуациях система должна "выполнять свои задачи", поскольку ситуации выходят за пределы спецификации. Если бы эти задачи были известны, аварийный случай стал бы частью спецификации, и мы бы снова вернулись в область корректности.
| Это определение "аварийной ситуации" нам еще понадобится при изучении обработки исключений (Об исключительных ситуациях см. лекция 12). Оно подразумевает, что понятия нормальной и аварийной ситуации всегда относительны по отношению к заданной спецификации; ситуация аварийна, если она выходит за рамки спецификации. Если расширить спецификацию, аварийные случаи становятся нормальными - даже если они соответствуют таким нежелательным событиям, как, например, ошибочный ввод пользователя. |
Термин "нормальный" в этом смысле не означает "желательный", а просто "запланированный в проекте ПО". Хотя на первый взгляд может показаться парадоксальным, что ошибочный ввод может называться нормальным случаем, любой другой подход опирается на субъективные критерии и, таким образом, бесполезен.
Всегда будут существовать случаи, на которые спецификация явно не распространяется. Роль требования устойчивости - удостовериться, что и в таких случаях система не приводит к непоправимой ситуации; она должна выдать соответствующее сообщение об ошибке, гладко завершить работу или войти в так называемый режим "постепенного вывода из работы".
В информатике , сохранение относится к характеристике состояния , что переживет процесс , который создал его. Это достигается на практике путем сохранения состояния в качестве данных в хранилище данных компьютера . Программы должны передавать данные и из запоминающих устройств и должно обеспечивать отображения из родных языков программирования структур данных для структур данных устройств хранения данных.
Программы для редактирования изображения или текстовые процессоры , например, достичь состояния упорства, сохраняя свои документы в файлы .
Постоянство называется « ортогональной » или «прозрачной» , когда она реализуется как внутреннее свойство среды выполнения программы. Ортогональная среда живучести не требует каких - либо конкретных действий со стороной программ , работающих в нем , чтобы получить или сохранить их состояние .
Неортогональная сохранение требует данные , которые будут записаны и считаны и из хранилища с использованием специальных инструкций в программе, в результате использования сохраняются как переходный глагол: По завершению программы сохраняется данные .
Преимущество ортогональных сред персистенции является более простыми и менее подверженными ошибкам программ.
Ортогональные сохранение широко применяется в операционных системах для зимовки и в виртуализации платформ систем , таких как VMware и VirtualBox для государственной экономии.
Языки Исследования прототипа , такие как PS-Algol , Napier88 , Фибоначчи и pJama, успешно продемонстрированы концепции наряду с преимуществами для программистов.
Система изображения
Использование образов системы является простейшей стратегией настойчивости. Ноутбук спящего режима является примером ортогональной персистентности с использованием образа системы , поскольку она не требует каких - либо действий со стороны программ , запущенных на машине. Пример неортогональных упорства с использованием образом системы является простой программой для редактирования текста выполнения конкретных инструкций , чтобы сохранить весь документ в файл.
Недостатки : Требует достаточно оперативной памяти для хранения всего состояния системы. Государственные изменения , внесенные в систему после последнего сохранения изображения теряется в случае системного сбоя или отключения. Сохранение изображения для каждого изменения было бы слишком много времени для большинства систем, так что изображения не используются в качестве единого метода персистентности для критических систем.
Использование журналов является вторым простейшим методом живучести. Журналирование является процессом хранения событий в журнале, прежде чем каждый из них применяются к системе. Такие журналы называются журналы.
При запуске, журнал для чтения и каждое событие вновь применяются к системе, избегая потери данных в случае сбоя системы или отключения.
Вся «Undo / Redo» История пользовательских команд в программе редактирования изображений, например, при записи в файл, представляет собой журнал, способное восстановление состояния редактируемого изображения в любой момент времени.
Журналы используются журнальной файловой системы , распространенных систем и систем управления базами данных , где они также называются «журналы транзакций» или «повтор журналов».
НЕДОСТАТКИ : Журналы часто в сочетании с другими методами постоянства так, чтобы вся (потенциально большая) история всех событий системы не должна быть повторно при запуске системы.
Этот метод является написание для хранения только тех частей состояния системы, которые были изменены (которые загрязнены) с момента их последней записи. Сложные приложения для редактирования документов, например, будут использовать грязную операции записи, чтобы сохранить только те части документа, которые на самом деле были изменены с момента последнего сохранения.
Недостатки: Этот метод требует изменений состояния , чтобы быть перехвачены в рамках программы. Это достигается в непрозрачном способе, требуя конкретные вызовы при хранении API или прозрачным способом с автоматическим преобразованием программ . Это приводит к тому, что код работает медленнее , чем машинный код и более сложным для отладки.
Любой слой программного обеспечения , что делает его более легким для программы сохраняется его состояние в общем случае называется сохранение слоя. Большинство инерционности слои не добьются настойчивости напрямую , но будут использовать базовую систему управления базами данных .
Распространенность системы является метод, который сочетает в себе образы системы и операционные журналы, упомянутые выше, чтобы преодолеть свои ограничения.
Недостатки: превалирующей система должна иметь достаточно оперативной памяти для хранения всего состояния системы.
СУБД использует комбинацию грязных операций записи и методов транзакций журналируемых упомянутую выше. Они обеспечивают не только сохранение , но и другие услуги , такие как запросы, аудит и контроль доступа.
Постоянные операционные системы операционные системы , которые остаются постоянными даже после аварии или неожиданного выключения. Операционные системы , которые используют эту способность включать в себя
Что такое программа? Это любой код, который можно рассматривать самостоятельно. Предположим, нам нужно написать браузер. Мы выполняем три задачи: проектируем представление программы для пользователя, затем пишем высокоуровневую схему программы, и, наконец, пишем код. По ходу написания кода мы понимаем, что нам нужно написать средство для форматирования текста. Здесь нам опять нужно решить три задачи: определить, какой текст это средство будет возвращать; выбрать алгоритм для форматирования; написать код. У этой задачи своя подзадача: правильно вставлять дефис в слова. Эту подзадачу мы тоже решаем в три шага — как видим, они повторяются на многих уровнях.
Рассмотрим более подробно первый шаг: какую задачу решает программа. Здесь мы чаще всего моделируем программу как функцию, которая получает некоторые входные данные и дает некоторые данные на выходе. В математике функция обычно описывается как упорядоченное множество пар. Например, функция возведения в квадрат для натуральных чисел описывается как множество {<0,0>, <1,1>, <2,4>, <3,9>, ...}. Область определения такой функции — множество первых элементов каждой пары, то есть натуральные числа. Чтобы определить функцию, нам нужно указать ее область определения и формулу.
Но функции в математике — это не то же, что функции в языках программирования. Математика значительно проще. Поскольку на сложные примеры у меня времени нет, рассмотрим простой: функция в языке С или статический метод в Java, возвращающий наибольший общий делитель двух целых чисел. В спецификации этого метода мы напишем: вычисляет GCD(M,N) для аргументов M и N, где GCD(M,N) — функция, область определения которой — множество пар целых чисел, а возвращаемое значение — наибольшее целое число, на которое делится M и N. Как с этой моделью соотносится реальность? Модель оперирует с целыми числами, а в C или Java мы имеем 32-битный int. Эта модель позволяет нам решить, правилен ли алгоритм GCD, но она не предотвратит ошибки переполнения. Для этого потребовалась бы более сложная модель, на которую нет времени.
Поговорим об ограничениях функции как модели. Работа некоторых программ (например, операционных систем) не сводится к тому, чтобы вернуть определенное значение для определенных аргументов, они могут выполняться непрерывно. Кроме того, функция как модель плохо подходит для второго шага: планирования способа решения задачи. Быстрая сортировка и сортировка пузырьком вычисляют одну и ту же функцию, но это совершенно разные алгоритмы. Поэтому для описания способа достижения цели программы я использую другую модель, назовем ее стандартная поведенческая модель. Программа в ней представлена как множество всех допустимых поведений, каждое из которых, в свою очередь, является последовательностью состояний, а состояние — это присвоение значений переменным.
Давайте посмотрим, как будет выглядеть второй шаг для алгоритма Евклида. Нам нужно вычислить GCD(M, N). Мы инициализируем M как x, а N как y, затем повторно отнимаем меньшую из этих переменных от большей до тех пор, пока они не будут равны. Например, если M = 12, а N = 18, мы можем описать следующее поведение:
[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]
А если M = 0 и N = 0? Ноль делится на все числа, поэтому наибольшего делителя в этом случае нет. В этой ситуации нам нужно вернуться к первому шагу и спросить: действительно ли нам нужно вычислять НОД для неположительных чисел? Если в этом нет необходимости, то нужно просто изменить спецификацию.
Здесь следует сделать небольшое отступление о продуктивности. Ее часто измеряют в количестве строк кода, написанных за день. Но ваш труд значительно полезнее, если вы избавились от определенного количества строк, потому что у вас стало меньше места для багов. И избавляться от кода проще всего именно на первом шаге. Вполне возможно, что вам просто не нужны все те навороты, которые вы пытаетесь реализовать. Самый быстрый способ упростить программу и сэкономить время — не делать вещи, которые не стоит делать. Второй шаг — на втором месте по потенциалу для экономии времени. Если вы измеряете продуктивность в количестве написанных строк, то продумывание способа выполнения задачи сделает вас менее продуктивными, поскольку вы сможете решить ту же задачу меньшим объемом кода. Точную статистику я здесь привести не могу, поскольку у меня нет способа посчитать то количество строк, которые я не написал благодаря тому, что потратил время на спецификацию, то есть на первый и второй шаги. И эксперимент тут тоже не поставить, потому что в эксперименте мы не имеем права выполнить первый шаг, задание определено заранее.
В неформальных спецификациях легко не учесть многие трудности. Ничего сложного в написании строгих спецификаций для функций нет, обсуждать это я не буду. Вместо этого мы поговорим о написании строгих спецификаций для стандартных поведенческих моделей. Есть теорема, которая гласит, что любое множество поведений можно описать с помощью свойства безопасности (safety) и свойства живучести (liveness). Безопасность означает, что ничего плохого не произойдет, программа не выдаст неверный ответ. Живучесть означает, что рано или поздно произойдет что-то хорошее, т. е. программа рано или поздно даст правильный ответ. Как правило, безопасность является более важным показателем, ошибки чаще всего возникают именно здесь. Поэтому для экономии времени я не буду говорить об живучести, хотя она, конечно, тоже важна.
Мы добиваемся безопасности, прописывая, во-первых, множество возможных исходных состояний. И, во-вторых, отношения со всеми возможными следующими состояниями для каждого состояния. Будем вести себя как ученые и определим состояния математически. Набор исходных состояний описывается формулой, например, в случае алгоритма Евклида: (x = M) ∧ (y = N). Для определенных значений M и N существует только одно исходное состояние. Отношение со следующим состоянием описывается формулой, в которой переменные следующего состояния записываются со штрихом, а текущего состояния — без штриха. В случае с алгоритмом Евклида мы будем иметь дело с дизъюнкцией двух формул, в одной из которых x является наибольшим значением, а во второй — y:
В первом случае новое значение y равно прежнему значению y, а новое значение x мы получаем, отняв от большей переменной меньшую. Во втором случае мы делаем наоборот.
Вернемся к алгоритму Евклида. Предположим вновь, что M = 12, N = 18. Это определяет единственное исходное состояние, (x = 12) ∧ (y = 18). Затем мы подставляем эти значения в формулу выше и получаем:
Здесь единственное возможное решение: x' = 18 - 12 ∧ y' = 12, и мы получаем поведение: [x = 12, y = 18]. Точно так же мы можем описать все состояния в нашем поведении: [x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6].
В последнем состоянии [x = 6, y = 6] обе части выражения будут ложны, следовательно, следующего состояния у него нет. Итак, мы имеем полную спецификацию второго шага — как видим, это вполне обычная математика, как у инженеров и ученых, а не странная, как в computer science.
Эти две формулы можно объединить в одну формулу темпоральной логики. Она элегантна и объяснить ее нетрудно, но на нее сейчас нет времени. Темпоральная логика нам может понадобиться только для свойства живости, для безопасности она не нужна. Темпоральная логика как таковая не нравится, это не вполне обычная математика, но в случае с живостью она является необходимым злом.
В алгоритме Евклида для каждого значения x и y есть уникальные значения x' и y', которые делают отношение со следующим состоянием истинным. Другими словами, алгоритм Евклида детерминированный. Чтобы смоделировать недетерминированный алгоритм, нужно, чтобы у текущего состояния было несколько возможных будущих состояний, и чтобы у каждого значения переменной без штриха было несколько значений переменной со штрихом, при которых отношение со следующим состоянием является истинным. Это несложно сделать, но сейчас приводить примеры я не буду.
Чтобы сделать работающий инструмент, нужна формальная математика. Как сделать спецификацию формальной? Для этого нам понадобится формальный язык, например, TLA+. Спецификация алгоритма Евклида будет на этом языке выглядеть следующим образом:
Символ знака равенства с треугольником означает, что значение слева от знака определено как равное значению справа от знака. В сущности, спецификация — это определение, в нашем случае два определения. К спецификации в TLA+ нужно добавить объявления и некоторый синтаксис, как на слайде выше. В ASCII это будет выглядеть так:
Как видим, ничего сложного. Спецификацию на TLA+ можно проверить, т. е. обойти все возможные поведения в небольшой модели. В нашем случае этой моделью будут определенные значения M и N. Это очень эффективный и простой способ проверки, который целиком выполняется автоматически. Кроме того, можно написать формальные доказательства истинности и проверить их механически, но для этого нужно много времени, поэтому так почти никто не делает.
Главный недостаток TLA+ в том, что это математика, а программисты и computer scientists боятся математики. На первый взгляд это звучит как шутка, но, к сожалению, я говорю это на полном серьезе. Мой коллега только что рассказывал мне, как он пытался объяснить TLA+ нескольким разработчикам. Как только на экране появились формулы, у них сразу же сделались стеклянные глаза. Так что если TLA+ пугает, можно использовать PlusCal, это своего рода игрушечный язык программирования. Выражение в PlusCal может быть любым выражением TLA+, то есть, по большому счету, любым математическим выражением. Кроме того, в PlusCal есть синтаксис для недетерминистичных алгоритмов. Благодаря тому, что в PlusCal можно записать любое выражение TLA+, он является значительно более выразительным любого реального языка программирования. Далее, PlusCal компилируется в легко читаемую спецификацию TLA+. Это не значит, конечно, что сложная спецификация PlusCal превратится в простую на TLA+ — просто соответствие между ними очевидное, не появится дополнительной сложности. Наконец, эту спецификацию можно будет проверить инструментами TLA+. В общем, PlusCal может помочь преодолеть фобию математики, его легко понять даже программистам и computer scientists. В прошлом я какое-то время (около 10 лет) публиковал на нем алгоритмы.
Возможно, кто-то возразит, что TLA+ и PlusCal — это математика, а математика работает только на придуманных примерах. На практике же нужен реальный язык с типами, процедурами, объектами и так далее. Это не так. Вот, что пишет Крис Ньюкомб, работавший в Amazon: «Мы использовали TLA+ в десяти крупных проектах, и в каждом случае его использование вносило значительный вклад в разработку, потому что мы смогли отловить опасные баги до попадания в продакшн, и потому что он дал нам понимание и уверенность, необходимые для агрессивных оптимизаций производительности, не влияющих на истинность программы». Часто можно услышать, что при использовании формальных методов мы получаем неэффективный код — на практике же все ровно наоборот. Кроме того, бытует мнение, что менеджеров невозможно убедить в необходимости формальных методов, даже если программисты убеждены в их полезности. А Ньюкомб пишет: «Менеджеры теперь всячески подталкивают к тому, чтобы писать спецификации на TLA+, и специально выделяют на это время». Так что когда менеджеры видят, что TLA+ работает, они с радостью его принимают. Крис Ньюкомб написал это где-то шесть месяцев тому назад (в октябре 2014 года), сейчас же, насколько я знаю, TLA+ используется в 14 проектах, а не 10. Другой пример относится к проектированию XBox 360. К Чарльзу Текеру пришел стажер и написал спецификацию для системы памяти. Благодаря этой спецификации был найден баг, который иначе был бы не замечен, и из-за которого каждая XBox 360 падала бы после четырех часов использования. Инженеры из IBM подтвердили, что их тесты не обнаружили бы этот баг.
Более подробно про TLA+ вы можете почитать в интернете, а сейчас давайте поговорим о неформальных спецификациях. Нам редко приходится писать программы, которые вычисляют наименьший общий делитель и тому подобное. Значительно чаще мы пишем программы вроде инструмента структурной распечатки (pretty-printer), который я написал для TLA+. После самой простой обработки код на TLA+ выглядел бы следующим образом:
Но в приведенном примере пользователь скорее всего хотел, чтобы знаки конъюнкции и равенства были выравнены. Так что правильное форматирование выглядело бы скорее так:
Рассмотрим другой пример:
Здесь, наоборот, выравнивание знаков равенства, сложения и умножения в источнике было случайным, поэтому самой простой обработки вполне достаточно. В общем, точного математического определения верного форматирования нет, потому что «правильное» в данном случае значит «такое, какое хочет пользователь», а это математически определить нельзя.
Казалось бы, если у нас нет определения истинности, то спецификация бесполезна. Но это не так. Если мы не знаем, что именно программа должна сделать, это не значит, что нам не нужно продумывать ее работу — наоборот, мы должны потратить на это еще больше усилий. Спецификация здесь особенно важна. Определить оптимальную программу для структурной распечатки невозможно, но это не значит, что мы не должны за нее браться вообще, а писать код как поток сознания — это не дело. В итоге я написал спецификацию из шести правил с определениями в форме комментариев в Java-файле. Вот пример одного из правил: a left-comment token is LeftComment aligned with its covering token. Это правило написано на, скажем так, математическом английском: LeftComment aligned, left-comment и covering token — термины с определениями. Это то, как математики описывают математику: пишут определения терминов и на основе них — правила. Польза от такой спецификации в том, что понять и отладить шесть правил значительно проще, чем 850 строк кода. Надо сказать, что написать эти правила было непросто, довольно много времени ушло на их отладку. Специально для этой цели я написал код, который сообщал, какое именно правило используется. Благодаря тому, что я проверил эти шесть правил на нескольких примерах, мне не нужно было отлаживать 850 строк кода, и баги оказалось довольно легко найти. В Java для этого есть отличные инструменты. Если бы я просто написал код, то у меня ушло бы значительно больше времени, и форматирование получилось бы худшего качества.
Почему нельзя было использовать формальную спецификацию? С одной стороны, правильность выполнения здесь не слишком важна. Структурная распечатка обязательно кому-то не угодит, так что мне не нужно было добиваться правильной работы во всех неординарных ситуациях. Еще важнее тот факт, что у меня не было адекватных инструментов. Средство для проверки моделей TLA+ здесь бесполезно, так что мне пришлось бы вручную писать примеры.
У приведенной спецификации есть черты, общие для всех спецификаций. Она более высокого уровня, чем код. Реализовать ее можно на любом языке. Для ее написания бесполезны какие-либо инструменты или методы. Никакой курс программирования вам не поможет написать эту спецификацию. И не существует инструментов, которые могли бы сделать эту спецификацию ненужной, если, конечно, вы не пишете язык специально для написания программ структурной распечатки на TLA+. Наконец, эта спецификация ничего не говорит о том, как именно мы будем писать код, в ней только указывается, что этот код делает. Мы пишем спецификацию, чтобы помочь нам продумать проблему, прежде чем мы начнем думать о коде.
Но у этой спецификации есть и особенности, отличающие ее от других спецификаций. 95% других спецификаций значительно короче и проще:
Далее, эта спецификация является набором правил. Как правило, это признак плохой спецификации. Понять последствия набора правил довольно трудно, и именно поэтому мне пришлось потратить много времени на их отладку. Тем не менее, в данном случае лучшего способа мне было не найти.
Стоит сказать несколько слов о программах, которые работают непрерывно. Как правило, они работают параллельно, например, операционные системы или распределенные системы. Разобраться в них в уме или на бумаге могут очень немногие, и я к их числу не принадлежу, хотя когда-то мне это было по силам. Поэтому необходимы инструменты, которые будут проверять нашу работу — например, TLA+ или PlusCal.
Зачем нужно было писать спецификацию, если я и так знал, что именно код должен делать? На самом деле, мне только казалось, будто бы я это знаю. Кроме того, при наличии спецификации постороннему человеку уже не нужно залезать в код, чтобы понять, что именно он делает. У меня есть правило: не должно быть никаких общих правил. У этого правила, конечно же, есть исключение, это единственное общее правило, которому я следую: спецификация того, что делает код, должна сообщать людям все, что им нужно знать при использовании этого кода.
Итак, что именно программистам нужно знать о мышлении? Для начала, то же, что и всем: если ты не пишешь, то тебе только кажется, что ты мыслишь. Кроме того, нужно думать, прежде чем кодить, а это значит, нужно писать, прежде чем кодить. Спецификация — это то, что мы пишем перед тем, как начать кодить. Спецификация нужна для любого кода, который может быть кем-либо использован или изменен. И этим «кто-либо» может оказаться сам автор кода через месяц после его написания. Спецификация нужна для больших программ и систем, для классов, для методов и иногда даже для сложных участков отдельного метода. Что именно нужно писать о коде? Нужно описать, что он делает, то есть то, что может быть полезно любому человеку, использующему этот код. Иногда может также быть необходимо указать, как именно код достигает своей цели. Если этот способ мы проходили в курсе алгоритмов, то мы называем это алгоритмом. Если же это нечто более специальное и новое, то мы называем это высокоуровневым проектированием. Формальной разницы здесь нет: и то, и другое является абстрактной моделью программы.
Как именно следует писать спецификацию кода? Главное: она должна быть на уровень выше самого кода. Она должна описывать состояния и поведения. Она должна быть настолько строгой, насколько этого требует задача. Если вы пишете спецификацию способа реализации задачи, то ее можно написать на псевдокоде или при помощи PlusCal. Учиться писать спецификации нужно на формальных спецификациях. Это даст вам необходимые навыки, которые помогут в том числе и с неформальными. А как научиться писать формальные спецификации? Когда мы учились программированию, мы писали программы, а затем отлаживали их. То же самое здесь: нужно написать спецификацию, проверить ее при помощи средства проверки моделей и исправить ошибки. TLA+, возможно, не самый лучший язык для формальной спецификации, и для ваших конкретных нужд скорее всего лучше подойдет другой язык. Преимущество TLA+ в том, что он отлично учит математическому мышлению.
Как связать спецификацию и код? При помощи комментариев, которые связывают математические понятия и их реализацию. Если вы работаете с графами, то на уровне программы у вас будут массивы узлов и массивы связей. Поэтому вам нужно написать, как именно граф реализуется этими структурами программирования.
Нужно заметить, что ничто из вышесказанного не относится к самому процессу написания кода. Когда вы пишете код, то есть выполняете третий шаг, вам тоже нужно мыслить и продумывать программу. Если подзадача оказывается сложной или неочевидной, нужно написать для нее спецификацию. Но о самом коде я здесь не говорю. Вы можете пользоваться любым языком программирования, любой методологией, речь не о них. Кроме того, ничто из вышесказанного не избавляет от необходимости тестировать и отлаживать код. Даже если абстрактная модель написана верно, в ее реализации могут быть баги.
Написание спецификаций — дополнительный этап в процессе написания кода. Благодаря нему многие ошибки можно отловить меньшими усилиями — мы это знаем по опыту программистов из Amazon. Со спецификациями качество программ становится выше. Так почему же тогда мы так часто обходимся без них? Потому что писать трудно. А писать трудно, потому что для этого нужно думать, а думать тоже трудно. Всегда проще делать вид, что думаешь. Здесь можно провести аналогию с бегом — чем меньше вы бегаете, тем медленнее вы бежите. Нужно тренировать свои мускулы и упражняться в письме. Нужна практика.
Спецификация может быть неверной. Вы могли где-то сделать ошибку, или могли измениться требования, или оказалось необходимо сделать улучшение. Любой код, которым кто-либо пользуется, приходится менять, поэтому рано или поздно спецификация перестанет соответствовать программе. В идеале в этом случае нужно написать новую спецификацию и полностью переписать код. Мы прекрасно знаем, что так никто не делает. На практике мы патчим код и, возможно, обновляем спецификацию. Если это обязательно рано или поздно происходит, то зачем вообще писать спецификации? Во-первых, для человека, который будет править ваш код, каждое лишнее слово в спецификации будет на вес золота, и этим человеком вполне можете быть вы сами. Я часто ругаю себя за недостаточную спецификацию, когда правлю свой код. А я пишу больше спецификаций, чем кода. Поэтому, когда вы правите код, спецификацию всегда нужно обновлять. Во-вторых, с каждой правкой код становится хуже, его становится все труднее читать и поддерживать. Это нарастание энтропии. Но если вы не начинаете со спецификации, то каждая написанная строка будет правкой, и код с самого начала будет громоздким и трудночитаемым.
Как говорил Эйзенхауер, ни одна битва не была выиграна по плану, и ни одна битва не была выиграна без плана. А он знал кое-что о битвах. Существует мнение, что написание спецификаций — пустая трата времени. Иногда это действительно так, и задача настолько проста, что продумывать ее нечего. Но всегда нужно помнить, что, когда вам советуют не писать спецификаций, это значит, что вам советуют не думать. И об этом каждый раз следует подумать. Продумывание задачи не гарантирует, что вы не совершите ошибок. Как мы знаем, волшебной палочки никто не изобрел, и программирование — сложное занятие. Но если вы не продумываете задачу, вы гарантированно сделаете ошибки.
1 The ResiliNets Research Initiative definition of survivability.
2 Abdul Jabbar Mohammad, David Hutchison, and James P.G. Sterbenz "Poster: Towards Quantifying Metrics for Resilient and Survivable Networks", 14th IEEE International Conference on Network Protocols (ICNP 2006), Santa Barbara, California, USA, November 2006
3 Balzer, Стефани (17 ноября 2005). «Контрактная программирование Стойкие объекта» (PDF) . Университет Глазго - Школа CS - исследования . ETH Zürich
4. Попков В. К. Математические модели живучести сетей связи. – Новосибирск: СО АН СССР. 1990. –235 с.
5. Черкесов Г. Н. Методы и модели оценки живучести сложных систем. — М.: Знание, —1987. —55 с.
6. Нетес В.А. Надежность сетей связи в период перехода к NGN. М : – Вестник связи, №9. 2007. – 4-5 с
7. ДСТУ В3265 – 95 Зв'язок військовий. Терміни та визначення. Чинний від 1997–01–01 Державний стандарт України, С.23
8 Stanford Seminar - Programing Should Be More Than Coding https://youtu be.com/watch?v=6QsTfL-uXd8
Исследование, описанное в статье про живучесть, подчеркивает ее значимость в современном мире. Надеюсь, что теперь ты понял что такое живучесть, живучесть в системах связи, живучесть любой системы, survivability, живучесть в параллельных вычислениях, liveness, формы живости, различие между безопасностью и живостью, ограниченный обгон, живучесть в ооп, persistence, живучесть в программном обеспечении, устойчивость программ, robustness, живучесть в информатике, persistence computer science, постоянство в информатике, ортогональное сохранение, прозрачное сохранение, теорема об описании множества поведений и для чего все это нужно, а если не понял, или есть замечания, то не стесняйся, пиши или спрашивай в комментариях, с удовольствием отвечу. Для того чтобы глубже понять настоятельно рекомендую изучить всю информацию из категории Информатика
Ответы на вопросы для самопроверки пишите в комментариях, мы проверим, или же задавайте свой вопрос по данной теме.
Комментарии
Оставить комментарий
Информатика
Термины: Информатика