Распределенные алгоритмы
Категория реферата: Рефераты по информатике, программированию
Теги реферата: налоги и налогообложение, план дипломной работы
Добавил(а) на сайт: Ноздрин.
Предыдущая страница реферата | 11 12 13 14 15 16 17 18 19 20 21 | Следующая страница реферата
Возможно включить условия справедливости в формальную модель явно, как это сделано Манна и Пнули [MP88]. Большинство алгоритмов, с которыми мы имеем дело в этой книге, не полагаются на эти условия; поэтому мы решили не включать их в модель, а устанавливать эти условия явно, когда они используются для конкретного алгоритма или проблемы. Также, существует спор, приемлемо ли включать предположение справедливости в модели распределенных систем. Было выдвинуто утверждение, что предположение справедливости не должны производиться, более того алгоритмы не должны разрабатываться с учетом этих предположений. Дискуссия по некоторым запутанным вопросам, относящимся к предположению справедливости может быть найдена в [Fra86].
2.2 Доказательство свойств систем перехода
Рассматривая распределенный алгоритм для некоторой проблемы, необходимо
продемонстрировать, что алгоритм есть корректное решение этой проблемы.
Проблема указывает, какие свойства требуемый алгоритм должен иметь; должно
быть показано, что решение обладает этими свойства. Вопрос проверки
распределенных алгоритмов получил значительное внимание и есть большое
количество статей, обсуждающих формальные методы проверки; см. [CM88,
Fra86, Kel76, MP88]. В этом разделе обсуждаются некоторые простые, но часто
используемые методы для демонстрации правильности распределенных
алгоритмов. Эти методы полагаются только на определение системы переходов.
Многие из требуемых свойств распределенных алгоритмов попадают в один из двух типов: требования безопасности и требования живости. Требования безопасности накладывают ограничение, что определенное свойство должно выполняться для каждого исполнения системы в каждой конфигурации, достигаемой в этом исполнении. Требования живости определяют, что определенное свойство должно выполняться для каждого исполнения системы в некоторых конфигурациях, достигаемых в этом исполнении. Эти требования могут также встречаться в ослабленной форме, например, они могут удовлетворяться с некоторой фиксированной вероятностью над множеством возможных исполнений. Другие требования к алгоритмам могут включать ограничения, которые основываются только на использовании некоторого данного знания (см. подраздел 2.4.4), что они гибки по отношен ию к нарушениям в некоторых процессах (см. часть 3), что процессы равны (см. главу 9), и т.д.
Методы проверки, описанные в этом разделе, базируются на истинности утверждений в конфигурациях, достигаемых в исполнении. Такие методы называются методами проверки утверждений. Утверждение это унарное отношение на множестве конфигураций, то есть, предикат, который принимает значение истина на одном подмножестве конфигураций и ложь – на другом.
2.2.1 Свойства безопасности
Свойство безопасности алгоритма это свойство в форме «Утверждение P истина в каждой конфигурации каждого исполнения алгоритма». Неформально это формулируется как «Утверждение Р всегда истина». Основной метод для того, чтобы показать, что утверждение Р всегда истина, это продемонстрировать, что Р инвариант согласно следующим определениям. Нотация P((), где ( это конфигурация, есть булево выражение, чье значение истина, если Р выполняется в (, и ложь в противном случае.
Определения зависят от данной системы переходов S = (C, (, I). Далее, мы будем писать {P} ( {Q}, чтобы обозначить, что для каждого перехода ( ( (
(системы S), если Р(() то Q((). Таким образом {P} ( {Q} означает, что, если
Р выполняется перед любым переходом, то Q выполняется после этого перехода.
Определение 2.9 Утверждение Р инвариант системы S, если
1) для всех ( ( I, и
2) {P} ( {P}.
Определение говорит, что инвариант выполняется в каждой начальной конфигурации, и сохраняется при каждом переходе. Из этого следует, что он сохраняется в каждой достигаемой конфигурации, как и формулируется в следующем теореме.
Теорема 2.10 Если Р это инвариант системы S, то Р выполняется для каждой конфигурации каждого исполнения системы S.
Доказательство. Пусть Е = ((0, (1, (2, ...) исполнение системы S. Будет показано по индукции, что Р((i) выполняется для каждого i. Во-первых, Р((0) выполняется, потому что (0 ( I и по первому предложению определения 2.9. Во- вторых, предположим P((i ) выполняется и (i ( (i+1 есть переход, который встречается в E. По второму предложению определения 2.9 P((i+1) выполняется, что и завершает доказательство. (
И наоборот, утверждение, которое выполняется в каждой конфигурации каждого исполнения, есть инвариант (см. упражнение 2.2). Отсюда не каждое свойство безопасности может быть доказано применением теоремы 2.10. В этом случае, однако, каждое утверждение, которое всегда истинно, включено в инвариант; отсюда может быть показано, применением следующей теоремы, что утверждение всегда истинно. (Нужно помнить, однако, что часто очень трудно найти подходящий инвариант Q, к которому можно применить теорему.)
Теорема 2.11 Пусть Q будет инвариантом системы S и положим Q ( P (для каждого ( ( С). Тогда Р выполняется в каждой конфигурации каждого исполнения системы S.
Доказательство. По теореме 2.10, Q выполняется в каждой конфигурации, и так как Q включает P, то P выполняется в каждой конфигурации также. (
Иногда полезно доказать сначала слабый инвариант, и впоследствии использовать его для доказательства более сильного инварианта. Как можно сделать инвариант более сильным демонстрируется в следующем определении и теореме.
Определение 2.12 Пусть S будет системой переходов и P, Q будут утверждениями. Р называется Q-производным, если
1) для всех ( ( I, Q(() ( Р((); и
2) {Q ( Р} ( {Q ( Р}.
Теорема 2.13 Если Q есть инвариант и Р – Q-производное, то Q ( P есть инвариант.
Доказательство. Согласно определению 2.9, должно быть показано, что
1) для всех ( ( I, Q(() ( Р((); и
2) {Q ( Р} ( {Q ( Р}.
Рекомендуем скачать другие рефераты по теме: педагогические рефераты, реферат машини.
Предыдущая страница реферата | 11 12 13 14 15 16 17 18 19 20 21 | Следующая страница реферата