Protocol refinements based on formal verification

[pavel-kirienko]

See the formal verification notes for the rationale.

The model revealed that uniform ageing rates speed up convergence. The current imprecise logical clock is a poor solution. Use either:

• Wall clock. Synchronization is not needed, only rate matters.
• A stricter logical clock.

Collisions should not be checked for if the topic is known.

• If a divergence is not discovered, then there may be no collision as it would have been discovered locally.
• If a divergence is discovered and we win arbitration, then the remote will adjust and the collision will be resolved on that end.
• If we lose arbitration, the local replica will be moved either into a new slot, or by displacing the contender.