Relation analysis with immutable and lazy data structures

[natgavrilenko]

No description provided.

[hernanponcedeleon]

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?

[natgavrilenko]

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.

[ThomasHaas]

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.

[hernanponcedeleon]

@natgavrilenko can you please remove those both here and in the native analysis?

[natgavrilenko]

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.

[hernanponcedeleon]

But then this commit should not add unnecessary code (as suggested by the comment in the commit)

[natgavrilenko]

??? without this the lazy sets will not match the native sets

[hernanponcedeleon]

Then the claim that this commit has nothing to do with the native analysis does not hold and this needs to be fixed.

[ThomasHaas]

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).

[hernanponcedeleon]

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.

[ThomasHaas]

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?

[natgavrilenko]

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?

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.

[ThomasHaas]

Ok, that sounds great. I guess the speedup can be almost linear in the number of available/used threads when doing bulk copying.