Add model for interaction between Lucene & Version Map on replicas #28
Conversation
The replica does not inspect the version field, so it can simply be removed.
|
Summary of verbal review with @bleskes: The document versions are not relevant for the replica - they are a relic of older models that modelled more of the primary too. Removed in 0165d83. However, the model of Lucene needs refinement: we model replacement of a document as if calling the update API, but there is also an add API which doesn't delete any previous versions first. The add API can only be used if we're sure there is nothing that needs removing, but is more efficient so should be used where possible. The add API can be modelled as having the same effect as the update API but with an additional assertion that there is no document to overwrite. |
|
@dnhatn it's likely you will be involved in the implementation of this so it might be useful for you to contemplate this PR too. Not sure what level you're at with this kind of modelling but I have time to walk you through it if needed. |
DaveCTurner
force-pushed
the
2018-02-13-version-map
branch
from
c7d21d2 to
8e8fcfd
Compare
|
@DaveCTurner Thanks for pinging me. I think I will focus on the implementation. I will surely have a look on this but mainly for learning purpose. |
Generator should generate ADD operations only with seq# 1. Retried ADD operations are treated as UPDATEs.
|
|
||
| else | ||
|
|
||
| AdvanceLocalCheckPoint: |
There was a problem hiding this comment.
Do we want the advancing of the local checkpoint to be a separate process?
|
|
||
| Termination == <>(\A self \in ProcSet: pc[self] = "Done") | ||
|
|
||
| \* END TRANSLATION |
There was a problem hiding this comment.
Do we want some more invariants below? At the moment they're mostly about properties at termination, which is simple and ought to be sufficient, but we could have more if desired.
|
Closing this in favour of #29. |
This adds a model for how we should track sequence numbers for indexing and deletions in the replica, using the Version Map and Lucene. It includes an optimisation that can avoid the need to perform these (relatively expensive) checks for append-only operations when it is safe to do so.