Add data structure benchmarks
authorweiyu <weiyuluo1232@gmail.com>
Tue, 4 Aug 2020 19:37:20 +0000 (12:37 -0700)
committerweiyu <weiyuluo1232@gmail.com>
Tue, 4 Aug 2020 19:37:20 +0000 (12:37 -0700)
44 files changed:
cdschecker_modified_benchmarks/Makefile [new file with mode: 0644]
cdschecker_modified_benchmarks/barrier/Makefile [new file with mode: 0644]
cdschecker_modified_benchmarks/barrier/barrier.cc [new file with mode: 0644]
cdschecker_modified_benchmarks/barrier/barrier.h [new file with mode: 0644]
cdschecker_modified_benchmarks/benchmarks.mk [new file with mode: 0644]
cdschecker_modified_benchmarks/chase-lev-deque/Makefile [new file with mode: 0644]
cdschecker_modified_benchmarks/chase-lev-deque/deque.cc [new file with mode: 0644]
cdschecker_modified_benchmarks/chase-lev-deque/deque.h [new file with mode: 0644]
cdschecker_modified_benchmarks/chase-lev-deque/main.cc [new file with mode: 0644]
cdschecker_modified_benchmarks/dekker-fences/Makefile [new file with mode: 0644]
cdschecker_modified_benchmarks/dekker-fences/dekker-fences.cc [new file with mode: 0644]
cdschecker_modified_benchmarks/include/cds_atomic.h [new file with mode: 0755]
cdschecker_modified_benchmarks/include/cds_threads.h [new file with mode: 0755]
cdschecker_modified_benchmarks/include/librace.h [new file with mode: 0755]
cdschecker_modified_benchmarks/include/model-assert.h [new file with mode: 0755]
cdschecker_modified_benchmarks/include/unrelacy.h [new file with mode: 0755]
cdschecker_modified_benchmarks/linuxrwlocks/Makefile [new file with mode: 0644]
cdschecker_modified_benchmarks/linuxrwlocks/linuxrwlocks.cc [new file with mode: 0644]
cdschecker_modified_benchmarks/mcs-lock/Makefile [new file with mode: 0644]
cdschecker_modified_benchmarks/mcs-lock/mcs-lock.cc [new file with mode: 0644]
cdschecker_modified_benchmarks/mcs-lock/mcs-lock.h [new file with mode: 0644]
cdschecker_modified_benchmarks/mpmc-queue/Makefile [new file with mode: 0644]
cdschecker_modified_benchmarks/mpmc-queue/mpmc-queue.cc [new file with mode: 0644]
cdschecker_modified_benchmarks/mpmc-queue/mpmc-queue.h [new file with mode: 0644]
cdschecker_modified_benchmarks/ms-queue-tsan11/Makefile [new file with mode: 0755]
cdschecker_modified_benchmarks/ms-queue-tsan11/main.cc [new file with mode: 0755]
cdschecker_modified_benchmarks/ms-queue-tsan11/main.o [new file with mode: 0644]
cdschecker_modified_benchmarks/ms-queue-tsan11/my_queue.cc [new file with mode: 0755]
cdschecker_modified_benchmarks/ms-queue-tsan11/my_queue.h [new file with mode: 0755]
cdschecker_modified_benchmarks/ms-queue-tsan11/my_queue.o [new file with mode: 0644]
cdschecker_modified_benchmarks/ms-queue/Makefile [new file with mode: 0644]
cdschecker_modified_benchmarks/ms-queue/main.cc [new file with mode: 0644]
cdschecker_modified_benchmarks/ms-queue/my_queue.c.correct [new file with mode: 0644]
cdschecker_modified_benchmarks/ms-queue/my_queue.cc [new file with mode: 0644]
cdschecker_modified_benchmarks/ms-queue/my_queue.h [new file with mode: 0644]
cdschecker_modified_benchmarks/spsc-queue/Makefile [new file with mode: 0644]
cdschecker_modified_benchmarks/spsc-queue/eventcount-relacy.h [new file with mode: 0644]
cdschecker_modified_benchmarks/spsc-queue/eventcount.h [new file with mode: 0644]
cdschecker_modified_benchmarks/spsc-queue/queue-relacy.h [new file with mode: 0644]
cdschecker_modified_benchmarks/spsc-queue/queue.h [new file with mode: 0644]
cdschecker_modified_benchmarks/spsc-queue/spsc-queue.cc [new file with mode: 0644]
cdschecker_modified_benchmarks/spsc-queue/spsc-relacy.cc [new file with mode: 0644]
cdschecker_modified_benchmarks/test.sh [new file with mode: 0755]
cdschecker_modified_benchmarks/test_all.sh [new file with mode: 0755]

