Update consensus protocol spec

[arssher]

The spec was written for the buggy protocol which we had before the one more similar to Raft was implemented. Update the spec with what we currently have.

ref #8699

[github-actions]

7018 tests run: 6710 passed, 0 failed, 308 skipped (full report)

---

Flaky tests (3)

Postgres 17

• test_physical_replication_config_mismatch_too_many_known_xids: release-arm64
• test_scrubber_physical_gc_ancestors[2]: debug-x86-64

Postgres 14

• test_prefetch[4]: release-x86-64

Code coverage* (full report)

• functions: 30.4% (8268 of 27227 functions)
• lines: 47.7% (65191 of 136583 lines)

* collected from Rust tests only

---

_{The comment gets automatically updated with the latest test results
96b7d0c at 2024-12-02T16:10:08.553Z :recycle:}

[problame]

Read through everything reachable from Spec and Next.

Impressive work, very clearly readable and especially TypeOk is super helpful to understand what's going on.

---

This model doesn't include the membership change stuff, right? I suppose that'll be a separate PR on top of this one.

---

The modelcheck.sh doesn't work out of the box on Debian 12 with the toolbox .deb 1.7.4~20240808-1326

I had to comment out ALIAS.

--- a/safekeeper/spec/models/MCProposerAcceptorStatic_p2_a3_t2_l2.cfg
+++ b/safekeeper/spec/models/MCProposerAcceptorStatic_p2_a3_t2_l2.cfg
@@ -15,5 +15,5 @@ LogSafety
 CommittedNotTruncated
 SYMMETRY ProposerAcceptorSymmetry
 CHECK_DEADLOCK FALSE
-ALIAS Alias
+\* ALIAS Alias

---

Disclaimers:

• I have very limited TLA+ experience. Reading is ok, but I wouldn't be able to write a spec like this one (yet :) )
• I never trust myself with the relation of Lsn and WAL record.
  • Does it mean "up to the byte offset in the WAL"?
  • Does it mean "including the record that starts at byte offset X"
  • Does it mean "including the record that ends at byte offset X"
  • In this model, Lsn means just Nat index into the wal sequence of proposer and acceptor. So, it's side-stepping that question. Plus, TLA+ sequences start at 1.
  • So, overall, I wouldn't trust myself to certify that we're free of off-by-one errors in this spec.

[problame]

Reviewed the invariants, all look correct to me, left some comments.

---

Do I understand correctly that we don't check liveness?

---

Regarding the playing/debugging invariants: I would expect that the core spec file only contains

• actions that are actually reachable by Spec (e.g. remove unreachable "code" like BadQuorum)
• invariants that are universally true (e.g. remove CommittedNotTruncated)

Can we somehow turn BadQuorum into a unit test for the spec? Like, make Quorum a constant. Have all current configs use the correct implementation. And add a "negative test" config that uses BadQuorum and somewhere check that an invariant will be violated.

[arssher]

This model doesn't include the membership change stuff, right? I suppose that'll be a separate PR on top of this one.

Yes, working on it.

I had to comment out ALIAS.

Right, it is available only since pre-release 1.8.0; added comment on this.

In this model, Lsn means just Nat index into the wal sequence of proposer and acceptor. So, it's side-stepping that question.

I wouldn't say it is side stepping. Indeed, when we are talking about 'record LSN' it might either mean beginning of that record or end of it (which is the same as beginning of the next except alignment, and alignment is indeed side stepped here). So we must be careful to always specify which is of these is meant (and explain in comments), and that's important in the spec. For instance, FlushLsn is end of last entry, while term history entry contain LSN of the first record with this term.

[arssher]

Do I understand correctly that we don't check liveness?

Yes, I'm curious to do it, but in our case it is fairly trivial (when a proposer + majority of acceptors is alive and network is good), so not a high priority.

[arssher]

Can we somehow turn BadQuorum into a unit test for the spec?

I'm not aware of options which wouldn't need a lot of boilerplate. Generally I think the idea is that spec should be small / lightweight enough to be comfortably working with without unit tests, it's a bit too much.