From 8df2b24e6af31ff3fdff9687182738f5cc61ff5f Mon Sep 17 00:00:00 2001 From: nolouch Date: Mon, 29 Oct 2018 16:14:42 +0800 Subject: [PATCH 1/4] add joint consensus --- JointConsensus/JointConsensus.tla | 540 ++++++++++++++++++ .../JointConsensus___ConfigCheck.launch | 62 ++ RaftMerge/RaftMerge.tla | 2 +- 3 files changed, 603 insertions(+), 1 deletion(-) create mode 100644 JointConsensus/JointConsensus.tla create mode 100644 JointConsensus/JointConsensus.toolbox/JointConsensus___ConfigCheck.launch diff --git a/JointConsensus/JointConsensus.tla b/JointConsensus/JointConsensus.tla new file mode 100644 index 0000000..fb1ee94 --- /dev/null +++ b/JointConsensus/JointConsensus.tla @@ -0,0 +1,540 @@ +--------------------------------- MODULE JointConsensus --------------------------------- +\* This is the formal specification for the Raft consensus algorithm. +\* +\* Copyright 2014 Diego Ongaro. +\* This work is licensed under the Creative Commons Attribution-4.0 +\* International License https://creativecommons.org/licenses/by/4.0/ + +EXTENDS Naturals, FiniteSets, Sequences, TLC + +\* The set of server IDs +CONSTANTS InitialServers, NewServers + +CONSTANTS ValueEntry,ConfigEntry + +\* Servers states. +CONSTANTS Follower, Candidate, Leader + +\* A reserved value. +CONSTANTS Nil + +\* Message types: +CONSTANTS RequestVoteRequest, RequestVoteResponse, + AppendEntriesRequest, AppendEntriesResponse + + +\* Maximum number of client requests +CONSTANTS MaxClientRequests + +---- +\* Global variables + +\* A bag of records representing requests and responses sent from one server +\* to another. TLAPS doesn't support the Bags module, so this is a function +\* mapping Message to Nat. +VARIABLE messages + +\* A history variable used in the proof. This would not be present in an +\* implementation. +\* Keeps track of successful elections, including the initial logs of the +\* leader and voters' logs. Set of functions containing various things about +\* successful elections (see BecomeLeader). +VARIABLE elections + +\* Servers list all known servers. +VARIABLE allServers + +\* The members of the server at that time. +VARIABLE votersOfServer + +nodeVars == <> +---- +\* The following variables are all per server (functions with domain Servers). + +\* The server's term number. +VARIABLE currentTerm +\* The server's state (Follower, Candidate, or Leader). +VARIABLE state +\* The candidate the server voted for in its current term, or +\* Nil if it hasn't voted for any. +VARIABLE votedFor +serverVars == <> + +\* The set of requests that can go into the log +VARIABLE clientRequests + +\* A Sequence of log entries. The index into this sequence is the index of the +\* log entry. Unfortunately, the Sequence module defines Head(s) as the entry +\* with index 1, so be careful not to use that! +VARIABLE log +\* The index of the latest entry in the log the state machine may apply. +VARIABLE commitIndex +\* The index that gets committed +VARIABLE committedLog +\* Does the commited Index decrease +VARIABLE committedLogDecrease +logVars == <> + +\* The following variables are used only on candidates: +\* The set of servers from which the candidate has received a RequestVote +\* response in its currentTerm. +VARIABLE votesResponded +\* The set of servers from which the candidate has received a vote in its +\* currentTerm. +VARIABLE votesGranted +\* A history variable used in the proof. This would not be present in an +\* implementation. +\* Function from each server that voted for this candidate in its currentTerm +\* to that voter's log. +VARIABLE voterLog +candidateVars == <> + +\* The following variables are used only on leaders: +\* The next entry to send to each follower. +VARIABLE nextIndex +\* The latest entry that each follower has acknowledged is the same as the +\* leader's. This is used to calculate commitIndex on the leader. +VARIABLE matchIndex +leaderVars == <> + +\* End of per server variables. +---- + +\* All variables; used for stuttering (asserting state hasn't changed). +vars == <> + +---- +\* Helpers + +\* The set of all quorums. This just calculates simple majorities, but the only +\* important property is that every quorum overlaps with every other. +Quorum(Server) == {i \in SUBSET(Server) : Cardinality(i) * 2 > Cardinality(Server)} + +\* The term of the last entry in a log, or 0 if the log is empty. +LastTerm(xlog) == IF Len(xlog) = 0 THEN 0 ELSE xlog[Len(xlog)].term + +\* Send a message. +Send(m) == messages' = messages \cup {m} + +\* Remove a message from the set of messages. Used when a server is done +\* processing a message. +Discard(m) == messages' = messages \ {m} + +\* Combination of Send and Discard. +Reply(reply, request) == messages' = (messages \cup {reply}) \ {request} + +\* Return the minimum value from a set, or undefined if the set is empty. +Min(s) == CHOOSE x \in s : \A y \in s : x <= y +\* Return the maximum value from a set, or undefined if the set is empty. +Max(s) == CHOOSE x \in s : \A y \in s : x >= y + +\* Get the maximum config from log[1..l]. +GetMaxConfigIndex(i, l) == + LET chonfigIndexes == {index \in 1..l: log[i][index].type = ConfigEntry} + IN IF chonfigIndexes = {} THEN 0 + ELSE Max(chonfigIndexes) +\* Get the latest config in all log of server i. +GetLatestConfig(i) == + LET length == Len(log[i]) + maxIndex == GetMaxConfigIndex(i, length) + IN IF maxIndex = 0 THEN InitialServers + ELSE log[i][maxIndex].value +\* Get the latest commit config of server i. +GetLatestCommitConfig(i) == + LET length == commitIndex[i] + maxIndex == GetMaxConfigIndex(i, length) + IN IF maxIndex = 0 THEN InitialServers + ELSE log[i][maxIndex].value + +---- +\* Define initial values for all variables +InitHistoryVars == /\ elections = {} + /\ voterLog = [i \in allServers |-> [j \in {} |-> <<>>]] + +InitServerVars == /\ allServers = InitialServers \cup NewServers + /\ currentTerm = [i \in allServers |-> 1] + /\ state = [i \in allServers |-> Follower] + /\ votedFor = [i \in allServers |-> Nil] + /\ votersOfServer = + LET initalVoters == InitialServers + newVoters == (InitialServers \cup NewServers) \ InitialServers + IN [i \in initalVoters |-> initalVoters] @@ [i \in newVoters |-> {}] + +InitCandidateVars == /\ votesResponded = [i \in allServers |-> {}] + /\ votesGranted = [i \in allServers |-> {}] +\* The values nextIndex[i][i] and matchIndex[i][i] are never read, since the +\* leader does not send itself messages. It's still easier to include these +\* in the functions. +InitLeaderVars == /\ nextIndex = [i \in allServers |-> [j \in allServers |-> 1]] + /\ matchIndex = [i \in allServers |-> [j \in allServers |-> 0]] +InitLogVars == /\ log = [i \in allServers |-> << >>] + /\ commitIndex = [i \in allServers |-> 0] + /\ clientRequests = 1 + /\ committedLog = << >> + /\ committedLogDecrease = FALSE +Init == /\ messages = {} + /\ InitServerVars + /\ InitHistoryVars + /\ InitServerVars + /\ InitCandidateVars + /\ InitLeaderVars + /\ InitLogVars + +---- +\* Servers i times out and starts a new election. +Timeout(i) == /\ state[i] \in {Follower, Candidate} + /\ state' = [state EXCEPT ![i] = Candidate] + /\ currentTerm' = [currentTerm EXCEPT ![i] = currentTerm[i] + 1] + \* Most implementations would probably just set the local vote + \* atomically, but messaging localhost for it is weaker. + /\ votedFor' = [votedFor EXCEPT ![i] = Nil] + /\ votesResponded' = [votesResponded EXCEPT ![i] = {}] + /\ votesGranted' = [votesGranted EXCEPT ![i] = {}] + /\ voterLog' = [voterLog EXCEPT ![i] = [j \in {} |-> <<>>]] + /\ UNCHANGED <> + +\* Candidate i sends j a RequestVote request. +RequestVote(i, j) == + /\ j \in votersOfServer[i] + /\ state[i] = Candidate + /\ j \notin votesResponded[i] + /\ Send([mtype |-> RequestVoteRequest, + mterm |-> currentTerm[i], + mlastLogTerm |-> LastTerm(log[i]), + mlastLogIndex |-> Len(log[i]), + msource |-> i, + mdest |-> j]) + /\ UNCHANGED <> + +\* Leader i sends j an AppendEntries request containing up to 1 entry. +\* While implementations may want to send more than 1 at a time, this spec uses +\* just 1 because it minimizes atomic regions without loss of generality. +AppendEntries(i, j) == + /\ i /= j + /\ state[i] = Leader + /\ j \in votersOfServer[i] + /\ LET prevLogIndex == nextIndex[i][j] - 1 + prevLogTerm == IF prevLogIndex > 0 THEN + log[i][prevLogIndex].term + ELSE + 0 + \* Send up to 1 entry, constrained by the end of the log. + lastEntry == Min({Len(log[i]), nextIndex[i][j]}) + entries == SubSeq(log[i], nextIndex[i][j], lastEntry) + IN /\ Len(entries) > 0 /\ matchIndex[i][j] < Len(log[i]) + /\ Send([mtype |-> AppendEntriesRequest, + mterm |-> currentTerm[i], + mprevLogIndex |-> prevLogIndex, + mprevLogTerm |-> prevLogTerm, + mentries |-> entries, + mcommitIndex |-> Min({commitIndex[i], lastEntry}), + msource |-> i, + mdest |-> j]) + /\ UNCHANGED <> + +\* Candidate i transitions to leader. +BecomeLeader(i) == + /\ state[i] = Candidate + /\ votesGranted[i] \in Quorum(votersOfServer[i]) + /\ state' = [state EXCEPT ![i] = Leader] + /\ nextIndex' = [nextIndex EXCEPT ![i] = + [j \in allServers |-> Len(log[i]) + 1]] + /\ matchIndex' = [matchIndex EXCEPT ![i] = + [j \in allServers |-> 0]] + /\ elections' = elections \cup + {[eterm |-> currentTerm[i], + eleader |-> i, + elog |-> log[i], + evotes |-> votesGranted[i], + evoterLog |-> voterLog[i]]} + /\ UNCHANGED <> + +\* Leader i receives a client request to add v to the log. +ClientRequest(i) == + /\ state[i] = Leader + /\ clientRequests < MaxClientRequests + /\ LET entry == [term |-> currentTerm[i], + type |-> ValueEntry, + value |-> clientRequests] + newLog == Append(log[i], entry) + IN /\ log' = [log EXCEPT ![i] = newLog] + /\ clientRequests' = clientRequests + 1 + /\ UNCHANGED <> + +\* Leader i advances its commitIndex. +\* This is done as a separate step from handling AppendEntries responses, +\* in part to minimize atomic regions, and in part so that leaders of +\* single-server clusters are able to mark entries committed. +AdvanceCommitIndex(i) == + /\ state[i] = Leader + /\ LET \* The set of servers that agree up through index. + Agree(index) == {i} \cup {k \in allServers : + matchIndex[i][k] >= index} + \* The maximum indexes for which a quorum agrees + agreeIndexes == {index \in 1..Len(log[i]) : + Agree(index) \in Quorum(votersOfServer[i])} + \* New value for commitIndex'[i] + newCommitIndex == + IF /\ agreeIndexes /= {} + /\ log[i][Max(agreeIndexes)].term = currentTerm[i] + THEN + Max(agreeIndexes) + ELSE + commitIndex[i] + newCommittedLog == + IF newCommitIndex > 1 + THEN + [j \in 1..newCommitIndex |-> log[i][j]] + ELSE + <<>> + IN /\ commitIndex' = [commitIndex EXCEPT ![i] = newCommitIndex] + /\ committedLogDecrease' = \/ ( newCommitIndex < Len(committedLog)) + \/ \E j \in 1..Len(committedLog) : committedLog[j] /= newCommittedLog[j] + /\ committedLog' = newCommittedLog + /\ UNCHANGED <> + +AdvanceCommitConfig(i) == + /\ GetMaxConfigIndex(i,commitIndex[i]) > 0 + /\ LET config == GetLatestCommitConfig(i) + IN IF votersOfServer[i] /= config.newConf + THEN /\ \/ \* leader not in the new configuration. + \* switch to Follwer. + /\ i \notin config.newConf + /\ state[i] = Leader + /\ state' = [state EXCEPT ![i] = Follower] + \/ /\ i \in config.newConf + /\ UNCHANGED <> + /\ votersOfServer' = [ votersOfServer EXCEPT ![i] = config.newConf] + ELSE UNCHANGED <> + /\ UNCHANGED <> + + +\* Leader i add a group servers to cluster. +SetNodes(i, newNodes) == + /\ state[i] = Leader + /\ \* for reducing the state space, just verify once. + Len(SelectSeq(log[i], LAMBDA logEntry : logEntry.type = ConfigEntry)) = 0 + /\ LET oldConfig == votersOfServer[i] + entry == [term |-> currentTerm[i], + type |-> ConfigEntry, + newConf |-> newNodes, + oldConf |-> oldConfig] + transitionConfig == oldConfig \cup newNodes + newLog == Append(log[i], entry) + IN /\ log' = [log EXCEPT ![i] = newLog] + /\ votersOfServer = [votersOfServer EXCEPT ![i] = transitionConfig] + /\ UNCHANGED <> + +---- +\* Message handlers +\* i = recipient, j = sender, m = message + +\* Server i receives a RequestVote request from server j with +\* m.mterm <= currentTerm[i]. +HandleRequestVoteRequest(i, j, m) == + LET logOk == \/ m.mlastLogTerm > LastTerm(log[i]) + \/ /\ m.mlastLogTerm = LastTerm(log[i]) + /\ m.mlastLogIndex >= Len(log[i]) + grant == /\ m.mterm = currentTerm[i] + /\ logOk + /\ votedFor[i] \in {Nil, j} + IN /\ m.mterm <= currentTerm[i] + /\ \/ grant /\ votedFor' = [votedFor EXCEPT ![i] = j] + \/ ~grant /\ UNCHANGED votedFor + /\ Reply([mtype |-> RequestVoteResponse, + mterm |-> currentTerm[i], + mvoteGranted |-> grant, + \* mlog is used just for the `elections' history variable for + \* the proof. It would not exist in a real implementation. + mlog |-> log[i], + msource |-> i, + mdest |-> j], + m) + /\ UNCHANGED <> + +\* Server i receives a RequestVote response from server j with +\* m.mterm = currentTerm[i]. +HandleRequestVoteResponse(i, j, m) == + \* This tallies votes even when the current state is not Candidate, but + \* they won't be looked at, so it doesn't matter. + /\ m.mterm = currentTerm[i] + /\ votesResponded' = [votesResponded EXCEPT ![i] = + votesResponded[i] \cup {j}] + /\ \/ /\ m.mvoteGranted + /\ votesGranted' = [votesGranted EXCEPT ![i] = + votesGranted[i] \cup {j}] + /\ voterLog' = [voterLog EXCEPT ![i] = + voterLog[i] @@ (j :> m.mlog)] + \/ /\ ~m.mvoteGranted + /\ UNCHANGED <> + /\ Discard(m) + /\ UNCHANGED <> + +\* Server i receives an AppendEntries request from server j with +\* m.mterm <= currentTerm[i]. This just handles m.entries of length 0 or 1, but +\* implementations could safely accept more by treating them the same as +\* multiple independent requests of 1 entry. +HandleAppendEntriesRequest(i, j, m) == + LET logOk == \/ m.mprevLogIndex = 0 + \/ /\ m.mprevLogIndex > 0 + /\ m.mprevLogIndex <= Len(log[i]) + /\ m.mprevLogTerm = log[i][m.mprevLogIndex].term + IN /\ m.mterm <= currentTerm[i] + /\ \/ /\ \* reject request + \/ m.mterm < currentTerm[i] + \/ /\ m.mterm = currentTerm[i] + /\ state[i] = Follower + /\ \lnot logOk + /\ Reply([mtype |-> AppendEntriesResponse, + mterm |-> currentTerm[i], + msuccess |-> FALSE, + mmatchIndex |-> 0, + msource |-> i, + mdest |-> j], + m) + /\ UNCHANGED <> + \/ \* return to follower state + /\ m.mterm = currentTerm[i] + /\ state[i] = Candidate + /\ state' = [state EXCEPT ![i] = Follower] + /\ UNCHANGED <> + \/ \* accept request + /\ m.mterm = currentTerm[i] + /\ state[i] = Follower + /\ logOk + /\ LET index == m.mprevLogIndex + 1 + IN \/ \* already done with request + /\ \/ m.mentries = << >> + \/ m.mentries /= << >> + /\ Len(log[i]) >= index + /\ log[i][index].term = m.mentries[1].term + \* This could make our commitIndex decrease (for + \* example if we process an old, duplicated request), + \* but that doesn't really affect anything. + /\ commitIndex' = [commitIndex EXCEPT ![i] = + m.mcommitIndex] + /\ Reply([mtype |-> AppendEntriesResponse, + mterm |-> currentTerm[i], + msuccess |-> TRUE, + mmatchIndex |-> m.mprevLogIndex + + Len(m.mentries), + msource |-> i, + mdest |-> j], + m) + /\ UNCHANGED <> + \/ \* conflict: remove 1 entry + /\ m.mentries /= << >> + /\ Len(log[i]) >= index + /\ log[i][index].term /= m.mentries[1].term + /\ LET new == [index2 \in 1..(Len(log[i]) - 1) |-> + log[i][index2]] + IN log' = [log EXCEPT ![i] = new] + /\ UNCHANGED <> + \/ \* no conflict: append entry + /\ m.mentries /= << >> + /\ Len(log[i]) = m.mprevLogIndex + /\ log' = [log EXCEPT ![i] = + Append(log[i], m.mentries[1])] + /\ UNCHANGED <> + /\ UNCHANGED <> + +\* Servers i receives an AppendEntries response from server j with +\* m.mterm = currentTerm[i]. +HandleAppendEntriesResponse(i, j, m) == + /\ m.mterm = currentTerm[i] + /\ \/ /\ m.msuccess \* successful + /\ nextIndex' = [nextIndex EXCEPT ![i][j] = m.mmatchIndex + 1] + /\ matchIndex' = [matchIndex EXCEPT ![i][j] = m.mmatchIndex] + \/ /\ \lnot m.msuccess \* not successful + /\ nextIndex' = [nextIndex EXCEPT ![i][j] = + Max({nextIndex[i][j] - 1, 1})] + /\ UNCHANGED <> + /\ Discard(m) + /\ UNCHANGED <> + +\* Any RPC with a newer term causes the recipient to advance its term first. +UpdateTerm(i, j, m) == + /\ m.mterm > currentTerm[i] + /\ currentTerm' = [currentTerm EXCEPT ![i] = m.mterm] + /\ state' = [state EXCEPT ![i] = Follower] + /\ votedFor' = [votedFor EXCEPT ![i] = Nil] + \* messages is unchanged so m can be processed further. + /\ UNCHANGED <> + +\* Responses with stale terms are ignored. +DropStaleResponse(i, j, m) == + /\ m.mterm < currentTerm[i] + /\ Discard(m) + /\ UNCHANGED <> + +\* Receive a message. +Receive(m) == + LET i == m.mdest + j == m.msource + IN \* Any RPC with a newer term causes the recipient to advance + \* its term first. Responses with stale terms are ignored. + \/ UpdateTerm(i, j, m) + \/ /\ m.mtype = RequestVoteRequest + /\ HandleRequestVoteRequest(i, j, m) + \/ /\ m.mtype = RequestVoteResponse + /\ \/ DropStaleResponse(i, j, m) + \/ HandleRequestVoteResponse(i, j, m) + \/ /\ m.mtype = AppendEntriesRequest + /\ HandleAppendEntriesRequest(i, j, m) + \/ /\ m.mtype = AppendEntriesResponse + /\ \/ DropStaleResponse(i, j, m) + \/ HandleAppendEntriesResponse(i, j, m) + +\* End of message handlers. +---- +\* Defines how the variables may transition. +Next == + \* Leader election + \/ \E i,j \in allServers : RequestVote(i, j) + \/ \E i \in allServers : BecomeLeader(i) + \* Client request + \/ \E i \in allServers : ClientRequest(i) + \* Config changed with joint consensus + \/ \E i \in InitialServers: SetNodes(i, NewServers) + \* Log replica + \/ \E i \in allServers : AdvanceCommitIndex(i) + \/ \E i \in allServers : AdvanceCommitConfig(i) + \/ \E i,j \in allServers : AppendEntries(i, j) + \* Network + \/ \E m \in messages : Receive(m) + \/ \/ /\ \A i \in allServers : state[i] = Follower + /\ \E i \in allServers : Timeout(i) + \/ /\ \E i \in allServers : state[i] /= Follower + /\ UNCHANGED <> + + +\* The specification must start with the initial state and transition according +\* to Next. +Spec == Init /\ [][Next]_vars + +---- +\* The following are a set of verification. + +MoreThanOneLeader == + Cardinality({i \in allServers: state[i]=Leader}) > 1 + +TransitionPhaseChecker == + \A i \in allServers: LET inTransition == /\ commitIndex[i] < GetMaxConfigIndex(i,Len(log[i])) + /\ GetMaxConfigIndex(i,Len(log[i])) > 0 + configEntry == GetLatestConfig(i) + IN IF inTransition THEN + IF state[i] = Leader THEN + votersOfServer[i] = configEntry.oldConf \cup configEntry.newConf + ELSE votersOfServer[i] = configEntry.oldConf + ELSE TRUE +CommittedPhaseChecker == + \A i \in allServers: LET committed == /\ commitIndex[i] > 0 + /\ GetMaxConfigIndex(i,commitIndex[i]) > 0 + /\ commitIndex[i] > GetMaxConfigIndex(i,commitIndex[i]) + configEntry == GetLatestCommitConfig(i) + IN IF committed THEN + votersOfServer[i] = configEntry.newConf + ELSE TRUE + +=============================================================================== diff --git a/JointConsensus/JointConsensus.toolbox/JointConsensus___ConfigCheck.launch b/JointConsensus/JointConsensus.toolbox/JointConsensus___ConfigCheck.launch new file mode 100644 index 0000000..1e0e64b --- /dev/null +++ b/JointConsensus/JointConsensus.toolbox/JointConsensus___ConfigCheck.launch @@ -0,0 +1,62 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/RaftMerge/RaftMerge.tla b/RaftMerge/RaftMerge.tla index f9240b2..244c9b4 100644 --- a/RaftMerge/RaftMerge.tla +++ b/RaftMerge/RaftMerge.tla @@ -213,7 +213,7 @@ ClientRequest(i, r, log) == /\ LET new_logs == Append(raft[i][r].logs, log) new_match_index == [raft[i][r].match_index EXCEPT ![i] = @ + 1] - IN + IN /\ raft' = [raft EXCEPT ![i][r].logs = new_logs, ![i][r].match_index = new_match_index] /\ client_requests_index' = client_requests_index + 1 From 20e94038fb2ed3a3a91f2544d290bda0d3975d3d Mon Sep 17 00:00:00 2001 From: nolouch Date: Tue, 30 Oct 2018 10:11:41 +0800 Subject: [PATCH 2/4] fix --- JointConsensus/JointConsensus.tla | 159 +++++++++--------- .../JointConsensus___ConfigCheck.launch | 3 +- RaftMerge/RaftMerge.tla | 2 +- 3 files changed, 84 insertions(+), 80 deletions(-) diff --git a/JointConsensus/JointConsensus.tla b/JointConsensus/JointConsensus.tla index fb1ee94..b18e55f 100644 --- a/JointConsensus/JointConsensus.tla +++ b/JointConsensus/JointConsensus.tla @@ -21,7 +21,7 @@ CONSTANTS Nil \* Message types: CONSTANTS RequestVoteRequest, RequestVoteResponse, AppendEntriesRequest, AppendEntriesResponse - + \* Maximum number of client requests CONSTANTS MaxClientRequests @@ -45,9 +45,9 @@ VARIABLE elections VARIABLE allServers \* The members of the server at that time. -VARIABLE votersOfServer - -nodeVars == <> +VARIABLE voters +VARIABLE nextVoters +nodeVars == <> ---- \* The following variables are all per server (functions with domain Servers). @@ -58,7 +58,7 @@ VARIABLE state \* The candidate the server voted for in its current term, or \* Nil if it hasn't voted for any. VARIABLE votedFor -serverVars == <> +serverVars == <> \* The set of requests that can go into the log VARIABLE clientRequests @@ -95,6 +95,7 @@ VARIABLE nextIndex \* The latest entry that each follower has acknowledged is the same as the \* leader's. This is used to calculate commitIndex on the leader. VARIABLE matchIndex + leaderVars == <> \* End of per server variables. @@ -110,6 +111,13 @@ vars == <> \* important property is that every quorum overlaps with every other. Quorum(Server) == {i \in SUBSET(Server) : Cardinality(i) * 2 > Cardinality(Server)} +BothQuorum(old, new) == IF old /= {} /\ new /= {} THEN + {x[1] \cup x[2]: x \in (Quorum(old) \X Quorum(new))} + ELSE IF new = {} THEN + Quorum(old) + ELSE IF old = {} THEN + Quorum(new) + ELSE {} \* The term of the last entry in a log, or 0 if the log is empty. LastTerm(xlog) == IF Len(xlog) = 0 THEN 0 ELSE xlog[Len(xlog)].term @@ -138,28 +146,29 @@ GetLatestConfig(i) == LET length == Len(log[i]) maxIndex == GetMaxConfigIndex(i, length) IN IF maxIndex = 0 THEN InitialServers - ELSE log[i][maxIndex].value + ELSE log[i][maxIndex] \* Get the latest commit config of server i. GetLatestCommitConfig(i) == LET length == commitIndex[i] maxIndex == GetMaxConfigIndex(i, length) IN IF maxIndex = 0 THEN InitialServers - ELSE log[i][maxIndex].value + ELSE log[i][maxIndex] ---- \* Define initial values for all variables InitHistoryVars == /\ elections = {} /\ voterLog = [i \in allServers |-> [j \in {} |-> <<>>]] - + InitServerVars == /\ allServers = InitialServers \cup NewServers /\ currentTerm = [i \in allServers |-> 1] /\ state = [i \in allServers |-> Follower] /\ votedFor = [i \in allServers |-> Nil] - /\ votersOfServer = + /\ voters = LET initalVoters == InitialServers - newVoters == (InitialServers \cup NewServers) \ InitialServers - IN [i \in initalVoters |-> initalVoters] @@ [i \in newVoters |-> {}] - + newVoters == (InitialServers \cup NewServers) \ InitialServers + IN [i \in initalVoters |-> initalVoters] @@ [i \in newVoters |-> {}] + /\ nextVoters = [i \in allServers |-> {}] + InitCandidateVars == /\ votesResponded = [i \in allServers |-> {}] /\ votesGranted = [i \in allServers |-> {}] \* The values nextIndex[i][i] and matchIndex[i][i] are never read, since the @@ -167,11 +176,13 @@ InitCandidateVars == /\ votesResponded = [i \in allServers |-> {}] \* in the functions. InitLeaderVars == /\ nextIndex = [i \in allServers |-> [j \in allServers |-> 1]] /\ matchIndex = [i \in allServers |-> [j \in allServers |-> 0]] + InitLogVars == /\ log = [i \in allServers |-> << >>] /\ commitIndex = [i \in allServers |-> 0] /\ clientRequests = 1 /\ committedLog = << >> /\ committedLogDecrease = FALSE + Init == /\ messages = {} /\ InitServerVars /\ InitHistoryVars @@ -195,7 +206,7 @@ Timeout(i) == /\ state[i] \in {Follower, Candidate} \* Candidate i sends j a RequestVote request. RequestVote(i, j) == - /\ j \in votersOfServer[i] + /\ j \in (voters[i] \cup nextVoters[i]) /\ state[i] = Candidate /\ j \notin votesResponded[i] /\ Send([mtype |-> RequestVoteRequest, @@ -212,7 +223,7 @@ RequestVote(i, j) == AppendEntries(i, j) == /\ i /= j /\ state[i] = Leader - /\ j \in votersOfServer[i] + /\ j \in (voters[i] \cup nextVoters[i]) /\ LET prevLogIndex == nextIndex[i][j] - 1 prevLogTerm == IF prevLogIndex > 0 THEN log[i][prevLogIndex].term @@ -221,7 +232,7 @@ AppendEntries(i, j) == \* Send up to 1 entry, constrained by the end of the log. lastEntry == Min({Len(log[i]), nextIndex[i][j]}) entries == SubSeq(log[i], nextIndex[i][j], lastEntry) - IN /\ Len(entries) > 0 /\ matchIndex[i][j] < Len(log[i]) + IN /\ Len(entries) > 0 /\ matchIndex[i][j] < lastEntry /\ Send([mtype |-> AppendEntriesRequest, mterm |-> currentTerm[i], mprevLogIndex |-> prevLogIndex, @@ -235,8 +246,9 @@ AppendEntries(i, j) == \* Candidate i transitions to leader. BecomeLeader(i) == /\ state[i] = Candidate - /\ votesGranted[i] \in Quorum(votersOfServer[i]) + /\ votesGranted[i] \in BothQuorum(voters[i], nextVoters[i]) /\ state' = [state EXCEPT ![i] = Leader] + \*/\ PrintT(i \cup "became leader") /\ nextIndex' = [nextIndex EXCEPT ![i] = [j \in allServers |-> Len(log[i]) + 1]] /\ matchIndex' = [matchIndex EXCEPT ![i] = @@ -249,19 +261,6 @@ BecomeLeader(i) == evoterLog |-> voterLog[i]]} /\ UNCHANGED <> -\* Leader i receives a client request to add v to the log. -ClientRequest(i) == - /\ state[i] = Leader - /\ clientRequests < MaxClientRequests - /\ LET entry == [term |-> currentTerm[i], - type |-> ValueEntry, - value |-> clientRequests] - newLog == Append(log[i], entry) - IN /\ log' = [log EXCEPT ![i] = newLog] - /\ clientRequests' = clientRequests + 1 - /\ UNCHANGED <> - \* Leader i advances its commitIndex. \* This is done as a separate step from handling AppendEntries responses, \* in part to minimize atomic regions, and in part so that leaders of @@ -269,11 +268,11 @@ ClientRequest(i) == AdvanceCommitIndex(i) == /\ state[i] = Leader /\ LET \* The set of servers that agree up through index. - Agree(index) == {i} \cup {k \in allServers : + Agree(index) == {i} \cup {k \in (voters[i] \cup nextVoters[i]) : matchIndex[i][k] >= index} \* The maximum indexes for which a quorum agrees agreeIndexes == {index \in 1..Len(log[i]) : - Agree(index) \in Quorum(votersOfServer[i])} + Agree(index) \in BothQuorum(voters[i] ,nextVoters[i])} \* New value for commitIndex'[i] newCommitIndex == IF /\ agreeIndexes /= {} @@ -283,21 +282,24 @@ AdvanceCommitIndex(i) == ELSE commitIndex[i] newCommittedLog == - IF newCommitIndex > 1 + IF newCommitIndex >= 1 THEN [j \in 1..newCommitIndex |-> log[i][j]] ELSE <<>> - IN /\ commitIndex' = [commitIndex EXCEPT ![i] = newCommitIndex] + IN /\ commitIndex[i] /= newCommitIndex + /\ commitIndex' = [commitIndex EXCEPT ![i] = newCommitIndex] /\ committedLogDecrease' = \/ ( newCommitIndex < Len(committedLog)) \/ \E j \in 1..Len(committedLog) : committedLog[j] /= newCommittedLog[j] /\ committedLog' = newCommittedLog - /\ UNCHANGED <> + \*/\ PrintT(Len(log[i])\cup newCommitIndex) + /\ UNCHANGED <> -AdvanceCommitConfig(i) == +\* Leader i apply its committed confiuration. +ApplyConfig(i) == /\ GetMaxConfigIndex(i,commitIndex[i]) > 0 /\ LET config == GetLatestCommitConfig(i) - IN IF votersOfServer[i] /= config.newConf + IN IF voters[i] /= config.newConf THEN /\ \/ \* leader not in the new configuration. \* switch to Follwer. /\ i \notin config.newConf @@ -305,27 +307,39 @@ AdvanceCommitConfig(i) == /\ state' = [state EXCEPT ![i] = Follower] \/ /\ i \in config.newConf /\ UNCHANGED <> - /\ votersOfServer' = [ votersOfServer EXCEPT ![i] = config.newConf] - ELSE UNCHANGED <> - /\ UNCHANGED <> + /\ voters' = [ voters EXCEPT ![i] = config.newConf] + /\ nextVoters' = [nextVoters EXCEPT ![i] = {}] + ELSE UNCHANGED <> + /\ UNCHANGED <> - \* Leader i add a group servers to cluster. SetNodes(i, newNodes) == /\ state[i] = Leader /\ \* for reducing the state space, just verify once. Len(SelectSeq(log[i], LAMBDA logEntry : logEntry.type = ConfigEntry)) = 0 - /\ LET oldConfig == votersOfServer[i] + /\ LET oldConfig == voters[i] entry == [term |-> currentTerm[i], type |-> ConfigEntry, newConf |-> newNodes, oldConf |-> oldConfig] - transitionConfig == oldConfig \cup newNodes newLog == Append(log[i], entry) - IN /\ log' = [log EXCEPT ![i] = newLog] - /\ votersOfServer = [votersOfServer EXCEPT ![i] = transitionConfig] - /\ UNCHANGED <> + IN /\ log' = [log EXCEPT ![i] = Append(@,entry)] + /\ nextVoters' = [nextVoters EXCEPT ![i] = newNodes] + /\ UNCHANGED <> +\* Leader i receives a client request to add v to the log. +ClientRequest(i) == + /\ state[i] = Leader + /\ clientRequests < MaxClientRequests + /\ LET entry == [term |-> currentTerm[i], + type |-> ValueEntry, + value |-> clientRequests] + newLog == Append(log[i], entry) + IN /\ log' = [log EXCEPT ![i] = newLog] + /\ clientRequests' = clientRequests + 1 + /\ UNCHANGED <> ---- \* Message handlers \* i = recipient, j = sender, m = message @@ -393,12 +407,12 @@ HandleAppendEntriesRequest(i, j, m) == msource |-> i, mdest |-> j], m) - /\ UNCHANGED <> + /\ UNCHANGED <> \/ \* return to follower state /\ m.mterm = currentTerm[i] /\ state[i] = Candidate /\ state' = [state EXCEPT ![i] = Follower] - /\ UNCHANGED <> + /\ UNCHANGED <> \/ \* accept request /\ m.mterm = currentTerm[i] /\ state[i] = Follower @@ -422,7 +436,7 @@ HandleAppendEntriesRequest(i, j, m) == msource |-> i, mdest |-> j], m) - /\ UNCHANGED <> + /\ UNCHANGED <> \/ \* conflict: remove 1 entry /\ m.mentries /= << >> /\ Len(log[i]) >= index @@ -430,14 +444,14 @@ HandleAppendEntriesRequest(i, j, m) == /\ LET new == [index2 \in 1..(Len(log[i]) - 1) |-> log[i][index2]] IN log' = [log EXCEPT ![i] = new] - /\ UNCHANGED <> + /\ UNCHANGED <> \/ \* no conflict: append entry /\ m.mentries /= << >> /\ Len(log[i]) = m.mprevLogIndex /\ log' = [log EXCEPT ![i] = Append(log[i], m.mentries[1])] - /\ UNCHANGED <> - /\ UNCHANGED <> + /\ UNCHANGED <> + /\ UNCHANGED <> \* Servers i receives an AppendEntries response from server j with \* m.mterm = currentTerm[i]. @@ -489,52 +503,43 @@ Receive(m) == \* End of message handlers. ---- \* Defines how the variables may transition. -Next == +Next == \* Leader election \/ \E i,j \in allServers : RequestVote(i, j) \/ \E i \in allServers : BecomeLeader(i) - \* Client request - \/ \E i \in allServers : ClientRequest(i) - \* Config changed with joint consensus - \/ \E i \in InitialServers: SetNodes(i, NewServers) - \* Log replica - \/ \E i \in allServers : AdvanceCommitIndex(i) - \/ \E i \in allServers : AdvanceCommitConfig(i) - \/ \E i,j \in allServers : AppendEntries(i, j) \* Network \/ \E m \in messages : Receive(m) \/ \/ /\ \A i \in allServers : state[i] = Follower /\ \E i \in allServers : Timeout(i) \/ /\ \E i \in allServers : state[i] /= Follower - /\ UNCHANGED <> - + /\ UNCHANGED <> + \* Client request + \/ \E i \in allServers : ClientRequest(i) + \* Config changed with joint consensus + \/ \E i \in allServers: SetNodes(i, NewServers) + \* Log replica + \/ \E i,j \in allServers : AppendEntries(i, j) + \/ \E i \in allServers : AdvanceCommitIndex(i) + \/ \E i \in allServers : ApplyConfig(i) \* The specification must start with the initial state and transition according \* to Next. Spec == Init /\ [][Next]_vars - ---- \* The following are a set of verification. MoreThanOneLeader == Cardinality({i \in allServers: state[i]=Leader}) > 1 -TransitionPhaseChecker == - \A i \in allServers: LET inTransition == /\ commitIndex[i] < GetMaxConfigIndex(i,Len(log[i])) +TransitionPhaseChecker == + \A i \in allServers: LET inTransition == /\ commitIndex[i] > 1 + /\ commitIndex[i] < GetMaxConfigIndex(i,Len(log[i])) /\ GetMaxConfigIndex(i,Len(log[i])) > 0 configEntry == GetLatestConfig(i) - IN IF inTransition THEN + IN IF inTransition THEN IF state[i] = Leader THEN - votersOfServer[i] = configEntry.oldConf \cup configEntry.newConf - ELSE votersOfServer[i] = configEntry.oldConf - ELSE TRUE -CommittedPhaseChecker == - \A i \in allServers: LET committed == /\ commitIndex[i] > 0 - /\ GetMaxConfigIndex(i,commitIndex[i]) > 0 - /\ commitIndex[i] > GetMaxConfigIndex(i,commitIndex[i]) - configEntry == GetLatestCommitConfig(i) - IN IF committed THEN - votersOfServer[i] = configEntry.newConf + /\ voters[i] = configEntry.oldConf + /\ nextVoters[i] = configEntry.newConf + ELSE /\ voters[i] = configEntry.oldConf ELSE TRUE - =============================================================================== diff --git a/JointConsensus/JointConsensus.toolbox/JointConsensus___ConfigCheck.launch b/JointConsensus/JointConsensus.toolbox/JointConsensus___ConfigCheck.launch index 1e0e64b..d7f155d 100644 --- a/JointConsensus/JointConsensus.toolbox/JointConsensus___ConfigCheck.launch +++ b/JointConsensus/JointConsensus.toolbox/JointConsensus___ConfigCheck.launch @@ -19,13 +19,12 @@ - + - diff --git a/RaftMerge/RaftMerge.tla b/RaftMerge/RaftMerge.tla index 244c9b4..f9240b2 100644 --- a/RaftMerge/RaftMerge.tla +++ b/RaftMerge/RaftMerge.tla @@ -213,7 +213,7 @@ ClientRequest(i, r, log) == /\ LET new_logs == Append(raft[i][r].logs, log) new_match_index == [raft[i][r].match_index EXCEPT ![i] = @ + 1] - IN + IN /\ raft' = [raft EXCEPT ![i][r].logs = new_logs, ![i][r].match_index = new_match_index] /\ client_requests_index' = client_requests_index + 1 From d2c6785665c7cb51e0a437d989655c399c5ed329 Mon Sep 17 00:00:00 2001 From: nolouch Date: Thu, 8 Nov 2018 03:02:24 +0800 Subject: [PATCH 3/4] reduce state space --- JointConsensus/JointConsensus.tla | 67 ++++++++----------- .../JointConsensus___ConfigCheck.launch | 8 +-- 2 files changed, 33 insertions(+), 42 deletions(-) diff --git a/JointConsensus/JointConsensus.tla b/JointConsensus/JointConsensus.tla index b18e55f..c2e99a5 100644 --- a/JointConsensus/JointConsensus.tla +++ b/JointConsensus/JointConsensus.tla @@ -69,11 +69,7 @@ VARIABLE clientRequests VARIABLE log \* The index of the latest entry in the log the state machine may apply. VARIABLE commitIndex -\* The index that gets committed -VARIABLE committedLog -\* Does the commited Index decrease -VARIABLE committedLogDecrease -logVars == <> +logVars == <> \* The following variables are used only on candidates: \* The set of servers from which the candidate has received a RequestVote @@ -180,8 +176,6 @@ InitLeaderVars == /\ nextIndex = [i \in allServers |-> [j \in allServers |-> 1] InitLogVars == /\ log = [i \in allServers |-> << >>] /\ commitIndex = [i \in allServers |-> 0] /\ clientRequests = 1 - /\ committedLog = << >> - /\ committedLogDecrease = FALSE Init == /\ messages = {} /\ InitServerVars @@ -232,23 +226,26 @@ AppendEntries(i, j) == \* Send up to 1 entry, constrained by the end of the log. lastEntry == Min({Len(log[i]), nextIndex[i][j]}) entries == SubSeq(log[i], nextIndex[i][j], lastEntry) - IN /\ Len(entries) > 0 /\ matchIndex[i][j] < lastEntry - /\ Send([mtype |-> AppendEntriesRequest, + msg == [mtype |-> AppendEntriesRequest, mterm |-> currentTerm[i], mprevLogIndex |-> prevLogIndex, mprevLogTerm |-> prevLogTerm, mentries |-> entries, mcommitIndex |-> Min({commitIndex[i], lastEntry}), msource |-> i, - mdest |-> j]) + mdest |-> j] + IN /\ matchIndex[i][j] < lastEntry + /\ msg \notin messages + /\ Send(msg) /\ UNCHANGED <> \* Candidate i transitions to leader. BecomeLeader(i) == /\ state[i] = Candidate + /\ \* already delete member should not become leader. + i \in voters[i] /\ votesGranted[i] \in BothQuorum(voters[i], nextVoters[i]) /\ state' = [state EXCEPT ![i] = Leader] - \*/\ PrintT(i \cup "became leader") /\ nextIndex' = [nextIndex EXCEPT ![i] = [j \in allServers |-> Len(log[i]) + 1]] /\ matchIndex' = [matchIndex EXCEPT ![i] = @@ -281,23 +278,12 @@ AdvanceCommitIndex(i) == Max(agreeIndexes) ELSE commitIndex[i] - newCommittedLog == - IF newCommitIndex >= 1 - THEN - [j \in 1..newCommitIndex |-> log[i][j]] - ELSE - <<>> - IN /\ commitIndex[i] /= newCommitIndex - /\ commitIndex' = [commitIndex EXCEPT ![i] = newCommitIndex] - /\ committedLogDecrease' = \/ ( newCommitIndex < Len(committedLog)) - \/ \E j \in 1..Len(committedLog) : committedLog[j] /= newCommittedLog[j] - /\ committedLog' = newCommittedLog - \*/\ PrintT(Len(log[i])\cup newCommitIndex) + IN /\ commitIndex' = [commitIndex EXCEPT ![i] = newCommitIndex] /\ UNCHANGED <> \* Leader i apply its committed confiuration. ApplyConfig(i) == - /\ GetMaxConfigIndex(i,commitIndex[i]) > 0 + /\ GetMaxConfigIndex(i, commitIndex[i]) > 0 /\ LET config == GetLatestCommitConfig(i) IN IF voters[i] /= config.newConf THEN /\ \/ \* leader not in the new configuration. @@ -326,7 +312,7 @@ SetNodes(i, newNodes) == IN /\ log' = [log EXCEPT ![i] = Append(@,entry)] /\ nextVoters' = [nextVoters EXCEPT ![i] = newNodes] /\ UNCHANGED <> + leaderVars, commitIndex, allServers, voters, clientRequests>> \* Leader i receives a client request to add v to the log. ClientRequest(i) == @@ -339,7 +325,7 @@ ClientRequest(i) == IN /\ log' = [log EXCEPT ![i] = newLog] /\ clientRequests' = clientRequests + 1 /\ UNCHANGED <> + leaderVars, commitIndex, nodeVars>> ---- \* Message handlers \* i = recipient, j = sender, m = message @@ -436,7 +422,7 @@ HandleAppendEntriesRequest(i, j, m) == msource |-> i, mdest |-> j], m) - /\ UNCHANGED <> + /\ UNCHANGED <> \/ \* conflict: remove 1 entry /\ m.mentries /= << >> /\ Len(log[i]) >= index @@ -444,13 +430,13 @@ HandleAppendEntriesRequest(i, j, m) == /\ LET new == [index2 \in 1..(Len(log[i]) - 1) |-> log[i][index2]] IN log' = [log EXCEPT ![i] = new] - /\ UNCHANGED <> + /\ UNCHANGED <> \/ \* no conflict: append entry /\ m.mentries /= << >> /\ Len(log[i]) = m.mprevLogIndex /\ log' = [log EXCEPT ![i] = Append(log[i], m.mentries[1])] - /\ UNCHANGED <> + /\ UNCHANGED <> /\ UNCHANGED <> \* Servers i receives an AppendEntries response from server j with @@ -459,6 +445,7 @@ HandleAppendEntriesResponse(i, j, m) == /\ m.mterm = currentTerm[i] /\ \/ /\ m.msuccess \* successful /\ nextIndex' = [nextIndex EXCEPT ![i][j] = m.mmatchIndex + 1] + /\ matchIndex[i][j] < m.mmatchIndex /\ matchIndex' = [matchIndex EXCEPT ![i][j] = m.mmatchIndex] \/ /\ \lnot m.msuccess \* not successful /\ nextIndex' = [nextIndex EXCEPT ![i][j] = @@ -511,7 +498,7 @@ Next == \/ \E m \in messages : Receive(m) \/ \/ /\ \A i \in allServers : state[i] = Follower /\ \E i \in allServers : Timeout(i) - \/ /\ \E i \in allServers : state[i] /= Follower + \/ /\ \E i \in allServers: state[i] /= Follower /\ UNCHANGED <> \* Client request \/ \E i \in allServers : ClientRequest(i) @@ -529,17 +516,21 @@ Spec == Init /\ [][Next]_vars \* The following are a set of verification. MoreThanOneLeader == - Cardinality({i \in allServers: state[i]=Leader}) > 1 - -TransitionPhaseChecker == - \A i \in allServers: LET inTransition == /\ commitIndex[i] > 1 - /\ commitIndex[i] < GetMaxConfigIndex(i,Len(log[i])) - /\ GetMaxConfigIndex(i,Len(log[i])) > 0 - configEntry == GetLatestConfig(i) + Cardinality({i \in allServers: state[i]=Leader}) > 1 + +TransitionPhase == + \A i \in allServers: LET maxConfigIndex == GetMaxConfigIndex(i,Len(log[i])) + inTransition == /\ commitIndex[i] > 0 + /\ maxConfigIndex > 0 + \* commitIndex less config index, but + /\ commitIndex[i] < maxConfigIndex + configEntry == GetLatestConfig(i) IN IF inTransition THEN IF state[i] = Leader THEN + \* Leader in stransition should contain Cold and Cnew. /\ voters[i] = configEntry.oldConf /\ nextVoters[i] = configEntry.newConf - ELSE /\ voters[i] = configEntry.oldConf + ELSE \/ voters[i] = configEntry.oldConf + \/ voters[i] = {} ELSE TRUE =============================================================================== diff --git a/JointConsensus/JointConsensus.toolbox/JointConsensus___ConfigCheck.launch b/JointConsensus/JointConsensus.toolbox/JointConsensus___ConfigCheck.launch index d7f155d..10a86e8 100644 --- a/JointConsensus/JointConsensus.toolbox/JointConsensus___ConfigCheck.launch +++ b/JointConsensus/JointConsensus.toolbox/JointConsensus___ConfigCheck.launch @@ -19,12 +19,12 @@ - + - + @@ -35,13 +35,13 @@ - + - + From bbca417783fa6cc49390573e3f7432fd9eb40c6b Mon Sep 17 00:00:00 2001 From: nolouch Date: Thu, 29 Nov 2018 02:20:29 +0800 Subject: [PATCH 4/4] add apply index Signed-off-by: nolouch --- JointConsensus/JointConsensus.tla | 104 +++++++++++------- .../JointConsensus___ConfigCheck.launch | 9 +- 2 files changed, 68 insertions(+), 45 deletions(-) diff --git a/JointConsensus/JointConsensus.tla b/JointConsensus/JointConsensus.tla index c2e99a5..4105679 100644 --- a/JointConsensus/JointConsensus.tla +++ b/JointConsensus/JointConsensus.tla @@ -2,6 +2,7 @@ \* This is the formal specification for the Raft consensus algorithm. \* \* Copyright 2014 Diego Ongaro. +\* \* This work is licensed under the Creative Commons Attribution-4.0 \* International License https://creativecommons.org/licenses/by/4.0/ @@ -10,7 +11,7 @@ EXTENDS Naturals, FiniteSets, Sequences, TLC \* The set of server IDs CONSTANTS InitialServers, NewServers -CONSTANTS ValueEntry,ConfigEntry +CONSTANTS NormalEntry, BeginConfChange, FinalizeConfChange \* Servers states. CONSTANTS Follower, Candidate, Leader @@ -67,9 +68,11 @@ VARIABLE clientRequests \* log entry. Unfortunately, the Sequence module defines Head(s) as the entry \* with index 1, so be careful not to use that! VARIABLE log -\* The index of the latest entry in the log the state machine may apply. +\* The index of the latest entry in the log the state machine has commited. VARIABLE commitIndex -logVars == <> +\* The index of the latest entry in the log the state machine has apply. +VARIABLE applyIndex +logVars == <> \* The following variables are used only on candidates: \* The set of servers from which the candidate has received a RequestVote @@ -134,7 +137,7 @@ Max(s) == CHOOSE x \in s : \A y \in s : x >= y \* Get the maximum config from log[1..l]. GetMaxConfigIndex(i, l) == - LET chonfigIndexes == {index \in 1..l: log[i][index].type = ConfigEntry} + LET chonfigIndexes == {index \in 1..l: log[i][index].type = BeginConfChange \/ log[i][index].type = FinalizeConfChange} IN IF chonfigIndexes = {} THEN 0 ELSE Max(chonfigIndexes) \* Get the latest config in all log of server i. @@ -175,6 +178,7 @@ InitLeaderVars == /\ nextIndex = [i \in allServers |-> [j \in allServers |-> 1] InitLogVars == /\ log = [i \in allServers |-> << >>] /\ commitIndex = [i \in allServers |-> 0] + /\ applyIndex = [i \in allServers |-> 0] /\ clientRequests = 1 Init == /\ messages = {} @@ -279,53 +283,71 @@ AdvanceCommitIndex(i) == ELSE commitIndex[i] IN /\ commitIndex' = [commitIndex EXCEPT ![i] = newCommitIndex] - /\ UNCHANGED <> - -\* Leader i apply its committed confiuration. -ApplyConfig(i) == - /\ GetMaxConfigIndex(i, commitIndex[i]) > 0 - /\ LET config == GetLatestCommitConfig(i) - IN IF voters[i] /= config.newConf - THEN /\ \/ \* leader not in the new configuration. - \* switch to Follwer. - /\ i \notin config.newConf - /\ state[i] = Leader - /\ state' = [state EXCEPT ![i] = Follower] - \/ /\ i \in config.newConf - /\ UNCHANGED <> - /\ voters' = [ voters EXCEPT ![i] = config.newConf] - /\ nextVoters' = [nextVoters EXCEPT ![i] = {}] - ELSE UNCHANGED <> - /\ UNCHANGED <> + /\ UNCHANGED <> + +\* ApplyLog apply the commit entrys of server i. +ApplyLog(i) == + LET + next == applyIndex[i] + 1 + entry == log[i][next] + IN + /\ applyIndex[i] < commitIndex[i] + /\ \/ \* apply normal entry + /\ entry.type = NormalEntry + /\ applyIndex' = [ applyIndex EXCEPT ![i] = next ] + /\ UNCHANGED <> + \/ \* begin the membership change + /\ entry.type = BeginConfChange + /\ nextVoters' = [nextVoters EXCEPT ![i] = entry.newConf] + /\ applyIndex' = [ applyIndex EXCEPT ![i] = next ] + /\ \/ /\ state[i] = Leader + /\ LET oldConfig == voters[i] + newEntry == [term |-> currentTerm[i], + type |-> FinalizeConfChange] + IN log' = [log EXCEPT ![i] = Append(@,newEntry)] + \/ /\ state[i] = Follower + /\ UNCHANGED <> + /\ UNCHANGED <> + \/ \* finalize the membership change + /\ entry.type = FinalizeConfChange + /\ /\ \/ \* leader not in the new configuration. + \* step to Follwer. + /\ i \notin nextVoters[i] + /\ state[i] = Leader + /\ state' = [state EXCEPT ![i] = Follower] + \/ /\ i \in nextVoters[i] + /\ UNCHANGED <> + /\ voters' = [ voters EXCEPT ![i] = nextVoters[i]] + /\ nextVoters' = [nextVoters EXCEPT ![i] = {}] + /\ applyIndex' = [ applyIndex EXCEPT ![i] = next ] + /\ UNCHANGED <> + /\ UNCHANGED <> \* Leader i add a group servers to cluster. -SetNodes(i, newNodes) == +ProposeMembership(i, newNodes) == /\ state[i] = Leader /\ \* for reducing the state space, just verify once. - Len(SelectSeq(log[i], LAMBDA logEntry : logEntry.type = ConfigEntry)) = 0 + Len(SelectSeq(log[i], LAMBDA logEntry : logEntry.type = BeginConfChange)) = 0 /\ LET oldConfig == voters[i] entry == [term |-> currentTerm[i], - type |-> ConfigEntry, + type |-> BeginConfChange, newConf |-> newNodes, oldConf |-> oldConfig] - newLog == Append(log[i], entry) - IN /\ log' = [log EXCEPT ![i] = Append(@,entry)] - /\ nextVoters' = [nextVoters EXCEPT ![i] = newNodes] + IN log' = [log EXCEPT ![i] = Append(@,entry)] /\ UNCHANGED <> + leaderVars, commitIndex, applyIndex, allServers, voters, nextVoters, clientRequests>> \* Leader i receives a client request to add v to the log. ClientRequest(i) == /\ state[i] = Leader /\ clientRequests < MaxClientRequests /\ LET entry == [term |-> currentTerm[i], - type |-> ValueEntry, + type |-> NormalEntry, value |-> clientRequests] - newLog == Append(log[i], entry) - IN /\ log' = [log EXCEPT ![i] = newLog] + IN /\ log' = [log EXCEPT ![i] = Append(@,entry)] /\ clientRequests' = clientRequests + 1 /\ UNCHANGED <> + leaderVars, commitIndex, applyIndex, nodeVars>> ---- \* Message handlers \* i = recipient, j = sender, m = message @@ -422,7 +444,7 @@ HandleAppendEntriesRequest(i, j, m) == msource |-> i, mdest |-> j], m) - /\ UNCHANGED <> + /\ UNCHANGED <> \/ \* conflict: remove 1 entry /\ m.mentries /= << >> /\ Len(log[i]) >= index @@ -430,13 +452,13 @@ HandleAppendEntriesRequest(i, j, m) == /\ LET new == [index2 \in 1..(Len(log[i]) - 1) |-> log[i][index2]] IN log' = [log EXCEPT ![i] = new] - /\ UNCHANGED <> + /\ UNCHANGED <> \/ \* no conflict: append entry /\ m.mentries /= << >> /\ Len(log[i]) = m.mprevLogIndex /\ log' = [log EXCEPT ![i] = Append(log[i], m.mentries[1])] - /\ UNCHANGED <> + /\ UNCHANGED <> /\ UNCHANGED <> \* Servers i receives an AppendEntries response from server j with @@ -503,11 +525,11 @@ Next == \* Client request \/ \E i \in allServers : ClientRequest(i) \* Config changed with joint consensus - \/ \E i \in allServers: SetNodes(i, NewServers) + \/ \E i \in allServers: ProposeMembership(i, NewServers) \* Log replica \/ \E i,j \in allServers : AppendEntries(i, j) \/ \E i \in allServers : AdvanceCommitIndex(i) - \/ \E i \in allServers : ApplyConfig(i) + \/ \E i \in allServers : ApplyLog(i) \* The specification must start with the initial state and transition according \* to Next. @@ -520,11 +542,11 @@ MoreThanOneLeader == TransitionPhase == \A i \in allServers: LET maxConfigIndex == GetMaxConfigIndex(i,Len(log[i])) + configEntry == GetLatestConfig(i) inTransition == /\ commitIndex[i] > 0 /\ maxConfigIndex > 0 - \* commitIndex less config index, but - /\ commitIndex[i] < maxConfigIndex - configEntry == GetLatestConfig(i) + /\ applyIndex[i] >= maxConfigIndex + /\ configEntry.type = BeginConfChange IN IF inTransition THEN IF state[i] = Leader THEN \* Leader in stransition should contain Cold and Cnew. diff --git a/JointConsensus/JointConsensus.toolbox/JointConsensus___ConfigCheck.launch b/JointConsensus/JointConsensus.toolbox/JointConsensus___ConfigCheck.launch index 10a86e8..789c182 100644 --- a/JointConsensus/JointConsensus.toolbox/JointConsensus___ConfigCheck.launch +++ b/JointConsensus/JointConsensus.toolbox/JointConsensus___ConfigCheck.launch @@ -6,7 +6,7 @@ - + @@ -19,7 +19,7 @@ - + @@ -32,9 +32,7 @@ - - @@ -43,6 +41,9 @@ + + +