TLA+ for reconciliation process after resuming #43
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Instead of checking only a particular table, we can now check all tables and ensure that Ghostferry works on all of them. The check time on my machine is not super large either, at about 3 minutes for a table size of 3.
shuhaowu
commented
Jun 26, 2018
| @@ -386,51 +494,90 @@ PossibleRecords == Records \cup {NoRecordHere} | |||
| ***************************************************************************) | |||
| \* BEGIN TRANSLATION | |||
There was a problem hiding this comment.
Everything below this is just automatically generated by TLA+.
This adds the ability to model reconciliation in Ghostferry.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
When we interrupt Ghostferry, we except to resume later. The two important things are: catching up the changes done to the source database by reading the binlogs and memorizing and restarting from a known PK position. The memorized binlog positions could also be configured by constants as an underestimate to the true locations of a previous run.
The changes to the source database while Ghostferry is down is performed by the Ferry process, as I haven't figured out a way generate a modified SourceTable directly during the Init. During the process that the source changes are initialized by the Ferry, the application is not writing to the database to simplify the model. Once the reconciliation starts, the modeled application begins writing to the database.
This is still kind of a WIP as I'm not 100% confident that it is correct. The model with the reconciliation is also not fast to verify as it took ~50min on my laptop (albeit within a VM), checking ~660M states (~190M unique states). This run is subject to an action constraint where the BinlogSize is restricted to 5 (with 3 already filled due to the changes that occurred while Ghostferry is theoretically down, so realistically 2 changes after starting Ghostferry). If the BinlogSize is restricted to 4, the amount of time reduce to ~5min.
The first two commit also addresses #14