-
Notifications
You must be signed in to change notification settings - Fork 29
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
Relation analysis with immutable and lazy data structures #743
Conversation
// Force adding must edges to match the result of native analysis | ||
// TODO: Is it really necessary? Method getEventGraph appends them anyway |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Do you mean that without this changes we get different sets for native and analysis, but you believe we could get rid of all the addAll(eg)
in both cases without affecting correctness?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
To me it looks inconsistent (and possibly redundant) that must edges of an axiom relation are added during the computation of encode sets and again in the "getEventGraph" method. But it is not related to the lazy relation analysis.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This comes from an ambiguity in our modelling. In reality, you have "active sets" which refers to sets of clauses/constraints that need to get respected (i.e., they are not trivially satisfiable) and "relevant literals" which can affect the truth-value of an active constraint.
In the mathematically precise sense, the axioms generate some encoding of arbitrary shape that refers to variables (edges) and all those variables are "relevant". For each relevant variable, its defining constraint now becomes active, which in turn causes other variables to become relevant and this propagates recursively downwards.
Our current modelling uses "encode sets" to kinda refer to both "relevant literals" and "active constraints" though it mostly means the latter (i.e, a Map<Definition, EventGraph>
would be more correct). And for active constraints, you can actually have an active defining constraint for a variable that is statically known (i.e., inside must or outside may) and that is why "encodeSet" does not always satisfy the expected must-set \subseteq encodeSet \subseteq may-set
inequality.
That being said, the method axiom.getEncodeGraph
actually refers to "relevant variables" of the axiom (I know, this is confusing) and there we can indeed (I believe) make sure to never include statically known variables.
Due to the ambiguity, we have thus far allowed axiom.getEncodeGraph
to contain statically known variables though.
In short, you can remove must-edges from the encode set of axioms if you want.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@natgavrilenko can you please remove those both here and in the native analysis?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I would prefer to keep things separately. This commit is for a lazy relation analysis. If someone wants to make changes to the native analysis, better to do it in a different commit.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
But then this commit should not add unnecessary code (as suggested by the comment in the commit)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
??? without this the lazy sets will not match the native sets
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Then the claim that this commit has nothing to do with the native analysis does not hold and this needs to be fixed.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
What needs to be fixed? Removing the must-sets also in the native analysis? I think it is fair to not touch the native analysis in this PR, take it as ground truth, and let the lazy analysis mimic its results (as it is done now).
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think it is a bad idea adding useless stuff to a new implementation just to mimic the behavior of another fishy implementation. But if you both agree that it it's not worth to properly fix this now, I will not object further.
dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/LazyRelationAnalysis.java
Show resolved
Hide resolved
dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/LazyRelationAnalysis.java
Show resolved
Hide resolved
dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/LazyRelationAnalysis.java
Show resolved
Hide resolved
dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/LazyRelationAnalysis.java
Show resolved
Hide resolved
dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/LazyRelationAnalysis.java
Show resolved
Hide resolved
dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/graph/EventGraph.java
Show resolved
Hide resolved
dartagnan/src/test/java/com/dat3m/dartagnan/encoding/RelationAnalysisTest.java
Outdated
Show resolved
Hide resolved
b632f5c
to
b97fa45
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I saw that you make use of a lot of parallel operations and ConcurrentHashMap
. Do you by chance have any data/estimate (even anecdotal is fine) on how much this improves performance compared to the standard sequential operations?
...gnan/src/main/java/com/dat3m/dartagnan/wmm/utils/graph/immutable/ImmutableMapEventGraph.java
Outdated
Show resolved
Hide resolved
dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/graph/immutable/LazyEventGraph.java
Outdated
Show resolved
Hide resolved
Depends on the tests and the hardware. For small litmus tests there can be overhead. In the "worst" examples (not a part of dartagnan tests), I saw up to 10 times speedup for some relations. |
Ok, that sounds great. I guess the speedup can be almost linear in the number of available/used threads when doing bulk copying. |
No description provided.