Определение взаимной блокировки

Задача: есть процессы, они могут друг друга ждать (в этот момент они ничего не могут делать и не меняют своё внутреннее состояние). Мы хотим запустить алгоритм, который будет нам сообщать о появлении взаимных блокировок, когда процессы ждут друг друга по циклу. Практическое применение — поиск ошибок в программах (динамические анализаторы распределённого кода, базы данных и SQL-запросы).

Алгоритм централизированный: есть выделенный координатор.

Каждый процесс [math]P_i[/math] поддерживает свою часть графа ожидания (ребра, которые из него исходят), а также флажок changed, который равен true, если его часть графа поменялась с последнего сообщения координатору. Координатор периодически опрашивает процессы, получая их графы. Процесс отвечает новым графом, если было изменение (даже если сейчас граф снова совпадает с тем, что был послан, во избежание ABA), а иначе шлет notChanged. Координатор собирает весь граф ожидания. Если в нем есть цикл, он отправляет процессам запрос на изменение. Если все процессы в цикле ответили notChanged, взаимная блокировка найдена.

Здесь мы пользуемся тем, что "процессы находятся во взаимной блокировке" — локально стабильный предикат и процесс в ожидании ничего не делает.

Рассмотрим два среза:

• когда взаимно блокирующие процессы прислали координатору свои графы;
• когда они прислали ему notChanged.

Эти срезы не обязательно согласованны, но они барьерно-синхронизированы (из-за сообщений координатору и обратно), а значит образуют согласованный интервал. Поэтому между ними есть согласованный срез [math]G[/math], а так как состояние процессов в цикле не менялось на всем интервале, и в первом срезе предикат выполнен, для [math]G[/math] он также выполнен.