QLS: test that we do not swallow exceptions #587
Merged
Conversation
This file contains hidden or 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
jorisdral
force-pushed
the
jdral/all-actions-get-errors
branch
from
c604654 to
cea8219
Compare
jorisdral
force-pushed
the
jdral/swallowed-exceptions
branch
3 times, most recently
from
9354949 to
72f7383
Compare
jorisdral
force-pushed
the
jdral/all-actions-get-errors
branch
2 times, most recently
from
6ac95c6 to
7c84a2a
Compare
jorisdral
force-pushed
the
jdral/swallowed-exceptions
branch
from
72f7383 to
ba32682
Compare
jorisdral
requested review from
dcoutts,
mheinzel,
recursion-ninja and
wenkokke
as code owners
Collaborator
Author
|
BTW, this PR depends on #578 being reviewed and merged first. |
jorisdral
commented
Feb 25, 2025
dcoutts
reviewed
Feb 25, 2025
jorisdral
force-pushed
the
jdral/all-actions-get-errors
branch
from
7c84a2a to
0969c5a
Compare
jorisdral
force-pushed
the
jdral/swallowed-exceptions
branch
from
ba32682 to
6243344
Compare
jorisdral
force-pushed
the
jdral/swallowed-exceptions
branch
from
6a3249b to
3e074a6
Compare
dcoutts
reviewed
Mar 5, 2025
Collaborator
dcoutts
left a comment
dcoutts
left a comment
There was a problem hiding this comment.
This is looking very good.
wenkokke
reviewed
Mar 5, 2025
| -- restrictive, but this automatically improves as we make more actions | ||
| -- exceptions safe. When we generate injected errors for these errors by default | ||
| -- (in @arbitraryWithVars@), the swallowed exception assertion automatically | ||
| -- runs for those actions as well. |
Collaborator
There was a problem hiding this comment.
What is the motivation behind only running the action with a definite error last?
Collaborator
Author
There was a problem hiding this comment.
It's mentioned in the text above this TODO: database behaviour should be considered undefined after an exception is thrown in exception unsafe code. If we run more actions afterwards, the SUT and model are almost certainly going to disagree on their responses
Collaborator
|
#607 is now in the merge queue, so this can be rebased on that. |
jorisdral
force-pushed
the
jdral/swallowed-exceptions
branch
4 times, most recently
from
f60ace5 to
ff129e7
Compare
dcoutts
approved these changes
Mar 10, 2025
Collaborator
dcoutts
left a comment
dcoutts
left a comment
There was a problem hiding this comment.
The changes based on review feedback look good.
Squash the fixups and merge! 😄
We will be testing that `lsm-tree` operations do not swallow errors by injecting errors into the simulated file system and checking after the fact whether we should have seen an exception or not. One way to check this would be to compare the `Errors` structure before and after the `lsm-tree` operations, but this is unfortunately not possible in general. `Errors` are potentially infinite structures, which means computing a comparison on `Errors` may diverge. Instead, what we do is we create an `ErrorsLog` structure that records errors as soon as they are injected. We can inspect this log to see if any errors were swallowed.
When we start testing that errors are not swallowed by `lsm-tree`, we'll be injecting errors into bits of code that are not exception safe (yet). As a result, the checks mentioned in the commit title would lead to property failures. However, we just want to test that errors are not swallowed, so we make these checks configurable. File system checks, cleanup checks, and reference checks can enabled/disabled independently.
This property runs a sequence of state machine actions where the last action definitely injects errors, at which point we can check if no errors are swallowed. See the documentation of `prop_noSwallowedExceptions` for more information. The property is currently expected to fail.
We replace the assertions by pure responses that are checked against the model.
jorisdral
force-pushed
the
jdral/swallowed-exceptions
branch
from
ff129e7 to
4e62a8a
Compare
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.
This PR adds
fs-simfs-sim. That is, the assertion checks that no noisy errors are swallowed.DL) formula that injects errors into alllsm-treeactions and runs the swallow error assertion afterwards.