Relation Model Implementation

[CapZTr]

This PR is related to #732 and contains the following:

1. Implementation of RelationModel, a representation of relations in Dartagnan dedicated for better witness generation, and the corresponding "RelationModelManager" that is responsible for construction of RelationModel and computation of derived relations.
2. Support of witness generation for showing relations defined in the model vmm.cat. Users may pass --witness.relationsToShow=r1,r2,r3... into the command to have witness for corresponding relations.
3. Add Local and Assert events to witness graph. But note code of this part is temporary and needs to be refined, which will be done in the next step: implementation of EventModel...

[ThomasHaas]

I would advice against reimplementing the computation of derived relations: this is very tricky.
Indeed, your code fails on recursive memory models and fixing this is non-trivial.

You should take a look into the package of CAATSolver, especially into the classes PredicateHierarchy and SimpleGraph.
A PredicateHierarchy has a concrete set of base predicates (~ base relations) and a set of derived predicates (~ derived relations), similar to Wmm. What you can then do is populate the base graphs with concrete edges (your RelationModels) and then let the PredicateHierarchy correctly populate all derived graphs.
Constructing a PredicateHierarchy from a Wmm has some minor edge cases, but you can check out ExecutionGraph which does precisely this.
However, that class uses custom graph implementations for the base predicates that can populate themselves from an SMT model.
In your case, I would just copy that code but replace all these special graphs for base relations by SimpleGraph, which you can populate however you want (e.g., with edges from your RelationModel of the base relations).

[CapZTr]

Thanks for the comment.

fails on recursive memory models

Could you please give me an example of this?

[ThomasHaas]

power.cat has recursive definitions. I have not checked what your code would do on that model, but I didn't see any handling of recursion.
For example:

// Alternative version of the SC memory model
let hb0 = rf | co | fr | po
let rec hb = hb0 | hb0;hb // same as "let hb = hb0+" just expressed with recursion.

irreflexive hb

// show hb

If you now have an execution model that has only relation models for rf, co, po, then your code would not be able to compute the relation model of hb as far as I can tell. But I guess that is the idea of your code, right?

[hernanponcedeleon]

Yes, this does not work ... there seems to be infinite recursive calls to

com.dat3m.dartagnan.verification.model.relation.RelationModelManager.extractRelation(RelationModelManager.java:68)

[CapZTr]

In your case, I would just copy that code but replace all these special graphs for base relations by SimpleGraph, which you can populate however you want (e.g., with edges from your RelationModel of the base relations).

Hey @ThomasHaas , thanks for the advice. For computation of derived relations, what about using the specific graphs also for each base relation and let them populate themselves? So we will have a consistent way on the relation computation for solving and witness generation, the only difference is that for latter we do not construct all relations but perform the computation on demand.

And for special requirements for witness, corresponding methods can be implemented to populate the RelationModels. E.g. in the graph we want PO edges to connect also Locals and Asserts.

[ThomasHaas]

That won't work out-of-the-box, because the specific graphs populate themselves based on the ExecutionModel or the underlying (SMT)Model. In this case, the ExecutionModel already needs to contain enough information for all base relations, i.e., it already needs rf, co, etc.
In other words, they populate themselves based on "implicit" RelationModels so you cannot generate the RelationModels from the special graphs without running into cycles :). Btw. the special graphs not only populate themselves but also rely on implicit representation, e.g., the ProgramOrderGraph uses only O(1) space to describe a relation of size O(n^2).
Now, it is true that e.g. ProgramOrderGraph can populate itself based solely on EventData and that could be reused, but at least for rf and co you need to do it differently.

Let me summarize what I think you should do:
(1) Have explicit(*) graphs for the base relations, i.e., SimpleGraph. This is as general as it gets because those explicit graphs can be generated from the SMT model, from parsing files, or even by hand.
(2) Reuse CAAT-functionality to compute all derived relations on demand.
(3) Do NOT add Locals and Asserts into po. This is incorrect and will cause all derived relations to be messed up. Instead, you should either have a special localPo relation model that you maintain but that is never used in the derived relations (well, you could compute po via let po = localPo & _*_ if you wanted), or you simply change the printing of witnesses to include the local events without relying on po to do so.

To elaborate more on point (3) above. I think your ExecutionModel should have EventData/Models for every piece of executed code (maybe modulo minor exceptions). But no matter what events it contains, the base relations used in the memory model should never contain any of the extra events (except maybe special internal relations like idd, if you even want to track them at all).
Also, just because the ExecutionModel contains information about events/relations, the printer does not necessarily have to print them! In particular, you should not force events into relations or omit events from the model just because you do/don't want to print them in the end. I can easily imagine that the user could specify levels-of-detail when printing the model.

(*) Well, for relations like po, int, ext and loc you could also have implicit representations based on the EventData/Model to save space (this is what CAAT does). But for now, it is easiest to just make all of them explicit.

[CapZTr]

OK, understood.

Eventually, the ExecutionModel should be:

(1) in the initialization, EventModels for all Events and RelationModels for at least po, rf, co should be constructed, which provides the necessary information for the solving purpose of CAAT-part, i.e. the special graphs can populate themselves and the PredicateHierarchy can perform the computation.
(2) for witness generation, more constructions of RelationModels and computations of derived ones happen on demand.

Am I right about this part?

BTW, my plan is to implement the RelationModel first and let this model interact perfectly with other parts of what we have now, which is also the goal of this PR. And the next step is to implement the EventModel and let it "replace" the current EventData and also adjust the ExecutionModel as what we want it to be (like discussed in #732 )

[ThomasHaas]

There is a question about efficiency here. If you always generate explicit models for po, rf, co, etc., you can also replace CAAT's special graphs and let it directly work over your explicit representation. The disadvantage, of course, is that this is theoretically more space/time-consuming. I can imagine that it does not matter much though.

But maybe, you should tackle this problem a little bit differently to avoid interacting with the CAAT-based solving at all for now (this makes things just more difficult).
You could keep the existing ExecutionModel class for use by CAAT (it was originally written with CAAT in mind), but introduce a new one for all other usages (mainly printing right now). There you can write all the code from scratch without worrying that it needs to work with existing infrastrucutre. Once you have a clean implementation of (New)ExecutionModel, EventModel and RelationModel, you can start replacing existing usages of the old ExecutionModel by the new one step-by-step, starting from printing-related code to eventually CAAT.
The point is that we first need a way to represent all the information of an execution we could possibly care about, and then we need to see how we can make use of it.