Imprecision in XRA

[ThomasHaas]

I noticed that on EBR, XRA under imm.cat produces a smaller may-set for rf than under other memory models. After some debugging, I found the source of this discrepancy. After reducing it to its core, I found this

acyclic (po | rf | fr) // Original
// ---- The following all give smaller rf-sets but have the same semantics
acyclic ((po | rf)+ | fr) 
acyclic ((po | rf | fr)+)
acyclic ((po | fr)+ | rf)

There are only two conclusions: Either our XRA handling of acyclicity axioms is imprecise ~or propagation through transitive closures is somehow wrong.~

EDIT: After quickly checking the code, I found that XRA for acyclicity axioms is indeed imprecise because it avoids the computation of the transitive must-closure. Now that we have must rf-edges between threads, it might be worth to compute the transitive closure.

[hernanponcedeleon]

I don't get the EDIT part of the comment. Where in the code we should compute the transitive closure?

[ThomasHaas]

In the Acyclicity axiom when doing top-down propagation.

[hernanponcedeleon]

method Acyclicity.transitivelyDerivableMustEdges()?

[ThomasHaas]

No, that one is correct. I believe it only is called when doing the active set computation. The issue is in both the knowledgeClosure functions, which use the must-set of the constrained relations without transitively closing it.