2.2 Доказательство свойств систем перехода
Рассматривая распределенный алгоритм для некоторой проблемы, необходимо продемонстрировать, что алгоритм есть корректное решение этой проблемы. Проблема указывает, какие свойства требуемый алгоритм должен иметь; должно быть показано, что решение обладает этими свойства. Вопрос проверки распределенных алгоритмов получил значительное внимание и есть большое количество статей, обсуждающих формальные методы проверки; см. [CM88, Fra86, Kel76, MP88]. В этом разделе обсуждаются некоторые простые, но часто используемые методы для демонстрации правильности распределенных алгоритмов. Эти методы полагаются только на определение системы переходов.
Многие из требуемых свойств распределенных алгоритмов попадают в один из двух типов: требования безопасности и требования живости. Требования безопасности накладывают ограничение, что определенное свойство должно выполняться для каждого исполнения системы в каждой конфигурации, достигаемой в этом исполнении. Требования живости определяют, что определенное свойство должно выполняться для каждого исполнения системы в некоторых конфигурациях, достигаемых в этом исполнении. Эти требования могут также встречаться в ослабленной форме, например, они могут удовлетворяться с некоторой фиксированной вероятностью над множеством возможных исполнений. Другие требования к алгоритмам могут включать ограничения, которые основываются только на использовании некоторого данного знания (см. подраздел 2.4.4), что они гибки по отношен ию к нарушениям в некоторых процессах (см. часть 3), что процессы равны (см. главу 9), и т.д.
Методы проверки, описанные в этом разделе, базируются на истинности утверждений в конфигурациях, достигаемых в исполнении. Такие методы называются методами проверки утверждений. Утверждение это унарное отношение на множестве конфигураций, то есть, предикат, который принимает значение истина на одном подмножестве конфигураций и ложь – на другом.
2.2.1 Свойства безопасности
Свойство безопасности алгоритма это свойство в форме «Утверждение 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.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.
2.2.2 Свойства живости
Свойство живости алгоритма это свойство в форме «Утверждение Р истина в некоторой конфигурации каждого исполнения алгоритма». Неформально это формулируется как «Утверждение Р в конечном счете истина». Основные методы, используемые, чтобы показать, что Р в конце концов истина – это нормирующие функции и беступиковость (или правильное завершение). Более простой метод может быть использован для алгоритмов, в которых разрешаются только исполнения с фиксированной, конечной длиной.
Пусть 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) выполняется.
Если приняты свойства справедливости, то можно заключить из более слабых посылок (чем в теореме 2.17), что Р в конце концов станет истиной. Значение нормирующей функции не должно уменьшаться при каждом переходе. Предположение справедливости может быть использовано, чтобы показать, что бесконечные исполнения содержат переходы определенного типа бесконечно часто. Затем будет достаточно показать, что f никогда не увеличивается, а уменьшается с каждым переходом этого типа.
В некоторых случаях мы будем использовать следующий результат, который есть специальный случай теоремы 2.17
Страницы: 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
