Exactly generic N elements in HOL

[Alberto Ercolani]

Good evening everyone,

i've been stuck on this for quite some time now so i'm seeking help here.

I'm currently trying to prove the Filterlock correct (mutual exclusion) and the pencil and paper proof goes by induction.

(

Filterlock is shown at page 9.

http://www.cs.tau.ac.il/~shanir/multiprocessor-synch-2003/mutex/notes/mutex2.pdf

)

The theorem i'm trying to prove is the following:

Statement(c:State) : bool =

FORALL (j:nat) : 0<=j AND j<=THREADS-1 => card( c'execs(j) ) <= THREADS-j

inv_filter_card : LEMMA

invariant(conc_aut, Statement)

"invariant(.,.)" is an inductive definition allowing me to carry out proofs by induction over reachable states, so i can evaluate the statement on each transition in my LTS (input/output automaton) and show it is preserved.

Only one case is left to be proved, the one were the set of processes moves and a generic executor enters the next level.

My problem is in bridging the proof (that apparently everybody employ to see Filterlock is correct) to PVS.

The inductive step is carried out by contraddiction and states: "suppose there are n-j+1" processes at level j, then..." and a contraddiction is reached. Therefore at most n-j processes can be at level j and the conclusion comes.

I've got no idea how to state there are generic N processes to show the transition for some of them can not occur (i know how to show it can not). If N was constant, i would simply unfold the predicate, generic N is behind my knowledge of HOL.

All help is appreciated, thanks!

Alberto Ercolani

[Tanner Slagel]

Alberto,

Very interesting problem. I am not familiar with Filterlock or the particular result you are trying to show (besides briefly looking at your link), but let me see if I can help at all.

"I've got no idea how to state there are generic N processes to show the transition for some of them can not occur (i know how to show it can not). If N was constant, i would simply unfold the predicate, generic N is behind my knowledge of HOL."

It seems like you want the property that if, for a set A and natural number n,  card(A) >= n  means you can generate at least n different elements of the set A. Then you will take these n elements and show there is a contradiction. I am thinking this can be done by creating a bijections from below(n) to A. There are a couple lemmas in the prelude file that can help with this:

card_bij : THEOREM card(S) = N

IFF (EXISTS (f: [(S) -> below[N]]): bijective?(f))

card_bij_inv : THEOREM card(S) = N

IFF (EXISTS (f: [below[N] -> (S)]): bijective?(f))

with a bijection like this. You can talk about f(i) for each i:below(n) as a transition, and have the fact that f(i) \neq f(j) for I \neq j. Also there is a k:below(n) for each entry of S such that f(k) is that particular entry 

Feel free to follow up, hope this helps.

sincerely,

Tanner Slagel

[Alberto Ercolani]

Hello Tanner, thanks for replying.

The idea of showing the presence of a bijection is very interesting, however i think i will suspend the task of proving the FilterLock correct.

I slightly cheated and forced PVS to reason about the existence of other processes in the next level through the commented lemma "card_n_has_n" that is close

to the ones you mentioned. Then i forced PVS to use the identity function to map the ids of other processes.

Eventually, i found myself unable to show the contraddiction, i expected an intuitive invariant to hold (the model checker agrees) but i'm currently unable to prove it in PVS.

Regards,

Alberto Ercolani

[Alberto Ercolani]

Good day, Tanner i have some news.

It looks like i was too hasty, i was able to prove 2 of the 3 conjuncts leading to a contraddiction, one is still missing.

Since the theorem requires a contraddiction stemming from "card(j+1)>=n-j-1", can you tell me what is the proper way to show that function X:[below(N)->T] is

an identity? I used card_n_has_n lemma and my intuition is that since function X exists i can choose what it is, however in PVS i need to skolemize it so i would like to see whats the proper way to do so.

Regards,

Alberto Ercolani

[Tanner Slagel]

Alberto,

Okay nice, "card_n_has_n" seems to give essentially the same thing that I was looking for with the bijection lemmas I sent you. 

"the proper way to show that function X:[below(N)->T] is n identity" Do you mean that X(i) = i for each I:below(N)? In this case we would be assuming that T is below(n) here. Am I confusing something here? 

" I used card_n_has_n lemma and my intuition is that since function X exists i can choose what it is, however in PVS i need to skolemize it so i would like to see whats the proper way to do so."

I am thinking when you use the "card_n_has_n" lemma, you get the existential statement about X in the antecedent? This does not give you the power to call a specific X of your choosing, only to skolemize.  (You can instantiate on universal quantifiers in the antecedent, and existential quantifiers in the consequent). This makes sense because If X exists, there is not a good reason (unless you can prove it) that the X is the specific one you are thinking of. 

Now if you want to get your specific X, I would suggest naming it.  (name  "X" "<lambda expression>"). For example (name "X" "LAMBDA(n:nat): n") will give you. X = LAMDA(n:nat): n in the antecedent. Then you need to show that this X has the property you desire. You could show this with a case (case "NOT  P(X)") where P is the predicate, this will split your proof into two branches: one you will have to prove P(X), then the other you will have P(X) in the antecedent.   For example (case "bij?(X)") would split my proof into a branch where I had to show X is a bijection, then the other branch I would have that it is a bijection. 

Let me know if any clarification is needed here! I  hope you are having a good day! 

sincerely,

Tanner 

[Alberto Ercolani]

Hello Tanner,

no, you are not mistaken: assuming that T is below(N) seems realistic to me since every process has a unique id from 0 to N-1 therefore below(N).

" This makes sense because If X exists, there is not a good reason (unless you can prove it) that the X is the specific one you are thinking of.  "

That's a good point! I was seeing it the other way round.

Ok, i see your point, good idea the one to use the "name" strategy. I will give it a shot when i'll be done proving the last contraddiction.

See you soon,

Alberto

[Tanner Slagel]

Alberto,

Sounds great - feel free to follow up, this is an interesting problem!

sincerely,

Tanner

[Alberto Ercolani]

Good day Tanner, the last contraddiction is still lagging behind. I've been thinking about this for weeks now and i came to the conclusion it takes something more to conclude the theorem holds. I've been able to find different proofs and only one of them is convincing me. The one found in the book "Distributed Algorithms" by Nancy Lynch, pg. 287.

The proof Lynch gives states that if all processes from level j made it to level j+1 then none of them found to be the victim; but victim must be set to some of their IDs, that's a contraddiction and the branch is discharged. The key problem is having a lemma stating that victim must be some processes that lost the competition for the next level. In my opinion, this is far simpler to see correct than other approaches still i'm having troubles in replicating her approach.

Nancy Lynch provides 2 lemmata, one stating the role of winners and loser, the other that victim is always some loser.

I'm doubful my formalization of the first theorem is correct because using her model i reach at least an unprovable branch.

I wold like to focus on the first one only and i would like a suggestion from somebody more experienced than me.

How would you formalize the following two predicates?

Let's assume:

- P(.) is the predicate we want to prove,

- invariant(P(.)) is an inductive predicate for reachability over the automaton,

- winner(i,c,k) formalizes the winner process i in state c at level k,

- comp(j,c,k) formalizes the competitor process j in state c at level k.

My attempts so far lead to this:

- winner(i:below(N), c:state, k:nat) : bool = c`level(i)>k OR ( c`level(i)=k AND c`pc(i)=CS )

- comp(i:below(N), c:state, k:nat) : bool = winner(i, c, k) OR ( c`level(i)=k AND ( c`pc(i)=check_flag OR c`pc(i)=check_turn ) )

