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

Fix AccReset

Browse Source
This commit is contained in:
Arseny Sher
2024-12-02 11:05:39 +01:00
parent a9662b6f64
commit 6b7af160bf
2 changed files with 17 additions and 10 deletions
Download Patch File Download Diff File Expand all files Collapse all files

12
safekeeper/spec/ProposerAcceptorReconfig.tla
View File

@@ -65,7 +65,7 @@ Init ==
/\ prop_conf = [p \in proposers |-> init_conf]
/\ acc_conf = [a \in acceptors |-> init_conf]
/\ conf_store = init_conf
/\ Cardinality(init_members) >= 3
/\ Cardinality(init_members) = Cardinality(acceptors) - 1
\********************************************************************************
\* Actions
@@ -233,9 +233,15 @@ AccSwitchConf(a) ==
\* Nuke all acceptor state if it is not a member of its current conf. Models
\* cleanup after migration/abort.
AccReset(a) ==
/\ a \notin acc_conf[a].members
/\ \/ (acc_conf[a].newMembers = NULL) /\ (a \notin acc_conf[a].members)
\/ (acc_conf[a].newMembers /= NULL) /\ (a \notin (acc_conf[a].members \union acc_conf[a].newMembers))
/\ acc_state' = [acc_state EXCEPT ![a] = PAS!InitAcc]
/\ UNCHANGED <<prop_state, committed, elected_history, prop_conf, acc_conf, conf_store>>
\* Set nextSendLsn to `a` to NULL everywhere. nextSendLsn serves as a mark
\* that elected proposer performed TruncateWal on the acceptor, which isn't
\* true anymore after state reset. In the impl local deletion is expected to
\* terminate all existing connections.
/\ prop_state' = [p \in proposers |-> [prop_state[p] EXCEPT !.nextSendLsn[a] = NULL]]
/\ UNCHANGED <<committed, elected_history, prop_conf, acc_conf, conf_store>>
\*******************************************************************************

15
safekeeper/spec/ProposerAcceptorStatic.tla
View File

@@ -145,10 +145,11 @@ TypeOk ==
/\ IsWal(prop_state[p].wal)
\* Map of acceptor -> next lsn to send. It is set when truncate_wal is
\* done so sending entries is allowed only after that. In the impl TCP
\* ensures this ordering.
\* ensures this ordering. We use NULL instead of missing value to use
\* EXCEPT in AccReset.
/\ \A a \in DOMAIN prop_state[p].nextSendLsn:
/\ a \in acceptors
/\ prop_state[p].nextSendLsn[a] \in Lsns
/\ prop_state[p].nextSendLsn[a] \in Lsns \union {NULL}
/\ \A a \in acceptors:
/\ DOMAIN acc_state[a] = {"term", "termHistory", "wal"}
/\ acc_state[a].term \in Terms
@@ -197,7 +198,7 @@ Init ==
votes |-> EmptyF,
termHistory |-> << >>,
wal |-> << >>,
nextSendLsn |-> EmptyF
nextSendLsn |-> [a \in acceptors |-> NULL]
]]
/\ acc_state = [a \in acceptors |-> InitAcc]
/\ committed = {}
@@ -214,7 +215,7 @@ RestartProposerWithTerm(p, new_term) ==
![p].votes = EmptyF,
![p].termHistory = << >>,
![p].wal = << >>,
![p].nextSendLsn = EmptyF]
![p].nextSendLsn = [a \in acceptors |-> NULL]]
/\ UNCHANGED <<acc_state, committed, elected_history>>
\* Proposer p loses all state, restarting.
@@ -361,8 +362,8 @@ NewEntry(p) ==
AppendEntry(p, a) ==
/\ prop_state[p].state = "leader"
/\ acc_state[a].term = prop_state[p].term
/\ a \in DOMAIN prop_state[p].nextSendLsn \* did TruncateWal
/\ prop_state[p].nextSendLsn[a] <= Len(prop_state[p].wal) \* have smth to send
/\ prop_state[p].nextSendLsn[a] /= NULL \* did TruncateWal
/\ prop_state[p].nextSendLsn[a] <= Len(prop_state[p].wal) \* have smth to send
/\ LET
send_lsn == prop_state[p].nextSendLsn[a]
entry == prop_state[p].wal[send_lsn]
@@ -391,7 +392,7 @@ QuorumCommitLsn(p, q) ==
\* Alternatively we could compare LastLogTerm here, but that's closer to
\* what we do in the impl (we check flushLsn in AppendResponse, but
\* AppendRequest is processed only if HandleElected handling was good).
/\ a \in DOMAIN prop_state[p].nextSendLsn
/\ prop_state[p].nextSendLsn[a] /= NULL
THEN
\* Now find the LSN present on all the quorum.
LET quorum_lsn == Minimum({FlushLsn(a): a \in q}) IN