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

MaxTruncatedTerms

Browse Source
This commit is contained in:
Arseny Sher
2024-11-01 13:50:05 +03:00
parent a9ced3573a
commit 664569ecdb
1 changed files with 12 additions and 2 deletions
Download Patch File Download Diff File Expand all files Collapse all files

14
safekeeper/spec/ProposerAcceptorStatic.tla
View File

@@ -387,6 +387,16 @@ MaxAccWalLen == \A a \in acceptors: Len(acc_state[a].wal) < 2
\* actually committing something.
MaxCommitLsn == Cardinality(committed) < 2
\* How many records with different terms can be removed in single WAL
\* truncation.
MaxTruncatedTerms ==
\A p \in proposers: \A a \in acceptors:
(/\ prop_state[p].state = "leader"
/\ prop_state[p].term = acc_state[a].term) =>
LET
hcp == FindHighestCommonPoint(prop_state[p].termHistory, AcceptorTermHistory(a), FlushLsn(a))
truncated_lsns == {lsn \in DOMAIN acc_state[a].wal: lsn >= hcp.lsn}
truncated_records_terms == {acc_state[a].wal[lsn]: lsn \in truncated_lsns}
IN
Cardinality(truncated_records_terms) < 2
====