Algoritmo de Lamport

UFMG - Pós-graduação em Ciência da Computação - Programação Paralela

``Prova'' de exclusão mútua:
suponha a existência de uma computação em que dois sítios i e j estão em suas seções críticas simultâneamente;
sem perda de generalidade, suponhamos que (T_i:i) tenha prioridade sobre (T_j:j);
no momento da entrada de j em sua seção crítica,
- se j não tinha recebido este request, para entrar em sua seção crítica j teria recebido outra mensagem de i, com prioridade menor que (T_j:j), o que é impossível pois o meio de transmissão conserva a ordem de envio, e as mensagens enviadas por i recebem timestamps crescentes;
- se j já tinha recebido este request, para entrar em sua seção crítica j teria que tê-lo eliminado de sua fila, o que só aconteceria com a chegada do <release> correspondente, o que contradiz a hipótese de simultaneidade das seções críticas;
portanto esta computação não pode existir