What is a counterexample for Lamport's distributed mutual exclusion algorithm with non-FIFO message queues?

Question

Lamport's distributed mutual exclusion algorithm (also described here) solves mutual exclusion problem for $N$ processes with $3(N-1)$ messages per request ("take and release lock" cycle).

It requires that for each pair of processes $P$ and $Q$ all messages send by $P$ to $Q$ are received and processed by $Q$ in the same order. E.g. if $P$ sends messages $m_1$ and $m_2$ in that order, $Q$ cannot receive $m_2$ before receiving $m_1$.

I would like to see how it breaks if I remove that First-In-First-Out condition and allow reordering. The only counterexample I was able to built uses two processes who want to acquire the shared resource:

1. $P$ starts with clock 10 and sends request $m_1$ to $Q$
2. $Q$ starts with clock 1 and sends request $m_2$ to $P$
3. $Q$ receives request $m_1$ with timestamp 10 and sends acknowledge message $m_3$ to $P$
4. $P$ receives message $m_3$ before $m_2$ and enters critical section. As far as $P$ is concerned, it's the only process wanting the resource
5. $P$ receives message $m_2$ and responds to $Q$ with acknowledge
6. $Q$ enter critical section as $Q$'s request has timestamp 1 and $P$'s request has timestamp 10, so $Q$ has priority

However, that requires $P$ to respond to $Q$'s request $m_2$ while in critical section. Otherwise, $Q$ will receive acknowledgment when $P$ is no longer in critical section and there will be no conflict.

Question being: how to construct a counterexample where processes do not respond to external messages while in critical section?

Answer 1

Looks like this modification is correct. Proof is similar to proof of Lamport algorithm and follows.

Consider two processes $P_i$ and $P_k$ who entered critical sections at moments $e$ and $f$, correspondingly, requested them at moments $e'$ and $f'$, and exited at moments $e''$ and $f''$.

At moment $e$ process $P_i$ have received a confirmation from $P_k$. Suppose it was sent by $P_k$ at moment $g \to e$.

Case 1: $g < f'$. In that case, process $P_k$ has both itself and $P_i$ in queue, and $P_k$'s ticket is greater than $P_i$'s (because we use logical clock as tickets). So process $P_k$ cannot enter the critical section until it receives a release from $P_i$, and we have a correct mutual exclusion.

Case 2: $f' < f < f'' < g$. In that case, $f'' \to g \to e$, and we have a correct mutual correct mutual exclusion.

Case 3: $f' < f < g < f''$. That case is impossible as $P_k$ have sent a confirmation while in critical section.

Case 4: $f' < g < f < f''$. In that case, process $P_k$ should've received a confirmation from process $P_i$ by $f$. Suppose it was sent by $P_i$ at moment $h$. If $h > e$, then $h > e''$ and we have a correct mutual exclusion ($e'' \to h \to f$). Otherwise, $h < e$, so process $P_i$ learns about $P_k$'s wish before entering the critical section. Similarly, as $g < f$, $P_k$ learns about $P_i$'s wish before entering the critical section. But only one of them has lower priority, hence, their critical sections happen in order.