/* ********************************************************************************* * * T. D. Chandra and S. Toueg. * Time and message efficient reliable broadcasts. * In Proceedings of the 4th international workshop on Distributed algorithms, * pages 289-303, New York, NY, USA, 1991. * * * Protocol 2, SEND-OMISSION FAILURES - Lemmas as system axiom * * 1st round..................................transitions 1-6 * 1st --> 2nd round..........................transitions 7,8 * 2nd round..................................transitions 9-12 * 2nd --> 3rd round..........................transition 13 * 3rd round..................................transitions 14-18 * 3rd --> 4th round (check received nack)....transition 19 * 4th --> 5th round..........................transition 20 * 5th round..................................transitions 21-24 * 5th --> 6th round..........................transition 25 * 6th round (coordinator election)...........transition 26 * coord election after coord crash...........transition 27 * decided processes..........................transition 28 * * ********************************************************************************* */ /* Round of the execution */ global nat round [nat] /* estimate of the processes (true = m; false = undefined) */ local bool estimate [nat] /* state of the processes (true = decided; false = undecided) */ local bool state [nat] /* who's the coordinator */ local bool coord [nat] /* who has already been coordinator */ local bool aCoord [nat] /* processes that has done the operations of the round */ local bool done [nat] /* someone sent a request? */ global bool request [nat] /* decision value of the processes (as estimate)*/ local bool decisionValue [nat] /* the process is faulty (as defined in send omission failure model) */ local bool faulty [nat] /* the process has received the estimate from the coordinator */ local bool received [nat] /* if nack[x] = true, process x received a negative ack */ local bool nack [nat] /* id of the coordinator who sent me an estimate */ local int id [nat] /* id of the coordinator who sent the estimate saved in tmpEstimate */ global int maxId [nat] /* temp. var used to send the estimate to the coordinator */ global bool tmpEstimate [nat] /* used for the Lemma 2.2 of the paper */ local bool processReceivedEstimate [nat] /* optimization (available from 1.0.1 version of mcmt) */ key_search round; /* tells to mcmt to use at most 4 vars of sort INDEX in invariants verification */ (:mcmt :inv_search_max_index_var 4 :) /* constraints for numerical vars */ system_axiom (universal x:nat) { (round[x] < 8) AND ( (maxId[x] + 3) > 0) AND ( (id[x] + 2) > 0) } /* LEMMA 2.1 */ system_axiom (universal x:nat, universal y:nat, universal z:nat) { (NOT ( (state[x] = true) AND (received[x] = true) AND (coord[y] = true) AND (state[z] = false) AND (faulty[z]= false) AND (estimate[y] != estimate[z]) AND (x != y) AND (y != z) AND (z != x) )) } /* LEMMA 2.2 */ system_axiom (universal x:nat, universal y:nat) { (NOT ( (round[x] > 1) AND (state[x] = false) AND (faulty[x] = false) AND (processReceivedEstimate[x] = true) AND (coord[y] = true) AND (estimate[x] != estimate[y]) AND (x != y) )) } /* LEMMA 2.3 */ system_axiom (universal x:nat, universal y:nat) { (NOT ( (coord[x] = true) AND (faulty[x] = false) AND (round[x] = 6) AND (state[y] = false) AND (faulty[y] = false) AND (x != y) )) } /* Exists only one coordinator in the system */ suggested_negated_invariant (existential x:nat, existential y:nat) { (coord[x] = true) AND (coord[y] = true) } /* If 'c' is coordinator, all other process with id < c have already been coordinator */ suggested_negated_invariant (existential x:nat, existential y:nat) { (coord[x] = true) AND (aCoord[y] = false) AND (y < x) } /* A coordinator can't have id[] greater than his identificator */ suggested_negated_invariant (existential x:nat) { (coord[x] = true) AND (id[x] > x) } /* A process can't have id[] greater than coordinator's identificator */ suggested_negated_invariant (existential x:nat, existential y:nat) { (coord[x] = true) AND (id[y] > x) } /* In the first round a process can't have id[] equals to the coordinator's identificator */ suggested_negated_invariant (existential x:nat, existential y:nat) { (round[x] = 1) AND (coord[x] = true) AND (id[y] = x) } /* A correct process can't receive any nack */ suggested_negated_invariant (existential x:nat) { (faulty[x] = false) AND (nack[x] = true) } /* Coordinators are elected in order by identificator */ suggested_negated_invariant (existential x:nat, existential y:nat) { (coord[x] = true) AND (aCoord[y] = true) AND (y > x) } /* initial configuration */ initial (universal x:nat) { (round[x] = 1) AND (state[x] = false) AND (coord[x] = false) AND (aCoord[x] = false) AND (done[x] = false) AND (received[x] = false) AND (nack[x] = false) AND (id[x] = -1) AND (maxId[x] = -2) AND (processReceivedEstimate[x] = false) } /* AGREEMENT - complete */ unsafe (existential x:nat, existential y:nat) { (state[x] = true) AND (faulty[x] = false) AND (state[y] = true) AND (faulty[y] = false) AND (decisionValue[x] != decisionValue[y]) } /* 1) Decided processes send request to coordinator if their id are greather than maxId */ transition (existential x:nat, existential y:nat) { guard: (round[x] = 1) AND (done[x] = false) AND (state[x] = false) AND (coord[y] = true) AND (id[x] > maxId[x]) update: done[x] := true; maxId := id[x]; tmpEstimate := estimate[x]; } /* 2) Undecided processes want to send a request, but their id is less or equal than maxId */ transition (existential x:nat, existential y:nat) { guard: (round[x] = 1) AND (done[x] = false) AND (state[x] = false) AND (coord[y] = true) AND (id[x] <= maxId[x]) update: done[x] := true; } /* 3) An undecided faulty process fails sending a request */ transition (existential x:nat, existential y:nat) { guard: (round[x] = 1) AND (done[x] = false) AND (state[x] = false) AND (coord[y] = true) AND (faulty[x] = true) update: done[x] := true; } /* 4) An undecided coordinator (with id > maxId) sends a request (to himself) */ transition (existential x:nat) { guard: (round[x] = 1) AND (done[x] = false) AND (state[x] = false) AND (coord[x] = true) AND (id[x] > maxId[x]) update: done[x] := true; maxId := id[x]; tmpEstimate := estimate[x]; } /* 5) An undecided coordinator (with id <= maxId) doesn't send a request to himself */ transition (existential x:nat) { guard: (round[x] = 1) AND (done[x] = false) AND (state[x] = false) AND (coord[x] = true) AND (id[x] <= maxId[x]) update: done[x] := true; } /* 6) Decided processes do nothing */ transition (existential x:nat) { guard: (round[x] = 1) AND (done[x] = false) AND (state[x] = true) update: done[x] := true; } /* 7) If all processes have completed the 1st round and the coordinator received a request (i.e. maxId > -2), the coordinator set his estimate to tmpEstimate value and all the processes go to 2nd round */ transition (existential x:nat, universal all:nat) { guard: (round[x] = 1) AND (maxId[x] > -2) AND (done[x] = true) AND (coord[x] = true) uguard: (done[all] = true) update: round := 2; done := lambda (j:nat) { false } estimate[x] := tmpEstimate[x]; } /* 8) ... otherwise (no request have been received by the coordinator) the coordinator is dismissed. */ transition (existential x:nat, universal all:nat) { guard: (round[x] = 1) AND (maxId[x] = -2) AND (done[x] = true) AND (coord[x] = true) uguard: (done[all] = true) update: coord[x] := false; aCoord[x] := true; } /* 9) An undecided process receives the estimate from the coordinator. */ transition (existential x:nat, existential y:nat) { guard: (round[x] = 2) AND (done[x] = false) AND (state[x] = false) AND (coord[y] = true) update: estimate[x] := estimate[y]; done[x] := true; received[x] := true; id[x] := y; processReceivedEstimate[x] := true; } /* 10) A faulty coordinator fails sending an estimate */ transition (existential x:nat, existential y:nat) { guard: (round[x] = 2) AND (done[x] = false) AND (state[x] = false) AND (coord[y] = true) AND (faulty[y] = true) update: done[x] := true; } /* 11) If the coordinator is undecided sends an estimate to himself */ transition (existential x:nat) { guard: (round[x] = 2) AND (done[x] = false) AND (state[x] = false) AND (coord[x] = true) update: done[x] := true; received[x] := true; id[x] := x; processReceivedEstimate[x] := true; } /* 12) Decided processes do nothing */ transition (existential x:nat) { guard: (round[x] = 2) AND (done[x] = false) AND (state[x] = true) update: done[x] := true; } /* 13) Round 2 completed. System goes to round 3. */ transition (existential x:nat, universal all:nat) { guard: (round[x] = 2) AND (done[x] = true) AND (coord[x] = true) uguard: (done[all] = true) update: round := 3; done := lambda (j:nat) { false } } /* 14) If an undecided process didn't received the estimate sends a nack to coord */ transition (existential x:nat, existential y:nat) { guard: (round[x] = 3) AND (state[x] = false) AND (done[x] = false) AND (received[x] = false) AND (coord[y] = true) update: done[x] := true; lambda (j:nat; j != x) { case (j = y): nack[j] := true; otherwise: nack[j] := nack[j]; } } /* 15) An undecided faulty process that didn't received the estimate fails sending the nack to the coordinator */ transition (existential x:nat, existential y:nat) { guard: (round[x] = 3) AND (state[x] = false) AND (done[x] = false) AND (received[x] = false) AND (coord[y] = true) AND (faulty[x] = true) update: done[x] := true; } /* 16) Af an undecided process has received the estimate does nothing */ transition (existential x:nat, existential y:nat) { guard: (round[x] = 3) AND (state[x] = false) AND (done[x] = false) AND (received[x] = true) AND (coord[y] = true) update: done[x] := true; } /* 17) the coordinator does nothing in this round */ transition (existential x:nat) { guard: (round[x] = 3) AND (done[x] = false) AND (coord[x] = true) update: done[x] := true; } /* 18) decided processes do nothing in this round */ transition (existential x:nat, existential y:nat) { guard: (round[x] = 3) AND (state[x] = true) AND (done[x] = false) AND (coord[y] = true) update: done[x] := true; } /* 19) When all the processes have done, system goes to the 4th round. */ transition (existential x:nat, universal all:nat) { guard: (round[x] = 3) AND (done[x] = true) AND (coord[x] = true) uguard: (done[all] = true) update: round := 4; } /* 20) If no nacks have been received, system goes to the 5th round (if the coordinator received one (or more) nack, he is killed by the system) */ transition (existential x:nat, universal all:nat) { guard: (round[x] = 4) AND (coord[x] = false) uguard: (nack[all] = false) update: round := 5; done := lambda (j:nat) { false } } /* 21) Coordinator sends a decide to an undecided process */ transition (existential x:nat, existential y:nat) { guard: (round[x] = 5) AND (done[x] = false) AND (state[x] = false) AND (coord[y] = true) update: state[x] := true; done[x] := true; decisionValue[x] := estimate[x]; } /* 22) A faulty coordinator fails sending the message */ transition (existential x:nat, existential y:nat) { guard: (round[x] = 5) AND (done[x] = false) AND (state[x] = false) AND (coord[y] = true) AND (faulty[y] = true) update: done[x] := true; } /* 23) A faulty coordinator sends a decide to himself */ transition (existential x:nat) { guard: (round[x] = 5) AND (done[x] = false) AND (state[x] = false) AND (coord[x] = true) update: state[x] := true; done[x] := true; decisionValue[x] := estimate[x]; } /* 24) Coordinator sends a decide to decided processes (but they ignore this message) */ transition (existential x:nat) { guard: (round[x] = 5) AND (done[x] = false) AND (state[x] = true) update: done[x] := true; } /* 25) Round n. 5 completed. System goes to round 6. */ transition (existential x:nat, universal all:nat) { guard: (round[x] = 5) AND (done[x] = true) AND (coord[x] = true) uguard: (done[all] = true) update: round := 6; done := lambda (j:nat) { false } } /* 26) Coordinator in office is dismissed. */ transition (existential x:nat) { guard: (round[x] = 6) AND (coord[x] = true) update: round := 7; coord[x] := false; aCoord[x] := true; } /* 27) There's no coordinator! (maybe the coordinator crashed) */ transition (existential x:nat, universal y:nat) { guard: (coord[x] = false) uguard: (coord[y] = false) update: round := 7; } /* 28) In this round a new process is elected as coordinator of the system. Then the system goes to 1st round. */ transition (existential x:nat, universal y:nat) { guard: (coord[x] = false) AND (aCoord[x] = false) AND (round[x] = 7) uguard: (y >= x) uguard: (y < x) AND (aCoord[y] = true) update: round := 1; coord[x] := true; received := lambda (j:nat) { false } done := lambda (j:nat) { false } nack := lambda (j:nat) { false } maxId := -2; }