Free relations in CAT

[ThomasHaas]

This PR adds the ability to define free relations in CAT via let r = free() (using function call syntax).

For example, with this it is possible to define co entirely in CAT:

let co = (free() & W*W & loc) // co is a relation on same-address writes
let co = co | [IW];loc;[W] \ id // co orders init writes before all other writes
let co = co+ // co is transitive
empty ((W*W & loc) \ (co | co^-1 | id)) // Co orders every same-address pair of writes ...
acyclic (co) // ... and it is acyclic, meaning it is a total order (per address)

Such an encoding would actually be more interesting for partial order co as defined in GPU models(*).
This way, we could likely get rid of special case treatment for GPU architectures as suggested in #532 .

More generally, this feature can be used to experiment more easily with the CAT model. For example, we could easily define a total order on (abstract) lock events and encode that hb should adhere to that order.

(*) Defining co in CAT comes with another issue (as discussed in #532) though: we use the standard notion of co to encode liveness properties and final memory values.
One would likely need to add further primitives like finalVal(co) and liveness(co) to tell the encoding which relation is responsible for defining final values.

[ThomasHaas]

What syntax is better to define a new and free relation: free() or new() (or other alternatives)?

[hernanponcedeleon]

I think with new() is more clear to understand what this is about

[ThomasHaas]

I think with new() is more clear to understand what this is about

Ok, then I will change the syntax to new(), but I will keep the internal class name as Free since this better describes the semantics.

[hernanponcedeleon]

Must is always empty do I don't see the point of having the conditional

[ThomasHaas]

I put it to have it uniform, i.e., if you decide to put a non-empty must-set later on, the option will still work. As long as we have this option, I would keep it as is. If we decide to remove the no must-set option, I would change it.

[hernanponcedeleon]

I did not see any easy way to specify the must set of a cat-introduced relation. Thus, realistically speaking, I don't think we will ever have a non-empty must set here

[ThomasHaas]

Realistically speaking we won't have non-empty must-sets. But I would like to avoid giving this one relation a different treatment that is not any more performant. I think it would just break a pattern for no benefit (with some practically unrealistic pitfalls).

[hernanponcedeleon]

There are a few other relations that do not use the enable must set option. Even more, visitSyncFence explicitly uses the empty graph

[ThomasHaas]

I think this is because those were made by @tonghaining and he was not aware of the existence of that option.
I think the option is implemented badly: the baseline code should simply always compute may/must-sets and the propagator engine should simply discard the must-set if the option is enabled.
Ideally, this would move the handling of that option into a single place into the code and developers don't need to think about the existence of that option when implementing their new relations/definitions.
Maybe I can take a look if this would be easy to implement.

[hernanponcedeleon]

I have the feeling that having this fine grained option is useless. Having a way to disable the whole RA might be useful, but AFAIR Implementing this was not as trivial as it sounds. @nagacek mentioned recently that debugging certain things gets harder with so many optimizations.

[ThomasHaas]

I can see if I can move that option into a central place and if not, I will just remove it.

[ThomasHaas]

I moved the handling into a central place. Incidentally, I found bugs in RA when computing must-sets for Range/Domain relations.