Improved liveness detection for store exclusives

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<TrackableFormula> encodeCATSpecificationViolations() {
         final EncodingContext ctx = this.context;
         final Wmm memoryModel = this.memoryModel;
         final List<Axiom> 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<Load> containedLoads = new ArrayList<>();
-            // Execution of the <boundJump> 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<CondJump> 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<Thread, List<SpinIteration>> spinloopsMap =
-                    Maps.toMap(program.getThreads(), t -> this.findSpinLoopsInThread(t, loopAnalysis));
-            // Compute "stuckness" encoding for all threads
-            final Map<Thread, BooleanFormula> 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<SpinIteration> loops, EncodingContext context) {
+        // ------------------------------------------------------------------------------
+        // Liveness issue due to non-terminating loops (~ deadlocks)
+
+        private record SpinIteration(List<Event> body, List<CondJump> spinningJumps) {
+            // Execution of the <spinningJumps> 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<Event, Set<Event>> rfMayIn = ra.getKnowledge(rf).getMaySet().getInMap();
 
-            if (loops.isEmpty()) {
-                return bmgr.makeFalse();
-            }
+            final List<Load> 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<RMWStoreExclusive> 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<SpinIteration> findSpinLoopsInThread(Thread thread, LoopAnalysis loopAnalysis) {
@@ -525,14 +573,7 @@ private List<SpinIteration> findSpinLoopsInThread(Thread thread, LoopAnalysis lo
                             .toList();
 
                     if (!spinningJumps.isEmpty()) {
-                        final List<Load> 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);
                     }
                 }

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)

dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/DynamicSpinLoopDetection.java

@@ -132,6 +132,7 @@ private void reduceToDominatingSideEffects(LoopData loop) {
         final List<Event> sideEffects = loop.sideEffects;
         final Event start = loop.getStart();
         final Event end = loop.getEnd();
+        final Predicate<Event> isAlwaysSideEffectful = (e -> e.cfImpliesExec() && sideEffects.contains(e));
 
         final DominatorTree<Event> preDominatorTree = DominatorAnalysis.computePreDominatorTree(start, end);
         final DominatorTree<Event> 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<Event> 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;
     }
 

dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Inlining.java

@@ -88,7 +88,7 @@ private void inlineAllCalls(Function function, Map<Function, Snapshot> 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 {

dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Intrinsics.java

@@ -901,7 +901,7 @@ private List<Event> 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);
     }