sync refactor

source/libs/sync/inc/syncOnMessage.h

@@ -25,6 +25,46 @@ extern "C" {
 #include <stdlib.h>
 #include "taosdef.h"
 
+// TLA+ Spec
+// 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)
+
+// DuplicateMessage(m) ==
+//     /\ Send(m)
+//     /\ UNCHANGED <<serverVars, candidateVars, leaderVars, logVars>>
+
+// DropMessage(m) ==
+//     /\ Discard(m)
+//     /\ UNCHANGED <<serverVars, candidateVars, leaderVars, logVars>>
+
+// Next == /\ \/ \E i \in Server : Restart(i)
+//            \/ \E i \in Server : Timeout(i)
+//            \/ \E i,j \in Server : RequestVote(i, j)
+//            \/ \E i \in Server : BecomeLeader(i)
+//            \/ \E i \in Server, v \in Value : ClientRequest(i, v)
+//            \/ \E i \in Server : AdvanceCommitIndex(i)
+//            \/ \E i,j \in Server : AppendEntries(i, j)
+//            \/ \E m \in DOMAIN messages : Receive(m)
+//            \/ \E m \in DOMAIN messages : DuplicateMessage(m)
+//            \/ \E m \in DOMAIN messages : DropMessage(m)
+//            \* History variable that tracks every log ever:
+//         /\ allLogs' = allLogs \cup {log[i] : i \in Server}
+//
+
 #ifdef __cplusplus
 }
 #endif

source/libs/sync/src/syncMain.c

@@ -151,6 +151,30 @@ SSyncNode* syncNodeOpen(const SSyncInfo* pSyncInfo) {
 
   // init life cycle
 
+  // TLA+ Spec
+  // InitHistoryVars == /\ elections = {}
+  //                    /\ allLogs   = {}
+  //                    /\ voterLog  = [i \in Server |-> [j \in {} |-> <<>>]]
+  // InitServerVars == /\ currentTerm = [i \in Server |-> 1]
+  //                   /\ state       = [i \in Server |-> Follower]
+  //                   /\ votedFor    = [i \in Server |-> Nil]
+  // InitCandidateVars == /\ votesResponded = [i \in Server |-> {}]
+  //                      /\ votesGranted   = [i \in Server |-> {}]
+  // \* 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 Server |-> [j \in Server |-> 1]]
+  //                   /\ matchIndex = [i \in Server |-> [j \in Server |-> 0]]
+  // InitLogVars == /\ log          = [i \in Server |-> << >>]
+  //                /\ commitIndex  = [i \in Server |-> 0]
+  // Init == /\ messages = [m \in {} |-> 0]
+  //         /\ InitHistoryVars
+  //         /\ InitServerVars
+  //         /\ InitCandidateVars
+  //         /\ InitLeaderVars
+  //         /\ InitLogVars
+  //
+
   // init TLA+ server vars
   pSyncNode->state = TAOS_SYNC_STATE_FOLLOWER;
   pSyncNode->pRaftStore = raftStoreOpen(pSyncNode->raftStorePath);
@@ -728,6 +752,16 @@ static int32_t syncNodeOnPingReplyCb(SSyncNode* ths, SyncPingReply* pMsg) {
   return ret;
 }
 
+// TLA+ Spec
+// ClientRequest(i, v) ==
+//     /\ state[i] = Leader
+//     /\ LET entry == [term  |-> currentTerm[i],
+//                      value |-> v]
+//            newLog == Append(log[i], entry)
+//        IN  log' = [log EXCEPT ![i] = newLog]
+//     /\ UNCHANGED <<messages, serverVars, candidateVars,
+//                    leaderVars, commitIndex>>
+//
 static int32_t syncNodeOnClientRequestCb(SSyncNode* ths, SyncClientRequest* pMsg) {
   int32_t ret = 0;
   syncClientRequestLog2("==syncNodeOnClientRequestCb==", pMsg);

source/libs/sync/src/syncOnMessage.c

@@ -14,3 +14,43 @@
  */
 
 #include "syncOnMessage.h"
+
+// TLA+ Spec
+// 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)
+
+// DuplicateMessage(m) ==
+//     /\ Send(m)
+//     /\ UNCHANGED <<serverVars, candidateVars, leaderVars, logVars>>
+
+// DropMessage(m) ==
+//     /\ Discard(m)
+//     /\ UNCHANGED <<serverVars, candidateVars, leaderVars, logVars>>
+
+// Next == /\ \/ \E i \in Server : Restart(i)
+//            \/ \E i \in Server : Timeout(i)
+//            \/ \E i,j \in Server : RequestVote(i, j)
+//            \/ \E i \in Server : BecomeLeader(i)
+//            \/ \E i \in Server, v \in Value : ClientRequest(i, v)
+//            \/ \E i \in Server : AdvanceCommitIndex(i)
+//            \/ \E i,j \in Server : AppendEntries(i, j)
+//            \/ \E m \in DOMAIN messages : Receive(m)
+//            \/ \E m \in DOMAIN messages : DuplicateMessage(m)
+//            \/ \E m \in DOMAIN messages : DropMessage(m)
+//            \* History variable that tracks every log ever:
+//         /\ allLogs' = allLogs \cup {log[i] : i \in Server}
+//