From 8c880d088b8d81adeb76ba5f92eabb0a72179095 Mon Sep 17 00:00:00 2001
From: Arseny Sher <sher-ars@yandex.ru>
Date: Tue, 26 Nov 2024 16:52:05 +0300
Subject: [PATCH] RestartProposer

---
 safekeeper/spec/ProposerAcceptorReconfig.tla | 20 +++++++++++++++-----
 safekeeper/spec/ProposerAcceptorStatic.tla   | 19 +++++++++++--------
 2 files changed, 26 insertions(+), 13 deletions(-)

diff --git a/safekeeper/spec/ProposerAcceptorReconfig.tla b/safekeeper/spec/ProposerAcceptorReconfig.tla
index b150d82fad..f5793bd2d4 100644
--- a/safekeeper/spec/ProposerAcceptorReconfig.tla
+++ b/safekeeper/spec/ProposerAcceptorReconfig.tla
@@ -38,8 +38,8 @@ IsConfig(c) ==
 TypeOk ==
     /\ PAS!TypeOk
     /\ \A p \in proposers:
-      \/ prop_conf[p] = NULL
-      \/ IsConfig(prop_conf[p])
+           \/ prop_conf[p] = NULL
+           \/ IsConfig(prop_conf[p])
     /\ \A a \in acceptors: IsConfig(acc_conf[a])
     /\ IsConfig(conf_store)
 
@@ -52,13 +52,23 @@ Init ==
   /\ prop_conf = [p \in proposers |-> NULL]
   /\ \E init_members \in SUBSET acceptors:
        LET init_conf == [generation |-> 1, members |-> init_members, newMembers |-> NULL] IN
-         /\ acc_conf = [a \in acceptors |-> init_conf]
-         /\ conf_store = init_conf
+           /\ acc_conf = [a \in acceptors |-> init_conf]
+           /\ conf_store = init_conf
 
 \********************************************************************************
 \* Actions
 \********************************************************************************
 
+\* Proposer p loses all state, restarting.
+\* In the static spec we bump restarted proposer term to max of some quorum + 1
+\* so that it has chance to win election. With reconfigurations it's harder
+\* to calculate such a term, so keep it simple and take random acceptor one
+\* + 1.
+RestartProposer(p) ==
+    /\ \E a \in acceptors: PAS!RestartProposerWithTerm(p, acc_state[a].term + 1)
+    /\ prop_conf' = [prop_conf EXCEPT ![p] = NULL]
+    /\ UNCHANGED <<acc_conf, conf_store>>
+
 \* Do CAS on the conf store, starting change into the new_members conf.
 StartChange(new_members) ==
     \* Possible only if we don't already have the change in progress.
@@ -72,7 +82,7 @@ StartChange(new_members) ==
 
 Next ==
   \/ \E new_members \in SUBSET acceptors: StartChange(new_members)
-\*   \/ \E q \in Quorums: \E p \in proposers: RestartProposer(p, q)
+  \/ \E p \in proposers: RestartProposer(p)
 \*   \/ \E p \in proposers: \E a \in acceptors: Vote(p, a)
 \*   \/ \E p \in proposers: BecomeLeader(p)
 \*   \/ \E p \in proposers: \E a \in acceptors: UpdateTerm(p, a)
diff --git a/safekeeper/spec/ProposerAcceptorStatic.tla b/safekeeper/spec/ProposerAcceptorStatic.tla
index b2d2f005db..e916440eb2 100644
--- a/safekeeper/spec/ProposerAcceptorStatic.tla
+++ b/safekeeper/spec/ProposerAcceptorStatic.tla
@@ -195,20 +195,23 @@ Init ==
 \* Actions
 \********************************************************************************
 
-\* Proposer loses all state.
+RestartProposerWithTerm(p, new_term) ==
+    /\ prop_state' = [prop_state EXCEPT ![p].state = "campaign",
+                                        ![p].term = new_term,
+                                        ![p].votes = EmptyF,
+                                        ![p].termHistory = << >>,
+                                        ![p].wal = << >>,
+                                        ![p].nextSendLsn = EmptyF]
+    /\ UNCHANGED <<acc_state, committed, elected_history>>
+
+\* Proposer p loses all state, restarting.
 \* For simplicity (and to reduct state space), we assume it immediately gets
 \* current state from quorum q of acceptors determining the term he will request
 \* to vote for.
 RestartProposer(p, q) ==
     /\ Quorum(q)
     /\ LET new_term == Maximum({acc_state[a].term : a \in q}) + 1 IN
-           /\ prop_state' = [prop_state EXCEPT ![p].state = "campaign",
-                                               ![p].term = new_term,
-                                               ![p].votes = EmptyF,
-                                               ![p].termHistory = << >>,
-                                               ![p].wal = << >>,
-                                               ![p].nextSendLsn = EmptyF]
-           /\ UNCHANGED <<acc_state, committed, elected_history>>
+           RestartProposerWithTerm(p, new_term)
 
 \* Term history of acceptor a's WAL: the one saved truncated to contain only <=
 \* local FlushLsn entries.