algorithms – PetersonNP, mechanical mutual exclusion proof

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” from Nancy Lynch. I find it more convincing because lemmata required for proving it are exposed (others 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.4) are spelled out in page 287 of the book.

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

I’ve been able to mechanically prove the first lemma ( 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=jland c'pc_p=CS)

comp(p, c, j)=
    winner(p, c, j) lor (c'i_p=jland c'pc_pin{cf, ct}) =
        (c'i_p>j) lor (c'i_p=jland c'pc_p=CS) lor (c'i_p=jland c'pc_pin{cf, ct})

What i tried so far:

Lemma states: “if process p is a competitor at level j, if pc_p=check-flag, and if any process qneq 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 very long due the plenty many case analysis it takes).

Lemma10.5.3.1(c)=forall p,q,j.
        comp(p, c, j)land c'pc_p=cf land (comp(q, c, j)land qneq pland qin c'S(p) )
        Rightarrow c'turn(j)neq p

The problem:

I’m facing difficulties in proving 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 states: “if process p is a winner at level k and if any other process is a competitor at level k, then turn(j)neq p.”

Up to now i tried:

forall p,q,j.big( winner(p, c, j) land comp(q, c, j) land pneq q big) Rightarrow c'turn(j)neq p

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

I then tried to move the quantificator on q inside:

forall p,j.big( winner(p, c, j) land forall q.(comp(q, c, j) land pneq 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 pneq 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.

UPDATE regarding

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

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, cz, j)land comp(q, cz, j)Rightarrow(cz'turn(j)=poocz'turn(j)=q)

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

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

Thanks in advance,