From 664569ecdbffb14d3f8da9ee947c747161be04e3 Mon Sep 17 00:00:00 2001 From: Arseny Sher Date: Fri, 1 Nov 2024 13:50:05 +0300 Subject: [PATCH] MaxTruncatedTerms --- safekeeper/spec/ProposerAcceptorStatic.tla | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) diff --git a/safekeeper/spec/ProposerAcceptorStatic.tla b/safekeeper/spec/ProposerAcceptorStatic.tla index 010f63f630..6d9fa8d023 100644 --- a/safekeeper/spec/ProposerAcceptorStatic.tla +++ b/safekeeper/spec/ProposerAcceptorStatic.tla @@ -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 ==== \ No newline at end of file