From c42c6d06d2986791ad1cb8742824818edd9b6323 Mon Sep 17 00:00:00 2001 From: "M. J. Fromberger" Date: Wed, 2 Mar 2022 06:08:39 -0800 Subject: [PATCH] Migration of TLA+ files from the spec repo (#8004) (#8018) Co-authored-by: Kukovec --- .../proposer-based-timestamp/tla/Apalache.tla | 109 ++++ .../proposer-based-timestamp/tla/MC_PBT.tla | 77 +++ .../tla/TendermintPBT_002_draft.tla | 540 +++++++++++------- .../proposer-based-timestamp/tla/typedefs.tla | 5 +- 4 files changed, 511 insertions(+), 220 deletions(-) create mode 100644 spec/consensus/proposer-based-timestamp/tla/Apalache.tla create mode 100644 spec/consensus/proposer-based-timestamp/tla/MC_PBT.tla diff --git a/spec/consensus/proposer-based-timestamp/tla/Apalache.tla b/spec/consensus/proposer-based-timestamp/tla/Apalache.tla new file mode 100644 index 000000000..044bff666 --- /dev/null +++ b/spec/consensus/proposer-based-timestamp/tla/Apalache.tla @@ -0,0 +1,109 @@ +--------------------------- 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 new file mode 100644 index 000000000..53f7336fb --- /dev/null +++ b/spec/consensus/proposer-based-timestamp/tla/MC_PBT.tla @@ -0,0 +1,77 @@ +----------------------------- 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 8a8fbd5de..983c7351b 100644 --- a/spec/consensus/proposer-based-timestamp/tla/TendermintPBT_002_draft.tla +++ b/spec/consensus/proposer-based-timestamp/tla/TendermintPBT_002_draft.tla @@ -5,10 +5,11 @@ the Tendermint TLA+ specification for fork accountability: https://github.com/tendermint/spec/blob/master/spec/light-client/accountability/TendermintAcc_004_draft.tla - * Version 1. A preliminary specification. + * 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 @@ -38,13 +39,11 @@ CONSTANTS \* @type: TIME; MaxTimestamp, \* the maximal value of the clock tick \* @type: TIME; - Delay, \* message delay + MinTimestamp, \* the minimal value of the clock tick \* @type: TIME; - Precision, \* clock precision: the maximal difference between two local clocks + Delay, \* message delay \* @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 + Precision \* clock precision: the maximal difference between two local clocks ASSUME(N = Cardinality(Corr \union Faulty)) @@ -66,24 +65,39 @@ 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 +Proposals == Values \X Timestamps \X Rounds \* @type: PROPOSAL; -NilProposal == <> +NilProposal == <> \* @type: Set(VALUE); ValuesOrNil == Values \union {NilValue} \* @type: Set(DECISION); -Decisions == Values \X Timestamps \X Rounds +Decisions == Proposals \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: (VALUE) => Bool; -IsValid(v) == v \in ValidValues +\* @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; @@ -91,23 +105,24 @@ 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) == CHOOSE x \in S : \A y \in S : x <= y +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) == CHOOSE x \in S : \A y \in S : y <= x - -(********************* TYPE ANNOTATIONS FOR APALACHE **************************) - -\* a type annotation for an empty set of messages -\* @type: Set(MESSAGE); -EmptyMsgSet == {} - -\* @type: Set(RCVPROP); -EmptyRcvProp == {} +Max(S) == FoldSet( Max2, NilTimestamp, S ) +\* Max(S) == CHOOSE x \in S : \A y \in S : y <= x -\* @type: Set(PROCESS); -EmptyProcSet == {} +\* @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 @@ -121,11 +136,15 @@ VARIABLES lockedValue, \* a locked value \* @type: PROCESS -> ROUND; lockedRound, \* a locked round - \* @type: PROCESS -> VALUE; + \* @type: PROCESS -> PROPOSAL; validValue, \* a valid value \* @type: PROCESS -> ROUND; validRound \* a valid round +coreVars == + <> + \* time-related variables VARIABLES \* @type: PROCESS -> TIME; @@ -133,6 +152,8 @@ VARIABLES \* @type: TIME; realTime \* a reference Newtonian real time +temporalVars == <> + \* book-keeping variables VARIABLES \* @type: ROUND -> Set(PROPMESSAGE); @@ -145,28 +166,35 @@ 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: Set(RCVPROP); + \* @type: PROCESS -> Set(PROPMESSAGE); receivedTimelyProposal, \* used to keep track when a process receives a timely PROPOSAL message - \* @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: <> -> 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: PROCESS -> TIME; endConsensus, \* the local time when a decision is made - \* @type: TIME; - lastBeginConsensus, \* the maximum of the local clocks in the initial state + \* @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 == + <> + (* to see a type invariant, check TendermintAccInv3 *) - -\* a handy definition used in UNCHANGED -vars == <> (********************* PROTOCOL INITIALIZATION ******************************) \* @type: (ROUND) => Set(PROPMESSAGE); @@ -255,30 +283,37 @@ BenignRoundsInMessages(msgfun) == \* The initial states of the protocol. Some faults can be in the system already. Init == /\ round = [p \in Corr |-> 0] - /\ \/ /\ ~ClockDrift - /\ localClock \in [Corr -> 0..Accuracy] - \/ /\ ClockDrift - /\ localClock = [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 |-> NilValue] + /\ 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 = EmptyRcvProp - /\ inspectedProposal = [r \in Rounds |-> EmptyProcSet] + /\ receivedTimelyProposal = [p \in Corr |-> {}] + /\ inspectedProposal = [r \in Rounds, p \in Corr |-> NilTimestamp] /\ BenignRoundsInMessages(msgsPropose) /\ BenignRoundsInMessages(msgsPrevote) /\ BenignRoundsInMessages(msgsPrecommit) - /\ evidence = EmptyMsgSet + /\ evidence = {} /\ action' = "Init" - /\ beginConsensus = Min({localClock[p] : p \in Corr}) + /\ beginRound = + [r \in Rounds |-> + IF r = 0 + THEN Min({localClock[p] : p \in Corr}) + ELSE MaxTimestamp + ] /\ endConsensus = [p \in Corr |-> NilTimestamp] - /\ lastBeginConsensus = Max({localClock[p] : p \in Corr}) + /\ 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] @@ -296,7 +331,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) == @@ -310,7 +345,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) == @@ -324,7 +359,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 **************************************) @@ -339,14 +374,14 @@ SynchronizedLocalClocks == /\ localClock[q] - localClock[p] < Precision \* [PBTS-PROPOSE.0] -\* @type: (VALUE, TIME) => PROPOSAL; -Proposal(v, t) == - <> +\* @type: (VALUE, TIME, ROUND) => PROPOSAL; +Proposal(v, t, r) == + <> \* [PBTS-DECISION-ROUND.0] -\* @type: (VALUE, TIME, ROUND) => DECISION; -Decision(v, t, r) == - <> +\* @type: (PROPOSAL, ROUND) => DECISION; +Decision(p, r) == + <> (**************** MESSAGE PROCESSING TRANSITIONS *************************) \* lines 12-13 @@ -354,7 +389,10 @@ Decision(v, t, 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"] + /\ 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; @@ -365,20 +403,22 @@ 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 value == - IF validValue[p] /= NilValue + LET proposal == + IF validValue[p] /= NilProposal THEN validValue[p] - ELSE v - IN LET - proposal == Proposal(value, localClock[p]) + ELSE Proposal(v, localClock[p], r) IN - /\ BroadcastProposal(p, round[p], proposal, validRound[p]) + /\ BroadcastProposal(p, r, proposal, validRound[p]) /\ proposalTime' = [proposalTime EXCEPT ![r] = realTime] - /\ UNCHANGED <> + /\ UNCHANGED <> + /\ UNCHANGED + <<(*msgsPropose,*) msgsPrevote, msgsPrecommit, + evidence, receivedTimelyProposal, inspectedProposal>> + /\ UNCHANGED + <> /\ action' = "InsertProposal" \* a new action used to filter messages that are not on time @@ -394,92 +434,120 @@ ReceiveProposal(p) == type |-> "PROPOSAL", src |-> Proposer[round[p]], round |-> round[p], - proposal |-> Proposal(v, t), + proposal |-> Proposal(v, t, r), validRound |-> NilRound ] IN /\ msg \in msgsPropose[round[p]] - /\ 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 <> + /\ 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 + <> /\ 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[round[p]], - round |-> round[p], - proposal |-> Proposal(v, t), + src |-> Proposer[r], + round |-> r, + proposal |-> prop, validRound |-> NilRound ] IN - /\ <> \in receivedTimelyProposal \* updated line 22 + /\ msg \in receivedTimelyProposal[p] \* updated line 22 /\ evidence' = {msg} \union evidence /\ LET mid == (* line 23 *) - IF IsValid(v) /\ (lockedRound[p] = NilRound \/ lockedValue[p] = v) - THEN Id(Proposal(v, t)) + IF IsValid(prop) /\ (lockedRound[p] = NilRound \/ lockedValue[p] = v) + THEN Id(prop) ELSE NilProposal IN - BroadcastPrevote(p, round[p], mid) \* lines 24-26 + BroadcastPrevote(p, r, 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, t1 \in Timestamps, t2 \in Timestamps, vr \in Rounds: - /\ step[p] = "PROPOSE" /\ 0 <= vr /\ vr < round[p] \* line 28, the while part - /\ LET + \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[round[p]], - round |-> round[p], - proposal |-> Proposal(v, t1), + src |-> Proposer[r], + round |-> r, + proposal |-> prop, validRound |-> vr ] IN - /\ <> \in receivedTimelyProposal \* updated line 28 - /\ LET PV == { m \in msgsPrevote[vr]: m.id = Id(Proposal(v, t2)) } 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(v) /\ (lockedRound[p] <= vr \/ lockedValue[p] = v) - THEN Id(Proposal(v, t1)) + IF IsValid(prop) /\ (lockedRound[p] <= vr \/ lockedValue[p] = v) + THEN Id(prop) ELSE NilProposal IN - BroadcastPrevote(p, round[p], mid) \* lines 24-26 + BroadcastPrevote(p, r, mid) \* lines 24-26 /\ step' = [step EXCEPT ![p] = "PREVOTE"] - /\ UNCHANGED <> + /\ UNCHANGED <> + /\ UNCHANGED + <> + /\ UNCHANGED + <> /\ action' = "UponProposalInProposeAndPrevote" \* lines 34-35 + lines 61-64 (onTimeoutPrevote) @@ -494,10 +562,13 @@ 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 @@ -505,36 +576,47 @@ 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[round[p]], - round |-> round[p], - proposal |-> Proposal(v, t), + src |-> Proposer[r], + round |-> r, + proposal |-> prop, validRound |-> vr ] IN - /\ <> \in receivedTimelyProposal \* updated line 36 - /\ LET PV == { m \in msgsPrevote[round[p]]: m.id = Id(Proposal(v, t)) } 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] = round[p]] - /\ BroadcastPrecommit(p, round[p], Id(Proposal(v, t))) + /\ lockedRound' = [lockedRound EXCEPT ![p] = r] + /\ BroadcastPrecommit(p, r, Id(prop)) /\ step' = [step EXCEPT ![p] = "PRECOMMIT"] ELSE UNCHANGED <> \* lines 42-43 - /\ validValue' = [validValue EXCEPT ![p] = v] - /\ validRound' = [validRound EXCEPT ![p] = round[p]] - /\ UNCHANGED <> + /\ validValue' = [validValue EXCEPT ![p] = prop] + /\ validRound' = [validRound EXCEPT ![p] = r] + /\ UNCHANGED <> + /\ UNCHANGED + <> + /\ UNCHANGED + <> /\ action' = "UponProposalInPrevoteOrCommitAndPrevote" \* lines 47-48 + 65-67 (onTimeoutPrecommit) @@ -547,11 +629,17 @@ UponQuorumOfPrecommitsAny(p) == /\ Cardinality(Committers) >= THRESHOLD2 \* line 47 /\ evidence' = MyEvidence \union evidence /\ round[p] + 1 \in Rounds - /\ StartRound(p, round[p] + 1) - /\ UNCHANGED <> + /\ StartRound(p, round[p] + 1) + /\ UNCHANGED temporalVars + /\ UNCHANGED + <<(*beginRound,*) endConsensus, (*lastBeginRound,*) + proposalTime, proposalReceivedTime>> + /\ UNCHANGED + <<(*round, step,*) decision, lockedValue, + lockedRound, validValue, validRound>> + /\ UNCHANGED + <> /\ action' = "UponQuorumOfPrecommitsAny" \* lines 49-54 @@ -559,7 +647,11 @@ UponQuorumOfPrecommitsAny(p) == \* @type: (PROCESS) => Bool; UponProposalInPrecommitNoDecision(p) == /\ decision[p] = NilDecision \* line 49 - /\ \E v \in ValidValues, t \in Timestamps (* line 50*) , r \in Rounds, vr \in RoundsOrNil: + /\ \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 == @@ -567,24 +659,30 @@ UponProposalInPrecommitNoDecision(p) == type |-> "PROPOSAL", src |-> Proposer[r], round |-> r, - proposal |-> Proposal(v, t), + proposal |-> prop, validRound |-> vr ] IN /\ msg \in msgsPropose[r] \* line 49 - /\ p \in inspectedProposal[r] - /\ LET PV == { m \in msgsPrecommit[r]: m.id = Id(Proposal(v, t)) } IN + /\ 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(v, t, round[p])] \* update the decision, line 51 + /\ 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 <> + /\ UNCHANGED temporalVars + /\ UNCHANGED + <> + /\ UNCHANGED + <> + /\ UNCHANGED + <> /\ action' = "UponProposalInPrecommitNoDecision" \* the actions below are not essential for safety, but added for completeness @@ -596,10 +694,13 @@ 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 @@ -611,10 +712,13 @@ 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 @@ -627,10 +731,16 @@ OnRoundCatchup(p) == /\ Cardinality(Faster) >= THRESHOLD1 /\ evidence' = MyEvidence \union evidence /\ StartRound(p, r) - /\ UNCHANGED <> + /\ UNCHANGED temporalVars + /\ UNCHANGED + <<(*beginRound,*) endConsensus, (*lastBeginRound,*) + proposalTime, proposalReceivedTime>> + /\ UNCHANGED + <<(*round, step,*) decision, lockedValue, + lockedRound, validValue, validRound>> + /\ UNCHANGED + <> /\ action' = "OnRoundCatchup" @@ -638,28 +748,24 @@ OnRoundCatchup(p) == \* advance the global clock \* @type: Bool; AdvanceRealTime == - /\ realTime < MaxTimestamp - /\ realTime' = realTime + 1 - /\ \/ /\ ~ClockDrift - /\ localClock' = [p \in Corr |-> localClock[p] + 1] - \/ /\ ClockDrift - /\ UNCHANGED localClock - /\ UNCHANGED <> + /\ ValidTime(realTime) + /\ \E t \in Timestamps: + /\ t > realTime + /\ realTime' = t + /\ localClock' = [p \in Corr |-> localClock[p] + (t - realTime)] + /\ UNCHANGED <> /\ action' = "AdvanceRealTime" -\* advance the local clock of node p -\* @type: (PROCESS) => Bool; -AdvanceLocalClock(p) == - /\ localClock[p] < MaxTimestamp - /\ localClock' = [localClock EXCEPT ![p] = @ + 1] - /\ UNCHANGED <> - /\ action' = "AdvanceLocalClock" +\* 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" \* process timely messages \* @type: (PROCESS) => Bool; @@ -684,10 +790,8 @@ 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) @@ -700,59 +804,62 @@ AgreementOnValue == \A p, q \in Corr: /\ decision[p] /= NilDecision /\ decision[q] /= NilDecision - => \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 + => \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, t \in Timestamps : + \A p \in Corr: \* if a process decides on v and t - (\E v \in ValidValues, r \in Rounds : decision[p] = Decision(v, t, r)) + \E v \in ValidValues, t \in Timestamps, pr \in Rounds, dr \in Rounds : + decision[p] = Decision(Proposal(v,t,pr), dr) \* then - => /\ beginConsensus - Precision <= t - /\ t < endConsensus[p] + Precision + Delay + \* 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, 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 + \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 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 + \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 : decision[p] = Decision(v, t, r)) - => /\ proposalReceivedTime[r] - Accuracy - Precision < t - /\ t < proposalReceivedTime[r] + Accuracy + Precision + Delay + (\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) - => inspectedProposal[r] = Corr + => \A p \in Corr: inspectedProposal[r,p] /= NilTimestamp \* [PBTS-CONSENSUS-TIME-LIVE.0] ConsensusTimeLive == @@ -761,19 +868,18 @@ ConsensusTimeLive == /\ proposalTime[r] + Delay < realTime /\ Proposer[r] \in Corr /\ round[p] <= r) - => \E msg \in RoundProposals(r) : <> \in receivedTimelyProposal + => \E msg \in RoundProposals(r) : msg \in receivedTimelyProposal[p] \* 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 cfa5d941a..72e76df54 100644 --- a/spec/consensus/proposer-based-timestamp/tla/typedefs.tla +++ b/spec/consensus/proposer-based-timestamp/tla/typedefs.tla @@ -7,9 +7,8 @@ @typeAlias: ACTION = Str; @typeAlias: TRACE = Seq(Str); @typeAlias: TIME = Int; - @typeAlias: PROPOSAL = <>; - @typeAlias: DECISION = <>; - @typeAlias: RCVPROP = <>; + @typeAlias: PROPOSAL = <>; + @typeAlias: DECISION = <>; @typeAlias: PROPMESSAGE = [ type: STEP,