You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
885 lines
30 KiB
885 lines
30 KiB
-------------------- MODULE TendermintPBT_002_draft ---------------------------
|
|
(*
|
|
A TLA+ specification of a simplified Tendermint consensus, with added clocks
|
|
and proposer-based timestamps. This TLA+ specification extends and modifies
|
|
the Tendermint TLA+ specification for fork accountability:
|
|
https://github.com/tendermint/spec/blob/master/spec/light-client/accountability/TendermintAcc_004_draft.tla
|
|
|
|
* Version 2. A preliminary specification.
|
|
|
|
Zarko Milosevic, Igor Konnov, Informal Systems, 2019-2020.
|
|
Ilina Stoilkovska, Josef Widder, Informal Systems, 2021.
|
|
Jure Kukovec, Informal Systems, 2022.
|
|
*)
|
|
|
|
EXTENDS Integers, FiniteSets, Apalache, typedefs
|
|
|
|
(********************* PROTOCOL PARAMETERS **********************************)
|
|
\* General protocol parameters
|
|
CONSTANTS
|
|
\* @type: Set(PROCESS);
|
|
Corr, \* the set of correct processes
|
|
\* @type: Set(PROCESS);
|
|
Faulty, \* the set of Byzantine processes, may be empty
|
|
\* @type: Int;
|
|
N, \* the total number of processes: correct, defective, and Byzantine
|
|
\* @type: Int;
|
|
T, \* an upper bound on the number of Byzantine processes
|
|
\* @type: Set(VALUE);
|
|
ValidValues, \* the set of valid values, proposed both by correct and faulty
|
|
\* @type: Set(VALUE);
|
|
InvalidValues, \* the set of invalid values, never proposed by the correct ones
|
|
\* @type: ROUND;
|
|
MaxRound, \* the maximal round number
|
|
\* @type: ROUND -> PROCESS;
|
|
Proposer \* the proposer function from Rounds to AllProcs
|
|
|
|
\* Time-related parameters
|
|
CONSTANTS
|
|
\* @type: TIME;
|
|
MaxTimestamp, \* the maximal value of the clock tick
|
|
\* @type: TIME;
|
|
MinTimestamp, \* the minimal value of the clock tick
|
|
\* @type: TIME;
|
|
Delay, \* message delay
|
|
\* @type: TIME;
|
|
Precision \* clock precision: the maximal difference between two local clocks
|
|
|
|
ASSUME(N = Cardinality(Corr \union Faulty))
|
|
|
|
(*************************** DEFINITIONS ************************************)
|
|
\* @type: Set(PROCESS);
|
|
AllProcs == Corr \union Faulty \* the set of all processes
|
|
\* @type: Set(ROUND);
|
|
Rounds == 0..MaxRound \* the set of potential rounds
|
|
\* @type: Set(TIME);
|
|
Timestamps == 0..MaxTimestamp \* the set of clock ticks
|
|
\* @type: ROUND;
|
|
NilRound == -1 \* a special value to denote a nil round, outside of Rounds
|
|
\* @type: TIME;
|
|
NilTimestamp == -1 \* a special value to denote a nil timestamp, outside of Ticks
|
|
\* @type: Set(ROUND);
|
|
RoundsOrNil == Rounds \union {NilRound}
|
|
\* @type: Set(VALUE);
|
|
Values == ValidValues \union InvalidValues \* the set of all values
|
|
\* @type: VALUE;
|
|
NilValue == "None" \* a special value for a nil round, outside of Values
|
|
\* @type: Set(PROPOSAL);
|
|
Proposals == Values \X Timestamps \X Rounds
|
|
\* @type: PROPOSAL;
|
|
NilProposal == <<NilValue, NilTimestamp, NilRound>>
|
|
\* @type: Set(VALUE);
|
|
ValuesOrNil == Values \union {NilValue}
|
|
\* @type: Set(DECISION);
|
|
Decisions == Proposals \X Rounds
|
|
\* @type: DECISION;
|
|
NilDecision == <<NilProposal, NilRound>>
|
|
|
|
ValidProposals == ValidValues \X (MinTimestamp..MaxTimestamp) \X Rounds
|
|
\* a value hash is modeled as identity
|
|
\* @type: (t) => t;
|
|
Id(v) == v
|
|
|
|
\* The validity predicate
|
|
\* @type: (PROPOSAL) => Bool;
|
|
IsValid(p) == p \in ValidProposals
|
|
|
|
\* Time validity check. If we want MaxTimestamp = \infty, set ValidTime(t) == TRUE
|
|
ValidTime(t) == t < MaxTimestamp
|
|
|
|
\* @type: (PROPMESSAGE) => VALUE;
|
|
MessageValue(msg) == msg.proposal[1]
|
|
\* @type: (PROPMESSAGE) => TIME;
|
|
MessageTime(msg) == msg.proposal[2]
|
|
\* @type: (PROPMESSAGE) => ROUND;
|
|
MessageRound(msg) == msg.proposal[3]
|
|
|
|
\* @type: (TIME, TIME) => Bool;
|
|
IsTimely(processTime, messageTime) ==
|
|
/\ processTime >= messageTime - Precision
|
|
/\ processTime <= messageTime + Precision + Delay
|
|
|
|
\* the two thresholds that are used in the algorithm
|
|
\* @type: Int;
|
|
THRESHOLD1 == T + 1 \* at least one process is not faulty
|
|
\* @type: Int;
|
|
THRESHOLD2 == 2 * T + 1 \* a quorum when having N > 3 * T
|
|
|
|
\* @type: (TIME, TIME) => TIME;
|
|
Min2(a,b) == IF a <= b THEN a ELSE b
|
|
\* @type: (Set(TIME)) => TIME;
|
|
Min(S) == FoldSet( Min2, MaxTimestamp, S )
|
|
\* Min(S) == CHOOSE x \in S : \A y \in S : x <= y
|
|
|
|
\* @type: (TIME, TIME) => TIME;
|
|
Max2(a,b) == IF a >= b THEN a ELSE b
|
|
\* @type: (Set(TIME)) => TIME;
|
|
Max(S) == FoldSet( Max2, NilTimestamp, S )
|
|
\* Max(S) == CHOOSE x \in S : \A y \in S : y <= x
|
|
|
|
\* @type: (Set(MESSAGE)) => Int;
|
|
Card(S) ==
|
|
LET
|
|
\* @type: (Int, MESSAGE) => Int;
|
|
PlusOne(i, m) == i + 1
|
|
IN FoldSet( PlusOne, 0, S )
|
|
|
|
(********************* PROTOCOL STATE VARIABLES ******************************)
|
|
VARIABLES
|
|
\* @type: PROCESS -> ROUND;
|
|
round, \* a process round number
|
|
\* @type: PROCESS -> STEP;
|
|
step, \* a process step
|
|
\* @type: PROCESS -> DECISION;
|
|
decision, \* process decision
|
|
\* @type: PROCESS -> VALUE;
|
|
lockedValue, \* a locked value
|
|
\* @type: PROCESS -> ROUND;
|
|
lockedRound, \* a locked round
|
|
\* @type: PROCESS -> PROPOSAL;
|
|
validValue, \* a valid value
|
|
\* @type: PROCESS -> ROUND;
|
|
validRound \* a valid round
|
|
|
|
coreVars ==
|
|
<<round, step, decision, lockedValue,
|
|
lockedRound, validValue, validRound>>
|
|
|
|
\* time-related variables
|
|
VARIABLES
|
|
\* @type: PROCESS -> TIME;
|
|
localClock, \* a process local clock: Corr -> Ticks
|
|
\* @type: TIME;
|
|
realTime \* a reference Newtonian real time
|
|
|
|
temporalVars == <<localClock, realTime>>
|
|
|
|
\* book-keeping variables
|
|
VARIABLES
|
|
\* @type: ROUND -> Set(PROPMESSAGE);
|
|
msgsPropose, \* PROPOSE messages broadcast in the system, Rounds -> Messages
|
|
\* @type: ROUND -> Set(PREMESSAGE);
|
|
msgsPrevote, \* PREVOTE messages broadcast in the system, Rounds -> Messages
|
|
\* @type: ROUND -> Set(PREMESSAGE);
|
|
msgsPrecommit, \* PRECOMMIT messages broadcast in the system, Rounds -> Messages
|
|
\* @type: Set(MESSAGE);
|
|
evidence, \* the messages that were used by the correct processes to make transitions
|
|
\* @type: ACTION;
|
|
action, \* we use this variable to see which action was taken
|
|
\* @type: PROCESS -> Set(PROPMESSAGE);
|
|
receivedTimelyProposal, \* used to keep track when a process receives a timely PROPOSAL message
|
|
\* @type: <<ROUND,PROCESS>> -> TIME;
|
|
inspectedProposal \* used to keep track when a process tries to receive a message
|
|
|
|
\* Action is excluded from the tuple, because it always changes
|
|
bookkeepingVars ==
|
|
<<msgsPropose, msgsPrevote, msgsPrecommit,
|
|
evidence, (*action,*) receivedTimelyProposal,
|
|
inspectedProposal>>
|
|
|
|
\* Invariant support
|
|
VARIABLES
|
|
\* @type: ROUND -> TIME;
|
|
beginRound, \* the minimum of the local clocks at the time any process entered a new round
|
|
\* @type: PROCESS -> TIME;
|
|
endConsensus, \* the local time when a decision is made
|
|
\* @type: ROUND -> TIME;
|
|
lastBeginRound, \* the maximum of the local clocks in each round
|
|
\* @type: ROUND -> TIME;
|
|
proposalTime, \* the real time when a proposer proposes in a round
|
|
\* @type: ROUND -> TIME;
|
|
proposalReceivedTime \* the real time when a correct process first receives a proposal message in a round
|
|
|
|
invariantVars ==
|
|
<<beginRound, endConsensus, lastBeginRound,
|
|
proposalTime, proposalReceivedTime>>
|
|
|
|
(* to see a type invariant, check TendermintAccInv3 *)
|
|
|
|
(********************* PROTOCOL INITIALIZATION ******************************)
|
|
\* @type: (ROUND) => Set(PROPMESSAGE);
|
|
FaultyProposals(r) ==
|
|
[
|
|
type : {"PROPOSAL"},
|
|
src : Faulty,
|
|
round : {r},
|
|
proposal : Proposals,
|
|
validRound: RoundsOrNil
|
|
]
|
|
|
|
\* @type: Set(PROPMESSAGE);
|
|
AllFaultyProposals ==
|
|
[
|
|
type : {"PROPOSAL"},
|
|
src : Faulty,
|
|
round : Rounds,
|
|
proposal : Proposals,
|
|
validRound: RoundsOrNil
|
|
]
|
|
|
|
\* @type: (ROUND) => Set(PREMESSAGE);
|
|
FaultyPrevotes(r) ==
|
|
[
|
|
type : {"PREVOTE"},
|
|
src : Faulty,
|
|
round: {r},
|
|
id : Proposals
|
|
]
|
|
|
|
\* @type: Set(PREMESSAGE);
|
|
AllFaultyPrevotes ==
|
|
[
|
|
type : {"PREVOTE"},
|
|
src : Faulty,
|
|
round: Rounds,
|
|
id : Proposals
|
|
]
|
|
|
|
\* @type: (ROUND) => Set(PREMESSAGE);
|
|
FaultyPrecommits(r) ==
|
|
[
|
|
type : {"PRECOMMIT"},
|
|
src : Faulty,
|
|
round: {r},
|
|
id : Proposals
|
|
]
|
|
|
|
\* @type: Set(PREMESSAGE);
|
|
AllFaultyPrecommits ==
|
|
[
|
|
type : {"PRECOMMIT"},
|
|
src : Faulty,
|
|
round: Rounds,
|
|
id : Proposals
|
|
]
|
|
|
|
\* @type: Set(PROPMESSAGE);
|
|
AllProposals ==
|
|
[
|
|
type : {"PROPOSAL"},
|
|
src : AllProcs,
|
|
round : Rounds,
|
|
proposal : Proposals,
|
|
validRound: RoundsOrNil
|
|
]
|
|
|
|
\* @type: (ROUND) => Set(PROPMESSAGE);
|
|
RoundProposals(r) ==
|
|
[
|
|
type : {"PROPOSAL"},
|
|
src : AllProcs,
|
|
round : {r},
|
|
proposal : Proposals,
|
|
validRound: RoundsOrNil
|
|
]
|
|
|
|
\* @type: (ROUND -> Set(MESSAGE)) => Bool;
|
|
BenignRoundsInMessages(msgfun) ==
|
|
\* the message function never contains a message for a wrong round
|
|
\A r \in Rounds:
|
|
\A m \in msgfun[r]:
|
|
r = m.round
|
|
|
|
\* The initial states of the protocol. Some faults can be in the system already.
|
|
Init ==
|
|
/\ round = [p \in Corr |-> 0]
|
|
/\ localClock \in [Corr -> MinTimestamp..(MinTimestamp + Precision)]
|
|
/\ realTime = 0
|
|
/\ step = [p \in Corr |-> "PROPOSE"]
|
|
/\ decision = [p \in Corr |-> NilDecision]
|
|
/\ lockedValue = [p \in Corr |-> NilValue]
|
|
/\ lockedRound = [p \in Corr |-> NilRound]
|
|
/\ validValue = [p \in Corr |-> NilProposal]
|
|
/\ validRound = [p \in Corr |-> NilRound]
|
|
/\ msgsPropose \in [Rounds -> SUBSET AllFaultyProposals]
|
|
/\ msgsPrevote \in [Rounds -> SUBSET AllFaultyPrevotes]
|
|
/\ msgsPrecommit \in [Rounds -> SUBSET AllFaultyPrecommits]
|
|
/\ receivedTimelyProposal = [p \in Corr |-> {}]
|
|
/\ inspectedProposal = [r \in Rounds, p \in Corr |-> NilTimestamp]
|
|
/\ BenignRoundsInMessages(msgsPropose)
|
|
/\ BenignRoundsInMessages(msgsPrevote)
|
|
/\ BenignRoundsInMessages(msgsPrecommit)
|
|
/\ evidence = {}
|
|
/\ action' = "Init"
|
|
/\ beginRound =
|
|
[r \in Rounds |->
|
|
IF r = 0
|
|
THEN Min({localClock[p] : p \in Corr})
|
|
ELSE MaxTimestamp
|
|
]
|
|
/\ endConsensus = [p \in Corr |-> NilTimestamp]
|
|
/\ lastBeginRound =
|
|
[r \in Rounds |->
|
|
IF r = 0
|
|
THEN Max({localClock[p] : p \in Corr})
|
|
ELSE NilTimestamp
|
|
]
|
|
/\ proposalTime = [r \in Rounds |-> NilTimestamp]
|
|
/\ proposalReceivedTime = [r \in Rounds |-> NilTimestamp]
|
|
|
|
(************************ MESSAGE PASSING ********************************)
|
|
\* @type: (PROCESS, ROUND, PROPOSAL, ROUND) => Bool;
|
|
BroadcastProposal(pSrc, pRound, pProposal, pValidRound) ==
|
|
LET
|
|
\* @type: PROPMESSAGE;
|
|
newMsg ==
|
|
[
|
|
type |-> "PROPOSAL",
|
|
src |-> pSrc,
|
|
round |-> pRound,
|
|
proposal |-> pProposal,
|
|
validRound |-> pValidRound
|
|
]
|
|
IN
|
|
/\ msgsPropose' = [msgsPropose EXCEPT ![pRound] = msgsPropose[pRound] \union {newMsg}]
|
|
|
|
\* @type: (PROCESS, ROUND, PROPOSAL) => Bool;
|
|
BroadcastPrevote(pSrc, pRound, pId) ==
|
|
LET
|
|
\* @type: PREMESSAGE;
|
|
newMsg ==
|
|
[
|
|
type |-> "PREVOTE",
|
|
src |-> pSrc,
|
|
round |-> pRound,
|
|
id |-> pId
|
|
]
|
|
IN
|
|
/\ msgsPrevote' = [msgsPrevote EXCEPT ![pRound] = msgsPrevote[pRound] \union {newMsg}]
|
|
|
|
\* @type: (PROCESS, ROUND, PROPOSAL) => Bool;
|
|
BroadcastPrecommit(pSrc, pRound, pId) ==
|
|
LET
|
|
\* @type: PREMESSAGE;
|
|
newMsg ==
|
|
[
|
|
type |-> "PRECOMMIT",
|
|
src |-> pSrc,
|
|
round |-> pRound,
|
|
id |-> pId
|
|
]
|
|
IN
|
|
/\ msgsPrecommit' = [msgsPrecommit EXCEPT ![pRound] = msgsPrecommit[pRound] \union {newMsg}]
|
|
|
|
(***************************** TIME **************************************)
|
|
|
|
\* [PBTS-CLOCK-PRECISION.0]
|
|
\* @type: Bool;
|
|
SynchronizedLocalClocks ==
|
|
\A p \in Corr : \A q \in Corr :
|
|
p /= q =>
|
|
\/ /\ localClock[p] >= localClock[q]
|
|
/\ localClock[p] - localClock[q] < Precision
|
|
\/ /\ localClock[p] < localClock[q]
|
|
/\ localClock[q] - localClock[p] < Precision
|
|
|
|
\* [PBTS-PROPOSE.0]
|
|
\* @type: (VALUE, TIME, ROUND) => PROPOSAL;
|
|
Proposal(v, t, r) ==
|
|
<<v, t, r>>
|
|
|
|
\* [PBTS-DECISION-ROUND.0]
|
|
\* @type: (PROPOSAL, ROUND) => DECISION;
|
|
Decision(p, r) ==
|
|
<<p, r>>
|
|
|
|
(**************** MESSAGE PROCESSING TRANSITIONS *************************)
|
|
\* lines 12-13
|
|
\* @type: (PROCESS, ROUND) => Bool;
|
|
StartRound(p, r) ==
|
|
/\ step[p] /= "DECIDED" \* a decided process does not participate in consensus
|
|
/\ round' = [round EXCEPT ![p] = r]
|
|
/\ step' = [step EXCEPT ![p] = "PROPOSE"]
|
|
\* We only need to update (last)beginRound[r] once a process enters round `r`
|
|
/\ beginRound' = [beginRound EXCEPT ![r] = Min2(@, localClock[p])]
|
|
/\ lastBeginRound' = [lastBeginRound EXCEPT ![r] = Max2(@, localClock[p])]
|
|
|
|
\* lines 14-19, a proposal may be sent later
|
|
\* @type: (PROCESS) => Bool;
|
|
InsertProposal(p) ==
|
|
LET r == round[p] IN
|
|
/\ p = Proposer[r]
|
|
/\ step[p] = "PROPOSE"
|
|
\* if the proposer is sending a proposal, then there are no other proposals
|
|
\* by the correct processes for the same round
|
|
/\ \A m \in msgsPropose[r]: m.src /= p
|
|
\* /\ localClock[p] >
|
|
/\ \E v \in ValidValues:
|
|
LET proposal ==
|
|
IF validValue[p] /= NilProposal
|
|
THEN validValue[p]
|
|
ELSE Proposal(v, localClock[p], r)
|
|
IN
|
|
/\ BroadcastProposal(p, r, proposal, validRound[p])
|
|
/\ proposalTime' = [proposalTime EXCEPT ![r] = realTime]
|
|
/\ UNCHANGED <<temporalVars, coreVars>>
|
|
/\ UNCHANGED
|
|
<<(*msgsPropose,*) msgsPrevote, msgsPrecommit,
|
|
evidence, receivedTimelyProposal, inspectedProposal>>
|
|
/\ UNCHANGED
|
|
<<beginRound, endConsensus, lastBeginRound,
|
|
(*proposalTime,*) proposalReceivedTime>>
|
|
/\ action' = "InsertProposal"
|
|
|
|
\* a new action used to filter messages that are not on time
|
|
\* [PBTS-RECEPTION-STEP.0]
|
|
\* @type: (PROCESS) => Bool;
|
|
ReceiveProposal(p) ==
|
|
\E v \in Values, t \in Timestamps:
|
|
/\ LET r == round[p] IN
|
|
LET
|
|
\* @type: PROPMESSAGE;
|
|
msg ==
|
|
[
|
|
type |-> "PROPOSAL",
|
|
src |-> Proposer[round[p]],
|
|
round |-> round[p],
|
|
proposal |-> Proposal(v, t, r),
|
|
validRound |-> NilRound
|
|
]
|
|
IN
|
|
/\ msg \in msgsPropose[round[p]]
|
|
/\ inspectedProposal[r,p] = NilTimestamp
|
|
/\ msg \notin receivedTimelyProposal[p]
|
|
/\ inspectedProposal' = [inspectedProposal EXCEPT ![r,p] = localClock[p]]
|
|
/\ LET
|
|
isTimely == IsTimely(localClock[p], t)
|
|
IN
|
|
\/ /\ isTimely
|
|
/\ receivedTimelyProposal' = [receivedTimelyProposal EXCEPT ![p] = @ \union {msg}]
|
|
/\ LET
|
|
isNilTimestamp == proposalReceivedTime[r] = NilTimestamp
|
|
IN
|
|
\/ /\ isNilTimestamp
|
|
/\ proposalReceivedTime' = [proposalReceivedTime EXCEPT ![r] = realTime]
|
|
\/ /\ ~isNilTimestamp
|
|
/\ UNCHANGED proposalReceivedTime
|
|
\/ /\ ~isTimely
|
|
/\ UNCHANGED <<receivedTimelyProposal, proposalReceivedTime>>
|
|
/\ UNCHANGED <<temporalVars, coreVars>>
|
|
/\ UNCHANGED
|
|
<<msgsPropose, msgsPrevote, msgsPrecommit,
|
|
evidence(*, receivedTimelyProposal, inspectedProposal*)>>
|
|
/\ UNCHANGED
|
|
<<beginRound, endConsensus, lastBeginRound,
|
|
proposalTime(*, proposalReceivedTime*)>>
|
|
/\ action' = "ReceiveProposal"
|
|
|
|
\* lines 22-27
|
|
\* @type: (PROCESS) => Bool;
|
|
UponProposalInPropose(p) ==
|
|
\E v \in Values, t \in Timestamps:
|
|
LET
|
|
r == round[p]
|
|
IN LET
|
|
\* @type: PROPOSAL;
|
|
prop == Proposal(v,t,r)
|
|
IN
|
|
/\ step[p] = "PROPOSE" (* line 22 *)
|
|
/\ LET
|
|
\* @type: PROPMESSAGE;
|
|
msg ==
|
|
[
|
|
type |-> "PROPOSAL",
|
|
src |-> Proposer[r],
|
|
round |-> r,
|
|
proposal |-> prop,
|
|
validRound |-> NilRound
|
|
]
|
|
IN
|
|
/\ msg \in receivedTimelyProposal[p] \* updated line 22
|
|
/\ evidence' = {msg} \union evidence
|
|
/\ LET mid == (* line 23 *)
|
|
IF IsValid(prop) /\ (lockedRound[p] = NilRound \/ lockedValue[p] = v)
|
|
THEN Id(prop)
|
|
ELSE NilProposal
|
|
IN
|
|
BroadcastPrevote(p, r, mid) \* lines 24-26
|
|
/\ step' = [step EXCEPT ![p] = "PREVOTE"]
|
|
/\ UNCHANGED <<temporalVars, invariantVars>>
|
|
/\ UNCHANGED
|
|
<<round, (*step,*) decision, lockedValue,
|
|
lockedRound, validValue, validRound>>
|
|
/\ UNCHANGED
|
|
<<msgsPropose, (*msgsPrevote,*) msgsPrecommit,
|
|
(*evidence,*) receivedTimelyProposal, inspectedProposal>>
|
|
/\ action' = "UponProposalInPropose"
|
|
|
|
\* lines 28-33
|
|
\* [PBTS-ALG-OLD-PREVOTE.0]
|
|
\* @type: (PROCESS) => Bool;
|
|
UponProposalInProposeAndPrevote(p) ==
|
|
\E v \in Values, t \in Timestamps, vr \in Rounds, pr \in Rounds:
|
|
LET
|
|
r == round[p]
|
|
IN LET
|
|
\* @type: PROPOSAL;
|
|
prop == Proposal(v,t,pr)
|
|
IN
|
|
/\ step[p] = "PROPOSE" /\ 0 <= vr /\ vr < r \* line 28, the while part
|
|
/\ pr <= vr
|
|
/\ LET
|
|
\* @type: PROPMESSAGE;
|
|
msg ==
|
|
[
|
|
type |-> "PROPOSAL",
|
|
src |-> Proposer[r],
|
|
round |-> r,
|
|
proposal |-> prop,
|
|
validRound |-> vr
|
|
]
|
|
IN
|
|
\* Changed from 001: no need to re-check timeliness
|
|
/\ msg \in msgsPropose[r] \* line 28
|
|
/\ LET PV == { m \in msgsPrevote[vr]: m.id = Id(prop) } IN
|
|
/\ Cardinality(PV) >= THRESHOLD2 \* line 28
|
|
/\ evidence' = PV \union {msg} \union evidence
|
|
/\ LET mid == (* line 29 *)
|
|
IF IsValid(prop) /\ (lockedRound[p] <= vr \/ lockedValue[p] = v)
|
|
THEN Id(prop)
|
|
ELSE NilProposal
|
|
IN
|
|
BroadcastPrevote(p, r, mid) \* lines 24-26
|
|
/\ step' = [step EXCEPT ![p] = "PREVOTE"]
|
|
/\ UNCHANGED <<temporalVars, invariantVars>>
|
|
/\ UNCHANGED
|
|
<<round, (*step,*) decision, lockedValue,
|
|
lockedRound, validValue, validRound>>
|
|
/\ UNCHANGED
|
|
<<msgsPropose, (*msgsPrevote,*) msgsPrecommit,
|
|
(*evidence,*) receivedTimelyProposal, inspectedProposal>>
|
|
/\ action' = "UponProposalInProposeAndPrevote"
|
|
|
|
\* lines 34-35 + lines 61-64 (onTimeoutPrevote)
|
|
\* @type: (PROCESS) => Bool;
|
|
UponQuorumOfPrevotesAny(p) ==
|
|
/\ step[p] = "PREVOTE" \* line 34 and 61
|
|
/\ \E MyEvidence \in SUBSET msgsPrevote[round[p]]:
|
|
\* find the unique voters in the evidence
|
|
LET Voters == { m.src: m \in MyEvidence } IN
|
|
\* compare the number of the unique voters against the threshold
|
|
/\ Cardinality(Voters) >= THRESHOLD2 \* line 34
|
|
/\ evidence' = MyEvidence \union evidence
|
|
/\ BroadcastPrecommit(p, round[p], NilProposal)
|
|
/\ step' = [step EXCEPT ![p] = "PRECOMMIT"]
|
|
/\ UNCHANGED <<temporalVars, invariantVars>>
|
|
/\ UNCHANGED
|
|
<<round, (*step,*) decision, lockedValue,
|
|
lockedRound, validValue, validRound>>
|
|
/\ UNCHANGED
|
|
<<msgsPropose, msgsPrevote, (*msgsPrecommit, *)
|
|
(*evidence,*) receivedTimelyProposal, inspectedProposal>>
|
|
/\ action' = "UponQuorumOfPrevotesAny"
|
|
|
|
\* lines 36-46
|
|
\* [PBTS-ALG-NEW-PREVOTE.0]
|
|
\* @type: (PROCESS) => Bool;
|
|
UponProposalInPrevoteOrCommitAndPrevote(p) ==
|
|
\E v \in ValidValues, t \in Timestamps, vr \in RoundsOrNil:
|
|
LET
|
|
r == round[p]
|
|
IN LET
|
|
\* @type: PROPOSAL;
|
|
prop == Proposal(v,t,r)
|
|
IN
|
|
/\ step[p] \in {"PREVOTE", "PRECOMMIT"} \* line 36
|
|
/\ LET
|
|
\* @type: PROPMESSAGE;
|
|
msg ==
|
|
[
|
|
type |-> "PROPOSAL",
|
|
src |-> Proposer[r],
|
|
round |-> r,
|
|
proposal |-> prop,
|
|
validRound |-> vr
|
|
]
|
|
IN
|
|
\* Changed from 001: no need to re-check timeliness
|
|
/\ msg \in msgsPropose[r] \* line 36
|
|
/\ LET PV == { m \in msgsPrevote[r]: m.id = Id(prop) } IN
|
|
/\ Cardinality(PV) >= THRESHOLD2 \* line 36
|
|
/\ evidence' = PV \union {msg} \union evidence
|
|
/\ IF step[p] = "PREVOTE"
|
|
THEN \* lines 38-41:
|
|
/\ lockedValue' = [lockedValue EXCEPT ![p] = v]
|
|
/\ lockedRound' = [lockedRound EXCEPT ![p] = r]
|
|
/\ BroadcastPrecommit(p, r, Id(prop))
|
|
/\ step' = [step EXCEPT ![p] = "PRECOMMIT"]
|
|
ELSE
|
|
UNCHANGED <<lockedValue, lockedRound, msgsPrecommit, step>>
|
|
\* lines 42-43
|
|
/\ validValue' = [validValue EXCEPT ![p] = prop]
|
|
/\ validRound' = [validRound EXCEPT ![p] = r]
|
|
/\ UNCHANGED <<temporalVars, invariantVars>>
|
|
/\ UNCHANGED
|
|
<<round, (*step,*) decision(*, lockedValue,
|
|
lockedRound, validValue, validRound*)>>
|
|
/\ UNCHANGED
|
|
<<msgsPropose, msgsPrevote, (*msgsPrecommit, *)
|
|
(*evidence,*) receivedTimelyProposal, inspectedProposal>>
|
|
/\ action' = "UponProposalInPrevoteOrCommitAndPrevote"
|
|
|
|
\* lines 47-48 + 65-67 (onTimeoutPrecommit)
|
|
\* @type: (PROCESS) => Bool;
|
|
UponQuorumOfPrecommitsAny(p) ==
|
|
/\ \E MyEvidence \in SUBSET msgsPrecommit[round[p]]:
|
|
\* find the unique committers in the evidence
|
|
LET Committers == { m.src: m \in MyEvidence } IN
|
|
\* compare the number of the unique committers against the threshold
|
|
/\ Cardinality(Committers) >= THRESHOLD2 \* line 47
|
|
/\ evidence' = MyEvidence \union evidence
|
|
/\ round[p] + 1 \in Rounds
|
|
/\ StartRound(p, round[p] + 1)
|
|
/\ UNCHANGED temporalVars
|
|
/\ UNCHANGED
|
|
<<(*beginRound,*) endConsensus, (*lastBeginRound,*)
|
|
proposalTime, proposalReceivedTime>>
|
|
/\ UNCHANGED
|
|
<<(*round, step,*) decision, lockedValue,
|
|
lockedRound, validValue, validRound>>
|
|
/\ UNCHANGED
|
|
<<msgsPropose, msgsPrevote, msgsPrecommit,
|
|
(*evidence,*) receivedTimelyProposal, inspectedProposal>>
|
|
/\ action' = "UponQuorumOfPrecommitsAny"
|
|
|
|
\* lines 49-54
|
|
\* [PBTS-ALG-DECIDE.0]
|
|
\* @type: (PROCESS) => Bool;
|
|
UponProposalInPrecommitNoDecision(p) ==
|
|
/\ decision[p] = NilDecision \* line 49
|
|
/\ \E v \in ValidValues, t \in Timestamps (* line 50*) , r \in Rounds, pr \in Rounds, vr \in RoundsOrNil:
|
|
LET
|
|
\* @type: PROPOSAL;
|
|
prop == Proposal(v,t,pr)
|
|
IN
|
|
/\ LET
|
|
\* @type: PROPMESSAGE;
|
|
msg ==
|
|
[
|
|
type |-> "PROPOSAL",
|
|
src |-> Proposer[r],
|
|
round |-> r,
|
|
proposal |-> prop,
|
|
validRound |-> vr
|
|
]
|
|
IN
|
|
/\ msg \in msgsPropose[r] \* line 49
|
|
/\ inspectedProposal[r,p] /= NilTimestamp \* Keep?
|
|
/\ LET PV == { m \in msgsPrecommit[r]: m.id = Id(prop) } IN
|
|
/\ Cardinality(PV) >= THRESHOLD2 \* line 49
|
|
/\ evidence' = PV \union {msg} \union evidence
|
|
/\ decision' = [decision EXCEPT ![p] = Decision(prop, r)] \* update the decision, line 51
|
|
\* The original algorithm does not have 'DECIDED', but it increments the height.
|
|
\* We introduced 'DECIDED' here to prevent the process from changing its decision.
|
|
/\ endConsensus' = [endConsensus EXCEPT ![p] = localClock[p]]
|
|
/\ step' = [step EXCEPT ![p] = "DECIDED"]
|
|
/\ UNCHANGED temporalVars
|
|
/\ UNCHANGED
|
|
<<round, (*step, decision,*) lockedValue,
|
|
lockedRound, validValue, validRound>>
|
|
/\ UNCHANGED
|
|
<<msgsPropose, msgsPrevote, msgsPrecommit,
|
|
(*evidence,*) receivedTimelyProposal, inspectedProposal>>
|
|
/\ UNCHANGED
|
|
<<beginRound, (*endConsensus,*) lastBeginRound,
|
|
proposalTime, proposalReceivedTime>>
|
|
/\ action' = "UponProposalInPrecommitNoDecision"
|
|
|
|
\* the actions below are not essential for safety, but added for completeness
|
|
|
|
\* lines 20-21 + 57-60
|
|
\* @type: (PROCESS) => Bool;
|
|
OnTimeoutPropose(p) ==
|
|
/\ step[p] = "PROPOSE"
|
|
/\ p /= Proposer[round[p]]
|
|
/\ BroadcastPrevote(p, round[p], NilProposal)
|
|
/\ step' = [step EXCEPT ![p] = "PREVOTE"]
|
|
/\ UNCHANGED <<temporalVars, invariantVars>>
|
|
/\ UNCHANGED
|
|
<<round, (*step,*) decision, lockedValue,
|
|
lockedRound, validValue, validRound>>
|
|
/\ UNCHANGED
|
|
<<msgsPropose, (*msgsPrevote,*) msgsPrecommit,
|
|
evidence, receivedTimelyProposal, inspectedProposal>>
|
|
/\ action' = "OnTimeoutPropose"
|
|
|
|
\* lines 44-46
|
|
\* @type: (PROCESS) => Bool;
|
|
OnQuorumOfNilPrevotes(p) ==
|
|
/\ step[p] = "PREVOTE"
|
|
/\ LET PV == { m \in msgsPrevote[round[p]]: m.id = Id(NilProposal) } IN
|
|
/\ Cardinality(PV) >= THRESHOLD2 \* line 36
|
|
/\ evidence' = PV \union evidence
|
|
/\ BroadcastPrecommit(p, round[p], Id(NilProposal))
|
|
/\ step' = [step EXCEPT ![p] = "PRECOMMIT"]
|
|
/\ UNCHANGED <<temporalVars, invariantVars>>
|
|
/\ UNCHANGED
|
|
<<round, (*step,*) decision, lockedValue,
|
|
lockedRound, validValue, validRound>>
|
|
/\ UNCHANGED
|
|
<<msgsPropose, msgsPrevote, (*msgsPrecommit,*)
|
|
(*evidence,*) receivedTimelyProposal, inspectedProposal>>
|
|
/\ action' = "OnQuorumOfNilPrevotes"
|
|
|
|
\* lines 55-56
|
|
\* @type: (PROCESS) => Bool;
|
|
OnRoundCatchup(p) ==
|
|
\E r \in {rr \in Rounds: rr > round[p]}:
|
|
LET RoundMsgs == msgsPropose[r] \union msgsPrevote[r] \union msgsPrecommit[r] IN
|
|
\E MyEvidence \in SUBSET RoundMsgs:
|
|
LET Faster == { m.src: m \in MyEvidence } IN
|
|
/\ Cardinality(Faster) >= THRESHOLD1
|
|
/\ evidence' = MyEvidence \union evidence
|
|
/\ StartRound(p, r)
|
|
/\ UNCHANGED temporalVars
|
|
/\ UNCHANGED
|
|
<<(*beginRound,*) endConsensus, (*lastBeginRound,*)
|
|
proposalTime, proposalReceivedTime>>
|
|
/\ UNCHANGED
|
|
<<(*round, step,*) decision, lockedValue,
|
|
lockedRound, validValue, validRound>>
|
|
/\ UNCHANGED
|
|
<<msgsPropose, msgsPrevote, msgsPrecommit,
|
|
(*evidence,*) receivedTimelyProposal, inspectedProposal>>
|
|
/\ action' = "OnRoundCatchup"
|
|
|
|
|
|
(********************* PROTOCOL TRANSITIONS ******************************)
|
|
\* advance the global clock
|
|
\* @type: Bool;
|
|
AdvanceRealTime ==
|
|
/\ ValidTime(realTime)
|
|
/\ \E t \in Timestamps:
|
|
/\ t > realTime
|
|
/\ realTime' = t
|
|
/\ localClock' = [p \in Corr |-> localClock[p] + (t - realTime)]
|
|
/\ UNCHANGED <<coreVars, bookkeepingVars, invariantVars>>
|
|
/\ action' = "AdvanceRealTime"
|
|
|
|
\* advance the local clock of node p to some larger time t, not necessarily by 1
|
|
\* #type: (PROCESS) => Bool;
|
|
\* AdvanceLocalClock(p) ==
|
|
\* /\ ValidTime(localClock[p])
|
|
\* /\ \E t \in Timestamps:
|
|
\* /\ t > localClock[p]
|
|
\* /\ localClock' = [localClock EXCEPT ![p] = t]
|
|
\* /\ UNCHANGED <<coreVars, bookkeepingVars, invariantVars>>
|
|
\* /\ UNCHANGED realTime
|
|
\* /\ action' = "AdvanceLocalClock"
|
|
|
|
\* process timely messages
|
|
\* @type: (PROCESS) => Bool;
|
|
MessageProcessing(p) ==
|
|
\* start round
|
|
\/ InsertProposal(p)
|
|
\* reception step
|
|
\/ ReceiveProposal(p)
|
|
\* processing step
|
|
\/ UponProposalInPropose(p)
|
|
\/ UponProposalInProposeAndPrevote(p)
|
|
\/ UponQuorumOfPrevotesAny(p)
|
|
\/ UponProposalInPrevoteOrCommitAndPrevote(p)
|
|
\/ UponQuorumOfPrecommitsAny(p)
|
|
\/ UponProposalInPrecommitNoDecision(p)
|
|
\* the actions below are not essential for safety, but added for completeness
|
|
\/ OnTimeoutPropose(p)
|
|
\/ OnQuorumOfNilPrevotes(p)
|
|
\/ OnRoundCatchup(p)
|
|
|
|
(*
|
|
* A system transition. In this specificatiom, the system may eventually deadlock,
|
|
* e.g., when all processes decide. This is expected behavior, as we focus on safety.
|
|
*)
|
|
Next ==
|
|
\/ AdvanceRealTime
|
|
\/ /\ SynchronizedLocalClocks
|
|
/\ \E p \in Corr: MessageProcessing(p)
|
|
|
|
-----------------------------------------------------------------------------
|
|
|
|
(*************************** INVARIANTS *************************************)
|
|
|
|
\* [PBTS-INV-AGREEMENT.0]
|
|
AgreementOnValue ==
|
|
\A p, q \in Corr:
|
|
/\ decision[p] /= NilDecision
|
|
/\ decision[q] /= NilDecision
|
|
=> \E v \in ValidValues, t \in Timestamps, pr \in Rounds, r1 \in Rounds, r2 \in Rounds :
|
|
LET prop == Proposal(v,t,pr)
|
|
IN
|
|
/\ decision[p] = Decision(prop, r1)
|
|
/\ decision[q] = Decision(prop, r2)
|
|
|
|
\* [PBTS-CONSENSUS-TIME-VALID.0]
|
|
ConsensusTimeValid ==
|
|
\A p \in Corr:
|
|
\* if a process decides on v and t
|
|
\E v \in ValidValues, t \in Timestamps, pr \in Rounds, dr \in Rounds :
|
|
decision[p] = Decision(Proposal(v,t,pr), dr)
|
|
\* then
|
|
\* TODO: consider tighter bound where beginRound[pr] is replaced
|
|
\* w/ MedianOfRound[pr]
|
|
=> (/\ beginRound[pr] - Precision - Delay <= t
|
|
/\ t <= endConsensus[p] + Precision)
|
|
|
|
\* [PBTS-CONSENSUS-SAFE-VALID-CORR-PROP.0]
|
|
ConsensusSafeValidCorrProp ==
|
|
\A v \in ValidValues:
|
|
\* and there exists a process that decided on v, t
|
|
/\ \E p \in Corr, t \in Timestamps, pr \in Rounds, dr \in Rounds :
|
|
\* if the proposer in the round is correct
|
|
(/\ Proposer[pr] \in Corr
|
|
/\ decision[p] = Decision(Proposal(v,t,pr), dr))
|
|
\* then t is between the minimal and maximal initial local time
|
|
=> /\ beginRound[pr] <= t
|
|
/\ t <= lastBeginRound[pr]
|
|
|
|
\* [PBTS-CONSENSUS-REALTIME-VALID-CORR.0]
|
|
ConsensusRealTimeValidCorr ==
|
|
\A r \in Rounds :
|
|
\E p \in Corr, v \in ValidValues, t \in Timestamps, pr \in Rounds:
|
|
(/\ decision[p] = Decision(Proposal(v,t,pr), r)
|
|
/\ proposalTime[r] /= NilTimestamp)
|
|
=> (/\ proposalTime[r] - Precision <= t
|
|
/\ t <= proposalTime[r] + Precision)
|
|
|
|
\* [PBTS-CONSENSUS-REALTIME-VALID.0]
|
|
ConsensusRealTimeValid ==
|
|
\A t \in Timestamps, r \in Rounds :
|
|
(\E p \in Corr, v \in ValidValues, pr \in Rounds :
|
|
decision[p] = Decision(Proposal(v,t,pr), r))
|
|
=> /\ proposalReceivedTime[r] - Precision < t
|
|
/\ t < proposalReceivedTime[r] + Precision + Delay
|
|
|
|
DecideAfterMin == TRUE
|
|
\* if decide => time > min
|
|
|
|
\* [PBTS-MSG-FAIR.0]
|
|
BoundedDelay ==
|
|
\A r \in Rounds :
|
|
(/\ proposalTime[r] /= NilTimestamp
|
|
/\ proposalTime[r] + Delay < realTime)
|
|
=> \A p \in Corr: inspectedProposal[r,p] /= NilTimestamp
|
|
|
|
\* [PBTS-CONSENSUS-TIME-LIVE.0]
|
|
ConsensusTimeLive ==
|
|
\A r \in Rounds, p \in Corr :
|
|
(/\ proposalTime[r] /= NilTimestamp
|
|
/\ proposalTime[r] + Delay < realTime
|
|
/\ Proposer[r] \in Corr
|
|
/\ round[p] <= r)
|
|
=> \E msg \in RoundProposals(r) : msg \in receivedTimelyProposal[p]
|
|
|
|
\* a conjunction of all invariants
|
|
Inv ==
|
|
/\ AgreementOnValue
|
|
/\ ConsensusTimeValid
|
|
/\ ConsensusSafeValidCorrProp
|
|
\* /\ ConsensusRealTimeValid
|
|
\* /\ ConsensusRealTimeValidCorr
|
|
\* /\ BoundedDelay
|
|
|
|
\* Liveness ==
|
|
\* ConsensusTimeLive
|
|
|
|
=============================================================================
|