[DRAFT] Add interrupt handling

benchmarks/interrupts/assert_assume_race_v1.c

@@ -0,0 +1,24 @@
+#include <stdlib.h>
+#include <stdatomic.h>
+#include <pthread.h>
+#include <assert.h>
+#include <dat3m.h>
+
+// Test case: Racing assume and assert.
+// Expected: PASS, IH will not terminate on assert failure, main-thread performs assume.
+
+void *handler(void *arg)
+{
+    // assert(0);               // FAIL (assert failure terminates both IH and IT before assume executes)
+    __VERIFIER_assert(0);       // PASS (assert failure does not terminate IH nor IT, therefore assume will execute)
+    return NULL;
+}
+
+int main()
+{
+    __VERIFIER_register_interrupt_handler(handler);
+
+    __VERIFIER_assume(0);
+
+    return 0;
+}

benchmarks/interrupts/assert_assume_race_v2.c

@@ -0,0 +1,24 @@
+#include <stdlib.h>
+#include <stdatomic.h>
+#include <pthread.h>
+#include <assert.h>
+#include <dat3m.h>
+
+// Test case: Racing assume and assert.
+// Expected: FAIL, IH may interrupt before assume, fail its assertion and therefore terminate the program.
+
+void *handler(void *arg)
+{
+    assert(0);                  // FAIL (assert failure terminates both IH and IT before assume executes)
+    // __VERIFIER_assert(0);    // PASS (assert failure does not terminate IH nor IT, therefore assume will execute)
+    return NULL;
+}
+
+int main()
+{
+    __VERIFIER_register_interrupt_handler(handler);
+
+    __VERIFIER_assume(0);
+
+    return 0;
+}

benchmarks/interrupts/c11_detour.c

@@ -0,0 +1,51 @@
+#include <stdlib.h>
+#include <stdatomic.h>
+#include <pthread.h>
+#include <assert.h>
+#include <dat3m.h>
+
+// Expected: PASS
+
+atomic_int x, y;
+int a, b;
+
+pthread_t h;
+void *handler(void *arg)
+{
+    atomic_store_explicit(&y, 3, memory_order_seq_cst);
+    return NULL;
+}
+
+void *thread_1(void *arg)
+{
+    __VERIFIER_make_interrupt_handler();
+    pthread_create(&h, NULL, handler, NULL);
+
+    atomic_store_explicit(&x, 1, memory_order_relaxed);
+    a = atomic_load_explicit(&y, memory_order_relaxed);
+
+    pthread_join(h, 0);
+
+    return NULL;
+}
+
+void *thread_2(void *arg)
+{
+    b = atomic_load_explicit(&x, memory_order_relaxed);
+    atomic_store_explicit(&y, 2, memory_order_release);
+    return NULL;
+}
+
+int main()
+{
+    pthread_t t1, t2;
+
+    pthread_create(&t1, 0, thread_1, NULL);
+    pthread_create(&t2, 0, thread_2, NULL);
+    pthread_join(t1, 0);
+    pthread_join(t2, 0);
+
+    __VERIFIER_assert(!(b == 1 && a == 3 && y == 3));
+
+    return 0;
+}

benchmarks/interrupts/c11_detour_disable.c

