mirror of
https://github.com/neondatabase/neon.git
synced 2026-01-04 03:52:56 +00:00
fa909c27fc
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 https://github.com/neondatabase/neon/issues/8699
13 lines
622 B
Markdown
13 lines
622 B
Markdown
The specifications, models and results of running of them of the compute <->
|
|
safekeepers consensus algorithm for committing WAL on the fleet of safekeepers.
|
|
Following Paxos parlance, compute which writes WAL is called (WAL) proposer here
|
|
and safekeepers which persist it are called (WAL) acceptors.
|
|
|
|
Directory structure:
|
|
- Use modelcheck.sh to run TLC.
|
|
- MC*.tla contains bits of TLA+ needed for TLC like constraining the state space, and models/ actual models.
|
|
- Other .tla files are the actual specs.
|
|
|
|
Structure is partially borrowed from
|
|
[logless-reconfig](https://github.com/will62794/logless-reconfig), thanks to it.
|