Skip to content

Optimize encodings of coherence and acyclicity (mostly IDL) #1015

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
ThomasHaas wants to merge 3 commits into
base: development
Choose a base branch
from
+71 −21
Open

Optimize encodings of coherence and acyclicity (mostly IDL) #1015

Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
016a5d6
Add new simplification for IDL encodings of coherence and acyclicity …
ThomasHaas Mar 22, 2026
3c6991c
Slight clean-up
ThomasHaas Mar 23, 2026
900e97e
Fix copy&paste error
ThomasHaas Mar 23, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
92 changes: 71 additions & 21 deletions dartagnan/src/main/java/com/dat3m/dartagnan/encoding/WmmEncoder.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -265,6 +266,33 @@ private EventGraph findTransitivelyImpliedCo() {
return transCo;
}

/*
The returned predicate checks whether a pair of events (x, y) in a given relation <rel>
can be unconditionally ordered.
Used to optimize encodings of "acyclic <rel>" 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<Event, Event> getIsUnconditionallyOrderablePredicate(Relation rel) {
final EventGraph mustSet = ra.getKnowledge(rel).getMustSet();
final Map<Event, Set<Event>> 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<BooleanFormula> enc) {
final BooleanFormulaManager bmgr = context.getBooleanFormulaManager();
ra.getContradictions().apply((e1, e2) -> enc.add(bmgr.not(context.execution(e1, e2))));
Expand Down Expand Up @@ -756,22 +784,25 @@ private BooleanFormula getUninitReadVar(Load load) {
@Override
public Void visitCoherence(Coherence coDef) {
final Relation co = coDef.getDefinedRelation();
boolean idl = !useSATEncoding;
List<MemoryCoreEvent> allWrites = program.getThreadEvents(MemoryCoreEvent.class).stream()
final BiPredicate<Event, Event> 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<MemoryCoreEvent> 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 ----
Expand All @@ -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) {
Expand Down Expand Up @@ -993,16 +1036,20 @@ private List<BooleanFormula> acyclicIDL(Relation rel, EventGraph relevantEdges)
final BooleanFormulaManager bmgr = context.getBooleanFormulaManager();
final IntegerFormulaManager imgr = context.getFormulaManager().getIntegerFormulaManager();
final String clockVarName = rel.getNameOrTerm();
final BiPredicate<Event, Event> alwaysOrder = getIsUnconditionallyOrderablePredicate(rel);

List<BooleanFormula> 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;
}

Expand Down Expand Up @@ -1078,16 +1125,19 @@ private List<BooleanFormula> acyclicSAT(Relation rel, EventGraph relevantEdges)
final EventGraph minSet = ra.getKnowledge(rel).getMustSet();
List<BooleanFormula> enc = new ArrayList<>();
final EncodingContext.EdgeEncoder edge = context.edge(rel);
final BiPredicate<Event, Event> 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])));
}
Expand Down
Loading