@@ -0,0 +1,53 @@
+#include <stdlib.h>
+#include <stdatomic.h>
+#include <pthread.h>
+#include <assert.h>
+#include <dat3m.h>
+
+// Expected: FAIL
+
+atomic_int x, y;
+int a, b;
+
+pthread_t h;
+void *handler(void *arg)
+{
+    atomic_store_explicit(&y, 3, memory_order_seq_cst);
+    return NULL;
+}
+
+void *thread_1(void *arg)
+{
+    __VERIFIER_make_interrupt_handler();
+    pthread_create(&h, NULL, handler, NULL);
+
+    __VERIFIER_disable_irq();
+    atomic_store_explicit(&x, 1, memory_order_relaxed);
+    a = atomic_load_explicit(&y, memory_order_relaxed);
+    __VERIFIER_enable_irq();
+
+    pthread_join(h, 0);
+
+    return NULL;
+}
+
+void *thread_2(void *arg)
+{
+    b = atomic_load_explicit(&x, memory_order_relaxed);
+    atomic_store_explicit(&y, 2, memory_order_release);
+    return NULL;
+}
+
+int main()
+{
+    pthread_t t1, t2;
+
+    pthread_create(&t1, 0, thread_1, NULL);
+    pthread_create(&t2, 0, thread_2, NULL);
+    pthread_join(t1, 0);
+    pthread_join(t2, 0);
+
+    __VERIFIER_assert(!(b == 1 && a == 3 && y == 3));
+
+    return 0;
+}

benchmarks/interrupts/c11_detour_disable_release.c

@@ -0,0 +1,53 @@
+#include <stdlib.h>
+#include <stdatomic.h>
+#include <pthread.h>
+#include <assert.h>
+#include <dat3m.h>
+
+// Expected: FAIL
+
+atomic_int x, y;
+int a, b;
+
+pthread_t h;
+void *handler(void *arg)
+{
+    atomic_store_explicit(&y, 3, memory_order_seq_cst);
+    return NULL;
+}
+
+void *thread_1(void *arg)
+{
+    __VERIFIER_make_interrupt_handler();
+    pthread_create(&h, NULL, handler, NULL);
+
+    __VERIFIER_disable_irq();
+    atomic_store_explicit(&x, 1, memory_order_release);
+    a = atomic_load_explicit(&y, memory_order_relaxed);
+    __VERIFIER_enable_irq();
+
+    pthread_join(h, 0);
+
+    return NULL;
+}
+
+void *thread_2(void *arg)
+{
+    b = atomic_load_explicit(&x, memory_order_relaxed);
+    atomic_store_explicit(&y, 2, memory_order_release);
+    return NULL;
+}
+
+int main()
+{
+    pthread_t t1, t2;
+
+    pthread_create(&t1, 0, thread_1, NULL);
+    pthread_create(&t2, 0, thread_2, NULL);
+    pthread_join(t1, 0);
+    pthread_join(t2, 0);
+
+    __VERIFIER_assert(!(b == 1 && a == 3 && y == 3));
+
+    return 0;
+}

benchmarks/interrupts/c11_oota.c

@@ -0,0 +1,49 @@
+#include <stdlib.h>
+#include <stdatomic.h>
+#include <pthread.h>
+#include <assert.h>
+#include <dat3m.h>
+
+// Expected: PASS
+
+atomic_int x, y, z;
+
+pthread_t h;
+void *handler(void *arg)
+{
+    atomic_store_explicit(&z, 3, memory_order_relaxed);
+    __VERIFIER_assert(atomic_load_explicit(&y, memory_order_relaxed) == 0);
+    return NULL;
+}
+
+void *thread_1(void *arg)
+{
+    __VERIFIER_make_interrupt_handler();
+    pthread_create(&h, NULL, handler, NULL);
+
+    if(atomic_load_explicit(&x, memory_order_relaxed) == 1) {
+        atomic_store_explicit(&y, 2, memory_order_relaxed);
+    }
+
+    pthread_join(h, 0);
+
+    return NULL;
+}
+
+void *thread_2(void *arg)
+{
+    if(atomic_load_explicit(&z, memory_order_relaxed) == 3) {
+        atomic_store_explicit(&x, 1, memory_order_relaxed);
+    }
+    return NULL;
+}
+
+int main()
+{
+    pthread_t t1, t2;
+
+    pthread_create(&t1, 0, thread_1, NULL);
+    pthread_create(&t2, 0, thread_2, NULL);
+
+    return 0;
+}

benchmarks/interrupts/c11_weak_model.c

