Доброго дня!

Дело в том, что алгоритм Лампорта взаимного исключения требует, чтобы каналы связи между сайтами (я буду использовать термин "сайт" как наиболее общий и отражающий того, кому нужно иметь доступ к разделяемому ресурсу, т.е. входить в "критическую секцию") имели свойство FIFO. В модификации я хочу ослабить это требование, т.е. заменить: каналы с FIFO -> каналы с неопределенной последовательностью доставки. С другой стороны, "усилить" требование к очереди запросов: очередь -> очередь с приоритетом. Меня интересует прежде всего, повлияет ли такая замена на корректность алгоритма и верно ли мое доказательство корректности модифицированного алгоритма.

Алгоритм Лампорта

- Запросы на вход в CS (critical section) исполняются по мере возрастания меток времени запросов и время определяется по логическим часам.
- Каждый сайт Si содержит очередь request_queue_i, которая содержит запросы взаимного исключения (доступ к CS), отсортированные по меткам времени.
- Алгоритм требует, чтобы каналы передачи сообщений между сайтами поддерживали свойство FIFO.

Модифицированный алгоритм Лампорта

- Запросы на вход в CS (critical section) исполняются по мере возрастания меток времени запросов и время определяется по логическим часам.
- Каждый сайт Si содержит очередь с приоритетом request_queue_i, которая содержит запросы взаимного исключения (доступ к CS), отсортированные по меткам времени (меньшая метка времени имеет больший приоритет).
- Алгоритм требует, чтобы каналы передачи сообщений между сайтами (последовательность доставки сообщений не определена).

Обзор модифицированного алгоритма

Запрос критической секции

- Когда сайт Si хочет войти в критическую секцию, он рассылает сообщение REQUEST(ts_i, i) всем остальным сайтам и помещает данный запрос в свою очередь запросов. ((ts_i, i) обозначает метку времени запроса)
- Когда сайт Sj получает запрос REQUEST(ts_i, i) от сайта Si, сайт Sj помещает его в свою очередь сообщений request_queue_j. Сайт Sj возвращает ответ REPLY с меткой времени на запрос от Si тогда и только тогда, когда запрос REQUEST(ts_i, i) попадает на вершину очереди request_queue_j. (В таком случае (ts_i, i) есть минимальная метка времени)

Работа в критической секции

Сайт Si входит в критическую секцию при выполнении двух условий:

L1: Si получил сообщения с подтверждением запроса на вход от всех сайтов, причем каждая из меток времени подтверждений больше чем (ts_i, i)
L2: Запрос Si находится на вершине очереди request_queue_i

Освобождение критической секции

- Сайт Si, до выхода из критической секции, удаляет запрос из очереди request_queue_i, и рассылает запрос RELEASE с меткой времени всем остальным сайтам.
- Когда сайт Sj получает запрос RELEASE от Si, то Sj удаляет запрос из очереди request_queue_j.

Доказательство справедливости 

От противного. Пусть Si и Sj хотят войти в CS и посылают запросы req(ts_i, i) и req(ts_j, j) об этом всем остальным сайтам при условии, что (ts_i, i) < (ts_j, j), т.е. сайт Si запросил вход в CS раньше (*), чем Sj. Пусть впоследствии сайт Sj получил доступ к CS прежде (**), чем сайт Si, т.е. для Sj были выполнены условия L1 и L2. 

Учитывая, что каналы передачи данных не имеют свойства FIFO, то примем, что L2 выполняется. Вне зависимости от количества сайтов, всегда будет как минимум один сайт Si, который не даст согласия сайту Sj на вход в CS на основании алгоритма и условия (*), т.е. на вершине очереди request_queue_i будет req(ts_i, i), а не req(ts_j, j), т.к. (ts_i, i) < (ts_j, j). Таким образом, L1 не выполняется, а значит предположение (**) не верно.

Заранее спасибо за комментарии и советы.

Присоединённый файл ( Кол-во скачиваний: 4 )
 LamportsAlgorithmWithNoFIFO.pdf 39,02 Kb