Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Introduce ReplicaEngine model #29

Merged
Merged
Changes from 1 commit
Commits
Show all changes
27 commits
Select commit Hold shift + click to select a range
28b2442
Introduce ReplicaEngine model
DaveCTurner Mar 22, 2018
5f21a25
Fix modelling of deletions
DaveCTurner Mar 23, 2018
6fac39b
Introduce label in LuceneLoop
DaveCTurner Mar 23, 2018
857d9b3
Fix ApplyBufferedOperations
DaveCTurner Mar 23, 2018
cb9da3f
Fix invariant
DaveCTurner Mar 23, 2018
567dc45
Boaz fixes
DaveCTurner Mar 23, 2018
0ceddd1
Set versionMap_needsSafeAccess on deletion
DaveCTurner Mar 23, 2018
019272c
Do not create a DELETE as the first operation on the doc
DaveCTurner Mar 23, 2018
0b46bb7
Revert "Do not create a DELETE as the first operation on the doc"
DaveCTurner Mar 23, 2018
c843c79
Rename model to 'model' and remove generated files
DaveCTurner Mar 23, 2018
add11da
Remove bogus expression
DaveCTurner Mar 23, 2018
43478b9
Lucene can refresh even if the buffer is empty (because other docs)
DaveCTurner Mar 23, 2018
88ef32b
Need safe access after a forced refresh
DaveCTurner Mar 23, 2018
a1c7b7f
No need for modification history
DaveCTurner Mar 23, 2018
2306b48
Separate variables for Lucene
DaveCTurner Mar 23, 2018
0e31664
Shorter description of permitted requests
DaveCTurner Mar 23, 2018
f2fcecb
Track maxSeqNoOfNonAppendOnlyOperations
DaveCTurner Mar 23, 2018
33cbeda
Preserve GC deletes according to local checkpoint
DaveCTurner Mar 23, 2018
893a0ed
Add proposed fix for desync bug #3
DaveCTurner Mar 26, 2018
bd97a0a
Remove label within Lucene process
DaveCTurner Mar 26, 2018
a643c14
TIL \notIn
DaveCTurner Mar 27, 2018
36454d7
Model nondeterministically increasing maxSeqNoOfNonAppendOnlyOperations
DaveCTurner Mar 27, 2018
d1426a6
Flip needsSafeAccess both ways
DaveCTurner Mar 27, 2018
8cd6ce9
Account for duplicated messages
DaveCTurner Mar 27, 2018
74c017e
Limit number of duplicated messages processed
DaveCTurner Mar 27, 2018
8982236
Need to check the local checkpoint _after_ getVersionFromMap too
DaveCTurner Mar 27, 2018
8ac6716
Added ref to PR #29276
DaveCTurner Mar 28, 2018
File filter...
Filter file types
Jump to…
Jump to file or symbol
Failed to load files and symbols.

Always

Just for now

Add proposed fix for desync bug #3

  • Loading branch information...
DaveCTurner committed Mar 26, 2018
commit 893a0edbce86b2e114ea59de4170c838024fc6ac
@@ -381,6 +381,13 @@ begin
versionMap_entry := [ type |-> UPDATE, seqno |-> req.seqno ];
else
versionMap_isUnsafe := TRUE;

if /\ versionMap_entry /= NULL
/\ versionMap_entry.type = DELETE
/\ versionMap_entry.seqno < req.seqno
then
versionMap_entry := NULL; \* Desync bug #3 (no PR number yet)
end if;
end if;
end if;

ProTip! Use n and p to navigate between commits in a pull request.
You can’t perform that action at this time.