diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/PropertyEncoder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/PropertyEncoder.java index fa7ed2b267..36427a5adf 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/PropertyEncoder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/PropertyEncoder.java @@ -21,7 +21,6 @@ import com.dat3m.dartagnan.wmm.utils.EventGraph; import com.google.common.base.Preconditions; import com.google.common.collect.Lists; -import com.google.common.collect.Maps; import org.apache.logging.log4j.LogManager; import org.apache.logging.log4j.Logger; import org.sosy_lab.common.configuration.InvalidConfigurationException; @@ -36,8 +35,8 @@ import java.util.stream.Collectors; import static com.dat3m.dartagnan.configuration.Property.*; -import static com.dat3m.dartagnan.wmm.RelationNameRepository.CO; import static com.dat3m.dartagnan.program.Program.SourceLanguage.LLVM; +import static com.dat3m.dartagnan.wmm.RelationNameRepository.CO; public class PropertyEncoder implements Encoder { @@ -66,7 +65,7 @@ public class PropertyEncoder implements Encoder { Since we encode a lot of potential violations, and we want to trace back which one lead to our query being SAT, we use trackable formulas. */ - private static class TrackableFormula { + public static class TrackableFormula { private final BooleanFormula trackingLiteral; private final BooleanFormula trackedFormula; @@ -304,7 +303,7 @@ public List encodeCATSpecificationViolations() { final EncodingContext ctx = this.context; final Wmm memoryModel = this.memoryModel; final List flaggedAxioms = memoryModel.getAxioms().stream() - .filter(Axiom::isFlagged).collect(Collectors.toList()); + .filter(Axiom::isFlagged).toList(); if (flaggedAxioms.isEmpty()) { logger.info("No CAT specification in the WMM. Skipping encoding."); @@ -402,22 +401,30 @@ public TrackableFormula encodeDataRaces() { private TrackableFormula encodeDeadlocks() { logger.info("Encoding dead locks"); - return new LivenessEncoder().encodeDeadlocks(); + return new LivenessEncoder().encodeLivenessBugs(); } /* Encoder for the liveness property. We have a liveness violation in some execution if - - At least one thread is stuck inside a loop (*) + - At least one thread is stuck (*) - All other threads are either stuck or terminated normally (**) - (*) A thread is stuck if it finishes a loop iteration - - without causing side-effects (e.g., visible stores) - - while reading only from co-maximal stores - => Without external help, a stuck thread will never be able to exit the loop. + (*) A thread is stuck if + (1) it performs a loop iteration without causing side-effects (e.g., visible stores) + while satisfying fairness conditions + => Without external help, a stuck thread will never be able to exit the loop. + OR (2) the thread is blocked by a control barrier. + + Fairness conditions for loops: + - Memory fairness: the loop iteration reads only co-maximal values + - Excl-Store progress: all exclusive stores in the iteration succeed (infinite spurious failures are unfair) + NOTE: Here we assume strong progress. Under weak fairness, a loop with two exclusive stores that need + to succeed in the same iteration could fail liveness if they succeed in alternation. - (**) A thread terminates normally IFF it does not terminate early (denoted by EARLYTERMINATION-tagged jumps) + (**) A thread terminates normally IFF it does terminate (no NONTERMINATION-tagged jumps) non-exceptionally + (no EXCEPTIONAL_TERMINATION-tagged jumps) due to e.g., - violating an assertion - reaching the loop unrolling bound @@ -429,36 +436,19 @@ in a deadlock without satisfying the stated conditions (e.g., while producing si */ private class LivenessEncoder { - private static class SpinIteration { - public final List containedLoads = new ArrayList<>(); - // Execution of the means the loop performed a side-effect-free - // iteration without exiting. If such a jump is executed + all loads inside the loop - // were co-maximal, then we have a deadlock condition. - public final List spinningJumps = new ArrayList<>(); - } - - public TrackableFormula encodeDeadlocks() { + public TrackableFormula encodeLivenessBugs() { final Program program = PropertyEncoder.this.program; final EncodingContext context = PropertyEncoder.this.context; final BooleanFormulaManager bmgr = context.getBooleanFormulaManager(); - final LoopAnalysis loopAnalysis = LoopAnalysis.newInstance(program); - - // Find spin loops of all threads - final Map> spinloopsMap = - Maps.toMap(program.getThreads(), t -> this.findSpinLoopsInThread(t, loopAnalysis)); - // Compute "stuckness" encoding for all threads - final Map isStuckMap = Maps.toMap(program.getThreads(), t -> - bmgr.or(generateBarrierStucknessEncoding(t, context), - this.generateSpinloopStucknessEncoding(spinloopsMap.get(t), context))); // Deadlock <=> allStuckOrDone /\ atLeastOneStuck BooleanFormula allStuckOrDone = bmgr.makeTrue(); BooleanFormula atLeastOneStuck = bmgr.makeFalse(); for (Thread thread : program.getThreads()) { - final BooleanFormula isStuck = isStuckMap.get(thread); + final BooleanFormula isStuck = isStuckEncoding(thread, context); final BooleanFormula isTerminatingNormally = thread .getEvents().stream() - .filter(e -> e.hasTag(Tag.EARLYTERMINATION)) + .filter(e -> e.hasTag(Tag.EXCEPTIONAL_TERMINATION) || e.hasTag(Tag.NONTERMINATION)) .map(CondJump.class::cast) .map(j -> bmgr.not(bmgr.and(context.execution(j), context.jumpCondition(j)))) .reduce(bmgr.makeTrue(), bmgr::and); @@ -471,6 +461,16 @@ public TrackableFormula encodeDeadlocks() { return new TrackableFormula(bmgr.not(LIVENESS.getSMTVariable(context)), hasDeadlock); } + private BooleanFormula isStuckEncoding(Thread thread, EncodingContext context) { + return context.getBooleanFormulaManager().or( + generateSpinloopStucknessEncoding(thread, context), + generateBarrierStucknessEncoding(thread, context) + ); + } + + // ------------------------------------------------------------------------------ + // Liveness issue due to blocked execution (due to ControlBarrier) + private BooleanFormula generateBarrierStucknessEncoding(Thread thread, EncodingContext context) { final BooleanFormulaManager bmgr = context.getBooleanFormulaManager(); return bmgr.or(thread.getEvents().stream() @@ -479,37 +479,85 @@ private BooleanFormula generateBarrierStucknessEncoding(Thread thread, EncodingC .toList()); } - // Compute "stuckness": A thread is stuck if it reaches a spin loop bound event - // while only reading from co-maximal stores. - private BooleanFormula generateSpinloopStucknessEncoding(List loops, EncodingContext context) { + // ------------------------------------------------------------------------------ + // Liveness issue due to non-terminating loops (~ deadlocks) + + private record SpinIteration(List body, List spinningJumps) { + // Execution of the means the loop performed a side-effect-free + // iteration without exiting. If such a jump is executed + all loads inside the loop + // were co-maximal, then we have a deadlock condition. + } + + private BooleanFormula generateSpinloopStucknessEncoding(Thread thread, EncodingContext context) { + final LoopAnalysis loopAnalysis = LoopAnalysis.onFunction(thread); + final BooleanFormulaManager bmgr = context.getBooleanFormulaManager(); + + return this.findSpinLoopsInThread(thread, loopAnalysis).stream() + .map(loop -> generateSpinloopStucknessEncoding(loop, context)) + .reduce(bmgr.makeFalse(), bmgr::or); + } + + private BooleanFormula generateSpinloopStucknessEncoding(SpinIteration loop, EncodingContext context) { + return context.getBooleanFormulaManager().and( + isSideEffectFreeEncoding(loop, context), + fairnessEncoding(loop, context) + ); + } + + private BooleanFormula isSideEffectFreeEncoding(SpinIteration loop, EncodingContext context) { + // Note that we assume (for now) that a SPINLOOP-tagged jump is executed only if the loop iteration + // was side-effect free. + final BooleanFormulaManager bmgr = context.getBooleanFormulaManager(); + final BooleanFormula isSideEffectFree = loop.spinningJumps.stream() + .map(j -> bmgr.and(context.execution(j), context.jumpCondition(j))) + .reduce(bmgr.makeFalse(), bmgr::or); + return isSideEffectFree; + } + + private BooleanFormula fairnessEncoding(SpinIteration loop, EncodingContext context) { + return context.getBooleanFormulaManager().and( + memoryFairnessEncoding(loop, context), + exclStoreFairnessEncoding(loop, context) + ); + } + + private BooleanFormula memoryFairnessEncoding(SpinIteration loop, EncodingContext context) { final BooleanFormulaManager bmgr = context.getBooleanFormulaManager(); final RelationAnalysis ra = PropertyEncoder.this.ra; final Relation rf = memoryModel.getRelation(RelationNameRepository.RF); final EncodingContext.EdgeEncoder rfEncoder = context.edge(rf); final Map> rfMayIn = ra.getKnowledge(rf).getMaySet().getInMap(); - if (loops.isEmpty()) { - return bmgr.makeFalse(); - } + final List loads = loop.body.stream() + .filter(Load.class::isInstance) + .map(Load.class::cast) + .toList(); - BooleanFormula isStuck = bmgr.makeFalse(); - for (SpinIteration loop : loops) { - BooleanFormula allLoadsAreCoMaximal = bmgr.makeTrue(); - for (Load load : loop.containedLoads) { - final BooleanFormula readsCoMaximalStore = rfMayIn.getOrDefault(load, Set.of()).stream() - .map(store -> bmgr.and(rfEncoder.encode(store, load), lastCoVar(store))) - .reduce(bmgr.makeFalse(), bmgr::or); - final BooleanFormula isCoMaximalLoad = bmgr.implication(context.execution(load), readsCoMaximalStore); - allLoadsAreCoMaximal = bmgr.and(allLoadsAreCoMaximal, isCoMaximalLoad); - } - // Note that we assume (for now) that a SPINLOOP-tagged jump is executed only if the loop iteration - // was side-effect free. - final BooleanFormula isSideEffectFree = loop.spinningJumps.stream() - .map(j -> bmgr.and(context.execution(j), context.jumpCondition(j))) + BooleanFormula allLoadsAreCoMaximal = bmgr.makeTrue(); + for (Load load : loads) { + final BooleanFormula readsCoMaximalStore = rfMayIn.getOrDefault(load, Set.of()).stream() + .map(store -> bmgr.and(rfEncoder.encode(store, load), lastCoVar(store))) .reduce(bmgr.makeFalse(), bmgr::or); - isStuck = bmgr.or(isStuck, bmgr.and(isSideEffectFree, allLoadsAreCoMaximal)); + final BooleanFormula isCoMaximalLoad = bmgr.implication(context.execution(load), readsCoMaximalStore); + allLoadsAreCoMaximal = bmgr.and(allLoadsAreCoMaximal, isCoMaximalLoad); + } + + return allLoadsAreCoMaximal; + } + + private BooleanFormula exclStoreFairnessEncoding(SpinIteration loop, EncodingContext context) { + final BooleanFormulaManager bmgr = context.getBooleanFormulaManager(); + final List exclStores = loop.body.stream() + .filter(RMWStoreExclusive.class::isInstance) + .map(RMWStoreExclusive.class::cast) + .toList(); + BooleanFormula allExclStoresExecuted = bmgr.makeTrue(); + for (RMWStoreExclusive exclStore : exclStores) { + final BooleanFormula executedIfPossible = bmgr.implication(context.controlFlow(exclStore), context.execution(exclStore)); + allExclStoresExecuted = bmgr.and(allExclStoresExecuted, executedIfPossible); } - return isStuck; + + return allExclStoresExecuted; } private List findSpinLoopsInThread(Thread thread, LoopAnalysis loopAnalysis) { @@ -525,14 +573,7 @@ private List findSpinLoopsInThread(Thread thread, LoopAnalysis lo .toList(); if (!spinningJumps.isEmpty()) { - final List loads = iterBody.stream() - .filter(Load.class::isInstance) - .map(Load.class::cast) - .toList(); - - final SpinIteration spinIter = new SpinIteration(); - spinIter.spinningJumps.addAll(spinningJumps); - spinIter.containedLoads.addAll(loads); + final SpinIteration spinIter = new SpinIteration(iterBody, spinningJumps); spinIterations.add(spinIter); } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/Tag.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/Tag.java index b4cb282558..03cacda223 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/Tag.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/Tag.java @@ -27,9 +27,11 @@ private Tag() { } public static final String EXCL = "__EXCL"; // Marks the event that is reachable IFF a loop has not been fully unrolled. public static final String BOUND = "__BOUND"; - // Marks jumps that somehow terminate a thread earlier than "normally" - // This can be bound events, spinning events, assertion violations, etc. - public static final String EARLYTERMINATION = "__EARLYTERMINATION"; + // Marks jumps that designate an exceptional termination, typically due to assertion failures + public static final String EXCEPTIONAL_TERMINATION = "__EXCEPTIONAL_TERMINATION"; + // Marks jumps that designate non-termination, typically spinloops and bound events + // (and control barriers in the future) + public static final String NONTERMINATION = "__NONTERMINATION"; // Marks jumps that terminate a thread due to spinning behaviour, i.e. side-effect-free loop iterations public static final String SPINLOOP = "__SPINLOOP"; // Some events should not be optimized (e.g. fake dependencies) or deleted (e.g. bounds) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/DynamicSpinLoopDetection.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/DynamicSpinLoopDetection.java index 1c65201ce4..1a002d6b52 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/DynamicSpinLoopDetection.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/DynamicSpinLoopDetection.java @@ -132,6 +132,7 @@ private void reduceToDominatingSideEffects(LoopData loop) { final List sideEffects = loop.sideEffects; final Event start = loop.getStart(); final Event end = loop.getEnd(); + final Predicate isAlwaysSideEffectful = (e -> e.cfImpliesExec() && sideEffects.contains(e)); final DominatorTree preDominatorTree = DominatorAnalysis.computePreDominatorTree(start, end); final DominatorTree postDominatorTree = DominatorAnalysis.computePostDominatorTree(start, end); @@ -144,7 +145,7 @@ private void reduceToDominatingSideEffects(LoopData loop) { // (2) Check if always side-effect-full at the end of an iteration directly before entering the next one. // This is an approximation: If the end of the iteration is predominated by some side effect // then we always observe side effects. - loop.isAlwaysSideEffectful = Streams.stream(preDominatorTree.getDominators(end)).anyMatch(sideEffects::contains); + loop.isAlwaysSideEffectful = Streams.stream(preDominatorTree.getDominators(end)).anyMatch(isAlwaysSideEffectful); if (loop.isAlwaysSideEffectful) { return; } @@ -157,7 +158,7 @@ private void reduceToDominatingSideEffects(LoopData loop) { preDominatorTree.getStrictDominators(sideEffect), postDominatorTree.getStrictDominators(sideEffect) ); - final boolean isDominated = Iterables.tryFind(dominators, sideEffects::contains).isPresent(); + final boolean isDominated = Iterables.tryFind(dominators, isAlwaysSideEffectful::test).isPresent(); if (isDominated) { sideEffects.remove(i); } @@ -173,12 +174,22 @@ private void instrumentLoop(LoopData loop) { final ExpressionFactory expressions = ExpressionFactory.getInstance(); final Function func = loop.loopInfo.function(); final int loopNum = loop.loopInfo.loopNumber(); + final Register tempReg = func.newRegister("__possiblySideEffectless#" + loopNum, types.getBooleanType()); final Register trackingReg = func.newRegister("__sideEffect#" + loopNum, types.getBooleanType()); final Event init = EventFactory.newLocal(trackingReg, expressions.makeFalse()); loop.getStart().insertAfter(init); for (Event sideEffect : loop.sideEffects) { - final Event updateSideEffect = EventFactory.newLocal(trackingReg, expressions.makeTrue()); + final List updateSideEffect = new ArrayList<>(); + if (sideEffect.cfImpliesExec()) { + updateSideEffect.add(EventFactory.newLocal(trackingReg, expressions.makeTrue())); + } else { + updateSideEffect.addAll(List.of( + EventFactory.newExecutionStatus(tempReg, sideEffect), + EventFactory.newLocal(trackingReg, expressions.makeOr(trackingReg, expressions.makeNot(tempReg))) + )); + + } sideEffect.getPredecessor().insertAfter(updateSideEffect); } @@ -197,7 +208,7 @@ private Event newSpinTerminator(Expression guard, Function func) { final Event terminator = func instanceof Thread thread ? EventFactory.newJump(guard, (Label) thread.getExit()) : EventFactory.newAbortIf(guard); - terminator.addTags(Tag.SPINLOOP, Tag.EARLYTERMINATION, Tag.NOOPT); + terminator.addTags(Tag.SPINLOOP, Tag.NONTERMINATION, Tag.NOOPT); return terminator; } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Inlining.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Inlining.java index 38b2e1814f..a755d09f1e 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Inlining.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Inlining.java @@ -88,7 +88,7 @@ private void inlineAllCalls(Function function, Map snapshots if (depth > bound) { final AbortIf boundEvent = newAbortIf(ExpressionFactory.getInstance().makeTrue()); boundEvent.copyAllMetadataFrom(call); - boundEvent.addTags(Tag.BOUND, Tag.EARLYTERMINATION, Tag.NOOPT); + boundEvent.addTags(Tag.BOUND, Tag.NONTERMINATION, Tag.NOOPT); call.replaceBy(boundEvent); event = boundEvent; } else { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Intrinsics.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Intrinsics.java index db2871e546..b81f2a43e5 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Intrinsics.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Intrinsics.java @@ -901,7 +901,7 @@ private List inlineAssert(FunctionCall call, AssertionType skip, String e final Expression condition = expressions.makeFalse(); final Event assertion = EventFactory.newAssert(condition, errorMsg); final Event abort = EventFactory.newAbortIf(expressions.makeTrue()); - abort.addTags(Tag.EARLYTERMINATION); + abort.addTags(Tag.EXCEPTIONAL_TERMINATION); return List.of(assertion, abort); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopUnrolling.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopUnrolling.java index 7b6bca60a9..293f15f489 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopUnrolling.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopUnrolling.java @@ -191,7 +191,7 @@ private Event newBoundEvent(Function func) { final Event boundEvent = func instanceof Thread thread ? EventFactory.newGoto((Label) thread.getExit()) : EventFactory.newAbortIf(ExpressionFactory.getInstance().makeTrue()); - boundEvent.addTags(Tag.BOUND, Tag.EARLYTERMINATION, Tag.NOOPT); + boundEvent.addTags(Tag.BOUND, Tag.NONTERMINATION, Tag.NOOPT); return boundEvent; }