TLA Spec for ordered replication in Ambry with Replica Tokens #2
Conversation
Each replica tracks a replicaToken which is the offset upto which is it up-to-date with its peers. A replica only sends back only message from its log on recieving a replication request.
ankagrawal
force-pushed
the
ordered_replication
branch
from
dc48e1b to
fcefe12
Compare
ankagrawal
changed the title
| * Ambry generates the blobid for each user requests. | ||
| * In this spec, everytime new blob is written to Ambry, Ambry increments a zero-based counter and uses that as the blobid. | ||
| *) | ||
| BlobIds == 0 .. NumBlobs-1 |
There was a problem hiding this comment.
Weird nit: Any reason why these must be zero based?
There was a problem hiding this comment.
No reason. Just easier to think as a software engineer.
replication/OrderedReplication.tla
Outdated
| \/ RecvPut | ||
| \/ \E blobid \in BlobIds: | ||
| \/ RecvUpdateTtl(blobid) | ||
| \* \/ \E blobid \in BlobIds: |
There was a problem hiding this comment.
Yes. I will uncomment.
| /\ blobIdCtr <= NumBlobs \* To Remove | ||
| /\ \E r1, r2 \in Replicas: | ||
| /\ r1 # r2 | ||
| /\ orderedStoredMessagesPerReplica' = [r \in DOMAIN orderedStoredMessagesPerReplica |-> |
There was a problem hiding this comment.
This looks a little strange to me, but maybe it's because I don't understand it? It seems like we're setting orderedStoredMessagesPerReplica' to be some element of orderedStoredMessagesPerReplica by setting it equal to orderedStoredMessagesPerReplica[r]. Shouldn't it be something like orderedStoredMessagesPerReplica' = [orderedStoredMessagesPerReplica EXCEPT ....]?
There was a problem hiding this comment.
oh wait. I see. You've effectively done what EXCEPT does with r \in DOMAIN... Ok, in that case I think this works.
There was a problem hiding this comment.
Ok, other question.
\E r1, r2 \in Replicas. It seems that we do the operation on two Replicas at a time for all these Recv functions. Why is that? AFAICT, it looks like we do symmetrical operations for both replicas.
There was a problem hiding this comment.
We do the put operation on two replicas at a time because thats the quorum for each operation. Each operation is sent to two replicas and is successful only if applied to two replicas.
But you have a good point. There is no guarantee for the operation to be atomic, and the above implementation makes it atomic. Let me try to fix it and update.
| /\ inflightReplicationResponse[r] # {} | ||
| /\ \E msg \in inflightReplicationResponse[r]: | ||
| /\ \E message \in msg.messages: | ||
| /\ IF message.blobmessage = UPDATE_TTL THEN |
There was a problem hiding this comment.
Maybe pull some of these out to UPDATE_TTL/PUT/DELETE just for readabilities sake if possible?
| RecvReplicationResponse(r) == | ||
| /\ inflightReplicationResponse[r] # {} | ||
| /\ \E msg \in inflightReplicationResponse[r]: | ||
| /\ \E message \in msg.messages: |
There was a problem hiding this comment.
Is there any need for ordering? Are all messages downloaded in parallel in prod?
replication/OrderedReplication.tla
Outdated
| ELSE | ||
| orderedStoredMessagesPerReplica[rr] | ||
| ] | ||
| /\ \E message \in msg.messages: |
There was a problem hiding this comment.
So. This \E message \in msg.messages may refer to a different message then the one picked out in the above clause that looks identical. Is that ok? My initial thought looking at this was that we could combine these three for message update/offset update/token update. Buuuut.... if it's actually desirable they diverge, then maybe this is the way to go?
There was a problem hiding this comment.
Thanks for pointing this out. I will fix this. I totally missed the fact that \E can pick any entry.
This Spec fixes the limitation in AmbryReplication spec that the replica local log is not ordered, and that replication doesn't make progress via replica token.