Open joshuazh-x opened 3 months ago
cc @serathius @ahrtr @pav-kv @andreo @siyuanfoundation @MadhavJivrajani @zeu5 @felipecrv @lemmy
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
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.
Validation time should increase linearly with the length of the log, unless non-determinism causes state-space explosion along the log.
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.