Изменения

Перейти к: навигация, поиск

Формализм распределённых систем

2206 байт добавлено, 17:49, 2 июня 2019
Задачи
== Задачи ==
=== Взаимное исключение ===
 
Почти как в [[Алгоритмы взаимного исключения|параллельных системах]]:
 
{{Определение
|definition=
Критическая секция $CS_i$ — это пара из двух событий: $Enter(CS_i), Exit(CS_i) \in E$ (вход и выход из критической секции), при этом $Enter(CS_i) < Exit(CS_i)$ (в частности, они выполняются в одном процессе) и для всех $i$ верно: $Exit(CS_i) \to Enter(CS_{i+1})$ (т.е. критические секции линейно упорядочены).
}}
 
Это требование ''корректности'' — что алгоритм ''не может допустить''.
Мы здесь нигде не пользовались словом "одновременно".
Более того, нам даже не требуется вводить отдельные события входа/выхода, достаточно уже имеющихся событий отправки/получения сообщений (т.к. в системе ничего кроме сообщений принципиально происходить не может).
 
Также можно вводить дополнительные требования прогресса (что алгоритм ''должен делать''), но мы это делаем неформально. Можно требовать (от более слабых к более строгим):
 
# Если "сейчас" ни один процесс в критической секции не находится, но кто-то "хочет" в неё попасть, то хотя бы один процесс рано или поздно туда попадёт.
# "Честность": если процесс хочет попасть в критическую секции, то он рано или поздно туда попадёт независимо от действий остальных (если они, конечно, секцию будут освобождать).
292
правки

Навигация