From 13fd695e3fcf79054d701f8bf816cfc2102f90d3 Mon Sep 17 00:00:00 2001 From: Arseny Sher Date: Thu, 31 Oct 2024 16:02:20 +0300 Subject: [PATCH] Add TruncateWal --- safekeeper/spec/ProposerAcceptorStatic.tla | 101 +++++++++++---------- 1 file changed, 52 insertions(+), 49 deletions(-) diff --git a/safekeeper/spec/ProposerAcceptorStatic.tla b/safekeeper/spec/ProposerAcceptorStatic.tla index 82ff6c5a42..da949b29da 100644 --- a/safekeeper/spec/ProposerAcceptorStatic.tla +++ b/safekeeper/spec/ProposerAcceptorStatic.tla @@ -1,10 +1,10 @@ ---- MODULE ProposerAcceptorStatic ---- -\* Differences from current implementation: -\* - unified not-globally-unique epoch & term (node_id) -\* Simplifications: -\* - instant message delivery -\* - feedback is not modeled separately, commit_lsn is updated directly +\* Model simplifications: +\* - Instant message delivery. Notably, ProposerElected message (TruncateWal action) is not +\* delayed, so we don't attempt to truncate WAL when the same wp already appended something +\* 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. EXTENDS Integers, Sequences, FiniteSets, TLC @@ -190,7 +190,7 @@ Vote(p, a) == /\ LET vote == [termHistory |-> AcceptorTermHistory(a), flushLsn |-> FlushLsn(a)] IN - prop_state' = [prop_state EXCEPT ![p].votes = prop_state[p].votes @@ (a :> vote)] + prop_state' = [prop_state EXCEPT ![p].votes = (a :> vote) @@ prop_state[p].votes] /\ UNCHANGED <> @@ -234,50 +234,53 @@ UpdateTerm(p, a) == /\ acc_state' = [acc_state EXCEPT ![a].term = prop_state[p].term] /\ UNCHANGED <> +\* Find highest common point in the logs of proposer p and acceptor a. +\* Returns of the highest common point. +FindHighestCommonPoint(prop_th, acc_th, acc_flush_lsn) == + LET + \* First find index of the highest common term. + \* It must exist because we initialize th with <0, 1>. + last_common_idx == Maximum({i \in 1..Min(Len(prop_th), Len(acc_th)): prop_th[i].term = acc_th[i].term}) + last_common_term == prop_th[last_common_idx].term + \* Now find where it ends at both prop and acc and take min. End of term + \* is the start of the next unless it is the last one; there it is + \* flush_lsn in case of acceptor. In case of proposer it is the current + \* writing position, but it can't be less than flush_lsn, so we + \* take flush_lsn. + acc_common_term_end == IF last_common_idx = Len(acc_th) THEN acc_flush_lsn ELSE acc_th[last_common_idx + 1].lsn + prop_common_term_end == IF last_common_idx = Len(prop_th) THEN acc_flush_lsn ELSE prop_th[last_common_idx + 1].lsn + IN + [term |-> last_common_term, lsn |-> Min(acc_common_term_end, prop_common_term_end)] -\* Acceptor a which didn't participate in voting connects to elected proposer p -\* and p sets the streaming point -\* HandshakeWithLeader(p, a) == -\* /\ prop_state[p].state = "leader" -\* /\ acc_state[a].term = prop_state[p].term -\* /\ a \notin DOMAIN prop_state[p].next_send_lsn -\* /\ LET -\* next_send_lsn == prop_state[p].next_send_lsn @@ (a :> 1) -\* IN -\* prop_state' = [prop_state EXCEPT ![p].next_send_lsn = next_send_lsn] -\* /\ UNCHANGED <> - +\* Elected proposer p immediately truncates WAL (and term history) of acceptor a +\* before starting streaming. Establishes nextSendLsn for a. +\* +\* In impl this happens at each reconnection, here we also allow to do it multiple times. +TruncateWal(p, a) == + /\ prop_state[p].state = "leader" + /\ acc_state[a].term = prop_state[p].term + /\ LET + hcp == FindHighestCommonPoint(prop_state[p].termHistory, AcceptorTermHistory(a), FlushLsn(a)) + next_send_lsn == (a :> hcp.lsn) @@ prop_state[p].nextSendLsn + IN + \* Acceptor persists full history immediately; reads adjust it to the + \* really existing wal with AcceptorTermHistory. + /\ acc_state' = [acc_state EXCEPT ![a].termHistory = prop_state[p].termHistory, + \* note: SubSeq is inclusive, hence -1. + ![a].wal = SubSeq(acc_state[a].wal, 1, hcp.lsn - 1) + ] + /\ prop_state' = [prop_state EXCEPT ![p].nextSendLsn = next_send_lsn] + /\ UNCHANGED <> \* Append new log entry to elected proposer -\* NewEntry(p) == -\* /\ prop_state[p].state = "leader" -\* /\ Len(prop_state[p].wal) < max_entries \* model constraint -\* /\ LET -\* new_lsn == IF Len(prop_state[p].wal) = 0 THEN -\* prop_state[p].vcl + 1 -\* ELSE -\* \* lsn of last record + 1 -\* prop_state[p].wal[Len(prop_state[p].wal)].lsn + 1 -\* new_entry == [lsn |-> new_lsn, epoch |-> prop_state[p].term] -\* IN -\* /\ prop_state' = [prop_state EXCEPT ![p].wal = Append(prop_state[p].wal, new_entry)] -\* /\ UNCHANGED <> - - -\* \* Write entry new_e to log wal, rolling back all higher entries if e is different. -\* \* If bump_epoch is TRUE, it means we get record with lsn=vcl and going to update -\* \* the epoch. Truncate log in this case as well, as we might have correct <= vcl -\* \* part and some outdated entries behind it which we want to purge before -\* \* declaring us as recovered. Another way to accomplish this (in previous commit) -\* \* is wait for first-entry-from-new-epoch before bumping it. -\* WriteEntry(wal, new_e, bump_epoch) == -\* (new_e.lsn :> new_e) @@ -\* \* If wal has entry with such lsn and it is different, truncate all higher log. -\* IF \/ (new_e.lsn \in DOMAIN wal /\ wal[new_e.lsn] /= new_e) -\* \/ bump_epoch THEN -\* SelectSeq(wal, LAMBDA e: e.lsn < new_e.lsn) -\* ELSE -\* wal +NewEntry(p) == + /\ prop_state[p].state = "leader" + /\ LET + \* entry consists only of term, index serves as LSN. + new_entry == prop_state[p].term + IN + /\ prop_state' = [prop_state EXCEPT ![p].wal = Append(prop_state[p].wal, new_entry)] + /\ UNCHANGED <> \* \* Try to transfer entry from elected proposer p to acceptor a @@ -336,8 +339,8 @@ Next == \/ \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) -\* \/ \E p \in proposers: \E a \in acceptors: HandshakeWithLeader(p, a) -\* \/ \E p \in proposers: NewEntry(p) + \/ \E p \in proposers: \E a \in acceptors: TruncateWal(p, a) + \/ \E p \in proposers: NewEntry(p) \* \/ \E p \in proposers: \E a \in acceptors: TransferEntry(p, a) Spec == Init /\ [][Next]_<>