Живучесть - Liveness

В параллельные вычисления, живость относится к набору свойств параллельные системы, которые требуют от системы прогресса, несмотря на то, что ее одновременно выполняющиеся компоненты ("процессы"), возможно, должны "по очереди" в критические разделы, части программы, которые не могут одновременно выполняться несколькими процессами.^[1] Гарантии живучести являются важными свойствами операционных систем и распределенные системы.^[2]

В более общем смысле свойство живости утверждает, что «в конечном итоге произойдет что-то хорошее», в отличие от свойство безопасности в котором говорится, что «что-то плохое не происходит». Если свойство безопасности нарушено, всегда существует конечное выполнение, которое показывает нарушение («плохое» событие), но свойство живучести не может быть нарушено в конечном выполнении распределенного системе, потому что «хорошее» событие может произойти позже. Конечная последовательность является примером свойства живости.^[3] Все свойства линейного времени можно выразить как пересечение свойств безопасности и живучести.^[4] В то время как нарушение данного свойства безопасности допускает наличие ограниченного свидетеля, нарушение свойств живучести может быть труднее установить, поскольку конечный свидетель не может использоваться в качестве доказательства.^[5]

Формы жизни

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

• Свобода от тупик это форма жизни, хотя и слабая. Рассмотрим систему с несколькими процессами и одним критическим разделом, защищенным некоторыми взаимное исключение устройство. Такая система называется безблокировочной, если, когда группа процессов конкурирует за доступ к критической секции в какой-то момент времени, то немного процесс в конечном итоге прогрессирует в более поздний момент времени. Этот процесс не обязательно должен принадлежать к вышеупомянутой группе; он мог получить доступ раньше или даже позже.^[6]
• Свобода от голодание (или «конечный обход») - более надежная гарантия живучести, чем свобода от тупиков. В нем говорится, что все процессы, борющиеся за доступ к критическому региону, в конечном итоге достигают прогресса. Любая система без голодания тоже безблокировочная.^[6]
• Еще более сильным является требование ограниченного обхода. Это означает, что если п процессы конкурируют за доступ к критической области, затем каждый процесс достигает прогресса после того, как был обойден в лучшем случае ж(п) раз другими процессами для некоторой функции ж.^[6]

Живучесть и безопасность

По мнению Б. Альперна, свобода от тупиков - это безопасность свойство.^[7] Альперн предполагает, что состояния системы могут быть разделены между состояниями, в которых присутствует тупик (красные состояния), и состояниями, в которых тупик не существует (зеленые состояния). Свойство, которое гласит, что система всегда остается в зеленом состоянии (или, альтернативно, что система никогда не достигает красного состояния), является свойством безопасности. Однако, если невозможно различить зеленое и красное состояния, свойство, которое говорит о том, что в конечном итоге один из процессов в системе будет развиваться, является свойством жизнеспособности.

Формальное различие

Различие между безопасностью и живучестью можно формально установить с помощью предиката ${\displaystyle P(t)}$, куда ${\displaystyle t}$ относится ко времени. Позволять ${\displaystyle t_{0}}$ быть моментом времени, начиная с которого оцениваются свойства живучести и безопасности. В приведенных ниже примерах пусть ${\displaystyle x}$ быть процессом (или потоком), который нужно гарантировать, что он свободен от тупиков.

Безопасность: ${\displaystyle \forall t\geq t_{0}:P(t)={\textrm {False}}.}$

Пример: ${\displaystyle P(t)}$ средства "${\displaystyle x}$ находится в состоянии тупика во время ${\displaystyle t}$".

Живучесть: ${\displaystyle \forall t_{1}\geq t_{0},\exists t\geq t_{1},t<\infty :P(t)={\textrm {True}}.}$

Пример: ${\displaystyle P(t)}$ средства "${\displaystyle x}$ перестает ждать вовремя ${\displaystyle t}$".

Ограниченный объезд и ограниченный обгон

Также стоит отметить, что разница между свойством живучести ограниченного объезда и свойством безопасности ограниченного обгона тонкая. Свобода голода вместе с ограниченным обгоном подразумевает ограниченный объезд (т.е. хотя ограниченный объезд классифицируется как свойство живучести, на самом деле он представляет собой сочетание свойства живучести и свойства безопасности). Ограниченный обгон означает, что после того, как помеченный процесс заявляет о своей заинтересованности во входе в критическую секцию, каждый другой процесс будет обгонять помеченный процесс ограниченное количество раз, прежде чем помеченный процесс войдет в критическую секцию. Обратите внимание, что если помеченному процессу никогда не предоставляется разрешение на вход в его критическую секцию, ограниченный обгон все еще может сохраняться. Следовательно, ограниченный обгон сам по себе не является свойством живучести. В системе с тупиком ограниченный обгон выполняется тривиально, поскольку ни один процесс не обгоняет другой, а ограниченный обход - нет.^[8]

Смотрите также

• Неблокирующий алгоритм

Рекомендации

1. Лэмпорт, Л. (1977). «Доказательство правильности многопроцессорных программ». IEEE Transactions по разработке программного обеспечения (2): 125–143. CiteSeerX  10.1.1.137.9454. Дои:10.1109 / TSE.1977.229904.
2. Луис Родригес, Кристиан Кашен; Рашид Геррауи (2010). Введение в надежное и безопасное распределенное программирование (2-е изд.). Берлин: Springer Berlin. С. 22–24. ISBN  978-3-642-15259-7.
3. Bailis, P .; Годси, А. (2013). «Возможная согласованность сегодня: ограничения, расширения и не только». Очередь. 11 (3): 20. Дои:10.1145/2460276.2462076.
4. Alpern, B .; Шнайдер, Ф. Б. (1987). «Признавая безопасность и живучесть». Распределенных вычислений. 2 (3): 117. CiteSeerX  10.1.1.20.5470. Дои:10.1007 / BF01782772.
5. Гауда, Мохамед Г. (1993). «Проверка протокола - это просто: учебное пособие». Компьютерные сети и системы ISDN. 25 (9): 969–980. Дои:10.1016 / 0169-7552 (93) 90094-к.
6. Рейналь, Мишель (2012). Параллельное программирование: алгоритмы, принципы и основы. Springer Science & Business Media. С. 10–11. ISBN  978-3642320262.
7. Альперн, Б. (1985). «Определяя живость». Письма об обработке информации. 21 (4): 181–185. Дои:10.1016/0020-0190(85)90056-0.
8. Фанг, Ю. (2006). Живучесть невидимыми инвариантами. Международная конференция по формальным методам построения сетевых и распределенных систем. Конспект лекций по информатике. 4229. С. 356–371. Дои:10.1007/11888116_26. ISBN  978-3-540-46219-4.