dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java

@@ -3,6 +3,7 @@
 import com.dat3m.dartagnan.configuration.OptionNames;
 import com.dat3m.dartagnan.configuration.Property;
 import com.dat3m.dartagnan.encoding.EncodingContext;
+import com.dat3m.dartagnan.encoding.ProverWithTracker;
 import com.dat3m.dartagnan.expression.ExpressionPrinter;
 import com.dat3m.dartagnan.parsers.cat.ParserCat;
 import com.dat3m.dartagnan.parsers.program.ProgramParser;
@@ -163,7 +164,10 @@ public static void main(String[] args) throws Exception {
                     BasicLogManager.create(solverConfig),
                     sdm.getNotifier(),
                     o.getSolver());
-                    ProverEnvironment prover = ctx.newProverEnvironment(ProverOptions.GENERATE_MODELS)) {
+                    ProverWithTracker prover = new ProverWithTracker(ctx,
+                        o.getDumpSmtLib() ?
+                            System.getenv("DAT3M_OUTPUT") + String.format("/%s.smt2", p.getName()) : "",
+                        ProverOptions.GENERATE_MODELS)) {
                 ModelChecker modelChecker;
                 if (properties.contains(DATARACEFREEDOM)) {
                     if (properties.size() > 1) {

dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java

@@ -12,6 +12,7 @@ public class OptionNames {
     public static final String VALIDATE = "validate";
     public static final String COVERAGE = "coverage";
     public static final String WITNESS = "witness";
+    public static final String SMTLIB2 = "smtlib2";
 
     // Modeling Options
     public static final String THREAD_CREATE_ALWAYS_SUCCEEDS = "modeling.threadCreateAlwaysSucceeds";

dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ExpressionEncoder.java

@@ -11,7 +11,7 @@
 import com.dat3m.dartagnan.expression.type.TypeFactory;
 import com.dat3m.dartagnan.program.Register;
 import com.dat3m.dartagnan.program.event.Event;
-import com.dat3m.dartagnan.program.memory.Location;
+import com.dat3m.dartagnan.program.memory.FinalMemoryValue;
 import com.dat3m.dartagnan.program.memory.MemoryObject;
 import com.dat3m.dartagnan.program.misc.NonDetValue;
 import org.sosy_lab.java_smt.api.*;
@@ -298,9 +298,9 @@ public Formula visitMemoryObject(MemoryObject memObj) {
     }
 
     @Override
-    public Formula visitLocation(Location location) {
-        checkState(event == null, "Cannot evaluate %s at event %s.", location, event);
-        int size = types.getMemorySizeInBits(location.getType());
-        return context.lastValue(location.getMemoryObject(), location.getOffset(), size);
+    public Formula visitFinalMemoryValue(FinalMemoryValue val) {
+        checkState(event == null, "Cannot evaluate final memory value of %s at event %s.", val, event);
+        int size = types.getMemorySizeInBits(val.getType());
+        return context.lastValue(val.getMemoryObject(), val.getOffset(), size);
     }
 }

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,9 @@
 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.program.Program.SpecificationType.ASSERT;
+import static com.dat3m.dartagnan.wmm.RelationNameRepository.CO;
 
 public class PropertyEncoder implements Encoder {
 
@@ -66,7 +66,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;
 
@@ -276,17 +276,18 @@ private TrackableFormula encodeProgramSpecification() {
             case FORALL, NOT_EXISTS, ASSERT -> bmgr.not(PROGRAM_SPEC.getSMTVariable(context));
             case EXISTS -> PROGRAM_SPEC.getSMTVariable(context);
         };
-        if (!program.getFormat().equals(LLVM)) {
+        if (!ASSERT.equals(program.getSpecificationType())) {
             encoding = bmgr.and(encoding, encodeProgramTermination());
         }
         return new TrackableFormula(trackingLiteral, encoding);
     }
 
     private BooleanFormula encodeProgramTermination() {
         final BooleanFormulaManager bmgr = context.getBooleanFormulaManager();
-        return bmgr.and(program.getThreads().stream()
+        BooleanFormula exitReached = bmgr.and(program.getThreads().stream()
                 .map(t -> bmgr.equivalence(context.execution(t.getEntry()), context.execution(t.getExit())))
                 .toList());
+        return bmgr.and(exitReached, bmgr.not(encodeBoundEventExec()));
     }
 
     // ======================================================================
@@ -304,7 +305,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 +403,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 +438,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 +463,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 +481,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 +575,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);
                     }
                 }