Linearizability or atomic broadcast property

[tisonkun]

It seems that the Synod protocol defines a slot number based sequential proposals state in the Replica.

However, the leader retries the proposal with blot_number.round + 1 if it determinates a high-priority proposal. This can lead a reverse order of proposals if a latter proposal gets accepted first.

I wonder if I get it wrong or is there other extension to ensure linearizability or atomic broadcast property for the state changed apply order.

[tisonkun]

It seems that Replica#perform does some sort to keep the perform order. But I don't work out or find a prove for it.

[tisonkun]

If c″≠c′, that is, the replica proposed a different command for that slot, the replica returns c″ to set requests so c″ is proposed again at a later time. Next, the replica invokes perform(c′).

But a replica can silently repropose requests so the order is not promised.