(Winner and comp defs. are given in the book so i simply reported them in PVS.)

WinnerIsNotVictim(c:state) : bool =
%1

  FORALL i, j, (k:nat) : ( comp(i, c, k) AND c`pc(i)=check_flag AND comp(j, c, k) AND member(j, c`S(i)) AND i/=j ) IMPLIES c`turn(k)/=i

AND

%2

  FORALL i, j, (k:nat) : ( winner(i, c, k) AND comp(j, c, k) AND i/=j ) IMPLIES c`turn(k)/=i

inv_turn : LEMMA
  invariant(ioa_inst, WinnerIsNotVictim)

I strongly suspect this formalization is incorrect, but i can't figure out the right one... I'm open to suggestions.

Regards,

Alberto

PS: in my opinion 1 and 2 should be proved together otherwise the inductive hypothesis ceases to hold, for instance when trying to prove 1 alone and level=k before the level++ transition.

[Tanner Slagel]

Alberto,

Is this post still a relevant problem you are doing with? If so I am happy to look it over and try to help! 

sincerely,

Tanner

[Alberto Ercolani]

Hello Tanner,

it has been many months since I successfully completed the formalization and proved the Filter-Lock satisfies mutual exclusion, consequently this post is not relevant to me any longer.
Despite my formalization being somewhat rudimentary I could prove the result I was interested in, the whole formalization is available here: `https://github.com/AlbertoErcolani/FilterLock-final`.

I would like to thank you again, because the suggestion to employ bijections was central.

Best regards,

Alberto

[Tanner Slagel]

Alberto,

I am glad to hear the formalization worked out! Feel free to reach out with any future work in PVS, I enjoyed our discussion. 

sincerely,

Tanner