What is a counterexample for Lamport's distributed mutual exclusion algorithm with non-FIFO message queues?
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 &lt; 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' &lt; f &lt; f'' &lt; g$. In that case, $f'' \to g \to e$, and we have a correct mutual correct mutual exclusion.

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

Case 4: $f' &lt; g &lt; f &lt; 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 &gt; e$, then $h &gt; e''$ and we have a correct mutual exclusion ($e'' 
\to h \to f$). Otherwise, $h &lt; e$, so process $P_i$ learns about $P_k$'s wish before entering the critical section. Similarly, as $g &lt; 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.