Correctness

The algorithm works correctly if it guarantees mutual exclusion, progress and starvation freedom. These properties are shown by the following lemmas.

Lemma 1

The algorithm guarantees mutual exclusion.

Proof.Let processes p and q be two arbitrary processes which share a resource. Assume that p and q were in their critical section at the same time.

In order to gain access to their critical section processes p and q send request messages to all their neighbours. In particular they send request messages to each other. Let t_p denote the local clock time when process p sends its request messages and let t_q denote the local clock time when process q sends its request messages. Due to the lexical order of time either t_p<t_q or t_p>t_q is valid.

If t_p<t_q is valid then p would delay replying the request message of process q until p finished accessing its critical section, this implies that t_p>t_q is valid. However, if t_p>t_q is valid q would delay replying the request message of p until q finished with accessing its critical section, thus leading to a contradiction that both processes were at the same time in the critical section. $\Box$
 
 

Lemma 2

The algorithm guarantees progress.

Proof.Assume there is a point in the execution in which some processes are hungry, and after this point no process can enter its critical section. Then the system will reach a state where no messages are sent any longer and no process changes its state. Let p be a process in hungry state with the smallest request time. All neighbours in thinking state must have answered the request messages of p with sending fork messages. As p is the process that sent its request messages with the smallest time tuple, also all processes in hungry state will send fork messages to p. Thus p will receive fork messages from all its neighbours and will change its state to hungry. This is a contradiction to the assumption that no progress happens. $\Box$
 
 

Lemma 3

Every process is able to access its critical section.

Proof.Receiving a request message makes the local clock of a process at least one unit greater than the time stamp of the request message. Therefore, a process which sends request messages to all its neighbours will loose at most one competition with each neighbour whilst it tries to access a resource. Assume some processes never manage to enter their critical section, then there must exist for these processes at least one neighbour which requested the shared resource before, and also cannot enter its critical section. Let $C:=p_0, p_1, \ldots,p_l$ be the longest chain of neighbouring processes (p_i, p_i+1) such that all those processes never manage to enter their critical section and p_i+1 prevents p_i from using its resource. Each process p_i requested the resources from its neighbours at local clock time t_i. Thus $t_0 \gt t_1 \gt \ldots \gt t_l$ must hold. All neighbours of p_l which requested earlier for their resource will succeed with entering their critical section since they are not part of C. Therefore, p_l will be able to enter its critical section because it will receive a fork message from all neighbours which sent their request messages earlier. Receiving all fork messages from neighbours that sent their messages later than p_l is guaranteed by the algorithm. This leads to a contradiction due to the assumption that p_l never manages to enter its critical section. $\Box$
 

11/16/1999