Предыдущая страница реферата | 12  13  14  15  16  17  18  19  20  21  22 | Следующая страница реферата

Т.к. Q это инвариант, Q(() выполняется для всех ( ( I, и т.к. для всех
( ( I, Q(() ( Р((), P(() выполняется для всех ( ( I. Следовательно, Q(() (
P(() выполняется для всех ( ( I.

Предположим ( ( ( и Q(() ( Р((). Т.к. Q это инвариант, Q(() выполняется, и т.к. {Q ( P} ( {Q ( Р}, Q(() ( Р((), откуда Р(() вытекает.
Следовательно, Q(() ( Р(() выполняется. (

Примеры доказательства безопасности, основывающиеся на материале данного раздела, представлены в разделе 3.1.

2.2.2 Свойства живости

Свойство живости алгоритма это свойство в форме «Утверждение Р истина в некоторой конфигурации каждого исполнения алгоритма». Неформально это формулируется как «Утверждение Р в конечном счете истина». Основные методы, используемые, чтобы показать, что Р в конце концов истина – это нормирующие функции и беступиковость (или правильное завершение). Более простой метод может быть использован для алгоритмов, в которых разрешаются только исполнения с фиксированной, конечной длиной.

Пусть S будет системой переходов и Р – предикат. Определим term как предикат, который истина во всех терминальных конфигурациях и ложь во всех нетерминальных конфигурациях. Мы сначала предположим ситуации, где исполнение достигает терминальной конфигурации. Обычно нежелательно, чтобы такая конфигурация достигалась, в то время, как «цель» Р не была достигнута. Говорят, что в этом случае имеет место тупик. С другой стороны, завершение позволено, если цель была достигнута, в этом случае говорят о правильном завершении.

Определение 2.14 Система S завершается правильно (или без тупиков), если предикат (term ( Р) всегда истинен в системе S.

Нормирующие функции полагаются га математическое понятие обоснованных множеств. Это множество с порядком w3 ... .

Примеры обоснованных множеств, которые будут использоваться в этой книге – это натуральные числа с обычным порядком, и n-кортежи натуральных чисел с лексикографическим порядком (см. раздел 4.3). Свойство, что обоснованное множество не имеет бесконечной убывающей последовательности, может использоваться, чтобы показать, что утверждение Р в конечном счете истина. К этому моменту должно быть показано, что существует функция f из
C в обоснованное множество W такая, что в каждом переходе значение f убывает или Р становится истиной.

Определение 2.16 Пусть даны система переходов S и утверждение Р.
Функция f из С в обоснованное множество W называется нормирующей функцией
(по отношению к Р), если для каждого перехода ( ( ( , f(() > f(() или
Р(().

Теорема 2.17 Пусть даны система переходов S и утверждение Р. Если S завершается правильно и нормирующая функция f (w.r.t Р) существует, то Р – истина в некоторой конфигурации каждого исполнения системы S.

Доказательство. Пусть Е = ((0, (1, (3, ...) – исполнение системы S.
Если Е конечно, его последняя конфигурация является терминальной, и т.к. term ( Р всегда истина в системе S, то Р выполняется в этой конфигурации.
Если Е бесконечно, пусть E’ будет самым длинным префиксом Е, который не содержит конфигураций, в которых Р истина, и пусть s будет последовательностью (f((0 ), f((1), ...) для всех конфигураций (i, которые появляются в Е’. В зависимости от выбора Е’ и свойства f, s может быть убывающей последовательностью, и отсюда, по обоснованности W, s конечна.
Это подразумевает также, что Е’ – конечный префикс ((0, (1, ..., (k ) исполнения Е. В зависимости от выбора Е’, Р((k+1) выполняется. (

Если приняты свойства справедливости, то можно заключить из более слабых посылок (чем в теореме 2.17), что Р в конце концов станет истиной.
Значение нормирующей функции не должно уменьшаться при каждом переходе.
Предположение справедливости может быть использовано, чтобы показать, что бесконечные исполнения содержат переходы определенного типа бесконечно часто. Затем будет достаточно показать, что f никогда не увеличивается, а уменьшается с каждым переходом этого типа.

В некоторых случаях мы будем использовать следующий результат, который есть специальный случай теоремы 2.17

Теорема 2.18 Если S завершается правильно и есть число К такое, что каждое исполнение содержит по крайней мере К переходов, то Р истина в некоторой конфигурации каждого исполнения.

Рис. 2.1 Пример пространственно-временной диаграммы

2.3 Каузальный порядок событий и логические часы

Взгляд на исполнения как последовательности переходов естественным образом порождает понятие времени в исполнениях. Говорят, что переход а появляется раньше перехода b, если a встречается в последовательности перед b. Для исполнения Е = ((0, (1, ...) определим ассоциированную последовательность событий Е’=(е0, е1, ...), где еi – это событие, при котором конфигурация изменяется из (i в (i+1. Заметьте, что каждое исполнение определяет уникальную последовательность событий этим путем.
Исполнение может быть визуализировано в пространственно-временной диаграмме, рисунок 2.1, которой, представляет пример. В такой диаграмме, горизонтальная линия нарисована для каждого процесса, и каждое событие нарисовано точкой на линии процесса, где оно имеет место. Если сообщение m послано при событии s и получено при событии r, стрелка рисуется от s к r.
Говорят, что события s и r соответственные в этом случае.

Как мы увидим в подразделе 2.3.1, события распределенного исполнения могут иногда быть взаимно обменены без воздействия на последующие конфигурации исполнения. Поэтому понятие времени как абсолютного порядка на событиях исполнения не приемлемо для распределенных исполнений, и вместо этого представляется понятие каузальной зависимости. Эквивалентность исполнений при переупорядочивании событий изучается в подразделе 2.3.2. Мы обсуждаем в подразделе 2.3.3 как могут быть определены часы для измерения каузальной зависимости (а не времени), и представляем логические часы
Лампорта, важный пример таких часов.

2.3.1 Независимость и зависимость событий

Уже было замечено, что переходы распределенной системы влияют, и подвержены влиянию, только на часть конфигураций. Это ведет к тому наблюдению, что два последовательных события, влияя на разделенные части конфигурации, независимы и могут также появляться в обратном порядке. Для систем с асинхронной передачей сообщений, это выражается в следующей теореме.

Теорема 2.19 Пусть ( будет конфигурацией распределенной системы (с асинхронной передачей сообщений) и пусть ер и еq будут событиями различных процессов р и q, применимых в (. Тогда ер применимо в еq((), еq применимо в ер((), и ер(еq(()) = еq(ер(()).

Доказательство. Чтобы избежать анализа случаев, которые есть посылка, получение, или внутренние события, мы представим каждое событие однородной нотацией (с, х, у, d). Здесь с и d обозначают состояние процесса до и после события, х – набор сообщений, полученных во время события, и у – набор сообщений, посланных во течение события. Таким образом, внутренне событие
(с, d) обозначается как (c,(,(,d), событие отправки (с, m, d) обозначается как (с, (, {m}, d), и событие приема (с, m, d) – (c, {m}, (, d). В этой нотации, событие е = (с, x, y, d) процесса p применимо в конфигурации ( =
(Сp1, ..., Cp, ..., СрN, M), если ср = с и x ( M. В этом случае е(() = (Сp1, ..., d, ..., (M x) ( у).

Теперь предположим ер = (bp, xр, ур, dp) и еq = (bq, xq, уq, dq) применимы в

. = (..., ср, ..., сq, ..., M),

Рекомендуем скачать другие рефераты по теме: педагогические рефераты, реферат машини.





Предыдущая страница реферата | 12  13  14  15  16  17  18  19  20  21  22 | Следующая страница реферата