efficient / epaxos

http://efficient.github.io/epaxos/
Other
612 stars 134 forks source link

How to prove that `seq` of two command in a strong connected component are different? #11

Closed drmingdrmer closed 5 years ago

drmingdrmer commented 5 years ago

The execution order depends on the values of seq, if two commands depend on each other.

I didn't find proof of how to ensure that seqs are different in the paper.

And it seems like I can build a case to produce equal seq for two interfering commands, with 3 replicas(Maybe I missed something that could eliminate this issue):

Initially, all replicas have no data at all:

R0     R1     R2

R0 initiate command "a", R1 initiate command "b":

R0        R1         R2 
a,seq=0   b,seq=0

R0 and R1 send PreAccept to each other.
And R0 and R1 update their state:

R0        R1         R2 
a,seq=0   b,seq=0
b,seq=1   a,seq=1

When receiving PreAcceptOK responses,
both R0 and R1 believe that there is a conflicting command:
R0 has seen b, R1 has seen a.
And they both send Accept message to each other:

R0 send Accept(a, seq=1) to R1
R1 send Accept(b, seq=1) to R0

Finally R0 and R1 accepts a,seq=1 and b,seq=1:

R0        R1         R2 
a,seq=1   b,seq=1
b,seq=1   a,seq=1

And these two commands will be committed after then. but their execution order is undetermined because they have the same seq.

Please help me with what I had missed.

drmingdrmer commented 5 years ago

Oh I saw a correction tip on top of the PDF. 😄

imoraru commented 5 years ago

This is from the paper (page 8): "Case 1: Both commands are in each other’s dependency graph. By the way the graphs are constructed, this implies: (1) the dependency graphs are identical; and (2) γ and δ are in the same strongly connected component. Therefore, when executing one command, the other is also executed, and they are executed in the order of their sequence numbers (with arbitrary criteria to break ties)."

drmingdrmer commented 5 years ago

Yes I see now what "arbitrary criteria" mean. Thanks