From 016a5d6ba7f795f2d07258b517e387b7b0025dcb Mon Sep 17 00:00:00 2001 From: Thomas Haas Date: Sun, 22 Mar 2026 23:48:41 +0100 Subject: [PATCH 1/3] Add new simplification for IDL encodings of coherence and acyclicity constraints --- .../dat3m/dartagnan/encoding/WmmEncoder.java | 74 ++++++++++++++----- 1 file changed, 56 insertions(+), 18 deletions(-) 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..773ad28d80 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,29 @@ 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". + */ + private BiPredicate getIsUnconditionallyOrderablePredicate(Relation rel) { + // NOTE: 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) + 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; + } + return exec.isImplied(y, x) || + mustIn.getOrDefault(x, Set.of()).stream().allMatch(z -> 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 +780,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 ---- @@ -795,10 +822,17 @@ public Void visitCoherence(Coherence coDef) { 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))); + } else { + 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 { enc.add(bmgr.or(bmgr.not(coF), bmgr.not(coB))); if (!mustSet.contains(x, z) && !mustSet.contains(z, x)) { @@ -993,16 +1027,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; } From 3c6991cee778127e90d7f19f476cd31d67eddc15 Mon Sep 17 00:00:00 2001 From: Thomas Haas Date: Mon, 23 Mar 2026 10:39:55 +0100 Subject: [PATCH 2/3] Slight clean-up Added optimization also to idl2Sat encoding --- .../dat3m/dartagnan/encoding/WmmEncoder.java | 48 ++++++++++++------- 1 file changed, 32 insertions(+), 16 deletions(-) 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 773ad28d80..8b18c8b4b4 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/WmmEncoder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/WmmEncoder.java @@ -270,13 +270,14 @@ private EventGraph findTransitivelyImpliedCo() { 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) { - // NOTE: 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) final EventGraph mustSet = ra.getKnowledge(rel).getMustSet(); final Map> mustIn = mustSet.getInMap(); final ExecutionAnalysis exec = context.getAnalysisContext().requires(ExecutionAnalysis.class); @@ -284,8 +285,11 @@ private BiPredicate getIsUnconditionallyOrderablePredicate(Relatio 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 -> mustSet.contains(z, y)); + mustIn.getOrDefault(x, Set.of()).stream() + .allMatch(z -> exec.isImplied(z, x) || mustSet.contains(z, y)); }; } @@ -821,19 +825,24 @@ public Void visitCoherence(Coherence coDef) { } else { enc.add(bmgr.implication(bmgr.or(coF, coB), pairingCond)); } + if (idl) { 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))); - } else { - 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)))); } + + 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) { @@ -1116,17 +1125,24 @@ 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() + : minSet.contains(e1, e2) + ? context.execution(e1, e2) + : 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]) - : bmgr.and(getSMTCycleVar(rel, tri[0], tri[1]), getSMTCycleVar(rel, tri[1], tri[2])); + BooleanFormula cond = alwaysOrder.test(tri[0], tri[2]) + ? bmgr.makeTrue() + : minSet.contains(tri[0], tri[2]) + ? context.execution(tri[0], tri[2]) + : edge.encode(tri[0], tri[2]); enc.add(bmgr.implication(cond, getSMTCycleVar(rel, tri[0], tri[2]))); } From 900e97e9503e4ff302dcfe5d1e2fb15aa53edeb1 Mon Sep 17 00:00:00 2001 From: Thomas Haas Date: Mon, 23 Mar 2026 10:52:45 +0100 Subject: [PATCH 3/3] Fix copy&paste error --- .../java/com/dat3m/dartagnan/encoding/WmmEncoder.java | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) 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 8b18c8b4b4..8a412f5437 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/WmmEncoder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/WmmEncoder.java @@ -1128,11 +1128,7 @@ private List acyclicSAT(Relation rel, EventGraph relevantEdges) final BiPredicate alwaysOrder = getIsUnconditionallyOrderablePredicate(rel); // Basic lifting relevantEdges.apply((e1, e2) -> { - BooleanFormula cond = alwaysOrder.test(e1, e2) - ? bmgr.makeTrue() - : 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))); }); @@ -1142,7 +1138,7 @@ private List acyclicSAT(Relation rel, EventGraph relevantEdges) ? bmgr.makeTrue() : minSet.contains(tri[0], tri[2]) ? context.execution(tri[0], tri[2]) - : edge.encode(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]))); }