diff --git a/spec/consensus/proposer-based-timestamp/tla/Apalache.tla b/spec/consensus/proposer-based-timestamp/tla/Apalache.tla deleted file mode 100644 index 044bff666..000000000 --- a/spec/consensus/proposer-based-timestamp/tla/Apalache.tla +++ /dev/null @@ -1,109 +0,0 @@ ---------------------------- MODULE Apalache ----------------------------------- -(* - * This is a standard module for use with the Apalache model checker. - * The meaning of the operators is explained in the comments. - * Many of the operators serve as additional annotations of their arguments. - * As we like to preserve compatibility with TLC and TLAPS, we define the - * operator bodies by erasure. The actual interpretation of the operators is - * encoded inside Apalache. For the moment, these operators are mirrored in - * the class at.forsyte.apalache.tla.lir.oper.ApalacheOper. - * - * Igor Konnov, Jure Kukovec, Informal Systems 2020-2021 - *) - -(** - * An assignment of an expression e to a state variable x. Typically, one - * uses the non-primed version of x in the initializing predicate Init and - * the primed version of x (that is, x') in the transition predicate Next. - * Although TLA+ does not have a concept of a variable assignment, we find - * this concept extremely useful for symbolic model checking. In pure TLA+, - * one would simply write x = e, or x \in {e}. - * - * Apalache automatically converts some expressions of the form - * x = e or x \in {e} into assignments. However, if you like to annotate - * assignments by hand, you can use this operator. - * - * For a further discussion on that matter, see: - * https://github.com/informalsystems/apalache/blob/ik/idiomatic-tla/docs/idiomatic/assignments.md - *) -x := e == x = e - -(** - * A generator of a data structure. Given a positive integer `bound`, and - * assuming that the type of the operator application is known, we - * recursively generate a TLA+ data structure as a tree, whose width is - * bound by the number `bound`. - * - * The body of this operator is redefined by Apalache. - *) -Gen(size) == {} - -(** - * Convert a set of pairs S to a function F. Note that if S contains at least - * two pairs <> and <> such that x = u and y /= v, - * then F is not uniquely defined. We use CHOOSE to resolve this ambiguity. - * Apalache implements a more efficient encoding of this operator - * than the default one. - * - * @type: Set(<>) => (a -> b); - *) -SetAsFun(S) == - LET Dom == { x: <> \in S } - Rng == { y: <> \in S } - IN - [ x \in Dom |-> CHOOSE y \in Rng: <> \in S ] - -(** - * As TLA+ is untyped, one can use function- and sequence-specific operators - * interchangeably. However, to maintain correctness w.r.t. our type-system, - * an explicit cast is needed when using functions as sequences. - *) -LOCAL INSTANCE Sequences -FunAsSeq(fn, maxSeqLen) == SubSeq(fn, 1, maxSeqLen) - -(** - * Annotating an expression \E x \in S: P as Skolemizable. That is, it can - * be replaced with an expression c \in S /\ P(c) for a fresh constant c. - * Not every exisential can be replaced with a constant, this should be done - * with care. Apalache detects Skolemizable expressions by static analysis. - *) -Skolem(e) == e - -(** - * A hint to the model checker to expand a set S, instead of dealing - * with it symbolically. Apalache finds out which sets have to be expanded - * by static analysis. - *) -Expand(S) == S - -(** - * A hint to the model checker to replace its argument Cardinality(S) >= k - * with a series of existential quantifiers for a constant k. - * Similar to Skolem, this has to be done carefully. Apalache automatically - * places this hint by static analysis. - *) -ConstCardinality(cardExpr) == cardExpr - -(** - * The folding operator, used to implement computation over a set. - * Apalache implements a more efficient encoding than the one below. - * (from the community modules). - *) -RECURSIVE FoldSet(_,_,_) -FoldSet( Op(_,_), v, S ) == IF S = {} - THEN v - ELSE LET w == CHOOSE x \in S: TRUE - IN LET T == S \ {w} - IN FoldSet( Op, Op(v,w), T ) - -(** - * The folding operator, used to implement computation over a sequence. - * Apalache implements a more efficient encoding than the one below. - * (from the community modules). - *) -RECURSIVE FoldSeq(_,_,_) -FoldSeq( Op(_,_), v, seq ) == IF seq = <<>> - THEN v - ELSE FoldSeq( Op, Op(v,Head(seq)), Tail(seq) ) - -=============================================================================== diff --git a/spec/consensus/proposer-based-timestamp/tla/MC_PBT.tla b/spec/consensus/proposer-based-timestamp/tla/MC_PBT.tla deleted file mode 100644 index 53f7336fb..000000000 --- a/spec/consensus/proposer-based-timestamp/tla/MC_PBT.tla +++ /dev/null @@ -1,77 +0,0 @@ ------------------------------ MODULE MC_PBT ------------------------------- -CONSTANT - \* @type: ROUND -> PROCESS; - Proposer - -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 - -\* time-related variables -VARIABLES - \* @type: PROCESS -> TIME; - localClock, \* a process local clock: Corr -> Ticks - \* @type: TIME; - realTime \* a reference Newtonian real time - -\* 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 VALUE message - \* @type: <> -> TIME; - inspectedProposal \* used to keep track when a process tries to receive a message - -\* 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 - - -INSTANCE TendermintPBT_002_draft WITH - Corr <- {"c1", "c2"}, - Faulty <- {"f3", "f4"}, - N <- 4, - T <- 1, - ValidValues <- { "v0", "v1" }, - InvalidValues <- {"v2"}, - MaxRound <- 5, - MaxTimestamp <- 10, - MinTimestamp <- 2, - Delay <- 2, - Precision <- 2 - -\* run Apalache with --cinit=CInit -CInit == \* the proposer is arbitrary -- works for safety - Proposer \in [Rounds -> AllProcs] - -============================================================================= diff --git a/spec/consensus/proposer-based-timestamp/tla/TendermintPBT_002_draft.tla b/spec/consensus/proposer-based-timestamp/tla/TendermintPBT_002_draft.tla index 983c7351b..8a8fbd5de 100644 --- a/spec/consensus/proposer-based-timestamp/tla/TendermintPBT_002_draft.tla +++ b/spec/consensus/proposer-based-timestamp/tla/TendermintPBT_002_draft.tla @@ -5,11 +5,10 @@ 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. + * Version 1. 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 @@ -39,11 +38,13 @@ 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 + Precision, \* clock precision: the maximal difference between two local clocks + \* @type: TIME; + Accuracy, \* clock accuracy: the maximal difference between a local clock and the real time + \* @type: Bool; + ClockDrift \* is there clock drift between the local clocks and the global clock ASSUME(N = Cardinality(Corr \union Faulty)) @@ -65,39 +66,24 @@ 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 +Proposals == Values \X Timestamps \* @type: PROPOSAL; -NilProposal == <> +NilProposal == <> \* @type: Set(VALUE); ValuesOrNil == Values \union {NilValue} \* @type: Set(DECISION); -Decisions == Proposals \X Rounds +Decisions == Values \X Timestamps \X Rounds \* @type: DECISION; -NilDecision == <> +NilDecision == <> + -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 +\* @type: (VALUE) => Bool; +IsValid(v) == v \in ValidValues \* the two thresholds that are used in the algorithm \* @type: Int; @@ -105,24 +91,23 @@ 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 +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 +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 ) +(********************* TYPE ANNOTATIONS FOR APALACHE **************************) + +\* a type annotation for an empty set of messages +\* @type: Set(MESSAGE); +EmptyMsgSet == {} + +\* @type: Set(RCVPROP); +EmptyRcvProp == {} + +\* @type: Set(PROCESS); +EmptyProcSet == {} (********************* PROTOCOL STATE VARIABLES ******************************) VARIABLES @@ -136,15 +121,11 @@ VARIABLES lockedValue, \* a locked value \* @type: PROCESS -> ROUND; lockedRound, \* a locked round - \* @type: PROCESS -> PROPOSAL; + \* @type: PROCESS -> VALUE; validValue, \* a valid value \* @type: PROCESS -> ROUND; validRound \* a valid round -coreVars == - <> - \* time-related variables VARIABLES \* @type: PROCESS -> TIME; @@ -152,8 +133,6 @@ VARIABLES \* @type: TIME; realTime \* a reference Newtonian real time -temporalVars == <> - \* book-keeping variables VARIABLES \* @type: ROUND -> Set(PROPMESSAGE); @@ -166,35 +145,28 @@ VARIABLES 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); + \* @type: Set(RCVPROP); receivedTimelyProposal, \* used to keep track when a process receives a timely PROPOSAL message - \* @type: <> -> 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 == - <> - -\* Invariant support -VARIABLES - \* @type: ROUND -> TIME; - beginRound, \* the minimum of the local clocks at the time any process entered a new round + \* @type: ROUND -> Set(PROCESS); + inspectedProposal, \* used to keep track when a process tries to receive a message + \* @type: TIME; + beginConsensus, \* the minimum of the local clocks in the initial state \* @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: TIME; + lastBeginConsensus, \* the maximum of the local clocks in the initial state \* @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 == - <> - (* to see a type invariant, check TendermintAccInv3 *) + +\* a handy definition used in UNCHANGED +vars == <> (********************* PROTOCOL INITIALIZATION ******************************) \* @type: (ROUND) => Set(PROPMESSAGE); @@ -283,37 +255,30 @@ BenignRoundsInMessages(msgfun) == \* 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)] + /\ \/ /\ ~ClockDrift + /\ localClock \in [Corr -> 0..Accuracy] + \/ /\ ClockDrift + /\ localClock = [p \in Corr |-> 0] /\ 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] + /\ validValue = [p \in Corr |-> NilValue] /\ 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] + /\ receivedTimelyProposal = EmptyRcvProp + /\ inspectedProposal = [r \in Rounds |-> EmptyProcSet] /\ BenignRoundsInMessages(msgsPropose) /\ BenignRoundsInMessages(msgsPrevote) /\ BenignRoundsInMessages(msgsPrecommit) - /\ evidence = {} + /\ evidence = EmptyMsgSet /\ action' = "Init" - /\ beginRound = - [r \in Rounds |-> - IF r = 0 - THEN Min({localClock[p] : p \in Corr}) - ELSE MaxTimestamp - ] + /\ beginConsensus = Min({localClock[p] : p \in Corr}) /\ endConsensus = [p \in Corr |-> NilTimestamp] - /\ lastBeginRound = - [r \in Rounds |-> - IF r = 0 - THEN Max({localClock[p] : p \in Corr}) - ELSE NilTimestamp - ] + /\ lastBeginConsensus = Max({localClock[p] : p \in Corr}) /\ proposalTime = [r \in Rounds |-> NilTimestamp] /\ proposalReceivedTime = [r \in Rounds |-> NilTimestamp] @@ -331,7 +296,7 @@ BroadcastProposal(pSrc, pRound, pProposal, pValidRound) == validRound |-> pValidRound ] IN - /\ msgsPropose' = [msgsPropose EXCEPT ![pRound] = msgsPropose[pRound] \union {newMsg}] + msgsPropose' = [msgsPropose EXCEPT ![pRound] = msgsPropose[pRound] \union {newMsg}] \* @type: (PROCESS, ROUND, PROPOSAL) => Bool; BroadcastPrevote(pSrc, pRound, pId) == @@ -345,7 +310,7 @@ BroadcastPrevote(pSrc, pRound, pId) == id |-> pId ] IN - /\ msgsPrevote' = [msgsPrevote EXCEPT ![pRound] = msgsPrevote[pRound] \union {newMsg}] + msgsPrevote' = [msgsPrevote EXCEPT ![pRound] = msgsPrevote[pRound] \union {newMsg}] \* @type: (PROCESS, ROUND, PROPOSAL) => Bool; BroadcastPrecommit(pSrc, pRound, pId) == @@ -359,7 +324,7 @@ BroadcastPrecommit(pSrc, pRound, pId) == id |-> pId ] IN - /\ msgsPrecommit' = [msgsPrecommit EXCEPT ![pRound] = msgsPrecommit[pRound] \union {newMsg}] + msgsPrecommit' = [msgsPrecommit EXCEPT ![pRound] = msgsPrecommit[pRound] \union {newMsg}] (***************************** TIME **************************************) @@ -374,14 +339,14 @@ SynchronizedLocalClocks == /\ localClock[q] - localClock[p] < Precision \* [PBTS-PROPOSE.0] -\* @type: (VALUE, TIME, ROUND) => PROPOSAL; -Proposal(v, t, r) == - <> +\* @type: (VALUE, TIME) => PROPOSAL; +Proposal(v, t) == + <> \* [PBTS-DECISION-ROUND.0] -\* @type: (PROPOSAL, ROUND) => DECISION; -Decision(p, r) == - <> +\* @type: (VALUE, TIME, ROUND) => DECISION; +Decision(v, t, r) == + <> (**************** MESSAGE PROCESSING TRANSITIONS *************************) \* lines 12-13 @@ -389,10 +354,7 @@ Decision(p, r) == 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])] + /\ step' = [step EXCEPT ![p] = "PROPOSE"] \* lines 14-19, a proposal may be sent later \* @type: (PROCESS) => Bool; @@ -403,22 +365,20 @@ InsertProposal(p) == \* 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 + LET value == + IF validValue[p] /= NilValue THEN validValue[p] - ELSE Proposal(v, localClock[p], r) + ELSE v + IN LET + proposal == Proposal(value, localClock[p]) IN - /\ BroadcastProposal(p, r, proposal, validRound[p]) + /\ BroadcastProposal(p, round[p], proposal, validRound[p]) /\ proposalTime' = [proposalTime EXCEPT ![r] = realTime] - /\ UNCHANGED <> - /\ UNCHANGED - <<(*msgsPropose,*) msgsPrevote, msgsPrecommit, - evidence, receivedTimelyProposal, inspectedProposal>> - /\ UNCHANGED - <> + /\ UNCHANGED <> /\ action' = "InsertProposal" \* a new action used to filter messages that are not on time @@ -434,120 +394,92 @@ ReceiveProposal(p) == type |-> "PROPOSAL", src |-> Proposer[round[p]], round |-> round[p], - proposal |-> Proposal(v, t, r), + proposal |-> Proposal(v, t), 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 <> - /\ UNCHANGED <> - /\ UNCHANGED - <> - /\ UNCHANGED - <> + /\ p \notin inspectedProposal[r] + /\ <> \notin receivedTimelyProposal + /\ inspectedProposal' = [inspectedProposal EXCEPT ![r] = @ \union {p}] + /\ \/ /\ localClock[p] - Precision < t + /\ t < localClock[p] + Precision + Delay + /\ receivedTimelyProposal' = receivedTimelyProposal \union {<>} + /\ \/ /\ proposalReceivedTime[r] = NilTimestamp + /\ proposalReceivedTime' = [proposalReceivedTime EXCEPT ![r] = realTime] + \/ /\ proposalReceivedTime[r] /= NilTimestamp + /\ UNCHANGED proposalReceivedTime + \/ /\ \/ localClock[p] - Precision >= t + \/ t >= localClock[p] + Precision + Delay + /\ UNCHANGED <> + /\ UNCHANGED <> /\ 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, + src |-> Proposer[round[p]], + round |-> round[p], + proposal |-> Proposal(v, t), validRound |-> NilRound ] IN - /\ msg \in receivedTimelyProposal[p] \* updated line 22 + /\ <> \in receivedTimelyProposal \* updated line 22 /\ evidence' = {msg} \union evidence /\ LET mid == (* line 23 *) - IF IsValid(prop) /\ (lockedRound[p] = NilRound \/ lockedValue[p] = v) - THEN Id(prop) + IF IsValid(v) /\ (lockedRound[p] = NilRound \/ lockedValue[p] = v) + THEN Id(Proposal(v, t)) ELSE NilProposal IN - BroadcastPrevote(p, r, mid) \* lines 24-26 + BroadcastPrevote(p, round[p], mid) \* lines 24-26 /\ step' = [step EXCEPT ![p] = "PREVOTE"] - /\ UNCHANGED <> - /\ UNCHANGED - <> - /\ UNCHANGED - <> + /\ UNCHANGED <> /\ 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 + \E v \in Values, t1 \in Timestamps, t2 \in Timestamps, vr \in Rounds: + /\ step[p] = "PROPOSE" /\ 0 <= vr /\ vr < round[p] \* line 28, the while part + /\ LET \* @type: PROPMESSAGE; msg == [ type |-> "PROPOSAL", - src |-> Proposer[r], - round |-> r, - proposal |-> prop, + src |-> Proposer[round[p]], + round |-> round[p], + proposal |-> Proposal(v, t1), 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 + /\ <> \in receivedTimelyProposal \* updated line 28 + /\ LET PV == { m \in msgsPrevote[vr]: m.id = Id(Proposal(v, t2)) } 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) + IF IsValid(v) /\ (lockedRound[p] <= vr \/ lockedValue[p] = v) + THEN Id(Proposal(v, t1)) ELSE NilProposal IN - BroadcastPrevote(p, r, mid) \* lines 24-26 + BroadcastPrevote(p, round[p], mid) \* lines 24-26 /\ step' = [step EXCEPT ![p] = "PREVOTE"] - /\ UNCHANGED <> - /\ UNCHANGED - <> - /\ UNCHANGED - <> + /\ UNCHANGED <> /\ action' = "UponProposalInProposeAndPrevote" \* lines 34-35 + lines 61-64 (onTimeoutPrevote) @@ -562,13 +494,10 @@ UponQuorumOfPrevotesAny(p) == /\ evidence' = MyEvidence \union evidence /\ BroadcastPrecommit(p, round[p], NilProposal) /\ step' = [step EXCEPT ![p] = "PRECOMMIT"] - /\ UNCHANGED <> - /\ UNCHANGED - <> - /\ UNCHANGED - <> + /\ UNCHANGED <> /\ action' = "UponQuorumOfPrevotesAny" \* lines 36-46 @@ -576,47 +505,36 @@ UponQuorumOfPrevotesAny(p) == \* @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, + src |-> Proposer[round[p]], + round |-> round[p], + proposal |-> Proposal(v, t), 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 + /\ <> \in receivedTimelyProposal \* updated line 36 + /\ LET PV == { m \in msgsPrevote[round[p]]: m.id = Id(Proposal(v, t)) } 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)) + /\ lockedRound' = [lockedRound EXCEPT ![p] = round[p]] + /\ BroadcastPrecommit(p, round[p], Id(Proposal(v, t))) /\ step' = [step EXCEPT ![p] = "PRECOMMIT"] ELSE UNCHANGED <> \* lines 42-43 - /\ validValue' = [validValue EXCEPT ![p] = prop] - /\ validRound' = [validRound EXCEPT ![p] = r] - /\ UNCHANGED <> - /\ UNCHANGED - <> - /\ UNCHANGED - <> + /\ validValue' = [validValue EXCEPT ![p] = v] + /\ validRound' = [validRound EXCEPT ![p] = round[p]] + /\ UNCHANGED <> /\ action' = "UponProposalInPrevoteOrCommitAndPrevote" \* lines 47-48 + 65-67 (onTimeoutPrecommit) @@ -629,17 +547,11 @@ UponQuorumOfPrecommitsAny(p) == /\ 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 - <> + /\ StartRound(p, round[p] + 1) + /\ UNCHANGED <> /\ action' = "UponQuorumOfPrecommitsAny" \* lines 49-54 @@ -647,11 +559,7 @@ UponQuorumOfPrecommitsAny(p) == \* @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 + /\ \E v \in ValidValues, t \in Timestamps (* line 50*) , r \in Rounds, vr \in RoundsOrNil: /\ LET \* @type: PROPMESSAGE; msg == @@ -659,30 +567,24 @@ UponProposalInPrecommitNoDecision(p) == type |-> "PROPOSAL", src |-> Proposer[r], round |-> r, - proposal |-> prop, + proposal |-> Proposal(v, t), 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 + /\ p \in inspectedProposal[r] + /\ LET PV == { m \in msgsPrecommit[r]: m.id = Id(Proposal(v, t)) } IN /\ Cardinality(PV) >= THRESHOLD2 \* line 49 /\ evidence' = PV \union {msg} \union evidence - /\ decision' = [decision EXCEPT ![p] = Decision(prop, r)] \* update the decision, line 51 + /\ decision' = [decision EXCEPT ![p] = Decision(v, t, round[p])] \* 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 - <> - /\ UNCHANGED - <> - /\ UNCHANGED - <> + /\ UNCHANGED <> /\ action' = "UponProposalInPrecommitNoDecision" \* the actions below are not essential for safety, but added for completeness @@ -694,13 +596,10 @@ OnTimeoutPropose(p) == /\ p /= Proposer[round[p]] /\ BroadcastPrevote(p, round[p], NilProposal) /\ step' = [step EXCEPT ![p] = "PREVOTE"] - /\ UNCHANGED <> - /\ UNCHANGED - <> - /\ UNCHANGED - <> + /\ UNCHANGED <> /\ action' = "OnTimeoutPropose" \* lines 44-46 @@ -712,13 +611,10 @@ OnQuorumOfNilPrevotes(p) == /\ evidence' = PV \union evidence /\ BroadcastPrecommit(p, round[p], Id(NilProposal)) /\ step' = [step EXCEPT ![p] = "PRECOMMIT"] - /\ UNCHANGED <> - /\ UNCHANGED - <> - /\ UNCHANGED - <> + /\ UNCHANGED <> /\ action' = "OnQuorumOfNilPrevotes" \* lines 55-56 @@ -731,16 +627,10 @@ OnRoundCatchup(p) == /\ 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 - <> + /\ UNCHANGED <> /\ action' = "OnRoundCatchup" @@ -748,24 +638,28 @@ OnRoundCatchup(p) == \* 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 <> + /\ realTime < MaxTimestamp + /\ realTime' = realTime + 1 + /\ \/ /\ ~ClockDrift + /\ localClock' = [p \in Corr |-> localClock[p] + 1] + \/ /\ ClockDrift + /\ UNCHANGED localClock + /\ UNCHANGED <> /\ 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 <> -\* /\ UNCHANGED realTime -\* /\ action' = "AdvanceLocalClock" +\* advance the local clock of node p +\* @type: (PROCESS) => Bool; +AdvanceLocalClock(p) == + /\ localClock[p] < MaxTimestamp + /\ localClock' = [localClock EXCEPT ![p] = @ + 1] + /\ UNCHANGED <> + /\ action' = "AdvanceLocalClock" \* process timely messages \* @type: (PROCESS) => Bool; @@ -790,8 +684,10 @@ MessageProcessing(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 == +Next == \/ AdvanceRealTime + \/ /\ ClockDrift + /\ \E p \in Corr: AdvanceLocalClock(p) \/ /\ SynchronizedLocalClocks /\ \E p \in Corr: MessageProcessing(p) @@ -804,62 +700,59 @@ 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) + => \E v \in ValidValues, t1 \in Timestamps, t2 \in Timestamps, r1 \in Rounds, r2 \in Rounds : + /\ decision[p] = Decision(v, t1, r1) + /\ decision[q] = Decision(v, t2, r2) + +\* [PBTS-INV-TIME-AGR.0] +AgreementOnTime == + \A p, q \in Corr: + \A v1 \in ValidValues, v2 \in ValidValues, t1 \in Timestamps, t2 \in Timestamps, r \in Rounds : + /\ decision[p] = Decision(v1, t1, r) + /\ decision[q] = Decision(v2, t2, r) + => t1 = t2 \* [PBTS-CONSENSUS-TIME-VALID.0] ConsensusTimeValid == - \A p \in Corr: + \A p \in Corr, t \in Timestamps : \* 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) + (\E v \in ValidValues, r \in Rounds : decision[p] = Decision(v, t, r)) \* then - \* TODO: consider tighter bound where beginRound[pr] is replaced - \* w/ MedianOfRound[pr] - => (/\ beginRound[pr] - Precision - Delay <= t - /\ t <= endConsensus[p] + Precision) + => /\ beginConsensus - Precision <= t + /\ t < endConsensus[p] + Precision + Delay \* [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] + \A v \in ValidValues, t \in Timestamps : + \* if the proposer in the first round is correct + (/\ Proposer[0] \in Corr + \* and there exists a process that decided on v, t + /\ \E p \in Corr, r \in Rounds : decision[p] = Decision(v, t, r)) + \* then t is between the minimal and maximal initial local time + => /\ beginConsensus <= t + /\ t <= lastBeginConsensus \* [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) + \A t \in Timestamps, r \in Rounds : + (/\ \E p \in Corr, v \in ValidValues : decision[p] = Decision(v, t, r) + /\ proposalTime[r] /= NilTimestamp) + => /\ proposalTime[r] - Accuracy < t + /\ t < proposalTime[r] + Accuracy \* [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 + (\E p \in Corr, v \in ValidValues : decision[p] = Decision(v, t, r)) + => /\ proposalReceivedTime[r] - Accuracy - Precision < t + /\ t < proposalReceivedTime[r] + Accuracy + Precision + Delay \* [PBTS-MSG-FAIR.0] BoundedDelay == \A r \in Rounds : (/\ proposalTime[r] /= NilTimestamp /\ proposalTime[r] + Delay < realTime) - => \A p \in Corr: inspectedProposal[r,p] /= NilTimestamp + => inspectedProposal[r] = Corr \* [PBTS-CONSENSUS-TIME-LIVE.0] ConsensusTimeLive == @@ -868,18 +761,19 @@ ConsensusTimeLive == /\ proposalTime[r] + Delay < realTime /\ Proposer[r] \in Corr /\ round[p] <= r) - => \E msg \in RoundProposals(r) : msg \in receivedTimelyProposal[p] + => \E msg \in RoundProposals(r) : <> \in receivedTimelyProposal \* a conjunction of all invariants Inv == /\ AgreementOnValue + /\ AgreementOnTime /\ ConsensusTimeValid /\ ConsensusSafeValidCorrProp - \* /\ ConsensusRealTimeValid - \* /\ ConsensusRealTimeValidCorr - \* /\ BoundedDelay + /\ ConsensusRealTimeValid + /\ ConsensusRealTimeValidCorr + /\ BoundedDelay -\* Liveness == -\* ConsensusTimeLive +Liveness == + ConsensusTimeLive ============================================================================= diff --git a/spec/consensus/proposer-based-timestamp/tla/typedefs.tla b/spec/consensus/proposer-based-timestamp/tla/typedefs.tla index 72e76df54..cfa5d941a 100644 --- a/spec/consensus/proposer-based-timestamp/tla/typedefs.tla +++ b/spec/consensus/proposer-based-timestamp/tla/typedefs.tla @@ -7,8 +7,9 @@ @typeAlias: ACTION = Str; @typeAlias: TRACE = Seq(Str); @typeAlias: TIME = Int; - @typeAlias: PROPOSAL = <>; - @typeAlias: DECISION = <>; + @typeAlias: PROPOSAL = <>; + @typeAlias: DECISION = <>; + @typeAlias: RCVPROP = <>; @typeAlias: PROPMESSAGE = [ type: STEP,