From: weiyu <weiyuluo1232@gmail.com>
Date: Tue, 4 Aug 2020 19:37:20 +0000 (-0700)
Subject: Add data structure benchmarks
X-Git-Url: http://demsky.eecs.uci.edu/git/?p=c11concurrency-benchmarks.git;a=commitdiff_plain;h=1491fc3840762ae57661f247ae363be83e0132a2

Add data structure benchmarks
---

diff --git a/cdschecker_modified_benchmarks/Makefile b/cdschecker_modified_benchmarks/Makefile
new file mode 100644
index 0000000..01dae3f
--- /dev/null
+++ b/cdschecker_modified_benchmarks/Makefile
@@ -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
index 0000000..22df223
--- /dev/null
+++ b/cdschecker_modified_benchmarks/barrier/Makefile
@@ -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
index 0000000..4d3c8ba
--- /dev/null
+++ b/cdschecker_modified_benchmarks/barrier/barrier.cc
@@ -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
index 0000000..b52b849
--- /dev/null
+++ b/cdschecker_modified_benchmarks/barrier/barrier.h
@@ -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
index 0000000..b103419
--- /dev/null
+++ b/cdschecker_modified_benchmarks/benchmarks.mk
@@ -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
index 0000000..73266a3
--- /dev/null
+++ b/cdschecker_modified_benchmarks/chase-lev-deque/Makefile
@@ -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
index 0000000..feb3fc9
--- /dev/null
+++ b/cdschecker_modified_benchmarks/chase-lev-deque/deque.cc
@@ -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
index 0000000..c65da6f
--- /dev/null
+++ b/cdschecker_modified_benchmarks/chase-lev-deque/deque.h
@@ -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
index 0000000..706d812
--- /dev/null
+++ b/cdschecker_modified_benchmarks/chase-lev-deque/main.cc
@@ -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
index 0000000..ffbb77a
--- /dev/null
+++ b/cdschecker_modified_benchmarks/dekker-fences/Makefile
@@ -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
index 0000000..30a3633
--- /dev/null
+++ b/cdschecker_modified_benchmarks/dekker-fences/dekker-fences.cc
@@ -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
index 0000000..aa71b59
--- /dev/null
+++ b/cdschecker_modified_benchmarks/include/cds_atomic.h
@@ -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
index 0000000..5b13720
--- /dev/null
+++ b/cdschecker_modified_benchmarks/include/cds_threads.h
@@ -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
index 0000000..2445139
--- /dev/null
+++ b/cdschecker_modified_benchmarks/include/librace.h
@@ -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
index 0000000..5cba524
--- /dev/null
+++ b/cdschecker_modified_benchmarks/include/model-assert.h
@@ -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
index 0000000..555ec9b
--- /dev/null
+++ b/cdschecker_modified_benchmarks/include/unrelacy.h
@@ -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
index 0000000..b0c4612
--- /dev/null
+++ b/cdschecker_modified_benchmarks/linuxrwlocks/Makefile
@@ -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
index 0000000..73e3a68
--- /dev/null
+++ b/cdschecker_modified_benchmarks/linuxrwlocks/linuxrwlocks.cc
@@ -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
index 0000000..5a311b3
--- /dev/null
+++ b/cdschecker_modified_benchmarks/mcs-lock/Makefile
@@ -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
index 0000000..4fc4f0f
--- /dev/null
+++ b/cdschecker_modified_benchmarks/mcs-lock/mcs-lock.cc
@@ -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
index 0000000..d54e19b
--- /dev/null
+++ b/cdschecker_modified_benchmarks/mcs-lock/mcs-lock.h
@@ -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
index 0000000..560074f
--- /dev/null
+++ b/cdschecker_modified_benchmarks/mpmc-queue/Makefile
@@ -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
index 0000000..038fac3
--- /dev/null
+++ b/cdschecker_modified_benchmarks/mpmc-queue/mpmc-queue.cc
@@ -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
index 0000000..f86bec4
--- /dev/null
+++ b/cdschecker_modified_benchmarks/mpmc-queue/mpmc-queue.h
@@ -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
index 0000000..151ad71
--- /dev/null
+++ b/cdschecker_modified_benchmarks/ms-queue-tsan11/Makefile
@@ -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
index 0000000..e4bb181
--- /dev/null
+++ b/cdschecker_modified_benchmarks/ms-queue-tsan11/main.cc
@@ -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
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
index 0000000..be84c7d
--- /dev/null
+++ b/cdschecker_modified_benchmarks/ms-queue-tsan11/my_queue.cc
@@ -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
index 0000000..45849a4
--- /dev/null
+++ b/cdschecker_modified_benchmarks/ms-queue-tsan11/my_queue.h
@@ -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
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
index 0000000..c42add1
--- /dev/null
+++ b/cdschecker_modified_benchmarks/ms-queue/Makefile
@@ -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
index 0000000..fc31f9c
--- /dev/null
+++ b/cdschecker_modified_benchmarks/ms-queue/main.cc
@@ -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
index 0000000..b868d2e
--- /dev/null
+++ b/cdschecker_modified_benchmarks/ms-queue/my_queue.c.correct
@@ -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
index 0000000..d746bda
--- /dev/null
+++ b/cdschecker_modified_benchmarks/ms-queue/my_queue.cc
@@ -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
index 0000000..8bb8d58
--- /dev/null
+++ b/cdschecker_modified_benchmarks/ms-queue/my_queue.h
@@ -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
index 0000000..33b9d01
--- /dev/null
+++ b/cdschecker_modified_benchmarks/spsc-queue/Makefile
@@ -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
index 0000000..9eadcf3
--- /dev/null
+++ b/cdschecker_modified_benchmarks/spsc-queue/eventcount-relacy.h
@@ -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
index 0000000..f2b05f7
--- /dev/null
+++ b/cdschecker_modified_benchmarks/spsc-queue/eventcount.h
@@ -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
index 0000000..71aac2a
--- /dev/null
+++ b/cdschecker_modified_benchmarks/spsc-queue/queue-relacy.h
@@ -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
index 0000000..c77425f
--- /dev/null
+++ b/cdschecker_modified_benchmarks/spsc-queue/queue.h
@@ -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
index 0000000..1347f4e
--- /dev/null
+++ b/cdschecker_modified_benchmarks/spsc-queue/spsc-queue.cc
@@ -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
index 0000000..37ed989
--- /dev/null
+++ b/cdschecker_modified_benchmarks/spsc-queue/spsc-relacy.cc
@@ -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
index 0000000..ff2c3b5
--- /dev/null
+++ b/cdschecker_modified_benchmarks/test.sh
@@ -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
index 0000000..a7200eb
--- /dev/null
+++ b/cdschecker_modified_benchmarks/test_all.sh
@@ -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
+