CAAT dataraces/cat_spec #660
Merged
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
…nder an even number of negations (and thus are effectively positive). We perform a rewriting on the memory model so that the standard cutting approach does only cut truly negative relations. As a result, we can handle flagged axioms a lot more efficiently in many cases, in particular, when checking races. Due to this, Refinement can now handle CAT_SPEC.
… rhs of differences.
Fixed a non-progress situation that could occur when computing too many trivial core reasons related to out-of-bounds accesses or similar cases where our static analyses are not sound.
dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java
Outdated
Show resolved
Hide resolved
dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java
Outdated
Show resolved
Hide resolved
dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java
Outdated
Show resolved
Hide resolved
dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java
Outdated
Show resolved
Hide resolved
dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java
Outdated
Show resolved
Hide resolved
dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java
Outdated
Show resolved
Hide resolved
dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java
Show resolved
Hide resolved
Added proof of correctness to the new rewriting step.
dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java
Show resolved
Hide resolved
dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java
Outdated
Show resolved
Hide resolved
dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java
Outdated
Show resolved
Hide resolved
dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java
Outdated
Show resolved
Hide resolved
dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java
Outdated
Show resolved
Hide resolved
dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java
Show resolved
Hide resolved
dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java
Show resolved
Hide resolved
tonghaining
pushed a commit
to tonghaining/Dat3M
that referenced
this pull request
May 24, 2024
* Generalized RefinementSolver to better handle relations that appear under an even number of negations (and thus are effectively positive). We perform a rewriting on the memory model so that the standard cutting approach does only cut truly negative relations. As a result, we can handle flagged axioms a lot more efficiently in many cases, in particular, when checking races. Due to this, Refinement can now handle CAT_SPEC. * Fixed cat violation reporting with CAAT * Fixed a non-progress situation that could occur when computing too many trivial core reasons related to out-of-bounds accesses or similar cases where our static analyses are not sound.
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 support for checking
cat_specwith CAAT, in particular, for checking data races.Since data races are negatively formulated conditions, cutting is necessary.
Typically, this cutting approach would cut off so much of the memory model that most of it needs to get encoded eagerly again.
The trick this PR adds is a memory model rewriting step that makes sure that cutting affects only the parts of the model that are "truly negative", i.e., those that appear under an odd number of negations.
For example, in
~empty(dr), dr = conf \ hb, thehbis actually "positive" and the rewriting makes sure it does not get cut.More generally, the rewriting is irrespective of
cat_specand data races, but applies to all memory models that have nested negations. It's just that data races are a canonical example of nested negations where the complex relation (hb) is positive.Aside from this, the PR improves CAAT core reasoning and fixes a non-termination issue (for highly symmetric benchmarks) recently introduced in #656 .