diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/GlobalSettings.java b/dartagnan/src/main/java/com/dat3m/dartagnan/GlobalSettings.java index d32939749a..16fbd54753 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/GlobalSettings.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/GlobalSettings.java @@ -1,6 +1,6 @@ package com.dat3m.dartagnan; -import com.dat3m.dartagnan.solver.caat4wmm.Refiner; +import com.dat3m.dartagnan.solver.caat4wmm.coreReasoning.CoreReasoner; import org.apache.logging.log4j.LogManager; import org.apache.logging.log4j.Logger; import org.sosy_lab.common.configuration.Configuration; @@ -35,14 +35,14 @@ public static void configure(Configuration config) throws InvalidConfigurationEx */ public static final boolean REFINEMENT_GENERATE_GRAPHVIZ_DEBUG_FILES = false; - public static final Refiner.SymmetryLearning REFINEMENT_SYMMETRY_LEARNING = Refiner.SymmetryLearning.FULL; + public static final CoreReasoner.SymmetricLearning REFINEMENT_SYMMETRIC_LEARNING = CoreReasoner.SymmetricLearning.FULL; // -------------------- public static void LogGlobalSettings() { // Refinement settings logger.info("REFINEMENT_GENERATE_GRAPHVIZ_DEBUG_FILES: " + REFINEMENT_GENERATE_GRAPHVIZ_DEBUG_FILES); - logger.info("REFINEMENT_SYMMETRY_LEARNING: " + REFINEMENT_SYMMETRY_LEARNING.name()); + logger.info("REFINEMENT_SYMMETRIC_LEARNING: " + REFINEMENT_SYMMETRIC_LEARNING.name()); } public static String getOrCreateOutputDirectory() throws IOException { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/Refiner.java b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/Refiner.java index 03c6831c3e..249efa791a 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/Refiner.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/Refiner.java @@ -1,135 +1,61 @@ package com.dat3m.dartagnan.solver.caat4wmm; import com.dat3m.dartagnan.encoding.EncodingContext; -import com.dat3m.dartagnan.program.Thread; -import com.dat3m.dartagnan.program.analysis.ThreadSymmetry; -import com.dat3m.dartagnan.program.event.core.Event; import com.dat3m.dartagnan.program.event.core.MemoryCoreEvent; import com.dat3m.dartagnan.solver.caat4wmm.coreReasoning.AddressLiteral; import com.dat3m.dartagnan.solver.caat4wmm.coreReasoning.CoreLiteral; import com.dat3m.dartagnan.solver.caat4wmm.coreReasoning.ExecLiteral; import com.dat3m.dartagnan.solver.caat4wmm.coreReasoning.RelLiteral; -import com.dat3m.dartagnan.utils.equivalence.EquivalenceClass; import com.dat3m.dartagnan.utils.logic.Conjunction; import com.dat3m.dartagnan.utils.logic.DNF; -import com.dat3m.dartagnan.verification.Context; import com.dat3m.dartagnan.wmm.Relation; import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.BooleanFormulaManager; -import java.util.*; -import java.util.function.Function; - -import static com.dat3m.dartagnan.GlobalSettings.REFINEMENT_SYMMETRY_LEARNING; +import java.util.ArrayList; +import java.util.HashSet; +import java.util.List; /* This class handles the computation of refinement clauses from violations found by the WMM-solver procedure. - Furthermore, it incorporates symmetry reasoning if possible. */ public class Refiner { - public enum SymmetryLearning { NONE, LINEAR, QUADRATIC, FULL } - - private final ThreadSymmetry symm; - private final List<Function<Event, Event>> symmPermutations; - private final SymmetryLearning learningOption; - - public Refiner(Context analysisContext) { - this.learningOption = REFINEMENT_SYMMETRY_LEARNING; - symm = analysisContext.requires(ThreadSymmetry.class); - symmPermutations = computeSymmetryPermutations(); - } - + public Refiner() { } - // This method computes a refinement clause from a set of violations. - // Furthermore, it computes symmetric violations if symmetry learning is enabled. public BooleanFormula refine(DNF<CoreLiteral> coreReasons, EncodingContext context) { - //TODO: A specialized algorithm that computes the orbit under permutation may be better, - // since most violations involve only few threads and hence the orbit is far smaller than the full - // set of permutations. - HashSet<BooleanFormula> addedFormulas = new HashSet<>(); // To avoid adding duplicates - BooleanFormulaManager bmgr = context.getBooleanFormulaManager(); + final BooleanFormulaManager bmgr = context.getBooleanFormulaManager(); List<BooleanFormula> refinement = new ArrayList<>(); + HashSet<BooleanFormula> addedFormulas = new HashSet<>(); // To avoid adding duplicates // For each symmetry permutation, we will create refinement clauses - for (Function<Event, Event> perm : symmPermutations) { - for (Conjunction<CoreLiteral> reason : coreReasons.getCubes()) { - BooleanFormula permutedClause = bmgr.makeFalse(); - for (CoreLiteral lit : reason.getLiterals()) { - BooleanFormula litFormula = permuteAndConvert(lit, perm, context); - if (bmgr.isFalse(litFormula)) { - permutedClause = bmgr.makeTrue(); - break; - } else { - permutedClause = bmgr.or(permutedClause, bmgr.not(litFormula)); - } - } - if (addedFormulas.add(permutedClause)) { - refinement.add(permutedClause); + for (Conjunction<CoreLiteral> reason : coreReasons.getCubes()) { + BooleanFormula permutedClause = bmgr.makeFalse(); + for (CoreLiteral lit : reason.getLiterals()) { + final BooleanFormula litFormula = encode(lit, context); + if (bmgr.isFalse(litFormula)) { + permutedClause = bmgr.makeTrue(); + break; + } else { + permutedClause = bmgr.or(permutedClause, bmgr.not(litFormula)); } } - } - return bmgr.and(refinement); - } - - // Computes a list of permutations allowed by the program. - // Depending on the <learningOption>, the set of computed permutations differs. - // In particular, for the option NONE, only the identity permutation will be returned. - private List<Function<Event, Event>> computeSymmetryPermutations() { - Set<? extends EquivalenceClass<Thread>> symmClasses = symm.getNonTrivialClasses(); - List<Function<Event, Event>> perms = new ArrayList<>(); - perms.add(Function.identity()); - - for (EquivalenceClass<Thread> c : symmClasses) { - List<Thread> threads = new ArrayList<>(c); - threads.sort(Comparator.comparingInt(Thread::getId)); - - switch (learningOption) { - case NONE: - break; - case LINEAR: - for (int i = 0; i < threads.size(); i++) { - int j = (i + 1) % threads.size(); - perms.add(symm.createEventTransposition(threads.get(i), threads.get(j))); - } - break; - case QUADRATIC: - for (int i = 0; i < threads.size(); i++) { - for (int j = i + 1; j < threads.size(); j++) { - perms.add(symm.createEventTransposition(threads.get(i), threads.get(j))); - } - } - break; - case FULL: - List<Function<Event, Event>> allPerms = symm.createAllEventPermutations(c); - allPerms.remove(Function.identity()); // We avoid adding multiple identities - perms.addAll(allPerms); - break; - default: - throw new UnsupportedOperationException("Symmetry learning option: " - + learningOption + " is not recognized."); + if (addedFormulas.add(permutedClause)) { + refinement.add(permutedClause); } } - - return perms; + return bmgr.and(refinement); } - - // Changes a reasoning <literal> based on a given permutation <perm> and translates the result - // into a BooleanFormula for Refinement. - private BooleanFormula permuteAndConvert(CoreLiteral literal, Function<Event, Event> perm, EncodingContext encoder) { - BooleanFormulaManager bmgr = encoder.getBooleanFormulaManager(); - BooleanFormula enc; + private BooleanFormula encode(CoreLiteral literal, EncodingContext encoder) { + final BooleanFormulaManager bmgr = encoder.getBooleanFormulaManager(); + final BooleanFormula enc; if (literal instanceof ExecLiteral lit) { - enc = encoder.execution(perm.apply(lit.getData())); + enc = encoder.execution(lit.getData()); } else if (literal instanceof AddressLiteral loc) { - MemoryCoreEvent e1 = (MemoryCoreEvent) perm.apply(loc.getFirst()); - MemoryCoreEvent e2 = (MemoryCoreEvent) perm.apply(loc.getSecond()); - enc = encoder.sameAddress(e1, e2); + enc = encoder.sameAddress((MemoryCoreEvent) loc.getFirst(), (MemoryCoreEvent) loc.getSecond()); } else if (literal instanceof RelLiteral lit) { - Relation rel = encoder.getTask().getMemoryModel().getRelation(lit.getName()); - enc = encoder.edge(rel, - perm.apply(lit.getData().first()), - perm.apply(lit.getData().second())); + final Relation rel = encoder.getTask().getMemoryModel().getRelation(lit.getName()); + enc = encoder.edge(rel, lit.getData().first(), lit.getData().second()); } else { throw new IllegalArgumentException("CoreLiteral " + literal.toString() + " is not supported"); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/WMMSolver.java b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/WMMSolver.java index ee06d5b787..e078a3b0d2 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/WMMSolver.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/WMMSolver.java @@ -69,7 +69,7 @@ public Result check(Model model) { curTime = System.currentTimeMillis(); List<Conjunction<CoreLiteral>> coreReasons = new ArrayList<>(caatResult.getBaseReasons().getNumberOfCubes()); for (Conjunction<CAATLiteral> baseReason : caatResult.getBaseReasons().getCubes()) { - coreReasons.add(reasoner.toCoreReason(baseReason)); + coreReasons.addAll(reasoner.toCoreReasons(baseReason)); } stats.numComputedCoreReasons = coreReasons.size(); result.coreReasons = new DNF<>(coreReasons); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/coreReasoning/CoreReasoner.java b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/coreReasoning/CoreReasoner.java index ecf21cc220..73574f7e82 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/coreReasoning/CoreReasoner.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/coreReasoning/CoreReasoner.java @@ -1,6 +1,8 @@ package com.dat3m.dartagnan.solver.caat4wmm.coreReasoning; +import com.dat3m.dartagnan.program.Thread; import com.dat3m.dartagnan.program.analysis.ExecutionAnalysis; +import com.dat3m.dartagnan.program.analysis.ThreadSymmetry; import com.dat3m.dartagnan.program.event.core.Event; import com.dat3m.dartagnan.solver.caat.predicates.relationGraphs.Edge; import com.dat3m.dartagnan.solver.caat.reasoning.CAATLiteral; @@ -9,6 +11,7 @@ import com.dat3m.dartagnan.solver.caat4wmm.EventDomain; import com.dat3m.dartagnan.solver.caat4wmm.ExecutionGraph; import com.dat3m.dartagnan.solver.caat4wmm.basePredicates.FenceGraph; +import com.dat3m.dartagnan.utils.equivalence.EquivalenceClass; import com.dat3m.dartagnan.utils.logic.Conjunction; import com.dat3m.dartagnan.verification.Context; import com.dat3m.dartagnan.verification.VerificationTask; @@ -17,21 +20,26 @@ import com.dat3m.dartagnan.wmm.analysis.RelationAnalysis; import com.dat3m.dartagnan.wmm.definition.Fences; -import java.util.ArrayList; -import java.util.HashMap; -import java.util.List; -import java.util.Map; +import java.util.*; +import java.util.function.Function; +import static com.dat3m.dartagnan.GlobalSettings.REFINEMENT_SYMMETRIC_LEARNING; import static com.dat3m.dartagnan.wmm.relation.RelationNameRepository.*; -// The CoreReasoner transforms base reasons of the CAATSolver to core reason of the WMMSolver +// The CoreReasoner transforms base reasons of the CAATSolver to core reason of the WMMSolver. public class CoreReasoner { + public enum SymmetricLearning { NONE, LINEAR, QUADRATIC, FULL } + private final ExecutionGraph executionGraph; private final ExecutionAnalysis exec; private final RelationAnalysis ra; private final Map<String, Relation> termMap = new HashMap<>(); + private final ThreadSymmetry symm; + private final List<Function<Event, Event>> symmPermutations; + private final SymmetricLearning learningOption; + public CoreReasoner(VerificationTask task, Context analysisContext, ExecutionGraph executionGraph) { this.executionGraph = executionGraph; this.exec = analysisContext.requires(ExecutionAnalysis.class); @@ -39,72 +47,80 @@ public CoreReasoner(VerificationTask task, Context analysisContext, ExecutionGra for (Relation r : task.getMemoryModel().getRelations()) { termMap.put(r.getNameOrTerm(), r); } - } - - - public Conjunction<CoreLiteral> toCoreReason(Conjunction<CAATLiteral> baseReason) { - EventDomain domain = executionGraph.getDomain(); + this.learningOption = REFINEMENT_SYMMETRIC_LEARNING; + symm = analysisContext.requires(ThreadSymmetry.class); + symmPermutations = computeSymmetryPermutations(); + } - List<CoreLiteral> coreReason = new ArrayList<>(baseReason.getSize()); - for (CAATLiteral lit : baseReason.getLiterals()) { - if (lit instanceof ElementLiteral elLit) { - Event e = domain.getObjectById(elLit.getElement().getId()).getEvent(); - // We only have static tags, so all of them reduce to execution literals - coreReason.add(new ExecLiteral(e, lit.isNegative())); - } else { - - EdgeLiteral edgeLit = (EdgeLiteral) lit; - Edge edge = edgeLit.getEdge(); - Event e1 = domain.getObjectById(edge.getFirst()).getEvent(); - Event e2 = domain.getObjectById(edge.getSecond()).getEvent(); - Relation rel = termMap.get(lit.getName()); - - if (lit.isPositive() && ra.getKnowledge(rel).getMustSet().contains(e1, e2)) { - // Statically present edges - addExecReason(e1, e2, coreReason); - } else if (lit.isNegative() && !ra.getKnowledge(rel).getMaySet().contains(e1, e2)) { - // Statically absent edges + // Returns the (reduced) core reason of a base reason. If symmetry reasoning is enabled, + // this can return multiple core reasons corresponding to symmetric versions of the base reason. + public Set<Conjunction<CoreLiteral>> toCoreReasons(Conjunction<CAATLiteral> baseReason) { + final EventDomain domain = executionGraph.getDomain(); + final Set<Conjunction<CoreLiteral>> symmetricReasons = new HashSet<>(); + + //TODO: A specialized algorithm that computes the orbit under permutation may be better, + // since most violations involve only few threads and hence the orbit is far smaller than the full + // set of permutations. + for (Function<Event, Event> perm : symmPermutations) { + List<CoreLiteral> coreReason = new ArrayList<>(baseReason.getSize()); + for (CAATLiteral lit : baseReason.getLiterals()) { + if (lit instanceof ElementLiteral elLit) { + final Event e = perm.apply(domain.getObjectById(elLit.getElement().getId()).getEvent()); + // We only have static tags, so all of them reduce to execution literals + coreReason.add(new ExecLiteral(e, lit.isNegative())); } else { - String name = rel.getNameOrTerm(); - if (name.equals(RF) || name.equals(CO) - || executionGraph.getCutRelations().contains(rel)) { - coreReason.add(new RelLiteral(name, e1, e2, lit.isNegative())); - } else if (name.equals(LOC)) { - coreReason.add(new AddressLiteral(e1, e2, lit.isNegative())); - } else if (rel.getDefinition() instanceof Fences) { - // This is a special case since "fencerel(F) = po;[F];po". - // We should do this transformation directly on the Wmm to avoid this special reasoning - if (lit.isNegative()) { - throw new UnsupportedOperationException(String.format("FenceRel %s is not allowed on the rhs of differences.", rel)); - } - addFenceReason(rel, edge, coreReason); + final EdgeLiteral edgeLit = (EdgeLiteral) lit; + final Edge edge = edgeLit.getEdge(); + final Event e1 = perm.apply(domain.getObjectById(edge.getFirst()).getEvent()); + final Event e2 = perm.apply(domain.getObjectById(edge.getSecond()).getEvent()); + final Relation rel = termMap.get(lit.getName()); + + if (lit.isPositive() && ra.getKnowledge(rel).getMustSet().contains(e1, e2)) { + // Statically present edges + addExecReason(e1, e2, coreReason); + } else if (lit.isNegative() && !ra.getKnowledge(rel).getMaySet().contains(e1, e2)) { + // Statically absent edges } else { - //TODO: Right now, we assume many relations like Data, Ctrl and Addr to be - // static. - if (lit.isNegative()) { - // TODO: Support negated literals - throw new UnsupportedOperationException(String.format("Negated literals of type %s are not supported.", rel)); + final String name = rel.getNameOrTerm(); + if (name.equals(RF) || name.equals(CO) + || executionGraph.getCutRelations().contains(rel)) { + coreReason.add(new RelLiteral(name, e1, e2, lit.isNegative())); + } else if (name.equals(LOC)) { + coreReason.add(new AddressLiteral(e1, e2, lit.isNegative())); + } else if (rel.getDefinition() instanceof Fences) { + // This is a special case since "fencerel(F) = po;[F];po". + // We should do this transformation directly on the Wmm to avoid this special reasoning + if (lit.isNegative()) { + throw new UnsupportedOperationException(String.format("FenceRel %s is not allowed on the rhs of differences.", rel)); + } + addFenceReason(rel, edge, coreReason); + } else { + // FIXME: Right now, we assume many relations like data, ctrl and addr to be static. + // In order to fix this, we would need to cut/eagerly encode the dependency relations. + if (lit.isNegative()) { + // TODO: Support negated literals (ideally via lazy/on-demand cutting) + throw new UnsupportedOperationException(String.format("Negated literals of type %s are not supported.", rel)); + } + addExecReason(e1, e2, coreReason); } - addExecReason(e1, e2, coreReason); } } } + minimize(coreReason); + symmetricReasons.add(new Conjunction<>(coreReason)); } - minimize(coreReason); - return new Conjunction<>(coreReason); + return symmetricReasons; } + private void minimize(List<CoreLiteral> reason) { - //TODO: Make sure that his is correct for exclusive events - // Their execution variable can only be removed if it is contained in some - // RelLiteral but not if it gets cf-implied! reason.removeIf( lit -> { if (!(lit instanceof ExecLiteral execLit) || lit.isNegative()) { return false; } - Event ev = execLit.getData(); + final Event ev = execLit.getData(); return reason.stream().filter(e -> e instanceof RelLiteral && e.isPositive()) .map(RelLiteral.class::cast) .anyMatch(e -> exec.isImplied(e.getData().first(), ev) @@ -146,4 +162,50 @@ private void addFenceReason(Relation rel, Edge edge, List<CoreLiteral> coreReaso coreReasons.add(new ExecLiteral(e2.getEvent())); } } + + // ============================================================================================= + // ======================================== Symmetry =========================================== + // ============================================================================================= + + // Computes a list of permutations between events of symmetric threads. + // Depending on the <learningOption>, the set of computed permutations differs. + // In particular, for the option NONE, only the identity permutation will be returned. + private List<Function<Event, Event>> computeSymmetryPermutations() { + final Set<? extends EquivalenceClass<Thread>> symmClasses = symm.getNonTrivialClasses(); + final List<Function<Event, Event>> perms = new ArrayList<>(); + perms.add(Function.identity()); + + for (EquivalenceClass<Thread> c : symmClasses) { + final List<Thread> threads = new ArrayList<>(c); + threads.sort(Comparator.comparingInt(Thread::getId)); + + switch (learningOption) { + case NONE: + break; + case LINEAR: + for (int i = 0; i < threads.size(); i++) { + final int j = (i + 1) % threads.size(); + perms.add(symm.createEventTransposition(threads.get(i), threads.get(j))); + } + break; + case QUADRATIC: + for (int i = 0; i < threads.size(); i++) { + for (int j = i + 1; j < threads.size(); j++) { + perms.add(symm.createEventTransposition(threads.get(i), threads.get(j))); + } + } + break; + case FULL: + final List<Function<Event, Event>> allPerms = symm.createAllEventPermutations(c); + allPerms.remove(Function.identity()); // We avoid adding multiple identities + perms.addAll(allPerms); + break; + default: + throw new UnsupportedOperationException("Symmetry learning option: " + + learningOption + " is not recognized."); + } + } + + return perms; + } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java index df82c2a95a..9c737406de 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java @@ -214,7 +214,7 @@ private void runInternal(SolverContext ctx, ProverEnvironment prover, Verificati final BooleanFormulaManager bmgr = ctx.getFormulaManager().getBooleanFormulaManager(); final WMMSolver solver = WMMSolver.withContext(context, cutRelations, task, analysisContext); - final Refiner refiner = new Refiner(analysisContext); + final Refiner refiner = new Refiner(); final Property.Type propertyType = Property.getCombinedType(task.getProperty(), task); logger.info("Starting encoding using " + ctx.getVersion()); @@ -564,7 +564,7 @@ private static CharSequence generateSummary(RefinementTrace trace, long boundChe .append(" -- Refining time(ms): ").append(totalRefiningTime).append("\n") .append(" -- #Computed core reasons: ").append(totalNumReasons).append("\n") .append(" -- #Computed core reduced reasons: ").append(totalNumReducedReasons).append("\n"); - if (statList.size() > 0) { + if (!statList.isEmpty()) { message.append(" -- Min model size (#events): ").append(minModelSize).append("\n") .append(" -- Average model size (#events): ").append(totalModelSize / statList.size()) .append("\n")