5 ms·
FWIW they mention this at the bottom of their document > Just like BlazingMQ’s other subsystems, its leader election implementation (and general replicated sta
by fizwhiz 3y ago
FWIW they mention this at the bottom of their document
> Just like BlazingMQ’s other subsystems, its leader election implementation (and general replicated state machinery) is tested with unit and integration tests. In addition, we periodically run chaos testing on BlazingMQ using our Jepsen chaos testing suite, which we will be publishing soon as open source. We have also tested our implementation with a TLA+ specification for BlazingMQ’s elector state machine.
- callbacker 3y agoOne of the authors here. Thanks for pointing that out. TLA+ spec can be found here -- https://github.com/bloomberg/blazingmq/tree/main/etc/tlaplus https://github.com/bloomberg/blazingmq/tree/main/etc/tlaplus.
- amelius 3y agoHow is this "deliberately avoiding any formal specification or proof"?
- peheje 3y agoI think they are referring to the specific section below the notice.
- callbacker 3y agoCorrect