@@ -0,0 +1,65 @@
+#include <stdlib.h>
+#include <stdbool.h>
+#include <stdatomic.h>
+#include <pthread.h>
+#include <assert.h>
+#include <dat3m.h>
+
+// Expected: ???
+
+atomic_int x, y, a1, a2, b1, b2;
+int r1, r2, t1, u1, t2, u2;
+
+pthread_t h;
+void *handler(void *arg)
+{
+    r1 = atomic_load_explicit(&x, memory_order_relaxed);
+    atomic_thread_fence(memory_order_seq_cst);
+    r2 = atomic_load_explicit(&y, memory_order_relaxed);
+    return NULL;
+}
+
+void *thread_1(void *arg)
+{
+    __VERIFIER_make_interrupt_handler();
+    pthread_create(&h, NULL, handler, NULL);
+
+    atomic_store_explicit(&b1, 1, memory_order_relaxed);
+    atomic_store_explicit(&x, 1, memory_order_relaxed);
+    atomic_store_explicit(&a1, 1, memory_order_relaxed);
+    atomic_store_explicit(&b2, 1, memory_order_relaxed);
+    atomic_store_explicit(&y, 1, memory_order_relaxed);
+    atomic_store_explicit(&a2, 1, memory_order_relaxed);
+
+    pthread_join(h, 0);
+
+    return NULL;
+}
+
+void *thread_2(void *arg)
+{
+    t1 = atomic_load_explicit(&a1, memory_order_relaxed);
+    u1 = atomic_load_explicit(&b1, memory_order_relaxed);
+    atomic_thread_fence(memory_order_seq_cst);
+    t2 = atomic_load_explicit(&a2, memory_order_relaxed);
+    u2 = atomic_load_explicit(&b2, memory_order_relaxed);
+    return NULL;
+}
+
+int main()
+{
+    pthread_t thread1, thread2;
+
+    pthread_create(&thread1, 0, thread_1, NULL);
+    pthread_create(&thread2, 0, thread_2, NULL);
+    pthread_join(thread1, 0);
+    pthread_join(thread2, 0);
+
+    bool reorder_bx = (t1 == 1 && t2 == 0); 
+    bool reorder_ya = (u1 == 1 && u2 == 0);
+    if (r1 == 1 && r2 == 0) { 
+        __VERIFIER_assert(! reorder_bx || ! reorder_ya);
+    }
+
+    return 0;
+}

benchmarks/interrupts/c11_with_barrier.c

@@ -0,0 +1,52 @@
+#include <stdlib.h>
+#include <stdatomic.h>
+#include <pthread.h>
+#include <assert.h>
+#include <dat3m.h>
+
+/*
+    This test shows how interrupt handlers are spawned
+    Expected: PASS
+*/
+
+struct A { volatile int a; volatile int b; }; // Without "volatile" the compiler removes our assertions.
+struct A as[10];
+int cnt = 0;
+
+pthread_t h;
+void *handler(void *arg)
+{
+    int tindex = ((intptr_t) arg);
+    int i = cnt++;
+    __VERIFIER_make_cb();
+    as[i].a = tindex;
+    as[i].b = tindex;
+    __VERIFIER_assert(as[i].a == as[i].b);
+
+    return NULL;
+}
+
+void *run(void *arg)
+{
+    __VERIFIER_make_interrupt_handler(); // Buggy without this marker
+    pthread_create(&h, NULL, handler, 0);
+
+    int tindex = ((intptr_t) arg);
+    int i = cnt++;
+    __VERIFIER_make_cb();
+    as[i].a = tindex;
+    as[i].b = tindex;
+    __VERIFIER_assert(as[i].a == as[i].b);
+
+    pthread_join(h, NULL);
+
+    return NULL;
+}
+
+int main()
+{
+    pthread_t t;
+    pthread_create(&t, NULL, run, (void *)1);
+
+    return 0;
+}