diff --git a/PaxosCommit.tla b/PaxosCommit.tla new file mode 100644 index 0000000..37a2e9e --- /dev/null +++ b/PaxosCommit.tla @@ -0,0 +1,287 @@ +----------------------------- MODULE PaxosCommit ---------------------------- +(***************************************************************************) +(* This specification is discussed in "Paxos Commit", Lecture 6 of the *) +(* TLA+ Video Course. *) +(* *) +(* This module specifies the Paxos Commit algorithm. We specify only *) +(* safety properties, not liveness properties. We simplify the *) +(* specification in the following ways. *) +(* *) +(* - As in the specification of module TwoPhase, and for the same *) +(* reasons, we let the variable msgs be the set of all messages that *) +(* have ever been sent. If a message is sent to a set of recipients, *) +(* only one copy of the message appears in msgs. *) +(* *) +(* - We do not explicitly model the receipt of messages. If an *) +(* operation can be performed when a process has received a certain set *) +(* of messages, then the operation is represented by an action that is *) +(* enabled when those messages are in the set msgs of sent messages. *) +(* (We are specifying only safety properties, which assert what events *) +(* can occur, and the operation can occur if the messages that enable *) +(* it have been sent.) *) +(* *) +(* - We do not model leader selection. We define actions that the *) +(* current leader may perform, but do not specify who performs them. *) +(* *) +(* As in the specification of Two-Phase commit in module TwoPhase, we have *) +(* RMs spontaneously issue Prepared messages and we ignore Prepare *) +(* messages. *) +(***************************************************************************) +EXTENDS Integers + +Maximum(S) == + (*************************************************************************) + (* If S is a set of numbers, then this define Maximum(S) to be the *) + (* maximum of those numbers, or -1 if S is empty. *) + (*************************************************************************) + IF S = {} THEN -1 + ELSE CHOOSE n \in S : \A m \in S : n \geq m + +CONSTANT RM, \* The set of resource managers. + Acceptor, \* The set of acceptors. + Majority, \* The set of majorities of acceptors + Ballot \* The set of ballot numbers + +(***************************************************************************) +(* We assume the following properties of the declared constants. *) +(***************************************************************************) +ASSUME + /\ Ballot \subseteq Nat + /\ 0 \in Ballot + /\ Majority \subseteq SUBSET Acceptor + /\ \A MS1, MS2 \in Majority : MS1 \cap MS2 # {} + (********************************************************************) + (* All we assume about the set Majority of majorities is that any *) + (* two majorities have non-empty intersection. *) + (********************************************************************) + +Messages == + (*************************************************************************) + (* The set of all possible messages. There are messages of type *) + (* "Commit" and "Abort" to announce the decision, as well as messages *) + (* for each phase of each instance of ins of the Paxos consensus *) + (* algorithm. The acc field indicates the sender of a message from an *) + (* acceptor to the leader; messages from a leader are broadcast to all *) + (* acceptors. *) + (*************************************************************************) + [type : {"phase1a"}, ins : RM, bal : Ballot \ {0}] + \cup + [type : {"phase1b"}, ins : RM, mbal : Ballot, bal : Ballot \cup {-1}, + val : {"prepared", "aborted", "none"}, acc : Acceptor] + \cup + [type : {"phase2a"}, ins : RM, bal : Ballot, val : {"prepared", "aborted"}] + \cup + [type : {"phase2b"}, acc : Acceptor, ins : RM, bal : Ballot, + val : {"prepared", "aborted"}] + \cup + [type : {"Commit", "Abort"}] +----------------------------------------------------------------------------- +VARIABLES + rmState, \* rmState[r] is the state of resource manager r. + aState, \* aState[ins][ac] is the state of acceptor ac for instance + \* ins of the Paxos algorithm. + msgs \* The set of all messages ever sent. + +PCTypeOK == + (*************************************************************************) + (* The type-correctness invariant. Each acceptor maintains the values *) + (* mbal, bal, and val for each instance of the Paxos consensus *) + (* algorithm. *) + (*************************************************************************) + /\ rmState \in [RM -> {"working", "prepared", "committed", "aborted"}] + /\ aState \in [RM -> [Acceptor -> [mbal : Ballot, + bal : Ballot \cup {-1}, + val : {"prepared", "aborted", "none"}]]] + /\ msgs \subseteq Messages + +PCInit == \* The initial predicate. + /\ rmState = [r \in RM |-> "working"] + /\ aState = [r \in RM |-> + [ac \in Acceptor + |-> [mbal |-> 0, bal |-> -1, val |-> "none"]]] + /\ msgs = {} +----------------------------------------------------------------------------- +(***************************************************************************) +(* THE ACTIONS *) +(***************************************************************************) +Send(m) == msgs' = msgs \cup {m} + (*************************************************************************) + (* An action expression that describes the sending of message m. *) + (*************************************************************************) +----------------------------------------------------------------------------- +(***************************************************************************) +(* RM ACTIONS *) +(***************************************************************************) +RMPrepare(r) == + (*************************************************************************) + (* Resource manager r prepares by sending a phase 2a message for ballot *) + (* number 0 with value "prepared". *) + (*************************************************************************) + /\ rmState[r] = "working" + /\ rmState' = [rmState EXCEPT ![r] = "prepared"] + /\ Send([type |-> "phase2a", ins |-> r, bal |-> 0, val |-> "prepared"]) + /\ UNCHANGED aState + +RMChooseToAbort(r) == + (*************************************************************************) + (* Resource manager r spontaneously decides to abort. It may (but need *) + (* not) send a phase 2a message for ballot number 0 with value *) + (* "aborted". *) + (*************************************************************************) + /\ rmState[r] = "working" + /\ rmState' = [rmState EXCEPT ![r] = "aborted"] + /\ Send([type |-> "phase2a", ins |-> r, bal |-> 0, val |-> "aborted"]) + /\ UNCHANGED aState + +RMRcvCommitMsg(r) == + (*************************************************************************) + (* Resource manager r is told by the leader to commit. When this action *) + (* is enabled, rmState[r] must equal either "prepared" or "committed". *) + (* In the latter case, the action leaves the state unchanged (it is a *) + (* ``stuttering step''). *) + (*************************************************************************) + /\ [type |-> "Commit"] \in msgs + /\ rmState' = [rmState EXCEPT ![r] = "committed"] + /\ UNCHANGED <> + +RMRcvAbortMsg(r) == + (*************************************************************************) + (* Resource manager r is told by the leader to abort. It could be in *) + (* any state except "committed". *) + (*************************************************************************) + /\ [type |-> "Abort"] \in msgs + /\ rmState' = [rmState EXCEPT ![r] = "aborted"] + /\ UNCHANGED <> +----------------------------------------------------------------------------- +(***************************************************************************) +(* LEADER ACTIONS *) +(* *) +(* The following actions are performed by any process that believes itself *) +(* to be the current leader. Since leader selection is not assumed to be *) +(* reliable, multiple processes could simultaneously consider themselves *) +(* to be the leader. *) +(***************************************************************************) +Phase1a(bal, r) == + (*************************************************************************) + (* If the leader times out without learning that a decision has been *) + (* reached on resource manager r's prepare/abort decision, it can *) + (* perform this action to initiate a new ballot bal. (Sending duplicate *) + (* phase 1a messages is harmless.) *) + (*************************************************************************) + /\ Send([type |-> "phase1a", ins |-> r, bal |-> bal]) + /\ UNCHANGED <> + +Phase2a(bal, r) == + (*************************************************************************) + (* The action in which a leader sends a phase 2a message with ballot *) + (* bal > 0 in instance r, if it has received phase 1b messages for *) + (* ballot number bal from a majority of acceptors. If the leader *) + (* received a phase 1b message from some acceptor that had sent a phase *) + (* 2b message for this instance, then maxbal \geq 0 and the value val *) + (* the leader sends is determined by the phase 1b messages. (If *) + (* val = "prepared", then r must have prepared.) Otherwise, maxbal = -1 *) + (* and the leader sends the value "aborted". *) + (* *) + (* The first conjunct asserts that the action is disabled if any commit *) + (* leader has already sent a phase 2a message with ballot number bal. *) + (* In practice, this is implemented by having ballot numbers partitioned *) + (* among potential leaders, and having a leader record in stable storage *) + (* the largest ballot number for which it sent a phase 2a message. *) + (*************************************************************************) + /\ ~\E m \in msgs : /\ m.type = "phase2a" + /\ m.bal = bal + /\ m.ins = r + /\ \E MS \in Majority : + LET mset == {m \in msgs : /\ m.type = "phase1b" + /\ m.ins = r + /\ m.mbal = bal + /\ m.acc \in MS} + maxbal == Maximum({m.bal : m \in mset}) + val == IF maxbal = -1 + THEN "aborted" + ELSE (CHOOSE m \in mset : m.bal = maxbal).val + IN /\ \A ac \in MS : \E m \in mset : m.acc = ac + /\ Send([type |-> "phase2a", ins |-> r, bal |-> bal, val |-> val]) + /\ UNCHANGED <> + +PCDecide == + (*************************************************************************) + (* A leader can decide that Paxos Commit has reached a result and send a *) + (* message announcing the result if it has received the necessary phase *) + (* 2b messages. *) + (*************************************************************************) + /\ LET Decided(r, v) == + (****************************************************************) + (* True iff instance r of the Paxos consensus algorithm has *) + (* chosen the value v. *) + (****************************************************************) + \E b \in Ballot, MS \in Majority : + \A ac \in MS : [type |-> "phase2b", ins |-> r, + bal |-> b, val |-> v, acc |-> ac ] \in msgs + IN \/ /\ \A r \in RM : Decided(r, "prepared") + /\ Send([type |-> "Commit"]) + \/ /\ \E r \in RM : Decided(r, "aborted") + /\ Send([type |-> "Abort"]) + /\ UNCHANGED <> +----------------------------------------------------------------------------- +(***************************************************************************) +(* ACCEPTOR ACTIONS *) +(***************************************************************************) +Phase1b(acc) == + \E m \in msgs : + /\ m.type = "phase1a" + /\ aState[m.ins][acc].mbal < m.bal + /\ aState' = [aState EXCEPT ![m.ins][acc].mbal = m.bal] + /\ Send([type |-> "phase1b", + ins |-> m.ins, + mbal |-> m.bal, + bal |-> aState[m.ins][acc].bal, + val |-> aState[m.ins][acc].val, + acc |-> acc]) + /\ UNCHANGED rmState + +Phase2b(acc) == + /\ \E m \in msgs : + /\ m.type = "phase2a" + /\ aState[m.ins][acc].mbal \leq m.bal + /\ aState' = [aState EXCEPT ![m.ins][acc].mbal = m.bal, + ![m.ins][acc].bal = m.bal, + ![m.ins][acc].val = m.val] + /\ Send([type |-> "phase2b", ins |-> m.ins, bal |-> m.bal, + val |-> m.val, acc |-> acc]) + /\ UNCHANGED rmState +----------------------------------------------------------------------------- +PCNext == \* The next-state action + \/ \E r \in RM : \/ RMPrepare(r) + \/ RMChooseToAbort(r) + \/ RMRcvCommitMsg(r) + \/ RMRcvAbortMsg(r) + \/ \E bal \in Ballot \ {0}, r \in RM : Phase1a(bal, r) \/ Phase2a(bal, r) + \/ PCDecide + \/ \E acc \in Acceptor : Phase1b(acc) \/ Phase2b(acc) +----------------------------------------------------------------------------- +(***************************************************************************) +(* The following part of the spec is not covered in Lecture 7. It will be *) +(* explained in Lecture 8. *) +(***************************************************************************) +PCSpec == PCInit /\ [][PCNext]_<> + (*************************************************************************) + (* The complete spec of the Paxos Commit protocol. *) + (*************************************************************************) + +THEOREM PCSpec => []PCTypeOK +----------------------------------------------------------------------------- +(***************************************************************************) +(* We now assert that the Paxos Commit protocol implements the transaction *) +(* commit protocol of module TCommit. The following statement imports *) +(* into the current module the definitions from module TCommit, including *) +(* the definition of TCSpec. *) +(***************************************************************************) + +INSTANCE TCommit + +THEOREM PCSpec => TCSpec +============================================================================= +\* Modification History +\* Last modified Fri Dec 28 12:36:26 CET 2018 by veitheller +\* Created Fri Dec 28 12:01:42 CET 2018 by veitheller