rust/neon
1
0
Fork 0
mirror of https://github.com/neondatabase/neon.git synced 2026-05-26 09:30:37 +00:00
Code Issues Packages Projects Releases Wiki Activity

RestartProposer

Browse Source
This commit is contained in:
Arseny Sher
2024-11-26 16:52:05 +03:00
parent c940f196ce
commit 8c880d088b
2 changed files with 26 additions and 13 deletions
Download Patch File Download Diff File Expand all files Collapse all files

20
safekeeper/spec/ProposerAcceptorReconfig.tla
View File

@@ -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)

19
safekeeper/spec/ProposerAcceptorStatic.tla
View File

@@ -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.