Challenging benchmarks

benchmarks/challenging/README.md

@@ -0,0 +1,6 @@
+This directory contains a collection of benchmarks that
+are challenging for Dartagnan and thus are not run as
+part of its unit tests (even if they are solvable).
+
+The challenging benchmarks are useful to find bottlenecks in Dartagnan
+and evaluate potential fixes.

benchmarks/challenging/cna.c

@@ -0,0 +1,73 @@
+#include <pthread.h>
+#include <assert.h>
+#include "dat3m.h"
+
+// NOTE: This version of CNA is different to the one found in "benchmarks/locks/"
+// It comes from an implementation from "Universität Hannover"
+
+/*
+    This code exposed a bug fixed by https://github.com/hernanponcedeleon/Dat3M/pull/1014:
+    The following Dartagnan configuration would sometimes fail to be conclusive
+        <dat3m> cat/sc.cat client.c --method=lazy --bound=3 --encoding.integers=true --property=termination
+ */
+
+ /*
+    This benchmark shows interesting performance characteristics with
+                            sc.cat  --bound=3 --solver=z3
+    The bound is needed to get PASS.
+
+    (1) --method=eager seems to be a lot better than lazy (depending on config, but can be >5x faster)
+        This suggests that data-flow reasoning is hard for some reason.
+        with "--refinement.baseline=NO_OOTA", the solving times become similar again.
+    (2) For eager, "--encoding.wmm.idl2sat=true" is a lot faster than IDL (at least 5x faster?)
+    (3) Effect of "--encoding.integers=true" is unclear
+    (4) with #define FAIL, the code still satisfies program_spec (only termination fails) under SC.
+        However, verifying this is substantially(!) slower than the correct version.
+        Code-wise, the FAIL variant is only slightly larger.
+
+     Fastest configs:
+         --method=eager --encoding.wmm.idl2sat=true
+     AND --method=lazy  --encoding.wmm.idl2sat=true --refinement.baseline=NO_OOTA
+ */
+
+//#define FAIL          // Enable buggy version: termination violation under SC,
+                        // program_spec/data-races under weaker models.
+#include "cna.h"
+
+#ifndef NTHREADS
+#define NTHREADS 4      // Need 4 threads to find the bugs!
+#endif
+
+lock_t my_lock;
+__thread lock_handle_t handle;
+int sum = 0;
+
+
+void *thread_n(void *arg)
+{
+    // Assign arbitrary numa id to test all numa configurations
+    thread_numa_id = __VERIFIER_nondet_uint();
+
+    cna_lock(&my_lock, &handle);
+    sum++;
+    cna_unlock(&my_lock, &handle);
+    return NULL;
+}
+
+int main()
+{
+    cna_init(&my_lock);
+
+    pthread_t t[NTHREADS];
+
+    for (int i = 0; i < NTHREADS; i++)
+        pthread_create(&t[i], NULL, thread_n, NULL);
+
+    for (int i = 0; i < NTHREADS; i++)
+        pthread_join(t[i], NULL);
+
+    // If mutual exclusion is violated, an increment can get lost
+    assert(sum == NTHREADS);
+
+    return 0;
+}

benchmarks/challenging/cna.h

