292
правки
Изменения
Нет описания правки
Корректность гарантируется при помощи FIFO и ok: если $P$ получил ok от процесса $Q$, то запрос от $Q$ на вход в критическую секцию уже тоже получен.
Также гарантируется отсутствие блокировок: если стабилизировалось множество процессов, желающих получить блокировку, то рано или поздно все сообщения доедут, а тогда у всех станут одинаковые очереди (тут стоит аккуратно говорить, почему), и тогда кто-нибудь обязательно станет в очереди первым.
Отсутствие голоданий тоже гарантируется: если процесс хочет получить блокировку, то он рассылает всем сообщения. Процессы, которые захотят блокировку после получения такого сообщения, получат больший номер. То есть нам максимум придётся ждать блокировок, которые возникли до того, как каждый процесс получил наше сообщение.
== Доказательство ==
