cockroachdb / cockroachdb/cockroach
raft: extend TLA+ spec with leader-lease changes
Open
A-kv-replication
A-leader-leases
C-enhancement
T-kv
- Dominant language
- Go
- Stars
- 32.5k
- Forks
- 4.1k
- PR merge metrics
- PR metrics pending
Description
Extend the spec in [docs/tla-plus/LeaderLeases/RaftLeader.tla](https://github.com/cockroachdb/cockroach/pull/123189/files#diff-21b7037194f3f6e2a5a3ff9fcf10bd27b978a23e2af684392b3979deab85df70) with all leader-lease-related changes (e.g. fortification).
This will require using the store liveness spec. If we inline the it into the extended Raft spec, the model check will probably take a really long time. Instead, we can expose the external behavior of store liveness and its guarantees in a mini-spec and use that in the Raft spec.
Jira issue: CRDB-40999
Contributor guide
Assessment
This issue has not been assessed yet.