Fix witnesses excluding the rf edges they enforce. #771
Conversation
| for (Event r : g.getRange()) { | ||
| may.removeIf((e1, e2) -> e2 == r); | ||
| } | ||
| may.addAll(g); |
There was a problem hiding this comment.
I would change this code to do may.removeIf((e1, e2) -> e2 == r && !g.contains(e1, e2)).
The reason is that this way, if we actually do add an rf-edge between events that may not read from each other, we get the desired mutual exclusion.
Your solution, in some sense, introduces back imprecision in such cases (must-not may suddently become may).
Based on the large number of witnesses we manage to validate, I was initially surprised about this claim. However, I checked a few cases and the number of must edges in |
Should fix issue #767. When validating a witness, the Relation Analysis extracts
rfedges, that must occur. Becauserfis (usually) functional, any other candidate in-edge for the participating load event is disabled by the witness. The extraction code disabled even the extractedrfedge. The Extended Relation Analysis then inferred mutual exclusiveness between those events. Even without XRA, such loads always read 0, because of uninitialized memory.The bug should affect all violation witnesses with at least one
rfedge.