From 443a6fdfdb0d4b77b8a9ca7234c65bd83e2172cb Mon Sep 17 00:00:00 2001 From: Arseny Sher Date: Fri, 1 Nov 2024 14:33:12 +0300 Subject: [PATCH] bad quorums --- safekeeper/spec/ProposerAcceptorStatic.tla | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/safekeeper/spec/ProposerAcceptorStatic.tla b/safekeeper/spec/ProposerAcceptorStatic.tla index 6d9fa8d023..318a138d1b 100644 --- a/safekeeper/spec/ProposerAcceptorStatic.tla +++ b/safekeeper/spec/ProposerAcceptorStatic.tla @@ -6,6 +6,11 @@ \* on the acceptor since common point had been calculated (this should be rejected). \* - old WAL is immediately copied to proposer on its election, without on-demand fetch later. +\* Some ideas how to break it to play around to get a feeling: +\* - replace Quorums with BadQuorums. +\* - remove 'don't commit entries from previous terms separately' rule in +\* CommitEntries and observe figure 8 from the raft paper. + EXTENDS Integers, Sequences, FiniteSets, TLC VARIABLES @@ -62,6 +67,10 @@ Quorum(acc_set) == Cardinality(acc_set) >= (NumAccs \div 2 + 1) \* all quorums of acceptors Quorums == {subset \in SUBSET acceptors: Quorum(subset)} +\* For substituting Quorums and seeing what happens. +BadQuorum(acc_set) == Cardinality(acc_set) >= (NumAccs \div 2) +BadQuorums == {subset \in SUBSET acceptors: BadQuorum(subset)} + \* flushLsn (end of WAL, i.e. index of next entry) of acceptor a. FlushLsn(a) == Len(acc_state[a].wal) + 1