2016 Алгоритм возвращения кредита_ инвариант и корректность (подробное решение)
Описание файла
Документ из архива "2016 Алгоритм возвращения кредита_ инвариант и корректность (подробное решение)", который расположен в категории "". Всё это находится в предмете "распределенные алгоритмы" из 10 семестр (2 семестр магистратуры), которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Онлайн просмотр документа "2016 Алгоритм возвращения кредита_ инвариант и корректность (подробное решение)"
Текст из документа "2016 Алгоритм возвращения кредита_ инвариант и корректность (подробное решение)"
Распределенные алгоритмы.
Домашнее задание
Выполнили: Гуськов Дмитрий, Запутляев Иван, Савков Борис,
521 группа
Теорема:
Алгоритм возвращения кредита является корректным алгоритмом обнаружения завершения вычислений.
Доказательство:
1. С учетом правил П1-П5 и утверждений S1-S3, утверждение является инвариантом алгоритма возвращения кредита, где:
Алгоритм завершается (то есть завершение вычислений будет обнаружено) при ret=1. Это значит, что предикат term( )=True, где – заключительная конфигурация, в которой не может произойти ни одного базового события.
2. Обоснование корректности инварианта:
1) После завершения вычисления не происходит ни одно базовое событие, следовательно возможен только прием инициатором сообщений . Сообщений конечное число, после приема каждого такого сообщения их общее количество уменьшается на единицу, поэтому достигается заключительная конфигурация.
2) Рассмотрим состояние системы в этот момент:
-
По определению предиката term все процессы p находятся в состоянии passive, а значит, в силу утверждения S3, для всех процессов p: credp=0
-
По определению предиката term в каналах отсутствуют сообщения
-
По определению заключительной конфигурации в каналах отсутствуют сообщения
3) В итоге:
и завершение вычислений будет обнаружено.
Корректность инварианта обоснована. Теорема доказана.