PetersonNP, mechanical mutual exclusion proof

Question

Good day everyone, I'm currently trying to carry out the PetersonNP (a.k.a. FilterLock) correctness proof (mutual exclusion). I've found several proof sketches on concurrency books but I'm interested in the one shown in Distributed Algorithms (by Nancy Lynch). I find it more convincing because lemmata required for proving it are exposed (other authors provide an intuitive approach but I need more details).

The lemma implying mutual exclusion (Assertion 10.5.5) and the three lemmata for proving it (10.5.3.1, 10.5.3.2, 10.5.4) are spelled out on pg. 287.

I want to focus on 10.5.3.* and 10.5.4 first and consider 10.5.5 only when the others are proved.

I've been able to mechanically prove the first lemma (10.5.3.1). I carry out my proofs by hand employing sequent calculus and once I'm convinced they are correct I check them by PVS. I checked, so I'm confident the first one is correct.

I report the key concepts involved in all three proofs, as they are explained in the book:

$winner(p, c, j) = (c'i_p>j) \lor (c'i_p=j\land c'pc_p=CS)$

$comp(p, c, j)=\\ winner(p, c, j) \lor (c'i_p=j\land c'pc_p\in\{cf, ct\}) =\\ (c'i_p>j) \lor (c'i_p=j\land c'pc_p=CS) \lor (c'i_p=j\land c'pc_p\in\{cf, ct\})$

What i tried so far:

Lemma 10.5.3.1 states: "if process p is a competitor at level j, if $pc_p=check\text{-}flag$, and if any process $q\neq p$ in $S_p$ is a competitor at level j, then $turn(j)\neq p$."

I formalized the theorem as follows and proved it correct (the proof is not difficult but it is very long due the plenty many case analyses).

$Lemma10.5.3.1(c)=\forall p,q,j.\big(comp(p, c, j)\land c'pc_p=cf \land (comp(q, c, j)\land q\neq p\land q\in c'S(p) )\big)\Rightarrow c'turn(j)\neq p$

% PROVED.

The problem:

I'm facing difficulties in proving 10.5.3.2 and 10.5.4 because, in first place, I'm not sure about how they should be stated in first-order logic (more details to come).

Lemma 10.5.3.2 states: "if process p is a winner at level k and if any other process is a competitor at level k, then $turn(k)\neq p$."

Up to now i tried:

First formalization attempt: $\forall p,q,j.\big( winner(p, c, j) \land comp(q, c, j) \land p\neq q \big) \Rightarrow c'turn(j)\neq p$

however the inductive hypothesis fails to hold in a few cases and Lemma 10.5.3.1 does not apply, so I suspect it to be incorrect.

I then tried to move the quantificator on q inside:

Second formalization attempt: $\forall p,j .\big( winner(p, c, j) \land \forall q.(comp(q, c, j) \land p\neq q) \big) \Rightarrow c'turn(j)\neq p$

this lemma is provable. It suffices to skolemize $p$ and $j$ and when instantiating $q=p$ the constraint $p\neq q$ becomes unsatisfiable, causing the proof to end. This alternative formalization puzzles me because I don't see how to use the innermost forall when this lemma has to be applied.

As Kay correctly pointed out, my second formalization is incorrect, and as I stated more than one year ago, the correct formalization is the first one.

UPDATE regarding 10.5.3.2:

On page 292 (in the context of a different argument) Nancy Lynch points out that Lemma 10.5.3.2 can not be proved by induction, as it is. It must be strengthened, but I don't get how to do that.

UPDATE regarding 10.5.3.2: The proof can be completed by induction, provided supporting lemmata are identified and employed. No change to the statement is required, neither in words nor in the formal setting.

Eventually, Lemma 10.5.4 states: "if there is a competitor at level j, then the value of the turn(j) is the index of some competitor at level j."

I tried the following formalization:

$\forall p,q,j.comp(p, c, j)\land comp(q, c, j)\Rightarrow(c'turn(j)=p\lor c'turn(j)=q)$

but I get an unprovable case when both processes $p$ and $q$ are stopped, so I suspect this formalization is incorrect.

UPDATE regarding 10.5.4 The lemma has been proved and the proper formalization has been added in the response.

Could someone suggest me the proper formalization? Or how to strengthen the statement of Lemma 10.5.3.2?

Thanks in advance,

Answer 1

I eventually found the solution for the first problem I proposed. Lemma 10.5.3.2 CAN be proved by induction, but it requires additional lemmata for doing so. I was misled by the note on page 292, specifically by the mention of "strengthening". It is common to say that a theorem is strengthened when its inductive hypothesis is rewritten to hold in every case of interest, still, there's no standard nomenclature. There's no need to rewrite Lemma 10.5.3.2 it suffices to notice that in those seemingly unprovable cases the role of process Q only leads to contradictions.

Observing that Q must be in a contradictory situation is not immediate, it takes several suppositions that together with more lemmata cause the proof to terminate.

Some lemmata are quite obvious, namely, $level_p=i_p \lor level_p=i_p-1$. Others are not immediate to prove, like $\vert S_p\vert=n-1 \Rightarrow Q=qq_p$ where $qq_p$ is the process observed by $p$. The core point is the following, finding supporting invariants is fairly easy when one knows they are necessary and sufficient.

Currently, Lemma 10.5.3.2 is proved.

UPDATE regarding 10.5.4:

Lemma 10.5.4 is proved. The proof again is not difficult, it requires the human prover to observe that a victim qualifying as a competitor only leads to contradictions. To do so, one has to use lemmata 10.5.3.1 and 10.5.3.2 in a single case where the inductive hypothesis ceases to work.

The formal statement is possibly the simplest among the three lemmata used to support mutual exclusion.

$\forall j. \exists p . comp(p, c, j) \Rightarrow comp(turn(j), c, j)$