Add support for progress models (#731)

Co-authored-by: Hernan Ponce de Leon <[email protected]>

benchmarks/progress/progressFair.c

@@ -0,0 +1,27 @@
+#include <stdlib.h>
+#include <pthread.h>
+#include <assert.h>
+#include <stdatomic.h>
+
+// Required progress: fair
+
+atomic_int x = 0;
+
+void *thread_1(void *unused)
+{
+    while (x != 1);
+    return 0;
+}
+
+void *thread_2(void *unused)
+{
+    x = 1; // May not get scheduled under any weak progress model
+}
+
+int main()
+{
+    pthread_t t1, t2;
+    pthread_create(&t1, NULL, thread_1, NULL);
+    pthread_create(&t2, NULL, thread_2, NULL);
+    return 0;
+}

benchmarks/progress/progressHSA.c

@@ -0,0 +1,27 @@
+#include <stdlib.h>
+#include <pthread.h>
+#include <assert.h>
+#include <stdatomic.h>
+
+// Required progress: HSA
+
+atomic_int x = 0;
+
+void *thread_1(void *unused)
+{
+    x = 1; // OBE might not schedule this thread
+}
+
+void *thread_2(void *unused)
+{
+    while (x != 1);
+    return 0;
+}
+
+int main()
+{
+    pthread_t t1, t2;
+    pthread_create(&t1, NULL, thread_1, NULL);
+    pthread_create(&t2, NULL, thread_2, NULL);
+    return 0;
+}

benchmarks/progress/progressOBE-HSA.c

@@ -0,0 +1,24 @@
+#include <stdlib.h>
+#include <pthread.h>
+#include <assert.h>
+#include <stdatomic.h>
+
+// Required progress: HSA or OBE (stronger than unfair)
+
+atomic_int x = 0;
+
+void *thread_1(void *unused)
+{
+    while (x != 0);
+    return 0;
+}
+
+int main()
+{
+    pthread_t t1, t2;
+    pthread_create(&t1, NULL, thread_1, NULL);
+    x = 1;
+    // Under totally unfair scheduling, we can stop here so that T1 spins forever
+    x = 0;
+    return 0;
+}

benchmarks/progress/progressOBE.c

@@ -0,0 +1,29 @@
+#include <stdlib.h>
+#include <pthread.h>
+#include <assert.h>
+#include <stdatomic.h>
+
+// Required progress: OBE
+
+atomic_int x = 0;
+
+void *thread_1(void *unused)
+{
+    while (x != 0);
+    return 0;
+}
+
+void *thread_2(void *unused)
+{
+    x = 1;
+    // HSA may stop here causing a liveness issue (OBE cannot do this)
+    x = 0;
+}
+
+int main()
+{
+    pthread_t t1, t2;
+    pthread_create(&t1, NULL, thread_1, NULL);
+    pthread_create(&t2, NULL, thread_2, NULL);
+    return 0;
+}

benchmarks/progress/progressUnfair.c

@@ -0,0 +1,22 @@
+#include <stdlib.h>
+#include <pthread.h>
+#include <assert.h>
+#include <stdatomic.h>
+
+atomic_int x = 0;
+
+// Required progress: Unfair (terminates under all progress models)
+
+void *thread_1(void *unused)
+{
+    while (x != 1);
+    return 0;
+}
+
+int main()
+{
+    pthread_t t1, t2;
+    x = 1;
+    pthread_create(&t1, NULL, thread_1, NULL);
+    return 0;
+}

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

@@ -130,6 +130,7 @@ public static void main(String[] args) throws Exception {
 
         VerificationTaskBuilder builder = VerificationTask.builder()
                 .withConfig(config)
+                .withProgressModel(o.getProgressModel())
                 .withWitness(witness);
         // If the arch has been set during parsing (this only happens for litmus tests)
         // and the user did not explicitly add the target option, we use the one

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

@@ -15,6 +15,7 @@ public class OptionNames {
     public static final String SMTLIB2 = "smtlib2";
 
     // Modeling Options
+    public static final String PROGRESSMODEL = "modeling.progress";
     public static final String THREAD_CREATE_ALWAYS_SUCCEEDS = "modeling.threadCreateAlwaysSucceeds";
     public static final String RECURSION_BOUND = "modeling.recursionBound";
     public static final String MEMORY_IS_ZEROED = "modeling.memoryIsZeroed";

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

@@ -0,0 +1,22 @@
+package com.dat3m.dartagnan.configuration;
+
+import java.util.Arrays;
+
+public enum ProgressModel {
+    FAIR, // All threads are fairly scheduled
+    HSA, // Lowest id thread gets fairly scheduled.
+    OBE, // Threads that made at least one step get fairly scheduled.
+    UNFAIR; // No fair scheduling
+
+    public static ProgressModel getDefault() {
+        return FAIR;
+    }
+
+    // Used to decide the order shown by the selector in the UI
+    public static ProgressModel[] orderedValues() {
+        ProgressModel[] order = {FAIR, HSA, OBE, UNFAIR};
+        // Be sure no element is missing
+        assert (Arrays.asList(order).containsAll(Arrays.asList(values())));
+        return order;
+    }
+}

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

@@ -1,5 +1,6 @@
 package com.dat3m.dartagnan.encoding;
 
+import com.dat3m.dartagnan.configuration.ProgressModel;
 import com.dat3m.dartagnan.expression.Expression;
 import com.dat3m.dartagnan.expression.Type;
 import com.dat3m.dartagnan.expression.integers.IntCmpOp;
@@ -369,7 +370,11 @@ public Formula makeLiteral(Type type, BigInteger value) {
     }
 
     private void initialize() {
-        if (shouldMergeCFVars) {
+        // Only for the standard fair progress model we can merge CF variables.
+        // TODO: It would also be possible for OBE/HSA in some cases if we refine the cf-equivalence classes
+        //  to classes per thread.
+        final boolean mergeCFVars = shouldMergeCFVars && verificationTask.getProgressModel() == ProgressModel.FAIR;
+        if (mergeCFVars) {
             for (BranchEquivalence.Class cls : analysisContext.get(BranchEquivalence.class).getAllEquivalenceClasses()) {
                 BooleanFormula v = booleanFormulaManager.makeVariable("cf " + cls.getRepresentative().getGlobalId());
                 for (Event e : cls) {