Реферат: Распределенные алгоритмы
Рассматривая распределенный алгоритм для некоторой проблемы, необходимо продемонстрировать, что алгоритм есть корректное решение этой проблемы. Проблема указывает, какие свойства требуемый алгоритм должен иметь; должно быть показано, что решение обладает этими свойства. Вопрос проверки распределенных алгоритмов получил значительное внимание и есть большое количество статей, обсуждающих формальные методы проверки; см. [CM88, Fra86, Kel76, MP88]. В этом разделе обсуждаются некоторые простые, но часто используемые методы для демонстрации правильности распределенных алгоритмов. Эти методы полагаются только на определение системы переходов.
Многие из требуемых свойств распределенных алгоритмов попадают в один из двух типов: требования безопасности и требования живости. Требования безопасности накладывают ограничение, что определенное свойство должно выполняться для каждого исполнения системы в каждой конфигурации, достигаемой в этом исполнении. Требования живости определяют, что определенное свойство должно выполняться для каждого исполнения системы в некоторых конфигурациях, достигаемых в этом исполнении. Эти требования могут также встречаться в ослабленной форме, например, они могут удовлетворяться с некоторой фиксированной вероятностью над множеством возможных исполнений. Другие требования к алгоритмам могут включать ограничения, которые основываются только на использовании некоторого данного знания (см. подраздел 2.4.4), что они гибки по отношен ию к нарушениям в некоторых процессах (см. часть 3), что процессы равны (см. главу 9), и т.д.
Методы проверки, описанные в этом разделе, базируются на истинности утверждений в конфигурациях, достигаемых в исполнении. Такие методы называются методами проверки утверждений. Утверждение это унарное отношение на множестве конфигураций, то есть, предикат, который принимает значение истина на одном подмножестве конфигураций и ложь – на другом.
Свойство безопасности алгоритма это свойство в форме «Утверждение P истина в каждой конфигурации каждого исполнения алгоритма». Неформально это формулируется как «Утверждение Р всегда истина». Основной метод для того, чтобы показать, что утверждение Р всегда истина, это продемонстрировать, что Р инвариант согласно следующим определениям. Нотация P(g), где g это конфигурация, есть булево выражение, чье значение истина, если Р выполняется в g, и ложь в противном случае.
Определения зависят от данной системы переходов S = (C, à, I). Далее, мы будем писать {P} à {Q}, чтобы обозначить, что для каждого перехода g à d (системы S), если Р(g) то Q(d). Таким образом {P} à {Q} означает, что, если Р выполняется перед любым переходом, то Q выполняется после этого перехода.
Определение 2.9 Утверждение Р инвариант системы S, если
(1) для всех g Î I, и
(2) {P} à {P}.
Определение говорит, что инвариант выполняется в каждой начальной конфигурации, и сохраняется при каждом переходе. Из этого следует, что он сохраняется в каждой достигаемой конфигурации, как и формулируется в следующем теореме.
Теорема 2.10 Если Р это инвариант системы S, то Р выполняется для каждой конфигурации каждого исполнения системы S.
Доказательство. Пусть Е = (g0, g1, g2, ...) исполнение системы S. Будет показано по индукции, что Р(gi) выполняется для каждого i. Во-первых, Р(g0) выполняется, потому что g0 Î I и по первому предложению определения 2.9. Во-вторых, предположим P(gi ) выполняется и gi à gi+1 есть переход, который встречается в E. По второму предложению определения 2.9 P(gi+1) выполняется, что и завершает доказательство.
И наоборот, утверждение, которое выполняется в каждой конфигурации каждого исполнения, есть инвариант (см. упражнение 2.2). Отсюда не каждое свойство безопасности может быть доказано применением теоремы 2.10. В этом случае, однако, каждое утверждение, которое всегда истинно, включено в инвариант; отсюда может быть показано, применением следующей теоремы, что утверждение всегда истинно. (Нужно помнить, однако, что часто очень трудно найти подходящий инвариант Q, к которому можно применить теорему.)
Теорема 2.11 Пусть Q будет инвариантом системы S и положим Q Þ P (для каждого g Î С). Тогда Р выполняется в каждой конфигурации каждого исполнения системы S.
Доказательство. По теореме 2.10, Q выполняется в каждой конфигурации, и так как Q включает P, то P выполняется в каждой конфигурации также.
Иногда полезно доказать сначала слабый инвариант, и впоследствии использовать его для доказательства более сильного инварианта. Как можно сделать инвариант более сильным демонстрируется в следующем определении и теореме.
Определение 2.12 Пусть S будет системой переходов и P, Q будут утверждениями. Р называется Q-производным, если
(1) для всех g Î I, Q(g) Þ Р(g); и
(2) {Q Ù Р} à {Q Þ Р}.
Теорема 2.13 Если Q есть инвариант и Р – Q-производное, то Q Ù P есть инвариант.
Доказательство. Согласно определению 2.9, должно быть показано, что
(1) для всех g Î I, Q(g) Ù Р(g); и
(2) {Q Ù Р} à {Q Ù Р}.
Т.к. Q это инвариант, Q(g) выполняется для всех g Î I, и т.к. для всех g Î I, Q(g) Þ Р(g), P(g) выполняется для всех g Î I. Следовательно, Q(g) Ù P(g) выполняется для всех g Î I.
Предположим g à d и Q(g) Ù Р(g). Т.к. Q это инвариант, Q(d) выполняется, и т.к. {Q Ù P} à {Q Þ Р}, Q(d) Þ Р(d), откуда Р(d) вытекает. Следовательно, Q(d) Ù Р(d) выполняется.
Примеры доказательства безопасности, основывающиеся на материале данного раздела, представлены в разделе 3.1.
Свойство живости алгоритма это свойство в форме «Утверждение Р истина в некоторой конфигурации каждого исполнения алгоритма». Неформально это формулируется как «Утверждение Р в конечном счете истина». Основные методы, используемые, чтобы показать, что Р в конце концов истина – это нормирующие функции и беступиковость (или правильное завершение). Более простой метод может быть использован для алгоритмов, в которых разрешаются только исполнения с фиксированной, конечной длиной.
Пусть S будет системой переходов и Р – предикат. Определим term как предикат, который истина во всех терминальных конфигурациях и ложь во всех нетерминальных конфигурациях. Мы сначала предположим ситуации, где исполнение достигает терминальной конфигурации. Обычно нежелательно, чтобы такая конфигурация достигалась, в то время, как «цель» Р не была достигнута. Говорят, что в этом случае имеет место тупик. С другой стороны, завершение позволено, если цель была достигнута, в этом случае говорят о правильном завершении.
Определение 2.14 Система S завершается правильно (или без тупиков), если предикат (term Þ Р) всегда истинен в системе S.
Нормирующие функции полагаются га математическое понятие обоснованных множеств. Это множество с порядком <, где нет бесконечных убывающих последовательностей.
Определение 2.15 Частичный порядок (W, <) является обоснованным, если в нем нет бесконечной убывающей последовательности
w1 > w2 > w3 ... .
Примеры обоснованных множеств, которые будут использоваться в этой книге – это натуральные числа с обычным порядком, и n-кортежи натуральных чисел с лексикографическим порядком (см. раздел 4.3). Свойство, что обоснованное множество не имеет бесконечной убывающей последовательности, может использоваться, чтобы показать, что утверждение Р в конечном счете истина. К этому моменту должно быть показано, что существует функция f из C в обоснованное множество W такая, что в каждом переходе значение f убывает или Р становится истиной.
Определение 2.16 Пусть даны система переходов S и утверждение Р. Функция f из С в обоснованное множество W называется нормирующей функцией (по отношению к Р), если для каждого перехода g à d , f(g) > f(d) или Р(d).
Теорема 2.17 Пусть даны система переходов S и утверждение Р. Если S завершается правильно и нормирующая функция f (w.r.t Р) существует, то Р – истина в некоторой конфигурации каждого исполнения системы S.
Доказательство. Пусть Е = (g0, g1, g3, ...) – исполнение системы S. Если Е конечно, его последняя конфигурация является терминальной, и т.к. term Þ Р всегда истина в системе S, то Р выполняется в этой конфигурации. Если Е бесконечно, пусть E’ будет самым длинным префиксом Е, который не содержит конфигураций, в которых Р истина, и пусть s будет последовательностью (f(g0 ), f(g1), ...) для всех конфигураций gi, которые появляются в Е’. В зависимости от выбора Е’ и свойства f, s может быть убывающей последовательностью, и отсюда, по обоснованности W, s конечна. Это подразумевает также, что Е’ – конечный префикс (g0, g1, ..., gk ) исполнения Е. В зависимости от выбора Е’, Р(gk+1) выполняется.
Страницы: 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 58, 59, 60, 61, 62, 63, 64, 65, 66, 67, 68, 69, 70, 71, 72, 73, 74, 75, 76, 77, 78, 79, 80, 81, 82, 83, 84, 85, 86, 87, 88, 89, 90, 91, 92, 93, 94, 95, 96, 97, 98, 99, 100, 101, 102, 103, 104, 105
