4 ms·

"deliberately avoids any formal specification or proof" how is this possibly a selling point?

scottlamb 3y ago
> "deliberately avoids any formal specification or proof" > how is this possibly a selling point? Context. In an overview doc? The informal version is accessible to more audiences. As the canonical design doc for the system? It's certainly not.
- anentropic 3y ago
  Apologies! I was only blindly responding to the parent comment... FWIW the phrase seems to come from here: https://bloomberg.github.io/blazingmq/docs/architecture/election_rsm/#the-leader-election-algorithm-in-blazingmq https://bloomberg.github.io/blazingmq/docs/architecture/elec... The full sentence reads: "This section explains the leader election algorithm at a high level. It is by no means exhaustive and deliberately avoids any formal specification or proof." Which makes a lot more sense. And as noted in a sibling comment there is actually a TLA+ spec for the leader election: https://github.com/bloomberg/blazingmq/tree/main/etc/tlaplus https://github.com/bloomberg/blazingmq/tree/main/etc/tlaplus
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 ago
  One 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 ago
    How is this "deliberately avoiding any formal specification or proof"?
    - peheje 3y ago
      I think they are referring to the specific section below the notice.
      - callbacker 3y ago
        Correct

> "deliberately avoids any formal specification or proof" > how is this possibly a selling point? Context. In an overview doc? The informal version is accessible to more audiences. As the canonical design doc for the system? It's certainly not.

anentropic 3y ago
Apologies! I was only blindly responding to the parent comment... FWIW the phrase seems to come from here: https://bloomberg.github.io/blazingmq/docs/architecture/election_rsm/#the-leader-election-algorithm-in-blazingmq https://bloomberg.github.io/blazingmq/docs/architecture/elec... The full sentence reads: "This section explains the leader election algorithm at a high level. It is by no means exhaustive and deliberately avoids any formal specification or proof." Which makes a lot more sense. And as noted in a sibling comment there is actually a TLA+ spec for the leader election: https://github.com/bloomberg/blazingmq/tree/main/etc/tlaplus https://github.com/bloomberg/blazingmq/tree/main/etc/tlaplus

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 ago
One 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 ago
  How is this "deliberately avoiding any formal specification or proof"?
  - peheje 3y ago
    I think they are referring to the specific section below the notice.
    - callbacker 3y ago
      Correct