Proposal: Trace validation roadmap

[joshuazh-x]

I'd like to propose some ideas for improving our raft implementation's quality assurance using trace validation. A draft document is prepared to outline several potential improvements to achieve this.

I'd appreciate your valuable feedback and comments helping us solidify this into a solid roadmap.

You can find the proposal document in https://docs.google.com/document/d/1oaubSgCXouT6qQ5tawup49G01loBKn4tWGMokB3ejLM/edit#heading=h.c5tbkh30ka1f.

[joshuazh-x]

cc @serathius @ahrtr @pav-kv @andreo @siyuanfoundation @MadhavJivrajani @zeu5 @felipecrv @lemmy

[lemmy]

Automated trace validation tests to verify correctness of etcd-io/raft

The CCF project has already figured out most of the bits and bobs to run trace validation and model checking as part of Azure pipelines and Github workflows:
https://github.com/microsoft/CCF/blob/main/.azure-pipelines-templates/model_checking.yml
https://github.com/microsoft/CCF/blob/main/.github/workflows/tlaplus.yml

Verification of linearizability

The CCF project validates traces of KV reads and writes against its client-centric consistency specification. This work should directly translate. Other definitions can be taken over from https://github.com/lorin/tla-linearizability.

Improve trace validation test performance

Validation time should increase linearly with the length of the log, unless non-determinism causes state-space explosion along the log.