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