Fix bitcask_pulse model to know when a keydir may have been frozen. #181
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
* Rename `bitcask_nifs:keydir_remove/3` -> * `bitcask_nifs:keydir_remove_int/3`
* Use a compile-time -ifdef magic to add `pulse_log_call()` wrappers
around all keydir NIF calls that can mutate the keydir.
* Make several changes to the bitcask_pulse model:
* Filter out bad reads from either kind of bad folds
* If a bad read happens, that's bad
* If a bad fold happens, then figure out during what period of
at-last-one-folder-is-running-time that the bad result appeared.
Then figure out if a keydir mutating NIF was called; if yes,
then it's possible that the keydir was frozen ... we don't know
for sure, but we won't cause the model to fail in this case.
1. Use `keydir_call` and `keydir_return` for the trace labels for NIF mutations. 2. Only consider *successful* mutations when checking for keydir frozenness.
|
ping? |
1 similar comment
|
ping? |
|
@engelsanchez Whatchathink about this model change? |
|
Honestly @slfritchie, I'd like to do this in a different way. I think it should be possible to change our internal API to expose the epochs generated inside of Bitcask that determine the visibility of the values for the folds, as well as the epochs used when folding to verify. That way we can determine exactly what we should be seeing and have a stricter model. I will try to give that a go in the 2.0.2 cycle. |
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.
Fixes #180.
bitcask_nifs:keydir_remove/3-> *bitcask_nifs:keydir_remove_int/3pulse_log_call()wrappersaround all keydir NIF calls that can mutate the keydir.
at-last-one-folder-is-running-time that the bad result appeared.
Then figure out if a keydir mutating NIF was called; if yes,
then it's possible that the keydir was frozen ... we don't know
for sure, but we won't cause the model to fail in this case.