Updated the new Nontermination tests, mainly to be (almost) race-free

Fixed Nontermination verdict if nontermination was caused due to assertion failure.
Updated expected outcomes of LivenessTest caused by the above change.

benchmarks/nontermination/nontermination.c

@@ -1,24 +1,27 @@
 #include <pthread.h>
+#include <stdatomic.h>
 
 /*
     Test case: Oscillating memory value but the same value is constantly observed
     Expected result: FAIL under all memory models.
 */
 
-volatile int x = 0;
-volatile int y = 0;
+atomic_int x = 0;
+atomic_int y = 0;
 
 void *thread(void *unused)
 {
     while(y != 1) {
         x = 1;
         x = 2;
     }
+    return 0;
 }
 
 void *thread2(void *unused) {
     while (x != 2) { }
     y = 1;
+    return 0;
 }
 
 int main()

benchmarks/nontermination/nontermination_complex.c

@@ -1,14 +1,15 @@
 #include <pthread.h>
+#include <stdatomic.h>
 
 /*
     Test case: Three loops that interfere with each other..
     Expected result: FAIL under all memory models.
     NOTE: Any pair of loops would terminate, only all three together fail.
 */
 
-volatile int x = 0;
-volatile int y = 0;
-volatile int z = 0;
+atomic_int x = 0;
+atomic_int y = 0;
+atomic_int z = 0;
 
 void *thread(void *unused)
 {
@@ -17,6 +18,7 @@ void *thread(void *unused)
         x = 0;
         y = 1;
     }
+    return 0;
 }
 
 void *thread2(void *unused) {
@@ -25,14 +27,15 @@ void *thread2(void *unused) {
             z = i;
         }
     }
+    return 0;
 }
 
 void *thread3(void *unused) {
     while (z == 1) {
         y = 0;
         z = 0;
     }
-
+    return 0;
 }
 
 int main()

benchmarks/nontermination/nontermination_weak.c

@@ -7,24 +7,26 @@
 */
 
 volatile int x = 0;
-volatile int signal = 0;
-volatile int success = 0;
+atomic_int signal = 0;
+atomic_int success = 0;
 
 void *thread(void *unused)
 {
     while(!success) {
         x = 1;
-        signal = 1;
+        atomic_store_explicit(&signal, 1, memory_order_relaxed);
     }
+    return 0;
 }
 
 void *thread2(void *unused) {
-    while (signal == 1 && x == 0) {
+    while (atomic_load_explicit(&signal, memory_order_relaxed) == 1 && x == 0) {
         // Message was wrong, reset and wait for new one.
         x = 0;
         signal = 0;
     }
     success = 1;
+    return 0;
 }
 
 int main()

benchmarks/nontermination/nontermination_xchg.c

@@ -10,11 +10,13 @@ atomic_int lock;
 
 void *thread(void *unused)
 {
-    while (atomic_exchange(&lock, 1) == 1);
+    while (atomic_exchange(&lock, 1) != 0);
+    return 0;
 }
 
 void *thread2(void *unused) {
-    lock = 1;
+    atomic_exchange(&lock, 1);
+    return 0;
 }
 
 int main()

benchmarks/nontermination/nontermination_zero_effect.c

@@ -25,6 +25,7 @@ void *thread(void *unused)
 {
     acquireLock();
     releaseLock();
+    return 0;
 }
 
 int main()

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

@@ -192,16 +192,27 @@ private void computeEventToCaseInformation() {
     public BooleanFormula encodeNontermination() {
         final BooleanFormulaManager bmgr = context.getBooleanFormulaManager();
         final BooleanFormula atLeastOneStuckLoop = encodeLoopsAreStuck();
+        final BooleanFormula noExceptionalTermination = encodeNoExceptionalTermination();
         final BooleanFormula infixSuffixEquivalence = encodeInfixSuffixEquivalence();
         final BooleanFormula strongSuffixExtension = encodeStrongSuffixExtension();
 
         return bmgr.and(
+                noExceptionalTermination,
                 atLeastOneStuckLoop,
                 infixSuffixEquivalence,
                 strongSuffixExtension
         );
     }
 
+    private BooleanFormula encodeNoExceptionalTermination() {
+        final BooleanFormulaManager bmgr = context.getBooleanFormulaManager();
+        final BooleanFormula noExceptionalTermination = task.getProgram()
+                .getThreadEventsWithAllTags(Tag.EXCEPTIONAL_TERMINATION).stream()
+                .map(e -> bmgr.not(context.execution(e)))
+                .reduce(bmgr.makeTrue(), bmgr::and);
+        return noExceptionalTermination;
+    }
+
     private BooleanFormula encodeLoopsAreStuck() {
         final BooleanFormulaManager bmgr = context.getBooleanFormulaManager();
         final BooleanFormula atLeastOneNontermination = bound2Case.values().stream()

dartagnan/src/test/java/com/dat3m/dartagnan/c/LivenessTest.java

@@ -103,13 +103,13 @@ public static Iterable<Object[]> data() throws IOException {
                 {"locks/linuxrwlock", POWER, UNKNOWN},
                 {"locks/linuxrwlock", RISCV, UNKNOWN},
                 {"locks/linuxrwlock-acq2rx", TSO, UNKNOWN},
-                {"locks/linuxrwlock-acq2rx", ARM8, FAIL},
-                {"locks/linuxrwlock-acq2rx", POWER, FAIL},
-                {"locks/linuxrwlock-acq2rx", RISCV, FAIL},
+                {"locks/linuxrwlock-acq2rx", ARM8, UNKNOWN},
+                {"locks/linuxrwlock-acq2rx", POWER, UNKNOWN},
+                {"locks/linuxrwlock-acq2rx", RISCV, UNKNOWN},
                 {"locks/linuxrwlock-rel2rx", TSO, UNKNOWN},
-                {"locks/linuxrwlock-rel2rx", ARM8, FAIL},
-                {"locks/linuxrwlock-rel2rx", POWER, FAIL},
-                {"locks/linuxrwlock-rel2rx", RISCV, FAIL},
+                {"locks/linuxrwlock-rel2rx", ARM8, UNKNOWN},
+                {"locks/linuxrwlock-rel2rx", POWER, UNKNOWN},
+                {"locks/linuxrwlock-rel2rx", RISCV, UNKNOWN},
                 {"locks/mutex_musl", TSO, UNKNOWN},
                 {"locks/mutex_musl", ARM8, UNKNOWN},
                 {"locks/mutex_musl", POWER, UNKNOWN},