diff --git a/cdschecker_modified_benchmarks/Makefile b/cdschecker_modified_benchmarks/Makefile
new file mode 100644 (file)
index 0000000..01dae3f
--- /dev/null
@@ -0,0 +1,7 @@
+DIRS = barrier chase-lev-deque dekker-fences linuxrwlocks mcs-lock mpmc-queue ms-queue spsc-queue
+
+all :
+       set -e; set -u; for d in $(DIRS); do (cd $$d; $(MAKE) ); done
+
+clean :
+       set -e; set -u; for d in $(DIRS); do (cd $$d; $(MAKE) clean ); done
diff --git a/cdschecker_modified_benchmarks/barrier/Makefile b/cdschecker_modified_benchmarks/barrier/Makefile
new file mode 100644 (file)
index 0000000..22df223
--- /dev/null
@@ -0,0 +1,11 @@
+include ../benchmarks.mk
+
+TESTNAME = barrier
+
+all: $(TESTNAME)
+
+$(TESTNAME): $(TESTNAME).cc $(TESTNAME).h
+       $(CXX) -o $@ $< $(CXXFLAGS) $(LDFLAGS)
+
+clean:
+       rm -f $(TESTNAME) *.o
diff --git a/cdschecker_modified_benchmarks/barrier/barrier.cc b/cdschecker_modified_benchmarks/barrier/barrier.cc
new file mode 100644 (file)
index 0000000..4d3c8ba
--- /dev/null
@@ -0,0 +1,43 @@
+#include <stdio.h>
+
+#include "cds_threads.h"
+
+#include "barrier.h"
+
+#include "librace.h"
+
+spinning_barrier *barr;
+int var = 0;
+
+void threadA(void *arg)
+{
+//     std::this_thread::sleep_for(std::chrono::milliseconds(10));
+       store_32(&var, 1);
+       barr->wait();
+}
+
+void threadB(void *arg)
+{
+//     std::this_thread::sleep_for(std::chrono::milliseconds(10));
+       barr->wait();
+       printf("var = %d\n", load_32(&var));
+}
+
+#define NUMREADERS 3
+int user_main(int argc, char **argv)
+{
+       std::thread A, B[NUMREADERS];
+       int i;
+
+       barr = new spinning_barrier(NUMREADERS + 1);
+
+       A = std::thread(threadA, (void *)NULL);
+       for (i = 0; i < NUMREADERS; i++)
+               B[i] = std::thread(threadB, (void *)NULL);
+
+       for (i = 0; i < NUMREADERS; i++)
+               B[i].join();
+       A.join();
+
+       return 0;
+}
diff --git a/cdschecker_modified_benchmarks/barrier/barrier.h b/cdschecker_modified_benchmarks/barrier/barrier.h
new file mode 100644 (file)
index 0000000..b52b849
--- /dev/null
@@ -0,0 +1,36 @@
+#include "cds_atomic.h"
+
+class spinning_barrier {
+ public:
+       spinning_barrier (unsigned int n) : n_ (n) {
+               nwait_ = 0;
+               step_ = 0;
+       }
+
+       bool wait() {
+               unsigned int step = step_.load ();
+
+               if (nwait_.fetch_add (1) == n_ - 1) {
+                       /* OK, last thread to come.  */
+                       nwait_.store (0); // XXX: maybe can use relaxed ordering here ??
+                       step_.fetch_add (1, std::memory_order_relaxed);
+                       return true;
+               } else {
+                       /* Run in circles and scream like a little girl.  */
+                       while (step_.load () == step)
+                               thrd_yield();
+                       return false;
+               }
+       }
+
+ protected:
+       /* Number of synchronized threads. */
+       const unsigned int n_;
+
+       /* Number of threads currently spinning.  */
+       std::atomic<unsigned int> nwait_;
+
+       /* Number of barrier syncronizations completed so far, 
+        *      * it's OK to wrap.  */
+       std::atomic<unsigned int> step_;
+};
diff --git a/cdschecker_modified_benchmarks/benchmarks.mk b/cdschecker_modified_benchmarks/benchmarks.mk
new file mode 100644 (file)
index 0000000..b103419
--- /dev/null
@@ -0,0 +1,10 @@
+# A few common Makefile items
+
+CC=../../clang
+CXX=../../clang++
+
+CXXFLAGS=-std=c++0x -pthread -Wall $(SANITIZE) -g -I../include
+
+UNAME = $(shell uname)
+
+
diff --git a/cdschecker_modified_benchmarks/chase-lev-deque/Makefile b/cdschecker_modified_benchmarks/chase-lev-deque/Makefile
new file mode 100644 (file)
index 0000000..73266a3
--- /dev/null
@@ -0,0 +1,17 @@
+include ../benchmarks.mk
+
+TESTNAME = chase-lev-deque
+
+HEADERS = deque.h
+OBJECTS = main.o deque.o
+
+all: $(TESTNAME)
+
+$(TESTNAME): $(HEADERS) $(OBJECTS)
+       $(CXX) -o $@ $(OBJECTS) $(CXXFLAGS) $(LDFLAGS)
+
+%.o: %.c
+       $(CXX) -c -o $@ $< $(CXXFLAGS)
+
+clean:
+       rm -f $(TESTNAME) *.o
diff --git a/cdschecker_modified_benchmarks/chase-lev-deque/deque.cc b/cdschecker_modified_benchmarks/chase-lev-deque/deque.cc
new file mode 100644 (file)
index 0000000..feb3fc9
--- /dev/null
@@ -0,0 +1,85 @@
+#include "cds_atomic.h"
+#include <inttypes.h>
+#include "deque.h"
+#include <stdlib.h>
+#include <stdio.h>
+
+Deque * create() {
+       Deque * q = (Deque *) calloc(1, sizeof(Deque));
+       Array * a = (Array *) calloc(1, sizeof(Array)+2*sizeof(atomic_int));
+       atomic_store_explicit(&q->array, (uintptr_t)a, memory_order_relaxed);
+       atomic_store_explicit(&q->top, 0, memory_order_relaxed);
+       atomic_store_explicit(&q->bottom, 0, memory_order_relaxed);
+       atomic_store_explicit(&a->size, 2, memory_order_relaxed);
+       return q;
+}
+
+int take(Deque *q) {
+       size_t b = atomic_load_explicit(&q->bottom, memory_order_relaxed) - 1;
+       Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);
+       atomic_store_explicit(&q->bottom, b, memory_order_relaxed);
+       atomic_thread_fence(memory_order_seq_cst);
+       size_t t = atomic_load_explicit(&q->top, memory_order_relaxed);
+       int x;
+       if (t <= b) {
+               /* Non-empty queue. */
+               x = atomic_load_explicit(&a->buffer[b % atomic_load_explicit(&a->size,memory_order_relaxed)], memory_order_relaxed);
+               if (t == b) {
+                       /* Single last element in queue. */
+                       if (!atomic_compare_exchange_strong_explicit(&q->top, &t, t + 1, memory_order_seq_cst, memory_order_relaxed))
+                               /* Failed race. */
+                               x = EMPTY;
+                       atomic_store_explicit(&q->bottom, b + 1, memory_order_relaxed);
+               }
+       } else { /* Empty queue. */
+               x = EMPTY;
+               atomic_store_explicit(&q->bottom, b + 1, memory_order_relaxed);
+       }
+       return x;
+}
+
+void resize(Deque *q) {
+       Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);
+       size_t size=atomic_load_explicit(&a->size, memory_order_relaxed);
+       size_t new_size=size << 1;
+       Array *new_a = (Array *) calloc(1, new_size * sizeof(atomic_int) + sizeof(Array));
+       size_t top=atomic_load_explicit(&q->top, memory_order_relaxed);
+       size_t bottom=atomic_load_explicit(&q->bottom, memory_order_relaxed);
+       atomic_store_explicit(&new_a->size, new_size, memory_order_relaxed);
+       size_t i;
+       for(i=top; i < bottom; i++) {
+               atomic_store_explicit(&new_a->buffer[i % new_size], atomic_load_explicit(&a->buffer[i % size], memory_order_relaxed), memory_order_relaxed);
+       }
+       atomic_store_explicit(&q->array, (uintptr_t)new_a, memory_order_relaxed);
+       printf("resize\n");
+}
+
+void push(Deque *q, int x) {
+       size_t b = atomic_load_explicit(&q->bottom, memory_order_relaxed);
+       size_t t = atomic_load_explicit(&q->top, memory_order_acquire);
+       Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);
+       if (b - t > atomic_load_explicit(&a->size, memory_order_relaxed) - 1) /* Full queue. */ {
+               resize(q);
+               //Bug in paper...should have next line...
+               a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);
+       }
+       atomic_store_explicit(&a->buffer[b % atomic_load_explicit(&a->size, memory_order_relaxed)], x, memory_order_relaxed);
+       atomic_thread_fence(memory_order_release);
+       atomic_store_explicit(&q->bottom, b + 1, memory_order_relaxed);
+}
+
+int steal(Deque *q) {
+       size_t t = atomic_load_explicit(&q->top, memory_order_acquire);
+       atomic_thread_fence(memory_order_seq_cst);
+       size_t b = atomic_load_explicit(&q->bottom, memory_order_acquire);
+       int x = EMPTY;
+       if (t < b) {
+               /* Non-empty queue. */
+               Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);
+               x = atomic_load_explicit(&a->buffer[t % atomic_load_explicit(&a->size, memory_order_relaxed)], memory_order_relaxed);
+               if (!atomic_compare_exchange_strong_explicit(&q->top, &t, t + 1, memory_order_seq_cst, memory_order_relaxed))
+                       /* Failed race. */
+                       return ABORT;
+       }
+       return x;
+}
diff --git a/cdschecker_modified_benchmarks/chase-lev-deque/deque.h b/cdschecker_modified_benchmarks/chase-lev-deque/deque.h
new file mode 100644 (file)
index 0000000..c65da6f
--- /dev/null
@@ -0,0 +1,25 @@
+#ifndef DEQUE_H
+#define DEQUE_H
+
+#include "cds_atomic.h"
+
+typedef struct {
+       atomic_size_t size;
+       atomic_int buffer[];
+} Array;
+
+typedef struct {
+       atomic_size_t top, bottom;
+       atomic_uintptr_t array; /* Atomic(Array *) */
+} Deque;
+
+Deque * create();
+int take(Deque *q);
+int steal(Deque *q);
+void resize(Deque *q);
+void push(Deque *q, int x);
+
+#define EMPTY 0xffffffff
+#define ABORT 0xfffffffe
+
+#endif
diff --git a/cdschecker_modified_benchmarks/chase-lev-deque/main.cc b/cdschecker_modified_benchmarks/chase-lev-deque/main.cc
new file mode 100644 (file)
index 0000000..706d812
--- /dev/null
@@ -0,0 +1,52 @@
+#include <stdlib.h>
+#include <assert.h>
+#include <stdio.h>
+#include "cds_threads.h"
+//#include <atomic>
+
+#include "model-assert.h"
+
+#include "deque.h"
+
+#define ITERATION 1
+
+Deque *q;
+int a;
+int b;
+int c;
+
+static void task(void * param) {
+       for (int i = 0; i < ITERATION; i++)
+               a=steal(q);
+}
+
+int user_main(int argc, char **argv)
+{
+       q=create();
+       std::thread t(task, (void *)0);
+
+       for (int i = 0; i < ITERATION; i++) {
+               push(q, 1);
+               push(q, 2);
+               push(q, 4);
+               b=take(q);
+               c=take(q);
+       }
+
+       t.join();
+
+       bool correct=true;
+       if (a!=1 && a!=2 && a!=4 && a!= EMPTY)
+               correct=false;
+       if (b!=1 && b!=2 && b!=4 && b!= EMPTY)
+               correct=false;
+       if (c!=1 && c!=2 && c!=4 && a!= EMPTY)
+               correct=false;
+       if (a!=EMPTY && b!=EMPTY && c!=EMPTY && (a+b+c)!=7)
+               correct=false;
+       if (!correct)
+               printf("a=%d b=%d c=%d\n",a,b,c);
+       MODEL_ASSERT(correct);
+
+       return 0;
+}
diff --git a/cdschecker_modified_benchmarks/dekker-fences/Makefile b/cdschecker_modified_benchmarks/dekker-fences/Makefile
new file mode 100644 (file)
index 0000000..ffbb77a
--- /dev/null
@@ -0,0 +1,11 @@
+include ../benchmarks.mk
+
+TESTNAME = dekker-fences
+
+all: $(TESTNAME)
+
+$(TESTNAME): $(TESTNAME).cc
+       $(CXX) -o $@ $< $(CXXFLAGS) $(LDFLAGS)
+
+clean:
+       rm -f $(TESTNAME) *.o
diff --git a/cdschecker_modified_benchmarks/dekker-fences/dekker-fences.cc b/cdschecker_modified_benchmarks/dekker-fences/dekker-fences.cc
new file mode 100644 (file)
index 0000000..30a3633
--- /dev/null
@@ -0,0 +1,95 @@
+/*
+ * Dekker's critical section algorithm, implemented with fences.
+ *
+ * URL:
+ *   http://www.justsoftwaresolutions.co.uk/threading/
+ */
+
+
+#include "cds_threads.h"
+//#include "cds_atomic.h"
+#include <atomic>
+
+#include "librace.h"
+
+std::atomic<bool> flag0, flag1;
+std::atomic<int> turn;
+
+uint32_t var = 0;
+
+void p0()
+{
+//     std::this_thread::sleep_for(std::chrono::milliseconds(10));
+
+       flag0.store(true,std::memory_order_relaxed);
+       //std::atomic_thread_fence(std::memory_order_seq_cst);
+
+       while (flag1.load(std::memory_order_relaxed))
+       {
+               if (turn.load(std::memory_order_relaxed) != 0)
+               {
+                       flag0.store(false,std::memory_order_relaxed);
+                       while (turn.load(std::memory_order_relaxed) != 0)
+                       {
+                               thrd_yield();
+                       }
+                       flag0.store(true,std::memory_order_relaxed);
+                       std::atomic_thread_fence(std::memory_order_seq_cst);
+               } else
+                       thrd_yield();
+       }
+       std::atomic_thread_fence(std::memory_order_acquire);
+
+       // critical section
+       store_32(&var, 1);
+
+       turn.store(1,std::memory_order_relaxed);
+       std::atomic_thread_fence(std::memory_order_release);
+       flag0.store(false,std::memory_order_relaxed);
+}
+
+void p1()
+{
+//     std::this_thread::sleep_for(std::chrono::milliseconds(10));
+
+       flag1.store(true,std::memory_order_relaxed);
+       std::atomic_thread_fence(std::memory_order_seq_cst);
+
+       while (flag0.load(std::memory_order_relaxed))
+       {
+               if (turn.load(std::memory_order_relaxed) != 1)
+               {
+                       flag1.store(false,std::memory_order_relaxed);
+                       while (turn.load(std::memory_order_relaxed) != 1)
+                       {
+                               thrd_yield();
+                       }
+                       flag1.store(true,std::memory_order_relaxed);
+                       std::atomic_thread_fence(std::memory_order_seq_cst);
+               } else
+                       thrd_yield();
+       }
+       std::atomic_thread_fence(std::memory_order_acquire);
+
+       // critical section
+       store_32(&var, 2);
+
+       turn.store(0,std::memory_order_relaxed);
+       std::atomic_thread_fence(std::memory_order_release);
+       flag1.store(false,std::memory_order_relaxed);
+}
+
+int user_main(int argc, char **argv)
+{
+       flag0 = false;
+       flag1 = false;
+       turn = 0;
+
+       std::thread a(p0);
+       std::thread b(p1);
+
+       a.join();
+       b.join();
+
+       return 0;
+}
diff --git a/cdschecker_modified_benchmarks/include/cds_atomic.h b/cdschecker_modified_benchmarks/include/cds_atomic.h
new file mode 100755 (executable)
index 0000000..aa71b59
--- /dev/null
@@ -0,0 +1,52 @@
+#ifndef __STDATOMIC_H__
+#define __STDATOMIC_H__
+
+#ifdef __cplusplus
+
+#include <atomic>
+
+using std::atomic_flag;
+using std::atomic_bool;
+//using std::atomic_address;
+using std::atomic_char;
+using std::atomic_schar;
+using std::atomic_uchar;
+using std::atomic_short;
+using std::atomic_ushort;
+using std::atomic_int;
+using std::atomic_uint;
+using std::atomic_long;
+using std::atomic_ulong;
+using std::atomic_llong;
+using std::atomic_ullong;
+using std::atomic_wchar_t;
+
+using std::atomic_size_t;
+using std::atomic_uintptr_t;
+
+using std::atomic;
+using std::memory_order;
+using std::memory_order_relaxed;
+using std::memory_order_acquire;
+using std::memory_order_release;
+using std::memory_order_acq_rel;
+using std::memory_order_seq_cst;
+
+using std::atomic_thread_fence;
+using std::atomic_signal_fence;
+
+using std::atomic_init;
+
+#define atomic_init(A, V) *A=V
+
+#define atomic_load_explicit(A, MO) (*A).load(MO)
+#define atomic_store_explicit(A, V, MO) (*A).store(V, MO)
+
+#define atomic_fetch_add_explicit(A, V, MO) (*A).fetch_add(V, MO);
+#define atomic_fetch_sub_explicit(A, V, MO) (*A).fetch_sub(V, MO);
+#define atomic_compare_exchange_strong_explicit(A, E, V, MO, FMO) \
+    (*A).compare_exchange_strong(*E, V, MO, FMO)
+
+#endif
+
+#endif  // __STDATOMIC_H__
diff --git a/cdschecker_modified_benchmarks/include/cds_threads.h b/cdschecker_modified_benchmarks/include/cds_threads.h
new file mode 100755 (executable)
index 0000000..5b13720
--- /dev/null
@@ -0,0 +1,38 @@
+// Header to handle CDSChecker bullshit.
+// Handles most things, not just threads:
+//  - Catches C11 threads and forwards to C++11 threads.
+//  - Catches store_n and load_n and turns them into normal stores/loads.
+//  - Replaces user_main with just main.
+
+#ifndef __THREADS_H__
+#define __THREADS_H__
+
+#ifdef __cplusplus
+#include <thread>
+
+#include <map>
+#include <string>
+#include <cassert>
+
+#define thrd_t std::thread
+typedef int (*thrd_start_t)(void *); 
+
+static std::map<std::string, std::thread> thrs;
+
+#define thrd_create(T, F, A) new_thread(#T, F, A)
+static void new_thread(const char *t, thrd_start_t f, void *args) {
+  assert(thrs.emplace(std::string(++t), std::thread(*f, args)).second);
+}
+
+#define thrd_join(T) end_thread(#T)
+static void end_thread(const char *t) {
+  thrs[std::string(t)].join();
+}
+
+#define thrd_yield() std::this_thread::yield()
+
+#define user_main main
+
+#endif
+
+#endif  // __THREADS_H__
diff --git a/cdschecker_modified_benchmarks/include/librace.h b/cdschecker_modified_benchmarks/include/librace.h
new file mode 100755 (executable)
index 0000000..2445139
--- /dev/null
@@ -0,0 +1,29 @@
+#ifndef __LIBRACE_H__
+#define __LIBRACE_H__
+
+#include <stdint.h>
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+       void store_8(void *addr, uint8_t val) { *((uint8_t *)addr) = val; }
+       void store_16(void *addr, uint16_t val) { *((uint16_t *)addr) = val; }
+       void store_32(void *addr, uint32_t val) { *((uint32_t *)addr) = val; }
+       void store_64(void *addr, uint64_t val) { *((uint64_t *)addr) = val; }
+
+       void store_8_(void *addr);
+       void store_16_(void *addr);
+       void store_32_(void *addr);
+       void store_64_(void *addr);
+
+       uint8_t load_8(const void *addr) { return *((uint8_t *)addr); }
+       uint16_t load_16(const void *addr) { return *((uint16_t *)addr); }
+       uint32_t load_32(const void *addr) { return *((uint32_t *)addr); }
+       uint64_t load_64(const void *addr) { return *((uint64_t *)addr); }
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif  // __LIBRACE_H__
diff --git a/cdschecker_modified_benchmarks/include/model-assert.h b/cdschecker_modified_benchmarks/include/model-assert.h
new file mode 100755 (executable)
index 0000000..5cba524
--- /dev/null
@@ -0,0 +1,21 @@
+#ifndef __MODEL_ASSERT_H__
+#define __MODEL_ASSERT_H__
+
+#if __cplusplus
+extern "C" {
+#else
+#include <stdbool.h>
+#endif
+
+#include <cassert>
+
+static void model_assert(bool expr, const char *file, int line) {
+  assert(expr && file && line);
+}
+#define MODEL_ASSERT(expr) model_assert((expr), __FILE__, __LINE__)
+
+#if __cplusplus
+}
+#endif
+
+#endif /* __MODEL_ASSERT_H__ */
diff --git a/cdschecker_modified_benchmarks/include/unrelacy.h b/cdschecker_modified_benchmarks/include/unrelacy.h
new file mode 100755 (executable)
index 0000000..555ec9b
--- /dev/null
@@ -0,0 +1,96 @@
+#ifndef __UNRELACY_H__
+#define __UNRELACY_H__
+
+#include <atomic>
+#include <stdlib.h>
+#include <stdio.h>
+#include <mutex>
+#include <condition_variable>
+
+#include <model-assert.h>
+#include <librace.h>
+
+#define $
+
+#define ASSERT(expr) MODEL_ASSERT(expr)
+#define RL_ASSERT(expr) MODEL_ASSERT(expr)
+
+#define RL_NEW new
+#define RL_DELETE(expr) delete expr
+
+#define mo_seqcst memory_order_relaxed
+#define mo_release memory_order_release
+#define mo_acquire memory_order_acquire
+#define mo_acq_rel memory_order_acq_rel
+#define mo_relaxed memory_order_relaxed
+
+namespace rl {
+
+       /* This 'useless' struct is declared just so we can use partial template
+        * specialization in our store and load functions. */
+       template <typename T, size_t n>
+       struct useless {
+               static void store(void *addr, T val);
+               static T load(const void *addr);
+       };
+
+       template <typename T>
+       struct useless<T, 1> {
+               static void store(void *addr, T val) { store_8(addr, (uint8_t)val); }
+               static T load(const void *addr) { return (T)load_8(addr); }
+       };
+
+       template <typename T>
+       struct useless<T, 2> {
+               static void store(void *addr, T val) { store_16(addr, (uint16_t)val); }
+               static T load(const void *addr) { return (T)load_16(addr); }
+       };
+
+       template <typename T>
+       struct useless<T, 4> {
+               static void store(void *addr, T val) { store_32(addr, (uint32_t)val); }
+               static T load(const void *addr) { return (T)load_32(addr); }
+       };
+
+       template <typename T>
+       struct useless<T, 8> {
+               static void store(void *addr, T val) { store_64(addr, (uint64_t)val); }
+               static T load(const void *addr) { return (T)load_64(addr); }
+       };
+
+       template <typename T>
+       struct var {
+               var() { useless<T, sizeof(T)>::store(&value, 0); }
+               var(T v) { useless<T, sizeof(T)>::store(&value, v); }
+               var(var const& r) {
+                       value = r.value;
+               }
+               ~var() { }
+
+               void operator = (T v) { useless<T, sizeof(T)>::store(&value, v); }
+               T operator () () { return useless<T, sizeof(T)>::load(&value); }
+               void operator += (T v) {
+                       useless<T, sizeof(T)>::store(&value,
+                                       useless<T, sizeof(T)>::load(&value) + v);
+               }
+               bool operator == (const struct var<T> v) const { return useless<T, sizeof(T)>::load(&value) == useless<T, sizeof(T)>::load(&v.value); }
+
+               T value;
+       };
+
+       class backoff_t
+       {
+        public:
+               typedef int debug_info_param;
+               void yield(debug_info_param info) { }
+               void yield() { }
+       };
+
+
+       typedef backoff_t backoff;
+       typedef backoff_t linear_backoff;
+       typedef backoff_t exp_backoff;
+
+}
+
+#endif /* __UNRELACY_H__ */
diff --git a/cdschecker_modified_benchmarks/linuxrwlocks/Makefile b/cdschecker_modified_benchmarks/linuxrwlocks/Makefile
new file mode 100644 (file)
index 0000000..b0c4612
--- /dev/null
@@ -0,0 +1,11 @@
+include ../benchmarks.mk
+
+TESTNAME = linuxrwlocks
+
+all: $(TESTNAME)
+
+$(TESTNAME): $(TESTNAME).cc
+       $(CXX) -o $@ $< $(CXXFLAGS) $(LDFLAGS)
+
+clean:
+       rm -f $(TESTNAME) *.o
diff --git a/cdschecker_modified_benchmarks/linuxrwlocks/linuxrwlocks.cc b/cdschecker_modified_benchmarks/linuxrwlocks/linuxrwlocks.cc
new file mode 100644 (file)
index 0000000..73e3a68
--- /dev/null
@@ -0,0 +1,118 @@
+#include <stdio.h>
+#include "cds_threads.h"
+#include "cds_atomic.h"
+
+#include "librace.h"
+
+#define RW_LOCK_BIAS            0x00100000
+#define WRITE_LOCK_CMP          RW_LOCK_BIAS
+
+/** Example implementation of linux rw lock along with 2 thread test
+ *  driver... */
+
+typedef union {
+       atomic_int lock;
+} rwlock_t;
+
+static inline int read_can_lock(rwlock_t *lock)
+{
+       return atomic_load_explicit(&lock->lock, memory_order_relaxed) > 0;
+}
+
+static inline int write_can_lock(rwlock_t *lock)
+{
+       return atomic_load_explicit(&lock->lock, memory_order_relaxed) == RW_LOCK_BIAS;
+}
+
+static inline void read_lock(rwlock_t *rw)
+{
+       int priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
+       while (priorvalue <= 0) {
+               atomic_fetch_add_explicit(&rw->lock, 1, memory_order_relaxed);
+               while (atomic_load_explicit(&rw->lock, memory_order_relaxed) <= 0) {
+                       thrd_yield();
+               }
+               priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_relaxed);
+       }
+}
+
+static inline void write_lock(rwlock_t *rw)
+{
+       int priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
+       while (priorvalue != RW_LOCK_BIAS) {
+               atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_relaxed);
+               while (atomic_load_explicit(&rw->lock, memory_order_relaxed) != RW_LOCK_BIAS) {
+                       thrd_yield();
+               }
+               priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_relaxed);
+       }
+}
+
+static inline int read_trylock(rwlock_t *rw)
+{
+       int priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
+       if (priorvalue > 0)
+               return 1;
+
+       atomic_fetch_add_explicit(&rw->lock, 1, memory_order_relaxed);
+       return 0;
+}
+
+static inline int write_trylock(rwlock_t *rw)
+{
+       int priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
+       if (priorvalue == RW_LOCK_BIAS)
+               return 1;
+
+       atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_relaxed);
+       return 0;
+}
+
+static inline void read_unlock(rwlock_t *rw)
+{
+       atomic_fetch_add_explicit(&rw->lock, 1, memory_order_release);
+}
+
+static inline void write_unlock(rwlock_t *rw)
+{
+       atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_release);
+}
+
+rwlock_t mylock;
+int shareddata;
+
+void a()
+{
+//     std::this_thread::sleep_for(std::chrono::milliseconds(10));
+       int i, rs;
+       for(i = 0; i < 2; i++) {
+               if ((i % 2) == 0) {
+                       read_lock(&mylock);
+                       rs = load_32(&shareddata);
+                       read_unlock(&mylock);
+               } else {
+                       write_lock(&mylock);
+                       std::this_thread::yield();
+                       store_32(&shareddata,(unsigned int)i);
+                       write_unlock(&mylock);
+               }
+       }
+}
+
+int user_main(int argc, char **argv)
+{
+       //thrd_t t1, t2;
+       atomic_init(&mylock.lock, RW_LOCK_BIAS);
+
+       std::thread t1(a);
+       std::thread t2(a);
+       //thrd_create(&t1, (thrd_start_t)&a, NULL);
+       //thrd_create(&t2, (thrd_start_t)&a, NULL);
+
+       t1.join();
+       t2.join();
+       //thrd_join(t1);
+       //thrd_join(t2);
+
+       return 0;
+}
diff --git a/cdschecker_modified_benchmarks/mcs-lock/Makefile b/cdschecker_modified_benchmarks/mcs-lock/Makefile
new file mode 100644 (file)
index 0000000..5a311b3
--- /dev/null
@@ -0,0 +1,11 @@
+include ../benchmarks.mk
+
+TESTNAME = mcs-lock
+
+all: $(TESTNAME)
+
+$(TESTNAME): $(TESTNAME).cc $(TESTNAME).h
+       $(CXX) -o $@ $< $(CXXFLAGS) $(LDFLAGS)
+
+clean:
+       rm -f $(TESTNAME) *.o
diff --git a/cdschecker_modified_benchmarks/mcs-lock/mcs-lock.cc b/cdschecker_modified_benchmarks/mcs-lock/mcs-lock.cc
new file mode 100644 (file)
index 0000000..4fc4f0f
--- /dev/null
@@ -0,0 +1,43 @@
+#include <stdio.h>
+#include "cds_threads.h"
+
+#include "mcs-lock.h"
+
+/* For data race instrumentation */
+#include "librace.h"
+
+struct mcs_mutex *mutex;
+static uint32_t shared;
+
+void threadA(void *arg)
+{
+//     std::this_thread::sleep_for(std::chrono::milliseconds(10));
+       mcs_mutex::guard g(mutex);
+       printf("store: %d\n", 17);
+       store_32(&shared, 17);
+       mutex->unlock(&g);
+       mutex->lock(&g);
+       printf("load: %u\n", load_32(&shared));
+}
+
+void threadB(void *arg)
+{
+//     std::this_thread::sleep_for(std::chrono::milliseconds(10));
+       mcs_mutex::guard g(mutex);
+       printf("load: %u\n", load_32(&shared));
+       mutex->unlock(&g);
+       mutex->lock(&g);
+       printf("store: %d\n", 17);
+       store_32(&shared, 17);
+}
+
+int user_main(int argc, char **argv)
+{
+       mutex = new mcs_mutex();
+
+       std::thread A(threadA, (void *)NULL);
+       std::thread B(threadB, (void *)NULL);
+       A.join();
+       B.join();
+       return 0;
+}
diff --git a/cdschecker_modified_benchmarks/mcs-lock/mcs-lock.h b/cdschecker_modified_benchmarks/mcs-lock/mcs-lock.h
new file mode 100644 (file)
index 0000000..d54e19b
--- /dev/null
@@ -0,0 +1,93 @@
+// mcs on stack
+
+#include <atomic>
+#include <unrelacy.h>
+
+struct mcs_node {
+       std::atomic<mcs_node *> next;
+       std::atomic<int> gate;
+
+       mcs_node() {
+               next.store(0);
+               gate.store(0);
+       }
+};
+
+struct mcs_mutex {
+public:
+       // tail is null when lock is not held
+       std::atomic<mcs_node *> m_tail;
+
+       mcs_mutex() {
+               m_tail.store( NULL );
+       }
+       ~mcs_mutex() {
+               ASSERT( m_tail.load() == NULL );
+       }
+
+       class guard {
+       public:
+               mcs_mutex * m_t;
+               mcs_node    m_node; // node held on the stack
+
+               guard(mcs_mutex * t) : m_t(t) { t->lock(this); }
+               ~guard() { m_t->unlock(this); }
+       };
+
+       void lock(guard * I) {
+               mcs_node * me = &(I->m_node);
+
+               // set up my node :
+               // not published yet so relaxed :
+               me->next.store(NULL, std::mo_relaxed );
+               me->gate.store(1, std::mo_relaxed );
+
+               // publish my node as the new tail :
+               mcs_node * pred = m_tail.exchange(me, std::mo_acq_rel);
+               if ( pred != NULL ) {
+                       // (*1) race here
+                       // unlock of pred can see me in the tail before I fill next
+
+                       // publish me to previous lock-holder :
+                       pred->next.store(me, std::mo_release );
+
+                       // (*2) pred not touched any more       
+
+                       // now this is the spin -
+                       // wait on predecessor setting my flag -
+                       rl::linear_backoff bo;
+                       while ( me->gate.load(std::mo_relaxed) ) {
+                               thrd_yield();
+                       }
+               }
+       }
+
+       void unlock(guard * I) {
+               mcs_node * me = &(I->m_node);
+
+               mcs_node * next = me->next.load(std::mo_acquire);
+               if ( next == NULL )
+               {
+                       mcs_node * tail_was_me = me;
+                       if ( m_tail.compare_exchange_strong( tail_was_me,NULL,std::mo_acq_rel) ) {
+                               // got null in tail, mutex is unlocked
+                               return;
+                       }
+
+                       // (*1) catch the race :
+                       rl::linear_backoff bo;
+                       for(;;) {
+                               next = me->next.load(std::mo_relaxed);
+                               if ( next != NULL )
+                                       break;
+                               thrd_yield();
+                       }
+               }
+
+               // (*2) - store to next must be done,
+               //  so no locker can be viewing my node any more        
+
+               // let next guy in :
+               next->gate.store( 0, std::mo_release );
+       }
+};
diff --git a/cdschecker_modified_benchmarks/mpmc-queue/Makefile b/cdschecker_modified_benchmarks/mpmc-queue/Makefile
new file mode 100644 (file)
index 0000000..560074f
--- /dev/null
@@ -0,0 +1,24 @@
+include ../benchmarks.mk
+
+TESTNAME = mpmc-queue
+#TESTS = mpmc-queue mpmc-1r2w mpmc-2r1w mpmc-queue-rdwr
+#TESTS += mpmc-queue-noinit mpmc-1r2w-noinit mpmc-2r1w-noinit mpmc-rdwr-noinit
+TESTS = mpmc-queue
+
+all: $(TESTS)
+
+#mpmc-queue: CPPFLAGS += -DCONFIG_MPMC_READERS=2 -DCONFIG_MPMC_WRITERS=2
+mpmc-queue: CXXFLAGS += -DCONFIG_MPMC_READERS=0 -DCONFIG_MPMC_WRITERS=0 -DCONFIG_MPMC_RDWR=2
+mpmc-queue-rdwr: CPPFLAGS += -DCONFIG_MPMC_READERS=0 -DCONFIG_MPMC_WRITERS=0 -DCONFIG_MPMC_RDWR=2
+mpmc-1r2w: CPPFLAGS += -DCONFIG_MPMC_READERS=1 -DCONFIG_MPMC_WRITERS=2
+mpmc-2r1w: CPPFLAGS += -DCONFIG_MPMC_READERS=2 -DCONFIG_MPMC_WRITERS=1
+mpmc-queue-noinit: CPPFLAGS += -DCONFIG_MPMC_READERS=2 -DCONFIG_MPMC_WRITERS=2 -DCONFIG_MPMC_NO_INITIAL_ELEMENT
+mpmc-1r2w-noinit: CPPFLAGS += -DCONFIG_MPMC_READERS=1 -DCONFIG_MPMC_WRITERS=2 -DCONFIG_MPMC_NO_INITIAL_ELEMENT
+mpmc-2r1w-noinit: CPPFLAGS += -DCONFIG_MPMC_READERS=2 -DCONFIG_MPMC_WRITERS=1 -DCONFIG_MPMC_NO_INITIAL_ELEMENT
+mpmc-rdwr-noinit: CPPFLAGS += -DCONFIG_MPMC_READERS=0 -DCONFIG_MPMC_WRITERS=0 -DCONFIG_MPMC_RDWR=2 -DCONFIG_MPMC_NO_INITIAL_ELEMENT
+
+$(TESTS): $(TESTNAME).cc $(TESTNAME).h
+       $(CXX) -o $@ $< $(CXXFLAGS) $(LDFLAGS)
+
+clean:
+       rm -f $(TESTS) *.o
diff --git a/cdschecker_modified_benchmarks/mpmc-queue/mpmc-queue.cc b/cdschecker_modified_benchmarks/mpmc-queue/mpmc-queue.cc
new file mode 100644 (file)
index 0000000..038fac3
--- /dev/null
@@ -0,0 +1,143 @@
+#include <inttypes.h>
+#include "cds_threads.h"
+#include <stdio.h>
+#include <unistd.h>
+#include <stdlib.h>
+
+#include <librace.h>
+
+#include "mpmc-queue.h"
+
+void threadA(struct mpmc_boundq_1_alt<int32_t, sizeof(int32_t)> *queue)
+{
+//     std::this_thread::sleep_for(std::chrono::milliseconds(10));
+       int32_t *bin = queue->write_prepare();
+       store_32(bin, 1);
+       queue->write_publish();
+}
+
+void threadB(struct mpmc_boundq_1_alt<int32_t, sizeof(int32_t)> *queue)
+{
+//     std::this_thread::sleep_for(std::chrono::milliseconds(10));
+       int32_t *bin;
+       while ((bin = queue->read_fetch()) != NULL) {
+               printf("Read: %d\n", load_32(bin));
+               queue->read_consume();
+       }
+}
+
+void threadC(struct mpmc_boundq_1_alt<int32_t, sizeof(int32_t)> *queue)
+{
+//     std::this_thread::sleep_for(std::chrono::milliseconds(10));
+       int32_t *bin = queue->write_prepare();
+       store_32(bin, 1);
+       queue->write_publish();
+
+       while ((bin = queue->read_fetch()) != NULL) {
+               printf("Read: %d\n", load_32(bin));
+               queue->read_consume();
+       }
+}
+
+#define MAXREADERS 3
+#define MAXWRITERS 3
+#define MAXRDWR 3
+
+#ifdef CONFIG_MPMC_READERS
+#define DEFAULT_READERS (CONFIG_MPMC_READERS)
+#else
+#define DEFAULT_READERS 2
+#endif
+
+#ifdef CONFIG_MPMC_WRITERS
+#define DEFAULT_WRITERS (CONFIG_MPMC_WRITERS)
+#else
+#define DEFAULT_WRITERS 2
+#endif
+
+#ifdef CONFIG_MPMC_RDWR
+#define DEFAULT_RDWR (CONFIG_MPMC_RDWR)
+#else
+#define DEFAULT_RDWR 0
+#endif
+
+int readers = DEFAULT_READERS, writers = DEFAULT_WRITERS, rdwr = DEFAULT_RDWR;
+
+void print_usage()
+{
+       printf("Error: use the following options\n"
+               " -r <num>              Choose number of reader threads\n"
+               " -w <num>              Choose number of writer threads\n");
+       exit(EXIT_FAILURE);
+}
+
+void process_params(int argc, char **argv)
+{
+       const char *shortopts = "hr:w:";
+       int opt;
+       bool error = false;
+
+       while (!error && (opt = getopt(argc, argv, shortopts)) != -1) {
+               switch (opt) {
+               case 'h':
+                       print_usage();
+                       break;
+               case 'r':
+                       readers = atoi(optarg);
+                       break;
+               case 'w':
+                       writers = atoi(optarg);
+                       break;
+               default: /* '?' */
+                       error = true;
+                       break;
+               }
+       }
+
+       if (writers < 1 || writers > MAXWRITERS)
+               error = true;
+       if (readers < 1 || readers > MAXREADERS)
+               error = true;
+
+       if (error)
+               print_usage();
+}
+
+int user_main(int argc, char **argv)
+{
+       struct mpmc_boundq_1_alt<int32_t, sizeof(int32_t)> queue;
+       std::thread A[MAXWRITERS], B[MAXREADERS], C[MAXRDWR];
+
+       /* Note: optarg() / optind is broken in model-checker - workaround is
+        * to just copy&paste this test a few times */
+       //process_params(argc, argv);
+       printf("%d reader(s), %d writer(s)\n", readers, writers);
+
+#ifndef CONFIG_MPMC_NO_INITIAL_ELEMENT
+       printf("Adding initial element\n");
+       int32_t *bin = queue.write_prepare();
+       store_32(bin, 17);
+       queue.write_publish();
+#endif
+
+       printf("Start threads\n");
+
+       for (int i = 0; i < writers; i++)
+               A[i] = std::thread(threadA, &queue);
+       for (int i = 0; i < readers; i++)
+               B[i] = std::thread(threadB, &queue);
+
+       for (int i = 0; i < rdwr; i++)
+               C[i] = std::thread(threadC, &queue);
+
+       for (int i = 0; i < writers; i++)
+               A[i].join();
+       for (int i = 0; i < readers; i++)
+               B[i].join();
+       for (int i = 0; i < rdwr; i++)
+               C[i].join();
+
+       printf("Threads complete\n");
+
+       return 0;
+}
diff --git a/cdschecker_modified_benchmarks/mpmc-queue/mpmc-queue.h b/cdschecker_modified_benchmarks/mpmc-queue/mpmc-queue.h
new file mode 100644 (file)
index 0000000..f86bec4
--- /dev/null
@@ -0,0 +1,97 @@
+#include "cds_atomic.h"
+#include <unrelacy.h>
+
+template <typename t_element, size_t t_size>
+struct mpmc_boundq_1_alt
+{
+private:
+
+       // elements should generally be cache-line-size padded :
+       t_element               m_array[t_size];
+
+       // rdwr counts the reads & writes that have started
+       atomic<unsigned int>    m_rdwr;
+       // "read" and "written" count the number completed
+       atomic<unsigned int>    m_read;
+       atomic<unsigned int>    m_written;
+
+public:
+
+       mpmc_boundq_1_alt()
+       {
+               m_rdwr = 0;
+               m_read = 0;
+               m_written = 0;
+       }
+
+       //-----------------------------------------------------
+
+       t_element * read_fetch() {
+               unsigned int rdwr = m_rdwr.load(mo_acquire);
+               unsigned int rd,wr;
+               for(;;) {
+                       rd = (rdwr>>16) & 0xFFFF;
+                       wr = rdwr & 0xFFFF;
+
+                       if ( wr == rd ) // empty
+                               return NULL;
+
+                       if ( m_rdwr.compare_exchange_weak(rdwr,rdwr+(1<<16),mo_acquire) )
+                               break;
+                       else
+                               thrd_yield();
+               }
+
+               // (*1)
+               rl::backoff bo;
+               while ( (m_written.load(mo_acquire) & 0xFFFF) != wr ) {
+                       thrd_yield();
+               }
+
+               t_element * p = & ( m_array[ rd % t_size ] );
+
+               return p;
+       }
+
+       void read_consume() {
+               m_read.fetch_add(1,mo_release);
+       }
+
+       //-----------------------------------------------------
+
+       t_element * write_prepare() {
+               unsigned int rdwr = m_rdwr.load(mo_acquire);
+               unsigned int rd,wr;
+               for(;;) {
+                       rd = (rdwr>>16) & 0xFFFF;
+                       wr = rdwr & 0xFFFF;
+
+                       if ( wr == ((rd + t_size)&0xFFFF) ) // full
+                               return NULL;
+
+                       if ( m_rdwr.compare_exchange_weak(rdwr,(rd<<16) | ((wr+1)&0xFFFF),mo_acq_rel) )
+                               break;
+                       else
+                               thrd_yield();
+               }
+
+               // (*1)
+               rl::backoff bo;
+               while ( (m_read.load(mo_acquire) & 0xFFFF) != rd ) {
+                       thrd_yield();
+               }
+
+               t_element * p = & ( m_array[ wr % t_size ] );
+
+               return p;
+       }
+
+       void write_publish()
+       {
+               m_written.fetch_add(1,mo_relaxed);
+       }
+
+       //-----------------------------------------------------
+
+
+};
diff --git a/cdschecker_modified_benchmarks/ms-queue-tsan11/Makefile b/cdschecker_modified_benchmarks/ms-queue-tsan11/Makefile
new file mode 100755 (executable)
index 0000000..151ad71
--- /dev/null
@@ -0,0 +1,17 @@
+include ../benchmarks.mk
+
+TESTNAME = ms-queue
+
+HEADERS = my_queue.h
+OBJECTS = main.o my_queue.o
+
+all: $(TESTNAME)
+
+$(TESTNAME): $(HEADERS) $(OBJECTS)
+       $(CXX) -o $@ $(OBJECTS) $(CXXFLAGS) $(LDFLAGS)
+
+%.o: %.c
+       $(CXX) -c -o $@ $< $(CXXFLAGS)
+
+clean:
+       rm -f $(TESTNAME) *.o
diff --git a/cdschecker_modified_benchmarks/ms-queue-tsan11/main.cc b/cdschecker_modified_benchmarks/ms-queue-tsan11/main.cc
new file mode 100755 (executable)
index 0000000..e4bb181
--- /dev/null
@@ -0,0 +1,87 @@
+#include <stdlib.h>
+#include <stdio.h>
+#include "cds_threads.h"
+
+#include "my_queue.h"
+#include "model-assert.h"
+
+static int procs = 4;
+static queue_t *queue;
+static thrd_t *threads;
+static unsigned int *input;
+static unsigned int *output;
+static int num_threads;
+
+int get_thread_num()
+{
+       //thrd_t curr = thrd_current();
+       int i;
+       printf("thread id: %d\n", std::this_thread::get_id());
+       for (i = 0; i < num_threads; i++)
+               if (std::this_thread::get_id() == threads[i].get_id())
+                       return i;
+       MODEL_ASSERT(0);
+       return -1;
+}
+
+bool succ1, succ2;
+
+static void main_task(void *param)
+{
+       unsigned int val;
+       int pid = *((int *)param);
+       if (!pid) {
+               input[0] = 17;
+               enqueue(queue, input[0]);
+               succ1 = dequeue(queue, &output[0]);
+               //printf("Dequeue: %d\n", output[0]);
+       } else {
+               input[1] = 37;
+               enqueue(queue, input[1]);
+               succ2 = dequeue(queue, &output[1]);
+       }
+}
+
+int user_main(int argc, char **argv)
+{
+       int i;
+       int *param;
+       unsigned int in_sum = 0, out_sum = 0;
+
+       queue = (queue_t *)calloc(1, sizeof(*queue));
+       MODEL_ASSERT(queue);
+
+       num_threads = procs;
+       threads = (std::thread *)malloc(num_threads * sizeof(std::thread));
+       param = (int *)malloc(num_threads * sizeof(*param));
+       input = (unsigned *)calloc(num_threads, sizeof(*input));
+       output = (unsigned *)calloc(num_threads, sizeof(*output));
+
+       init_queue(queue, num_threads);
+       for (i = 0; i < num_threads; i++) {
+               param[i] = i;
+               //threads[i] = std::thread(main_task, &param[i]);
+                new (&threads[i])std::thread(main_task, &param[i]);
+       }
+       for (i = 0; i < num_threads; i++)
+               threads[i].join();
+
+       for (i = 0; i < num_threads; i++) {
+               in_sum += input[i];
+               out_sum += output[i];
+       }
+       for (i = 0; i < num_threads; i++)
+               printf("input[%d] = %u\n", i, input[i]);
+       for (i = 0; i < num_threads; i++)
+               printf("output[%d] = %u\n", i, output[i]);
+       if (succ1 && succ2)
+               MODEL_ASSERT(in_sum == out_sum);
+       else
+               MODEL_ASSERT (false);
+
+       free(param);
+       free(threads);
+       free(queue);
+
+       return 0;
+}
diff --git a/cdschecker_modified_benchmarks/ms-queue-tsan11/main.o b/cdschecker_modified_benchmarks/ms-queue-tsan11/main.o
new file mode 100644 (file)
index 0000000..e340deb
Binary files /dev/null and b/cdschecker_modified_benchmarks/ms-queue-tsan11/main.o differ
diff --git a/cdschecker_modified_benchmarks/ms-queue-tsan11/my_queue.cc b/cdschecker_modified_benchmarks/ms-queue-tsan11/my_queue.cc
new file mode 100755 (executable)
index 0000000..be84c7d
--- /dev/null
@@ -0,0 +1,161 @@
+#include "cds_threads.h"
+#include <stdlib.h>
+#include "librace.h"
+#include "model-assert.h"
+
+#include "my_queue.h"
+
+#define relaxed memory_order_relaxed
+#define release memory_order_release
+#define acquire memory_order_acquire
+
+#define MAX_FREELIST 4 /* Each thread can own up to MAX_FREELIST free nodes */
+#define INITIAL_FREE 2 /* Each thread starts with INITIAL_FREE free nodes */
+
+#define POISON_IDX 0x666
+
+static unsigned int (*free_lists)[MAX_FREELIST];
+
+/* Search this thread's free list for a "new" node */
+static unsigned int new_node()
+{
+       int i;
+       int t = get_thread_num();
+       for (i = 0; i < MAX_FREELIST; i++) {
+               unsigned int node = load_32(&free_lists[t][i]);
+               if (node) {
+                       store_32(&free_lists[t][i], 0);
+                       return node;
+               }
+       }
+       /* free_list is empty? */
+       MODEL_ASSERT(0);
+       return 0;
+}
+
+/* Place this node index back on this thread's free list */
+static void reclaim(unsigned int node)
+{
+       int i;
+       int t = get_thread_num();
+
+       /* Don't reclaim NULL node */
+       MODEL_ASSERT(node);
+
+       for (i = 0; i < MAX_FREELIST; i++) {
+               /* Should never race with our own thread here */
+               unsigned int idx = load_32(&free_lists[t][i]);
+
+               /* Found empty spot in free list */
+               if (idx == 0) {
+                       store_32(&free_lists[t][i], node);
+                       return;
+               }
+       }
+       /* free list is full? */
+       MODEL_ASSERT(0);
+}
+
+void init_queue(queue_t *q, int num_threads)
+{
+       int i, j;
+
+       /* Initialize each thread's free list with INITIAL_FREE pointers */
+       /* The actual nodes are initialized with poison indexes */
+       free_lists = (unsigned (*)[MAX_FREELIST])malloc(num_threads * sizeof(*free_lists));
+       for (i = 0; i < num_threads; i++) {
+               for (j = 0; j < INITIAL_FREE; j++) {
+                       free_lists[i][j] = 2 + i * MAX_FREELIST + j;
+                       atomic_init(&q->nodes[free_lists[i][j]].next, MAKE_POINTER(POISON_IDX, 0));
+               }
+       }
+
+       /* initialize queue */
+       atomic_init(&q->head, MAKE_POINTER(1, 0));
+       atomic_init(&q->tail, MAKE_POINTER(1, 0));
+       atomic_init(&q->nodes[1].next, MAKE_POINTER(0, 0));
+}
+
+void enqueue(queue_t *q, unsigned int val)
+{
+       int success = 0;
+       unsigned int node;
+       pointer tail;
+       pointer next;
+       pointer tmp;
+
+       node = new_node();
+       store_32(&q->nodes[node].value, val);
+       tmp = atomic_load_explicit(&q->nodes[node].next, relaxed);
+       set_ptr(&tmp, 0); // NULL
+       atomic_store_explicit(&q->nodes[node].next, tmp, relaxed);
+
+       while (!success) {
+               tail = atomic_load_explicit(&q->tail, acquire);
+               next = atomic_load_explicit(&q->nodes[get_ptr(tail)].next, acquire);
+               if (tail == atomic_load_explicit(&q->tail, relaxed)) {
+
+                       /* Check for uninitialized 'next' */
+                       MODEL_ASSERT(get_ptr(next) != POISON_IDX);
+
+                       if (get_ptr(next) == 0) { // == NULL
+                               pointer value = MAKE_POINTER(node, get_count(next) + 1);
+                               success = atomic_compare_exchange_strong_explicit(&q->nodes[get_ptr(tail)].next,
+                                               &next, value, release, release);
+                       }
+                       if (!success) {
+                               unsigned int ptr = get_ptr(atomic_load_explicit(&q->nodes[get_ptr(tail)].next, acquire));
+                               pointer value = MAKE_POINTER(ptr,
+                                               get_count(tail) + 1);
+                               atomic_compare_exchange_strong_explicit(&q->tail,
+                                               &tail, value,
+                                               release, release);
+                               thrd_yield();
+                       }
+               }
+       }
+       atomic_compare_exchange_strong_explicit(&q->tail,
+                       &tail,
+                       MAKE_POINTER(node, get_count(tail) + 1),
+                       release, release);
+}
+
+bool dequeue(queue_t *q, unsigned int *retVal)
+{
+       int success = 0;
+       pointer head;
+       pointer tail;
+       pointer next;
+
+       while (!success) {
+               head = atomic_load_explicit(&q->head, acquire);
+               tail = atomic_load_explicit(&q->tail, relaxed);
+               next = atomic_load_explicit(&q->nodes[get_ptr(head)].next, acquire);
+               if (atomic_load_explicit(&q->head, relaxed) == head) {
+                       if (get_ptr(head) == get_ptr(tail)) {
+
+                               /* Check for uninitialized 'next' */
+                               MODEL_ASSERT(get_ptr(next) != POISON_IDX);
+
+                               if (get_ptr(next) == 0) { // NULL
+                                       return false; // NULL
+                               }
+                               atomic_compare_exchange_strong_explicit(&q->tail,
+                                               &tail,
+                                               MAKE_POINTER(get_ptr(next), get_count(tail) + 1),
+                                               release, release);
+                               thrd_yield();
+                       } else {
+                               *retVal = load_32(&q->nodes[get_ptr(next)].value);
+                               success = atomic_compare_exchange_strong_explicit(&q->head,
+                                               &head,
+                                               MAKE_POINTER(get_ptr(next), get_count(head) + 1),
+                                               release, release);
+                               if (!success)
+                                       thrd_yield();
+                       }
+               }
+       }
+       reclaim(get_ptr(head));
+       return true;
+}
diff --git a/cdschecker_modified_benchmarks/ms-queue-tsan11/my_queue.h b/cdschecker_modified_benchmarks/ms-queue-tsan11/my_queue.h
new file mode 100755 (executable)
index 0000000..45849a4
--- /dev/null
@@ -0,0 +1,31 @@
+#include "cds_atomic.h"
+
+#define MAX_NODES                      0xf
+
+typedef unsigned long long pointer;
+typedef atomic_ullong pointer_t;
+
+#define MAKE_POINTER(ptr, count)       ((((pointer)count) << 32) | ptr)
+#define PTR_MASK 0xffffffffLL
+#define COUNT_MASK (0xffffffffLL << 32)
+
+static inline void set_count(pointer *p, unsigned int val) { *p = (*p & ~COUNT_MASK) | ((pointer)val << 32); }
+static inline void set_ptr(pointer *p, unsigned int val) { *p = (*p & ~PTR_MASK) | val; }
+static inline unsigned int get_count(pointer p) { return (p & COUNT_MASK) >> 32; }
+static inline unsigned int get_ptr(pointer p) { return p & PTR_MASK; }
+
+typedef struct node {
+       unsigned int value;
+       pointer_t next;
+} node_t;
+
+typedef struct {
+       pointer_t head;
+       pointer_t tail;
+       node_t nodes[MAX_NODES + 1];
+} queue_t;
+
+void init_queue(queue_t *q, int num_threads);
+void enqueue(queue_t *q, unsigned int val);
+bool dequeue(queue_t *q, unsigned int *retVal);
+int get_thread_num();
diff --git a/cdschecker_modified_benchmarks/ms-queue-tsan11/my_queue.o b/cdschecker_modified_benchmarks/ms-queue-tsan11/my_queue.o
new file mode 100644 (file)
index 0000000..306682f
Binary files /dev/null and b/cdschecker_modified_benchmarks/ms-queue-tsan11/my_queue.o differ
diff --git a/cdschecker_modified_benchmarks/ms-queue/Makefile b/cdschecker_modified_benchmarks/ms-queue/Makefile
new file mode 100644 (file)
index 0000000..c42add1
--- /dev/null
@@ -0,0 +1,19 @@
+include ../benchmarks.mk
+
+TESTNAME = ms-queue
+
+HEADERS = my_queue.h
+OBJECTS = main.o my_queue.o
+
+CXXFLAGS += -I /scratch/fuzzer/random-fuzzer/include 
+
+all: $(TESTNAME)
+
+$(TESTNAME): $(HEADERS) $(OBJECTS)
+       $(CC) -o $@ $(OBJECTS) $(CFLAGS) $(LDFLAGS)
+
+%.o: %.c
+       $(CC) -c -o $@ $(CFLAGS)
+
+clean:
+       rm -f $(TESTNAME) *.o
diff --git a/cdschecker_modified_benchmarks/ms-queue/main.cc b/cdschecker_modified_benchmarks/ms-queue/main.cc
new file mode 100644 (file)
index 0000000..fc31f9c
--- /dev/null
@@ -0,0 +1,88 @@
+#include <stdlib.h>
+#include <stdio.h>
+#include <threads.h>
+//#include "cds_threads.h"
+
+#include "my_queue.h"
+#include "model-assert.h"
+
+#define user_main main
+
+static int procs = 4;
+static queue_t *queue;
+static thrd_t *threads;
+static unsigned int *input;
+static unsigned int *output;
+static int num_threads;
+
+int get_thread_num()
+{
+       thrd_t curr = thrd_current();
+       int i;
+       for (i = 0; i < num_threads; i++)
+               if (curr.priv == threads[i].priv)
+                       return i;
+       MODEL_ASSERT(0);
+       return -1;
+}
+
+bool succ1, succ2;
+
+static void main_task(void *param)
+{
+       int pid = *((int *)param);
+       if (!pid) {
+               input[0] = 17;
+               enqueue(queue, input[0]);
+               succ1 = dequeue(queue, &output[0]);
+               //printf("Dequeue: %d\n", output[0]);
+       } else {
+               input[1] = 37;
+               enqueue(queue, input[1]);
+               succ2 = dequeue(queue, &output[1]);
+       }
+}
+
+int user_main(int argc, char **argv)
+{
+       int i;
+       int *param;
+       unsigned int in_sum = 0, out_sum = 0;
+
+       queue = (queue_t *)calloc(1, sizeof(*queue));
+       MODEL_ASSERT(queue);
+
+       num_threads = procs;
+       threads = (thrd_t *)malloc(num_threads * sizeof(thrd_t));
+       param = (int *)malloc(num_threads * sizeof(*param));
+       input = (unsigned *)calloc(num_threads, sizeof(*input));
+       output = (unsigned *)calloc(num_threads, sizeof(*output));
+
+       init_queue(queue, num_threads);
+       for (i = 0; i < num_threads; i++) {
+               param[i] = i;
+               thrd_create(&threads[i], main_task, &param[i]);
+       }
+       for (i = 0; i < num_threads; i++)
+               thrd_join(threads[i]);
+
+       for (i = 0; i < num_threads; i++) {
+               in_sum += input[i];
+               out_sum += output[i];
+       }
+       for (i = 0; i < num_threads; i++)
+               printf("input[%d] = %u\n", i, input[i]);
+       for (i = 0; i < num_threads; i++)
+               printf("output[%d] = %u\n", i, output[i]);
+/*
+       if (succ1 && succ2)
+               MODEL_ASSERT(in_sum == out_sum);
+       else
+               MODEL_ASSERT(false);
+*/
+       free(param);
+       free(threads);
+       free(queue);
+
+       return 0;
+}
diff --git a/cdschecker_modified_benchmarks/ms-queue/my_queue.c.correct b/cdschecker_modified_benchmarks/ms-queue/my_queue.c.correct
new file mode 100644 (file)
index 0000000..b868d2e
--- /dev/null
@@ -0,0 +1,260 @@
+#include <threads.h>
+#include <stdlib.h>
+#include "librace.h"
+#include "model-assert.h"
+
+#include "queue.h"
+
+#define relaxed memory_order_relaxed
+#define release memory_order_release
+#define acquire memory_order_acquire
+
+#define MAX_FREELIST 4 /* Each thread can own up to MAX_FREELIST free nodes */
+#define INITIAL_FREE 2 /* Each thread starts with INITIAL_FREE free nodes */
+
+#define POISON_IDX 0x666
+
+static unsigned int (*free_lists)[MAX_FREELIST];
+
+/* Search this thread's free list for a "new" node */
+static unsigned int new_node()
+{
+       int i;
+       int t = get_thread_num();
+       for (i = 0; i < MAX_FREELIST; i++) {
+               //unsigned int node = load_32(&free_lists[t][i]);
+               unsigned int node = free_lists[t][i];
+               if (node) {
+                       //store_32(&free_lists[t][i], 0);
+                       free_lists[t][i] = 0;
+                       return node;
+               }
+       }
+       /* free_list is empty? */
+       MODEL_ASSERT(0);
+       return 0;
+}
+
+/* Simulate the fact that when a node got recycled, it will get assigned to the
+ * same queue or for other usage */
+void simulateRecycledNodeUpdate(queue_t *q, unsigned int node) {
+       atomic_store_explicit(&q->nodes[node].next, -1, memory_order_release);
+}
+
+
+/* Place this node index back on this thread's free list */
+static void reclaim(unsigned int node)
+{
+       int i;
+       int t = get_thread_num();
+
+       /* Don't reclaim NULL node */
+       //MODEL_ASSERT(node);
+
+       for (i = 0; i < MAX_FREELIST; i++) {
+               /* Should never race with our own thread here */
+               //unsigned int idx = load_32(&free_lists[t][i]);
+               unsigned int idx = free_lists[t][i];
+
+               /* Found empty spot in free list */
+               if (idx == 0) {
+                       //store_32(&free_lists[t][i], node);
+                       free_lists[t][i] = node;
+                       return;
+               }
+       }
+       /* free list is full? */
+       //MODEL_ASSERT(0);
+}
+
+void init_queue(queue_t *q, int num_threads)
+{
+       int i, j;
+
+       /* Initialize each thread's free list with INITIAL_FREE pointers */
+       /* The actual nodes are initialized with poison indexes */
+       free_lists = ( unsigned int (*)[MAX_FREELIST] ) malloc(num_threads * sizeof(*free_lists));
+       for (i = 0; i < num_threads; i++) {
+               for (j = 0; j < INITIAL_FREE; j++) {
+                       free_lists[i][j] = 2 + i * MAX_FREELIST + j;
+                       atomic_init(&q->nodes[free_lists[i][j]].next, MAKE_POINTER(POISON_IDX, 0));
+               }
+       }
+
+       /* initialize queue */
+       atomic_init(&q->head, MAKE_POINTER(1, 0));
+       atomic_init(&q->tail, MAKE_POINTER(1, 0));
+       atomic_init(&q->nodes[1].next, MAKE_POINTER(0, 0));
+}
+
+/** @DeclareState: IntList *q;
+@Initial: q = new IntList;
+@Print:
+       model_print("\tSTATE(q): ");
+    printContainer(q);
+       model_print("\n"); */
+
+/** @Transition: STATE(q)->push_back(val);
+@Print: model_print("\tENQ #%d: val=%d\n", ID, val); */
+void enqueue(queue_t *q, unsigned int val, int n)
+{
+       int success = 0;
+       unsigned int node;
+       pointer tail;
+       pointer next;
+       pointer tmp;
+
+       node = new_node();
+       //store_32(&q->nodes[node].value, val);
+       q->nodes[node].value = val;
+       tmp = atomic_load_explicit(&q->nodes[node].next, relaxed);
+       set_ptr(&tmp, 0); // NULL
+    // XXX-known-bug-#1: This is a found bug in AutoMO, and testcase4 can reveal
+    // this known bug.
+    // To reproduce, weaken the parameter "memory_order_release" to
+    // "memory_order_relaxed", run "make" to recompile, and then run:
+    // "./run.sh ./ms-queue/testcase4 -m2 -y -u3 -tSPEC"
+       /**********    Detected KNOWN BUG (testcase4)    **********/
+       atomic_store_explicit(&q->nodes[node].next, tmp, release);
+
+       while (!success) {
+        // XXX-injection-#1: To reproduce, weaken the parameter
+        // "memory_order_acquire" to "memory_order_relaxed", run "make" to
+        // recompile, and then run:
+        // "./run.sh ./ms-queue/testcase2 -m2 -y -u3 -tSPEC"
+               /**********    Detected UL (testcase2)    **********/
+               tail = atomic_load_explicit(&q->tail, acquire);
+        // XXX-injection-#2: To reproduce, weaken the parameter
+        // "memory_order_acquire" to "memory_order_relaxed", run "make" to
+        // recompile, and then run:
+        // "./run.sh ./ms-queue/testcase4 -m2 -y -u3 -tSPEC"
+               /**********    Detected Correctness (testcase4)    **********/
+               next = atomic_load_explicit(&q->nodes[get_ptr(tail)].next, acquire);
+               if (tail == atomic_load_explicit(&q->tail, relaxed)) {
+
+                       /* Check for uninitialized 'next' */
+                       //MODEL_ASSERT(get_ptr(next) != POISON_IDX);
+
+                       if (get_ptr(next) == 0) { // == NULL
+                               pointer value = MAKE_POINTER(node, get_count(next) + 1);
+                // XXX-injection-#3: To reproduce, weaken the parameter
+                // "memory_order_release" to "memory_order_relaxed", run "make" to
+                // recompile, and then run:
+                // "./run.sh ./ms-queue/testcase1 -m2 -y -u3 -tSPEC"
+                               /**********    Detected Correctness (testcase1)    **********/
+                               success = atomic_compare_exchange_strong_explicit(&q->nodes[get_ptr(tail)].next,
+                                               &next, value, release, release);
+                               /** @OPClearDefine: success */
+                       }
+                       if (!success) {
+                // XXX-injection-#4: To reproduce, weaken the parameter
+                // "memory_order_acquire" to "memory_order_relaxed", run "make" to
+                // recompile, and then run:
+                // "./run.sh ./ms-queue/testcase2 -m2 -y -u3 -tSPEC"
+                               /**********    Detected UL (testcase2)    **********/
+                               unsigned int ptr = get_ptr(atomic_load_explicit(&q->nodes[get_ptr(tail)].next, acquire));
+                               pointer value = MAKE_POINTER(ptr,
+                                               get_count(tail) + 1);
+                // XXX-injection-#5: To reproduce, weaken the parameter
+                // "memory_order_release" to "memory_order_relaxed", run "make" to
+                // recompile, and then run:
+                // "./run.sh ./ms-queue/testcase2 -m2 -y -u3 -tSPEC"
+                               /**********    Detected Correctness (testcase2)    **********/
+                               atomic_compare_exchange_strong_explicit(&q->tail,
+                                               &tail, value,
+                                               release, release);
+                               thrd_yield();
+                       }
+               }
+       }
+
+    // XXX-injection-#6: To reproduce, weaken the parameter
+    // "memory_order_release" to "memory_order_relaxed", run "make" to
+    // recompile, and then run:
+    // "./run.sh ./ms-queue/testcase1 -m2 -y -u3 -tSPEC"
+       /**********    Detected Correctness (testcase1) **********/
+       atomic_compare_exchange_strong_explicit(&q->tail,
+                       &tail,
+                       MAKE_POINTER(node, get_count(tail) + 1),
+                       release, release);
+}
+
+/** @Transition: S_RET = STATE(q)->empty() ? 0 : STATE(q)->front();
+if (S_RET && C_RET) STATE(q)->pop_front();
+@JustifyingPostcondition: if (!C_RET)
+    return S_RET == C_RET;
+@PostCondition: return C_RET ? *retVal  == S_RET : true;
+@Print: model_print("\tDEQ #%d: C_RET=%d && *retVal=%d && S_RET=%d\n", ID,
+            C_RET, *retVal, S_RET);
+*/
+int dequeue(queue_t *q, unsigned int *retVal, unsigned int *reclaimNode)
+{
+       int success = 0;
+       pointer head;
+       pointer tail;
+       pointer next;
+
+       while (!success) {
+        // XXX-injection-#7: To reproduce, weaken the parameter
+        // "memory_order_acquire" to "memory_order_relaxed", run "make" to
+        // recompile, and then run:
+        // "./run.sh ./ms-queue/testcase3 -m2 -y -u3 -tSPEC"
+               /**********    Detected Correctness (testcase3)    **********/
+               head = atomic_load_explicit(&q->head, acquire);
+        // To reproduce, weaken the parameter "memory_order_acquire" to
+        // "memory_order_relaxed", run "make" to recompile, and then run:
+        // "./run.sh ./ms-queue/testcase4 -m2 -y -u3 -tSPEC"
+        // XXX-known-bug-#2: This is another known bug, and testcase2 can reveal
+        // this known bug
+               /**********    Detected KNOWN BUG (testcase2)    **********/
+               tail = atomic_load_explicit(&q->tail, acquire);
+
+        // XXX-injection-#8: To reproduce, weaken the parameter
+        // "memory_order_acquire" to "memory_order_relaxed", run "make" to
+        // recompile, and then run:
+        // "./run.sh ./ms-queue/testcase1 -m2 -y -u3 -tSPEC"
+               /**********    Detected Correctness (testcase1) **********/
+               next = atomic_load_explicit(&q->nodes[get_ptr(head)].next, acquire);
+               /** @OPClearDefine: true */
+               if (atomic_load_explicit(&q->head, relaxed) == head) {
+                       if (get_ptr(head) == get_ptr(tail)) {
+
+                               /* Check for uninitialized 'next' */
+                               MODEL_ASSERT(get_ptr(next) != POISON_IDX);
+
+                               if (get_ptr(next) == 0) { // NULL
+                                       return false; // NULL
+                               }
+
+                // XXX-injection-#9: To reproduce, weaken the parameter
+                // "memory_order_release" to "memory_order_relaxed", run "make" to
+                // recompile, and then run:
+                // "./run.sh ./ms-queue/testcase2 -m2 -y -u3 -tSPEC"
+                               /**********    Detected UL (testcase2)    **********/
+                               atomic_compare_exchange_strong_explicit(&q->tail,
+                                               &tail,
+                                               MAKE_POINTER(get_ptr(next), get_count(tail) + 1),
+                                               release, release);
+                               thrd_yield();
+                       } else {
+                               //*retVal = load_32(&q->nodes[get_ptr(next)].value);
+                               *retVal = q->nodes[get_ptr(next)].value;
+
+                // XXX-injection-#10: To reproduce, weaken the parameter
+                // "memory_order_release" to "memory_order_relaxed", run "make" to
+                // recompile, and then run:
+                // "./run.sh ./ms-queue/testcase3 -m2 -y -u3 -tSPEC"
+                               /**********    Detected Correctness (testcase3)    **********/
+                               success = atomic_compare_exchange_strong_explicit(&q->head,
+                                               &head,
+                                               MAKE_POINTER(get_ptr(next), get_count(head) + 1),
+                                               release, release);
+                               if (!success)
+                                       thrd_yield();
+                       }
+               }
+       }
+       *reclaimNode = get_ptr(head);
+       reclaim(get_ptr(head));
+       return true;
+}
diff --git a/cdschecker_modified_benchmarks/ms-queue/my_queue.cc b/cdschecker_modified_benchmarks/ms-queue/my_queue.cc
new file mode 100644 (file)
index 0000000..d746bda
--- /dev/null
@@ -0,0 +1,167 @@
+#include <threads.h>
+#include <stdlib.h>
+#include "librace.h"
+#include "model-assert.h"
+
+#include "my_queue.h"
+
+#define relaxed memory_order_relaxed
+#define release memory_order_release
+#define acquire memory_order_acquire
+
+#define MAX_FREELIST 4 /* Each thread can own up to MAX_FREELIST free nodes */
+#define INITIAL_FREE 2 /* Each thread starts with INITIAL_FREE free nodes */
+
+#define POISON_IDX 0x666
+
+static unsigned int (*free_lists)[MAX_FREELIST];
+
+/* Search this thread's free list for a "new" node */
+static unsigned int new_node()
+{
+       int i;
+       int t = get_thread_num();
+       for (i = 0; i < MAX_FREELIST; i++) {
+               unsigned int node = load_32(&free_lists[t][i]);
+               if (node) {
+                       store_32(&free_lists[t][i], 0);
+                       return node;
+               }
+       }
+       /* free_list is empty? */
+       MODEL_ASSERT(0);
+       return 0;
+}
+
+/* Place this node index back on this thread's free list */
+static void reclaim(unsigned int node)
+{
+       int i;
+       int t = get_thread_num();
+
+       /* Don't reclaim NULL node */
+       MODEL_ASSERT(node);
+
+       for (i = 0; i < MAX_FREELIST; i++) {
+               /* Should never race with our own thread here */
+               unsigned int idx = load_32(&free_lists[t][i]);
+
+               /* Found empty spot in free list */
+               if (idx == 0) {
+                       store_32(&free_lists[t][i], node);
+                       return;
+               }
+       }
+       /* free list is full? */
+       MODEL_ASSERT(0);
+}
+
+void init_queue(queue_t *q, int num_threads)
+{
+       int i, j;
+
+       /* Initialize each thread's free list with INITIAL_FREE pointers */
+       /* The actual nodes are initialized with poison indexes */
+       free_lists = (unsigned (*)[MAX_FREELIST])malloc(num_threads * sizeof(*free_lists));
+       for (i = 0; i < num_threads; i++) {
+               for (j = 0; j < INITIAL_FREE; j++) {
+                       free_lists[i][j] = 2 + i * MAX_FREELIST + j;
+                       atomic_init(&q->nodes[free_lists[i][j]].next, MAKE_POINTER(POISON_IDX, 0));
+               }
+       }
+
+       /* initialize queue */
+       atomic_init(&q->head, MAKE_POINTER(1, 0));
+       atomic_init(&q->tail, MAKE_POINTER(1, 0));
+       atomic_init(&q->nodes[1].next, MAKE_POINTER(0, 0));
+}
+
+void enqueue(queue_t *q, unsigned int val)
+{
+       int success = 0;
+       unsigned int node;
+       pointer tail;
+       pointer next;
+       pointer tmp;
+
+       node = new_node();
+       store_32(&q->nodes[node].value, val);
+       tmp = atomic_load_explicit(&q->nodes[node].next, relaxed);
+       set_ptr(&tmp, 0); // NULL
+
+       // Bug 1
+       atomic_store_explicit(&q->nodes[node].next, tmp, relaxed);
+       //atomic_store_explicit(&q->nodes[node].next, tmp, release);
+
+       while (!success) {
+               tail = atomic_load_explicit(&q->tail, acquire);
+               next = atomic_load_explicit(&q->nodes[get_ptr(tail)].next, acquire);
+               if (tail == atomic_load_explicit(&q->tail, relaxed)) {
+                       /* Check for uninitialized 'next' */
+                       MODEL_ASSERT(get_ptr(next) != POISON_IDX);
+
+                       if (get_ptr(next) == 0) { // == NULL
+                               pointer value = MAKE_POINTER(node, get_count(next) + 1);
+                               success = atomic_compare_exchange_strong_explicit(&q->nodes[get_ptr(tail)].next,
+                                               &next, value, release, release);
+                       }
+                       if (!success) {
+                               unsigned int ptr = get_ptr(atomic_load_explicit(&q->nodes[get_ptr(tail)].next, acquire));
+                               pointer value = MAKE_POINTER(ptr,
+                                               get_count(tail) + 1);
+                               atomic_compare_exchange_strong_explicit(&q->tail,
+                                               &tail, value,
+                                               release, release);
+                               thrd_yield();
+                       }
+               }
+       }
+       atomic_compare_exchange_strong_explicit(&q->tail,
+                       &tail,
+                       MAKE_POINTER(node, get_count(tail) + 1),
+                       release, release);
+}
+
+bool dequeue(queue_t *q, unsigned int *retVal)
+{
+       int success = 0;
+       pointer head;
+       pointer tail;
+       pointer next;
+
+       while (!success) {
+               head = atomic_load_explicit(&q->head, acquire);
+
+               // Bug 2
+               tail = atomic_load_explicit(&q->tail, relaxed);
+               //tail = atomic_load_explicit(&q->tail, acquire);
+
+               next = atomic_load_explicit(&q->nodes[get_ptr(head)].next, acquire);
+               if (atomic_load_explicit(&q->head, relaxed) == head) {
+                       if (get_ptr(head) == get_ptr(tail)) {
+
+                               /* Check for uninitialized 'next' */
+                               MODEL_ASSERT(get_ptr(next) != POISON_IDX);
+
+                               if (get_ptr(next) == 0) { // NULL
+                                       return false; // NULL
+                               }
+                               atomic_compare_exchange_strong_explicit(&q->tail,
+                                               &tail,
+                                               MAKE_POINTER(get_ptr(next), get_count(tail) + 1),
+                                               release, release);
+                               thrd_yield();
+                       } else {
+                               *retVal = load_32(&q->nodes[get_ptr(next)].value);
+                               success = atomic_compare_exchange_strong_explicit(&q->head,
+                                               &head,
+                                               MAKE_POINTER(get_ptr(next), get_count(head) + 1),
+                                               release, release);
+                               if (!success)
+                                       thrd_yield();
+                       }
+               }
+       }
+       reclaim(get_ptr(head));
+       return true;
+}
diff --git a/cdschecker_modified_benchmarks/ms-queue/my_queue.h b/cdschecker_modified_benchmarks/ms-queue/my_queue.h
new file mode 100644 (file)
index 0000000..8bb8d58
--- /dev/null
@@ -0,0 +1,32 @@
+#include <stdatomic.h>
+#include <stdbool.h>
+
+#define MAX_NODES                      0xf
+
+typedef unsigned long long pointer;
+typedef atomic_ullong pointer_t;
+
+#define MAKE_POINTER(ptr, count)       ((((pointer)count) << 32) | ptr)
+#define PTR_MASK 0xffffffffLL
+#define COUNT_MASK (0xffffffffLL << 32)
+
+static inline void set_count(pointer *p, unsigned int val) { *p = (*p & ~COUNT_MASK) | ((pointer)val << 32); }
+static inline void set_ptr(pointer *p, unsigned int val) { *p = (*p & ~PTR_MASK) | val; }
+static inline unsigned int get_count(pointer p) { return (p & COUNT_MASK) >> 32; }
+static inline unsigned int get_ptr(pointer p) { return p & PTR_MASK; }
+
+typedef struct node {
+       unsigned int value;
+       pointer_t next;
+} node_t;
+
+typedef struct {
+       pointer_t head;
+       pointer_t tail;
+       node_t nodes[MAX_NODES + 1];
+} queue_t;
+
+void init_queue(queue_t *q, int num_threads);
+void enqueue(queue_t *q, unsigned int val);
+bool dequeue(queue_t *q, unsigned int *retVal);
+int get_thread_num();
diff --git a/cdschecker_modified_benchmarks/spsc-queue/Makefile b/cdschecker_modified_benchmarks/spsc-queue/Makefile
new file mode 100644 (file)
index 0000000..33b9d01
--- /dev/null
@@ -0,0 +1,23 @@
+include ../benchmarks.mk
+
+TESTNAME = spsc-queue
+RELACYNAME = spsc-relacy
+
+all: $(TESTNAME)
+
+$(TESTNAME): $(TESTNAME).cc queue.h eventcount.h
+       $(CXX) -o $@ $< $(CXXFLAGS) $(LDFLAGS)
+
+relacy: $(RELACYNAME)
+
+$(RELACYNAME): spsc-relacy.cc queue-relacy.h eventcount-relacy.h
+ifdef RELACYPATH
+       $(CXX) -o $(RELACYNAME) spsc-relacy.cc -I$(RELACYPATH) -Wno-deprecated
+else
+       @echo "Please define RELACYPATH"
+       @echo "  e.g., make RELACYPATH=/path-to-relacy"
+       @exit 1
+endif
+
+clean:
+       rm -f $(TESTNAME) $(RELACYNAME) *.o
diff --git a/cdschecker_modified_benchmarks/spsc-queue/eventcount-relacy.h b/cdschecker_modified_benchmarks/spsc-queue/eventcount-relacy.h
new file mode 100644 (file)
index 0000000..9eadcf3
--- /dev/null
@@ -0,0 +1,64 @@
+class eventcount
+{
+public:
+       eventcount() : waiters(0)
+       {
+               count($) = 0;
+       }
+
+       void signal_relaxed()
+       {
+               unsigned cmp = count.load(std::memory_order_relaxed);
+               signal_impl(cmp);
+       }
+
+       void signal()
+       {
+               unsigned cmp = count.fetch_add(0, std::memory_order_seq_cst);
+               signal_impl(cmp);
+       }
+
+       unsigned get()
+       {
+               unsigned cmp = count.fetch_or(0x80000000,
+std::memory_order_seq_cst);
+               return cmp & 0x7FFFFFFF;
+       }
+
+       void wait(unsigned cmp)
+       {
+               unsigned ec = count.load(std::memory_order_seq_cst);
+               if (cmp == (ec & 0x7FFFFFFF))
+               {
+                       guard.lock($);
+                       ec = count.load(std::memory_order_seq_cst);
+                       if (cmp == (ec & 0x7FFFFFFF))
+                       {
+                               waiters($) += 1;
+                               cv.wait(guard, $);
+                       }
+                       guard.unlock($);
+               }
+       }
+
+private:
+       std::atomic<unsigned> count;
+       rl::var<unsigned> waiters;
+       std::mutex guard;
+       std::condition_variable cv;
+
+       void signal_impl(unsigned cmp)
+       {
+               if (cmp & 0x80000000)
+               {
+                       guard.lock($);
+                       while (false == count.compare_exchange_weak(cmp,
+                               (cmp + 1) & 0x7FFFFFFF, std::memory_order_relaxed));
+                       unsigned w = waiters($);
+                       waiters($) = 0;
+                       guard.unlock($);
+                       if (w)
+                               cv.notify_all($);
+               }
+       }
+};
diff --git a/cdschecker_modified_benchmarks/spsc-queue/eventcount.h b/cdschecker_modified_benchmarks/spsc-queue/eventcount.h
new file mode 100644 (file)
index 0000000..f2b05f7
--- /dev/null
@@ -0,0 +1,72 @@
+#include <unrelacy.h>
+#include <atomic>
+#include <mutex>
+#include <condition_variable>
+
+class eventcount
+{
+public:
+       eventcount() : waiters(0)
+       {
+               count = 0;
+       }
+
+       void signal_relaxed()
+       {
+               unsigned cmp = count.load(std::memory_order_relaxed);
+               signal_impl(cmp);
+       }
+
+       void signal()
+       {
+               unsigned cmp = count.fetch_add(0, std::memory_order_seq_cst);
+               signal_impl(cmp);
+       }
+
+       unsigned get()
+       {
+               unsigned cmp = count.fetch_or(0x80000000,
+std::memory_order_seq_cst);
+               return cmp & 0x7FFFFFFF;
+       }
+
+       void wait(unsigned cmp)
+       {
+               unsigned ec = count.load(std::memory_order_seq_cst);
+               if (cmp == (ec & 0x7FFFFFFF))
+               {
+                       //guard.lock($);
+                       std::unique_lock<std::mutex> lck(guard);
+                       ec = count.load(std::memory_order_seq_cst);
+                       if (cmp == (ec & 0x7FFFFFFF))
+                       {
+                               waiters += 1;
+                               //cv.wait(guard);
+                               cv.wait(lck);
+                       }
+                       guard.unlock($);
+                       //lck.unlock();
+               }
+       }
+
+private:
+       std::atomic<unsigned> count;
+       rl::var<unsigned> waiters;
+       std::mutex guard;
+       std::condition_variable cv;
+
+       void signal_impl(unsigned cmp)
+       {
+               if (cmp & 0x80000000)
+               {
+                       guard.lock($);
+                       while (false == count.compare_exchange_weak(cmp,
+                               (cmp + 1) & 0x7FFFFFFF, std::memory_order_relaxed));
+                       unsigned w = waiters($);
+                       waiters = 0;
+                       guard.unlock($);
+                       if (w)
+                               cv.notify_all($);
+               }
+       }
+};
diff --git a/cdschecker_modified_benchmarks/spsc-queue/queue-relacy.h b/cdschecker_modified_benchmarks/spsc-queue/queue-relacy.h
new file mode 100644 (file)
index 0000000..71aac2a
--- /dev/null
@@ -0,0 +1,74 @@
+#include "eventcount-relacy.h"
+
+template<typename T>
+class spsc_queue
+{
+public:
+       spsc_queue()
+       {
+               node* n = new node ();
+               head($) = n;
+               tail($) = n;
+       }
+
+       ~spsc_queue()
+       {
+               RL_ASSERT(head($) == tail($));
+               delete ((node*)head($));
+       }
+
+       void enqueue(T data)
+       {
+               node* n = new node (data);
+               head($)->next.store(n, std::memory_order_release);
+               head($) = n;
+               ec.signal_relaxed();
+       }
+
+       T dequeue()
+       {
+               T data = try_dequeue();
+               while (0 == data)
+               {
+                       int cmp = ec.get();
+                       data = try_dequeue();
+                       if (data)
+                               break;
+                       ec.wait(cmp);
+                       data = try_dequeue();
+                       if (data)
+                               break;
+               }
+               return data;
+       }
+
+private:
+       struct node
+       {
+               std::atomic<node*> next;
+               rl::var<T> data;
+
+               node(T data = T())
+                       : data(data)
+               {
+                       next($) = 0;
+               }
+       };
+
+       rl::var<node*> head;
+       rl::var<node*> tail;
+
+       eventcount ec;
+
+       T try_dequeue()
+       {
+               node* t = tail($);
+               node* n = t->next.load(std::memory_order_acquire);
+               if (0 == n)
+                       return 0;
+               T data = n->data($);
+               delete (t);
+               tail($) = n;
+               return data;
+       }
+};
diff --git a/cdschecker_modified_benchmarks/spsc-queue/queue.h b/cdschecker_modified_benchmarks/spsc-queue/queue.h
new file mode 100644 (file)
index 0000000..c77425f
--- /dev/null
@@ -0,0 +1,77 @@
+#include <unrelacy.h>
+#include <atomic>
+
+#include "eventcount.h"
+
+template<typename T>
+class spsc_queue
+{
+public:
+       spsc_queue()
+       {
+               node* n = new node ();
+               head = n;
+               tail = n;
+       }
+
+       ~spsc_queue()
+       {
+               RL_ASSERT(head == tail);
+               delete ((node*)head($));
+       }
+
+       void enqueue(T data)
+       {
+               node* n = new node (data);
+               head($)->next.store(n, std::memory_order_release);
+               head = n;
+               ec.signal_relaxed();
+       }
+
+       T dequeue()
+       {
+               T data = try_dequeue();
+               while (0 == data)
+               {
+                       int cmp = ec.get();
+                       data = try_dequeue();
+                       if (data)
+                               break;
+                       ec.wait(cmp);
+                       data = try_dequeue();
+                       if (data)
+                               break;
+               }
+               return data;
+       }
+
+private:
+       struct node
+       {
+               std::atomic<node*> next;
+               rl::var<T> data;
+
+               node(T data = T())
+                       : data(data)
+               {
+                       next = 0;
+               }
+       };
+
+       rl::var<node*> head;
+       rl::var<node*> tail;
+
+       eventcount ec;
+
+       T try_dequeue()
+       {
+               node* t = tail($);
+               node* n = t->next.load(std::memory_order_acquire);
+               if (0 == n)
+                       return 0;
+               T data = n->data($);
+               delete (t);
+               tail = n;
+               return data;
+       }
+};
diff --git a/cdschecker_modified_benchmarks/spsc-queue/spsc-queue.cc b/cdschecker_modified_benchmarks/spsc-queue/spsc-queue.cc
new file mode 100644 (file)
index 0000000..1347f4e
--- /dev/null
@@ -0,0 +1,34 @@
+#include "cds_threads.h"
+
+#include "queue.h"
+
+spsc_queue<int> *q;
+
+       void thread(unsigned thread_index)
+       {
+               if (0 == thread_index)
+               {
+                       q->enqueue(11);
+               }
+               else
+               {
+                       int d = q->dequeue();
+                       RL_ASSERT(11 == d);
+               }
+       }
+
+int user_main(int argc, char **argv)
+{
+       thrd_t A, B;
+
+       q = new spsc_queue<int>();
+
+       thrd_create(&A, (thrd_start_t)&thread, (void *)0);
+       thrd_create(&B, (thrd_start_t)&thread, (void *)1);
+       thrd_join(A);
+       thrd_join(B);
+
+       delete q;
+
+       return 0;
+}
diff --git a/cdschecker_modified_benchmarks/spsc-queue/spsc-relacy.cc b/cdschecker_modified_benchmarks/spsc-queue/spsc-relacy.cc
new file mode 100644 (file)
index 0000000..37ed989
--- /dev/null
@@ -0,0 +1,27 @@
+#include <relacy/relacy_std.hpp>
+
+#include "queue-relacy.h"
+
+struct spsc_queue_test : rl::test_suite<spsc_queue_test, 2>
+{
+       spsc_queue<int> q;
+
+       void thread(unsigned thread_index)
+       {
+               if (0 == thread_index)
+               {
+                       q.enqueue(11);
+               }
+               else
+               {
+                       int d = q.dequeue();
+                       RL_ASSERT(11 == d);
+               }
+       }
+};
+
+
+int main()
+{
+       rl::simulate<spsc_queue_test>();
+}
diff --git a/cdschecker_modified_benchmarks/test.sh b/cdschecker_modified_benchmarks/test.sh
new file mode 100755 (executable)
index 0000000..ff2c3b5
--- /dev/null
@@ -0,0 +1,46 @@
+#!/bin/bash
+
+EXE=$1
+TOTAL_RUN=5 #00
+CDSLIB="/scratch/fuzzer/random-fuzzer"
+export LD_LIBRARY_PATH=${CDSLIB}
+export C11TESTER='-x1'
+
+#ERROR_FILE="data-structure.log"
+TASKSET=""
+
+COUNT_DATA_RACE=0
+COUNT_TIME=0
+
+for i in `seq 1 1 $TOTAL_RUN` ; do
+#  time ${TASKSET} $EXE &> $ERROR_FILE
+#  OUTPUT=$(< $ERROR_FILE)
+
+  OUTPUT="$(/usr/bin/time -f "time: %U %S" $EXE -x1 2>&1)"
+  RACE="$(echo "$OUTPUT" | grep "race")"
+  if [ -n "$RACE" ] ; then
+    ((++COUNT_DATA_RACE))
+  fi
+
+  TIME="$(echo "$OUTPUT" | grep -o "time: .\... .\...")"
+  TIME_USER_S="$(echo "$TIME" | cut -d' ' -f2 | cut -d'.' -f1)"
+  TIME_USER_CS="$(echo "$TIME" | cut -d' ' -f2 | cut -d'.' -f2)"
+  TIME_SYSTEM_S="$(echo "$TIME" | cut -d' ' -f3 | cut -d'.' -f1)"
+  TIME_SYSTEM_CS="$(echo "$TIME" | cut -d' ' -f3 | cut -d'.' -f2)"
+
+  TIME_EXE=$((10#$TIME_USER_S * 1000 + 10#$TIME_USER_CS * 10 + 10#$TIME_SYSTEM_S * 1000 + 10#$TIME_SYSTEM_CS * 10))
+  COUNT_TIME=$((COUNT_TIME + TIME_EXE))
+done
+
+#rm $ERROR_FILE
+
+AVG_DATA_RACE=$(echo "${COUNT_DATA_RACE} * 100 / ${TOTAL_RUN}" | bc -l | xargs printf "%.1f")
+AVG_TIME_INT=$(echo "${COUNT_TIME} / ${TOTAL_RUN} + 0.5" | bc -l | xargs printf "%.0f")
+
+# -3 / log(1 - p) < n
+#NO_99=$(echo "-3 / (l(1 - (${AVG_DATA_RACE} / 100)) / l(10)) + 0.5" | bc -l | xargs printf "%.0f")
+#TIME_99=$(echo "${NO_99} * ${AVG_TIME_INT}" | bc -l)
+
+echo "Runs: $TOTAL_RUN | Data races: $COUNT_DATA_RACE | Total time: ${COUNT_TIME}ms"
+echo "Time: ${AVG_TIME_INT}ms | Race rate: ${AVG_DATA_RACE}%"
+#echo "Time: ${AVG_TIME_INT}ms | Race rate: ${AVG_DATA_RACE}% | No. 99.9%: ${NO_99} | Time 99.9%: ${TIME_99}ms"
diff --git a/cdschecker_modified_benchmarks/test_all.sh b/cdschecker_modified_benchmarks/test_all.sh
new file mode 100755 (executable)
index 0000000..a7200eb
--- /dev/null
@@ -0,0 +1,13 @@
+#!/bin/bash
+set -e
+set -u
+
+# Paul: skip `spsc-queue` as it deadlocks.
+
+for t in barrier chase-lev-deque dekker-fences linuxrwlocks mcs-lock mpmc-queue ms-queue; do
+  cd $t
+  echo -n "$t " 
+  ../test.sh ./$t
+  cd ..
+done
+