Recovery implementation violates Invariants 8 + 1

[kewbish]

(We're researchers from NJU/MSR/UIUC/UBC working on automating system specification in TLA+. We've been using our tool on SwiftPaxos and wanted to contribute our findings back, if the team finds this useful! We understand this is research code and just wanted to confirm if our reports are valid.)

Invariant 8 of the paper (pg 8) states: if a replica sends `Ack` at ballot `b` and `NewLeaderAck` at ballot `b' > b`, it sends `Ack` before `NewLeaderAck`.

The implementation does not seem to order acks in the channel during recovery. For example:

1. Before recovery, replica enqueues an old-ballot Ack into batcher (e.g. here)
2. Replica receives NewLeader(b') and enters recovery:
   • handleNewLeader immediately sends NewLeaderAckN here
3. It seems batcher is not stopped/drained by recovery and continues running (e.g. goroutine loop here)
4. batcher can still emit an old-ballot Ack afterwards, since there's no filtering of stale ballots in the sender channel itself.

Because producer goroutines race to enqueue into sender, there is no guarantee the old `Ack`s are enqueued before the new ones. It seems that flushing batcher might also be necessary.

---

Also, when merging the new ballots, there is no equality or conflict check before cmdIds are overwritten here. Because the map iteration orders are unstable per local replica, it is possible commands with different phases across replicas could be overridden.

This seems to violate Invariant 1 (pg 4), which states: any two replicas commit a command with the same set of dependencies. On recovery, two replicas could end up with different dependency phases.

Can you please confirm whether or not this is a valid bug in the system as it is currently implemented?

[vonaka]

Thanks again! I think you're right (again). But again, I believe the invariant as stated is stronger than what we actually need for correctness.

What we really need is to say that the state a process includes in a NewLeaderAck for a higher ballot is not older than its state when it sends Ack for a lower ballot. I believe in the implementation this holds regardless of the actual send order of those messages. In this particular case, it seems better to adjust the proof than enforce a specific send order without any good reason.

Regarding your second comment: the lines you're pointing to are executed by a single process per ballot (the leader of that ballot). Followers just adopt the state when they receive Sync. So within a ballot, there's no disagreement. There could be a disagreement across ballots, but there correctness follows from vanilla Paxos, since we do check ballot equality in all the relevant handlers.

[kewbish]

Good to know this shouldn't affect correctness!

In this particular case, it seems better to adjust the proof than enforce a specific send order without any good reason.

We're curious how the proof would need to change to accommodate this, do keep us updated if there's any progress.