Exercise 16: Paxos modification

[dag7dev]

Exercise 16: Assume that acceptors do not change their vote. In other words, if they vote for value $v$ in round $i$, they will not send learn messages with value different from $v$ in larger rounds. Show that Paxos, with this modification, is safe. Unfortunately, the modification introduces a severe liveness problem (the protocol can reach a livelock).

[Tommaso-Sgroi]

I don't see where the modification is. In fact, once a proposed value reaches the quorum, it will be included in the "accept" message sent by the acceptors. Eventually, in subsequent rounds, when another proposer reaches the quorum and sees a value in the "promise" messages, at least one of those messages will contain the value that reached the quorum. Therefore, the acceptors do not actually change their vote if they voted for value V in past rounds.

Am i missing something?

EDIT: i undestood what was the problem, i was thinking of Paxos as fault free; in fact if some accept messages only some acceptors will receive the proposed value. So it's possible to have more different values in acceptors in Paxos (in general not in this specific case).

[dag7dev]

I don't see where the modification is. In fact, once a proposed value reaches the quorum, it will be included in the "accept" message sent by the acceptors. Eventually, in subsequent rounds, when another proposer reaches the quorum and sees a value in the "promise" messages, at least one of those messages will contain the value that reached the quorum. Therefore, the acceptors do not actually change their vote if they voted for value V in past rounds.

Am i missing something?

Could implementing a timeout mechanism where if a proposer does not receive enough responses within a specified time, it can attempt to propose a different value be the solution to the liveness problem?

[Tommaso-Sgroi]

Could implementing a timeout mechanism where if a proposer does not receive enough responses within a specified time, it can attempt to propose a different value be the solution to the liveness problem?

The exercise doen't require a solution for the liveness problem.

[Lorenzoantonelli]

Could implementing a timeout mechanism where if a proposer does not receive enough responses within a specified time, it can attempt to propose a different value be the solution to the liveness problem?

The problem persists, even with the timeout solution. Consider a scenario with 6 acceptors, namely $a_1, \ldots, a_6$. If $a_1$ and $a_2$ vote for value $v_1$, $a_3$ and $a_4$ vote for a different value, $v_2$, which is not equal to $v_1$. Lastly, $a_5$ and $a_6$ vote for a third value $v_3$, which is also different from both $v_1$ and $v_2$. The system becomes stuck in this situation. With the timeout method in place, acceptors will still vote for value $v_1$, $v_2$, and $v_3$, respectively, resulting in the same problematic situation.

[Tommaso-Sgroi]

A possible solution i found is to demostrate the three properties mentioned in "A simpler Proof for Paxos and Fast Paxos":

1. CS1 Only a proposed value may be chosen.
2. CS2 Only a single value is chosen.
3. CS3 Only a chosen value may be learned by a correct learner.

1.: the acceptors only receive proposed values from proposers and will never change their preference, so larners will be forced to learn only a proposed value.
2.: here is the "tricky part", in fact if you try to solve it by induction as in the mentioned paper will be trivial, but a simple logic reason can be found. Since our assumption is that the value once proposed is never changed, we can see that the chosen value can be only one. That’s because that value will never change in the acceptors memory, so they’ll propose their value until one gets enough votes and the learners will choose it.
3.: the learners can learn only the most voted proposed value from the acceptors.

[EmanueleMagliaro]

Could implementing a timeout mechanism where if a proposer does not receive enough responses within a specified time, it can attempt to propose a different value be the solution to the liveness problem?

The problem persists, even with the timeout solution. Consider a scenario with 6 acceptors, namely $a_1, \ldots, a_6$. If $a_1$ and $a_2$ vote for value $v_1$, $a_3$ and $a_4$ vote for a different value, $v_2$, which is not equal to $v_1$. Lastly, $a_5$ and $a_6$ vote for a third value $v_3$, which is also different from both $v_1$ and $v_2$. The system becomes stuck in this situation. With the timeout method in place, acceptors will still vote for value $v_1$, $v_2$, and $v_3$, respectively, resulting in the same problematic situation.

I don't think that this is possible. After $a1$, $a2$, $a3$ and $a4$ have stored a value, it is impossible for a Proposer to form a majority quorum $P$ without having at least one of them in the quorum. If the quorum is formed by exactly these 4 acceptors, nothing will happen, but the next round can happen. Eventually it will come to the situation where 2 of them are in, in any combination, but the other 2 are $a5$ and $a6$.
In this case, the proposer will override its value with one of the two they have stored, the one stored in the most recent round, which could be both the one $a1$ and $a2$ have, if they are both in, or the one $a3$ and $a4$ have, if at least one of them is in. Once the accept messages get sent, $a5$ and $a6$ will store the value, and now there will be 4 acceptors with the same value, which is enough to have the learners accept the learn message and so the value is chosen; this could not happen in the next round, but can eventually happen.

Edit: Wrong

[luciafhub]

But why you say that acceptor1 vote one value, and others 2 acceptor vote for another different value? I mean this is FastPaxos, not Paxos. In Paxos, acceptors can only vote for one value in each round, so I dont understand why the modification can introduces a liveliock. Anyone knows ?

[AntoAndGar]

To show that Paxos with this modification is still safe it must satisfy the property:

1. Only a proposed value must be chosen.
2. Only a single value is chosen.
3. Only a chosen value may be learned by a correct learner.

The $1^{st}$ property is verified since nothing has changed w.r.t. the normal propose of values from Paxos, so the value v is still proposed by a proposer.

The $3^{rd}$ property is verified since if the value v is chosen by a majority of acceptors then it may be learned by a correct learner, as in Paxos.

The $2^{nd}$ property is respected as in Paxos but here is trivially verified since the acceptors can't change the value they have chosen.

So Paxos with this modification is still safe.
The liveness problem can be the same as in Paxos with the prepare followed by promises interleaved by various proposers, but this can be avoided with a leader election, so the problem introduced with the modification is as in the following example:

we have 3 acceptors, a proposer sends a prepare for round i the acceptors respond with a majority of promise(i, -, -) then the proposer sends accept(i,v), but 2 messages are lost so only 1 acceptor sends a learn(i,v). Then, another proposer sends a prepare(j) for round j>i then the 2 acceptors reply with promise(j, -, -) instead the other node does not receive the prepare so it does not reply, since the proposers got a majority of promises it sends accept(j, v') then 2 messages are lost and 1 arrive to an acceptor that has not send a learn before and now it sends a learn(j, v'), now the third acceptor crash, so from now on no majority can be formed since no one of the 2 nodes up can change its values and the protocol continues to issue new prepare and promises for greater rounds without having the possibility to change the value in the learn messages, so the protocol is in a livelock condition.
(The example is easier with a drawing than as written here)