@@ -0,0 +1,182 @@
+#include <stdatomic.h>
+#include <stdint.h>
+#include <stdbool.h>
+
+extern __thread uint32_t thread_numa_id;
+
+typedef struct cna_node {
+    _Atomic(struct cna_node *) next;
+    atomic_bool locked;
+    int32_t numa_id;
+} cna_node_t;
+
+typedef struct {
+    _Atomic(cna_node_t *) tail;
+    cna_node_t *secondary_head;
+    cna_node_t *secondary_tail;
+} cna_t;
+
+typedef union {
+    cna_t cna;
+} lock_t;
+
+typedef union {
+    cna_node_t cna_node;
+} lock_handle_t;
+
+
+
+
+void cna_init(lock_t *lock)
+{
+   cna_t *cna = &lock->cna;
+   cna->tail = NULL;
+   cna->secondary_head = NULL;
+   cna->secondary_tail = NULL;
+}
+
+// Enqueue current thread as new waiter.
+void cna_lock(lock_t *lock, lock_handle_t *handle)
+{
+   cna_t *cna = &lock->cna;
+   cna_node_t *node = &handle->cna_node;
+   // Init new handle object
+   node->next = NULL;
+   node->numa_id = thread_numa_id;
+
+   // Update tail pointer and get previous value
+   cna_node_t *previous = atomic_exchange(&cna->tail, node);
+   if (previous != NULL) {
+       node->locked = true;
+       previous->next = node;
+       while (atomic_load(&node->locked)) {
+           asm("PAUSE"); // Reduce CPU load
+       }
+   }
+}
+
+#ifndef FAIL
+
+void cna_unlock(lock_t *lock, lock_handle_t *handle)
+{
+   cna_node_t *node = &handle->cna_node;
+   cna_t *cna = &lock->cna;
+
+   while (true) {
+       // Try to put back secondary queue assuming we are the last node
+       // in the primary queue.
+       cna_node_t *old = node;
+       cna_node_t* old_sec_tail = cna->secondary_tail;
+       if (atomic_compare_exchange_strong(&cna->tail, &old, old_sec_tail)) {
+           if (old_sec_tail != NULL) {
+               // Some non-local waiters has been moved to main queue
+               // Reset secondary queue
+               node->next = cna->secondary_head;
+               cna->secondary_head = NULL;
+               cna->secondary_tail = NULL;
+               // Wakeup non-local successor
+               atomic_store(&node->next->locked, false);
+           }
+           return;
+       }
+       // There is at least one more waiter in the primary queue.
+       // Wait until he updated our next pointer if not already done.
+       while (atomic_load(&node->next) == NULL) {
+           asm("PAUSE"); // Reduce CPU load
+       }
+
+       cna_node_t *waiter = node->next;
+       if (waiter->numa_id != thread_numa_id) {
+           // Waiter is non-local
+           if (waiter->next != NULL) {
+               // Skip one non-local waiter if there are more waiters
+               // Move non-local waiter to secondary queue
+               node->next = waiter->next;
+               waiter->next = NULL;
+               if (cna->secondary_head == NULL) {
+                   cna->secondary_head = waiter;
+               } else {
+                   cna->secondary_tail->next = waiter;
+               }
+               cna->secondary_tail = waiter;
+               continue;
+           } else if (cna->secondary_tail) {
+               // If only a single non-local waiter left,
+               // merge secondary queue (if existing).
+               node->next = cna->secondary_head;
+               cna->secondary_tail->next = waiter;
+               cna->secondary_head = NULL;
+               cna->secondary_tail = NULL;
+           }
+       }
+       // Unlock next waiter
+       atomic_store(&node->next->locked, false);
+       return;
+   }
+
+#else        // #ifdef FAIL
+
+// This implementation is buggy:
+// Termination failure under SC
+// Under weaker models, also mutual exclusion failure / data races
+
+void cna_unlock(lock_t *lock, lock_handle_t *handle)
+{
+    cna_node_t *node = &handle->cna_node;
+    cna_t *cna = &lock->cna;
+
+    while (true) {
+
+        if (node->next == NULL) {
+            // No waiting successor
+            cna_node_t *old = node;
+            // Try to put back secondary queue
+            if (atomic_compare_exchange_strong(&cna->tail, &old, cna->secondary_tail)) {
+                if (cna->secondary_tail != NULL) {
+                    // Some non-local waiters has been moved to main queue
+                    // Reset secondary queue
+                    node->next = cna->secondary_head;
+                    cna->secondary_head = NULL;
+                    cna->secondary_tail = NULL;
+                    // Wakeup non-local successor
+                    atomic_store(&node->next->locked, false);
+                }
+                return;
+            }
+            // Someone tried to get the lock in the meantime
+            // Wait until he updated our next pointer
+            while (atomic_load(&node->next) == NULL) {
+                asm("PAUSE"); // Reduce CPU load
+            }
+        }
+
+        cna_node_t *waiter = node->next;
+        if (waiter->numa_id != thread_numa_id) {
+            // Waiter is non-local
+            if (waiter->next != NULL) {
+                // Skip one non-local waiter if there are more waiters
+                // Move non-local waiter to secondary queue
+                node->next = waiter->next;
+                waiter->next = NULL;
+                if (cna->secondary_head == NULL) {
+                    cna->secondary_head = waiter;
+                } else {
+                    cna->secondary_tail->next = waiter;
+                }
+                cna->secondary_tail = waiter;
+                continue;
+            } else if (cna->secondary_tail) {
+                // If only a single non-local waiter left,
+                // merge secondary queue (if existing).
+                node->next = cna->secondary_head;
+                cna->secondary_tail->next = waiter;
+                cna->secondary_head = NULL;
+                cna->secondary_tail = NULL;
+            }
+        }
+        // Unlock next waiter
+        atomic_store(&node->next->locked, false);
+        return;
+    }
+#endif
+}