Главная » Все файлы » Просмотр файлов из архивов » Документы » 2016 Алгоритм возвращения кредита_ инвариант и корректность (подробное решение)

2016 Алгоритм возвращения кредита_ инвариант и корректность (подробное решение)

Документ 2016 Алгоритм возвращения кредита_ инвариант и корректность (подробное решение), который располагается в категории "курсовые/домашние работы" в предмете "распределённые алгоритмы и системы (захаров)" издесятого семестра. 2016 Алгоритм возвращения кредита_ инвариант и корректность (подробное решение) - СтудИзба 2020-08-25 СтудИзба

Описание файла

Документ из архива "2016 Алгоритм возвращения кредита_ инвариант и корректность (подробное решение)", который расположен в категории "курсовые/домашние работы". Всё это находится в предмете "распределённые алгоритмы и системы (захаров)" из десятого семестра, которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .

Онлайн просмотр документа "2016 Алгоритм возвращения кредита_ инвариант и корректность (подробное решение)"

Текст из документа "2016 Алгоритм возвращения кредита_ инвариант и корректность (подробное решение)"

Распределенные алгоритмы.

Домашнее задание



Выполнили: Гуськов Дмитрий, Запутляев Иван, Савков Борис,

521 группа





Теорема:

Алгоритм возвращения кредита является корректным алгоритмом обнаружения завершения вычислений.



Доказательство:

1. С учетом правил П15 и утверждений S1-S3, утверждение является инвариантом алгоритма возвращения кредита, где:

Алгоритм завершается (то есть завершение вычислений будет обнаружено) при ret=1. Это значит, что предикат term( )=True, где – заключительная конфигурация, в которой не может произойти ни одного базового события.



2. Обоснование корректности инварианта:

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

2) Рассмотрим состояние системы в этот момент:

  • По определению предиката term все процессы p находятся в состоянии passive, а значит, в силу утверждения S3, для всех процессов p: credp=0

  • По определению предиката term в каналах отсутствуют сообщения

  • По определению заключительной конфигурации в каналах отсутствуют сообщения

3) В итоге:

и завершение вычислений будет обнаружено.



Корректность инварианта обоснована. Теорема доказана.



Свежие статьи
Популярно сейчас