diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/WmmEncoder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/WmmEncoder.java index 58b01fb6e8..8a412f5437 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/WmmEncoder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/WmmEncoder.java @@ -37,6 +37,7 @@ import org.sosy_lab.java_smt.api.NumeralFormula; import java.util.*; +import java.util.function.BiPredicate; import static com.dat3m.dartagnan.configuration.OptionNames.*; import static com.dat3m.dartagnan.encoding.ExpressionEncoder.ConversionMode.MEMORY_ROUND_TRIP_RELAXED; @@ -265,6 +266,33 @@ private EventGraph findTransitivelyImpliedCo() { return transCo; } + /* + The returned predicate checks whether a pair of events (x, y) in a given relation + can be unconditionally ordered. + Used to optimize encodings of "acyclic " and "co". + + This optimization tries to omit the guards of certain must-edges, i.e., + it promotes "exec(x) /\ exec(y) => clk(x) < clk(y)" to simply "clk(x) < clk(y)" + We can only do this when for a must-edge (x,y) we have + (i) exec(y) => exec(x) + OR (ii) for all z: must(z,x) => must(z,y) + */ + private BiPredicate getIsUnconditionallyOrderablePredicate(Relation rel) { + final EventGraph mustSet = ra.getKnowledge(rel).getMustSet(); + final Map> mustIn = mustSet.getInMap(); + final ExecutionAnalysis exec = context.getAnalysisContext().requires(ExecutionAnalysis.class); + return (x, y) -> { + if (!mustSet.contains(x, y)) { + return false; + } + // NOTE: The implication "exec(y) => exec(x)" can also be inverted, but we cannot check both directions! + // The direction "exec(y) => exec(x)" holds more often for unfair progress models. + return exec.isImplied(y, x) || + mustIn.getOrDefault(x, Set.of()).stream() + .allMatch(z -> exec.isImplied(z, x) || mustSet.contains(z, y)); + }; + } + private void encodeContradictions(List enc) { final BooleanFormulaManager bmgr = context.getBooleanFormulaManager(); ra.getContradictions().apply((e1, e2) -> enc.add(bmgr.not(context.execution(e1, e2)))); @@ -756,22 +784,25 @@ private BooleanFormula getUninitReadVar(Load load) { @Override public Void visitCoherence(Coherence coDef) { final Relation co = coDef.getDefinedRelation(); - boolean idl = !useSATEncoding; - List allWrites = program.getThreadEvents(MemoryCoreEvent.class).stream() + final BiPredicate alwaysOrdered = getIsUnconditionallyOrderablePredicate(co); + final boolean idl = !useSATEncoding; + final EventGraph maySet = ra.getKnowledge(co).getMaySet(); + final EventGraph mustSet = ra.getKnowledge(co).getMustSet(); + final EventGraph transCo = findTransitivelyImpliedCo(); + + final List allWrites = program.getThreadEvents(MemoryCoreEvent.class).stream() .filter(e -> e.hasTag(WRITE)) .sorted(Comparator.comparingInt(Event::getGlobalId)) .toList(); - EncodingContext.EdgeEncoder edge = context.edge(co); - EventGraph maySet = ra.getKnowledge(co).getMaySet(); - EventGraph mustSet = ra.getKnowledge(co).getMustSet(); - EventGraph transCo = findTransitivelyImpliedCo(); - IntegerFormulaManager imgr = idl ? context.getFormulaManager().getIntegerFormulaManager() : null; + final IntegerFormulaManager imgr = idl ? context.getFormulaManager().getIntegerFormulaManager() : null; + final EncodingContext.EdgeEncoder edge = context.edge(co); + if (idl) { // ---- Encode clock conditions (init = 0, non-init > 0) ---- NumeralFormula.IntegerFormula zero = imgr.makeNumber(0); for (MemoryCoreEvent w : allWrites) { NumeralFormula.IntegerFormula clock = memoryOrderClock(w); - enc.add(w.hasTag(INIT) ? imgr.equal(clock, zero) : imgr.greaterThan(clock, zero)); + enc.add(w.hasTag(INIT) ? imgr.equal(clock, zero) : imgr.lessThan(zero, clock)); } } // ---- Encode coherences ---- @@ -794,12 +825,24 @@ public Void visitCoherence(Coherence coDef) { } else { enc.add(bmgr.implication(bmgr.or(coF, coB), pairingCond)); } + if (idl) { - enc.add(bmgr.implication(coF, x.hasTag(INIT) || transCo.contains(x, z) ? bmgr.makeTrue() - : imgr.lessThan(memoryOrderClock(x), memoryOrderClock(z)))); - enc.add(bmgr.implication(coB, z.hasTag(INIT) || transCo.contains(z, x) ? bmgr.makeTrue() - : imgr.lessThan(memoryOrderClock(z), memoryOrderClock(x)))); + if (alwaysOrdered.test(x, z)) { + enc.add(imgr.lessThan(memoryOrderClock(x), memoryOrderClock(z))); + } else if (alwaysOrdered.test(z, x)) { + enc.add(imgr.lessThan(memoryOrderClock(z), memoryOrderClock(x))); + } + + enc.add(bmgr.implication(coF, x.hasTag(INIT) || transCo.contains(x, z) + ? bmgr.makeTrue() + : imgr.lessThan(memoryOrderClock(x), memoryOrderClock(z)) + )); + enc.add(bmgr.implication(coB, z.hasTag(INIT) || transCo.contains(z, x) + ? bmgr.makeTrue() + : imgr.lessThan(memoryOrderClock(z), memoryOrderClock(x)) + )); } else { + // SAT encoding enc.add(bmgr.or(bmgr.not(coF), bmgr.not(coB))); if (!mustSet.contains(x, z) && !mustSet.contains(z, x)) { for (MemoryEvent y : allWrites) { @@ -993,16 +1036,20 @@ private List acyclicIDL(Relation rel, EventGraph relevantEdges) final BooleanFormulaManager bmgr = context.getBooleanFormulaManager(); final IntegerFormulaManager imgr = context.getFormulaManager().getIntegerFormulaManager(); final String clockVarName = rel.getNameOrTerm(); + final BiPredicate alwaysOrder = getIsUnconditionallyOrderablePredicate(rel); + List enc = new ArrayList<>(); final EncodingContext.EdgeEncoder edge = context.edge(rel); relevantEdges.apply((e1, e2) -> - enc.add(bmgr.implication(edge.encode(e1, e2), - imgr.lessThan( - context.clockVariable(clockVarName, e1), - context.clockVariable(clockVarName, e2) - ) - )) + enc.add(bmgr.implication( + alwaysOrder.test(e1, e2) ? bmgr.makeTrue() : edge.encode(e1, e2), + imgr.lessThan( + context.clockVariable(clockVarName, e1), + context.clockVariable(clockVarName, e2) + ) + )) ); + return enc; } @@ -1078,16 +1125,19 @@ private List acyclicSAT(Relation rel, EventGraph relevantEdges) final EventGraph minSet = ra.getKnowledge(rel).getMustSet(); List enc = new ArrayList<>(); final EncodingContext.EdgeEncoder edge = context.edge(rel); + final BiPredicate alwaysOrder = getIsUnconditionallyOrderablePredicate(rel); // Basic lifting relevantEdges.apply((e1, e2) -> { - BooleanFormula cond = minSet.contains(e1, e2) ? context.execution(e1, e2) : edge.encode(e1, e2); + BooleanFormula cond = alwaysOrder.test(e1, e2) ? bmgr.makeTrue() : edge.encode(e1, e2); enc.add(bmgr.implication(cond, getSMTCycleVar(rel, e1, e2))); }); // Encode triangle rules for (Event[] tri : triangles) { - BooleanFormula cond = minSet.contains(tri[0], tri[2]) ? - context.execution(tri[0], tri[2]) + BooleanFormula cond = alwaysOrder.test(tri[0], tri[2]) + ? bmgr.makeTrue() + : minSet.contains(tri[0], tri[2]) + ? context.execution(tri[0], tri[2]) : bmgr.and(getSMTCycleVar(rel, tri[0], tri[1]), getSMTCycleVar(rel, tri[1], tri[2])); enc.add(bmgr.implication(cond, getSMTCycleVar(rel, tri[0], tri[2]))); }