302
правки
Изменения
→Алгоритмы взаимного исключения
===Корректность алгоритма===
=====Взаимное исключение=====
Потоки <tex>0</tex> и <tex>1</tex> никогда не могут попасть в критическую секцию в один момент времени: если <tex>0</tex> вошёл в секцию, он установил <tex>want[0]</tex> в <tex>true</tex>. Тогда либо <tex>want[1] == false</tex> (тогда поток <tex>1</tex> не в критической секции), либо <tex>waiting == 1</tex> (тогда поток <tex>1</tex> пытается войти в критическую секцию и крутится в цикле), либо поток <tex>1</tex> пытается войти в критическую секцию после установки <tex>want[1] == true</tex>, но до установки <tex>waiting</tex> и цикла. Таким образом, если оба процесса находятся в критической секции, должно быть <tex>want[0] && and want[1] && and waiting == 0 && and waiting == 1</tex>, но такого не может быть одновременно и мы пришли к противоречию.
=====Свобода от взаимной блокировки=====
Для того, чтобы оба процесса находились в ожидании, необходимы противоположные значения переменной <tex>waiting</tex>, что невозможно.