From: Brian Demsky <bdemsky@uci.edu>
Date: Sat, 7 Dec 2019 07:32:20 +0000 (-0800)
Subject: remove test cases
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=26ef34009330baf200909efe2e71c094e0ce022d;p=c11tester.git

remove test cases
---

diff --git a/test/Makefile b/test/Makefile
deleted file mode 100644
index 9d7acb08..00000000
--- a/test/Makefile
+++ /dev/null
@@ -1,26 +0,0 @@
-BASE := ..
-
-OBJECTS := $(patsubst %.c, %.o, $(wildcard *.c))
-OBJECTS += $(patsubst %.cc, %.o, $(wildcard *.cc))
-
-include $(BASE)/common.mk
-
-DIR := litmus
-include $(DIR)/Makefile
-
-DEPS := $(join $(addsuffix ., $(dir $(OBJECTS))), $(addsuffix .d, $(notdir $(OBJECTS))))
-
-CPPFLAGS += -I$(BASE) -I$(BASE)/include
-
-all: $(OBJECTS)
-
--include $(DEPS)
-
-%.o: %.c
-	$(CC) -MMD -MF $(@D)/.$(@F).d -o $@ $< $(CPPFLAGS) -L$(BASE) -l$(LIB_NAME)
-
-%.o: %.cc
-	$(CXX) -MMD -MF $(@D)/.$(@F).d -o $@ $< $(CPPFLAGS) -L$(BASE) -l$(LIB_NAME)
-
-clean::
-	rm -f $(OBJECTS) $(DEPS)
diff --git a/test/addr-satcycle.cc b/test/addr-satcycle.cc
deleted file mode 100644
index 699f1938..00000000
--- a/test/addr-satcycle.cc
+++ /dev/null
@@ -1,67 +0,0 @@
-/**
- * @file addr-satcycle.cc
- * @brief Address-based satisfaction cycle test
- *
- * This program has a peculiar behavior which is technically legal under the
- * current C++ memory model but which is a result of a type of satisfaction
- * cycle. We use this as justification for part of our modifications to the
- * memory model when proving our model-checker's correctness.
- */
-
-#include <atomic>
-#include <threads.h>
-#include <stdio.h>
-
-#include "model-assert.h"
-
-using namespace std;
-
-atomic_int x[2], idx, y;
-
-int r1, r2, r3;	/* "local" variables */
-
-static void a(void *obj)
-{
-	r1 = idx.load(memory_order_relaxed);
-	x[r1].store(0, memory_order_relaxed);
-
-	/* Key point: can we guarantee that &x[0] == &x[r1]? */
-	r2 = x[0].load(memory_order_relaxed);
-	y.store(r2);
-}
-
-static void b(void *obj)
-{
-	r3 = y.load(memory_order_relaxed);
-	idx.store(r3, memory_order_relaxed);
-}
-
-int user_main(int argc, char **argv)
-{
-	thrd_t t1, t2;
-
-	atomic_init(&x[0], 1);
-	atomic_init(&idx, 0);
-	atomic_init(&y, 0);
-
-	printf("Main thread: creating 2 threads\n");
-	thrd_create(&t1, (thrd_start_t)&a, NULL);
-	thrd_create(&t2, (thrd_start_t)&b, NULL);
-
-	thrd_join(t1);
-	thrd_join(t2);
-	printf("Main thread is finished\n");
-
-	printf("r1 = %d\n", r1);
-	printf("r2 = %d\n", r2);
-	printf("r3 = %d\n", r3);
-
-	/*
-	 * This condition should not be hit because it only occurs under a
-	 * satisfaction cycle
-	 */
-	bool cycle = (r1 == 1 && r2 == 1 && r3 == 1);
-	MODEL_ASSERT(!cycle);
-
-	return 0;
-}
diff --git a/test/condvar.cc b/test/condvar.cc
deleted file mode 100644
index 94bd8dbb..00000000
--- a/test/condvar.cc
+++ /dev/null
@@ -1,44 +0,0 @@
-#include <stdio.h>
-
-#include "threads.h"
-#include "librace.h"
-#include "stdatomic2.h"
-#include <mutex.h>
-#include <condition_variable>
-
-cdsc::mutex * m;
-cdsc::condition_variable *v;
-int shareddata;
-
-static void a(void *obj)
-{
-
-	m->lock();
-	while(load_32(&shareddata)==0)
-		v->wait(*m);
-	m->unlock();
-
-}
-
-static void b(void *obj)
-{
-	m->lock();
-	store_32(&shareddata, (unsigned int) 1);
-	v->notify_all();
-	m->unlock();
-}
-
-int user_main(int argc, char **argv)
-{
-	thrd_t t1, t2;
-	store_32(&shareddata, (unsigned int) 0);
-	m=new cdsc::mutex();
-	v=new cdsc::condition_variable();
-
-	thrd_create(&t1, (thrd_start_t)&a, NULL);
-	thrd_create(&t2, (thrd_start_t)&b, NULL);
-
-	thrd_join(t1);
-	thrd_join(t2);
-	return 0;
-}
diff --git a/test/csetest.c b/test/csetest.c
deleted file mode 100644
index 2058f9c2..00000000
--- a/test/csetest.c
+++ /dev/null
@@ -1,43 +0,0 @@
-#include <stdio.h>
-#include <threads.h>
-#include <stdatomic.h>
-
-#include "librace.h"
-
-atomic_int a;
-atomic_int b;
-
-static void r(void *obj)
-{
-	int r1=atomic_load_explicit(&a, memory_order_relaxed);
-	int r2=atomic_load_explicit(&a, memory_order_relaxed);
-	if (r1==r2)
-		atomic_store_explicit(&b, 2, memory_order_relaxed);
-	printf("r1=%d\n",r1);
-	printf("r2=%d\n",r2);
-}
-
-static void s(void *obj)
-{
-	int r3=atomic_load_explicit(&b, memory_order_relaxed);
-	atomic_store_explicit(&a, r3, memory_order_relaxed);
-	printf("r3=%d\n",r3);
-}
-
-int user_main(int argc, char **argv)
-{
-	thrd_t t1, t2;
-
-	atomic_init(&a, 0);
-	atomic_init(&b, 1);
-
-	printf("Main thread: creating 2 threads\n");
-	thrd_create(&t1, (thrd_start_t)&r, NULL);
-	thrd_create(&t2, (thrd_start_t)&s, NULL);
-
-	thrd_join(t1);
-	thrd_join(t2);
-	printf("Main thread is finished\n");
-
-	return 0;
-}
diff --git a/test/deadlock.cc b/test/deadlock.cc
deleted file mode 100644
index 4810aa45..00000000
--- a/test/deadlock.cc
+++ /dev/null
@@ -1,46 +0,0 @@
-#include <stdio.h>
-#include <threads.h>
-#include <mutex>
-
-#include "librace.h"
-
-std::mutex *x;
-std::mutex *y;
-uint32_t shared = 0;
-
-static void a(void *obj)
-{
-	x->lock();
-	y->lock();
-	printf("shared = %u\n", load_32(&shared));
-	y->unlock();
-	x->unlock();
-}
-
-static void b(void *obj)
-{
-	y->lock();
-	x->lock();
-	store_32(&shared, 16);
-	printf("write shared = 16\n");
-	x->unlock();
-	y->unlock();
-}
-
-int user_main(int argc, char **argv)
-{
-	thrd_t t1, t2;
-
-	x = new std::mutex();
-	y = new std::mutex();
-
-	printf("Main thread: creating 2 threads\n");
-	thrd_create(&t1, (thrd_start_t)&a, NULL);
-	thrd_create(&t2, (thrd_start_t)&b, NULL);
-
-	thrd_join(t1);
-	thrd_join(t2);
-	printf("Main thread is finished\n");
-
-	return 0;
-}
diff --git a/test/double-read-fv.c b/test/double-read-fv.c
deleted file mode 100755
index 120cdc3a..00000000
--- a/test/double-read-fv.c
+++ /dev/null
@@ -1,50 +0,0 @@
-/*
- * Try to read the same value as a future value twice.
- *
- * This test should be able to see r1 = r2 = 42. Currently, we never see that
- * (as of 2/21/13) because the r2 load won't have a potential future value of
- * 42 at the same time as r1, due to our scheduling (the loads for r1 and r2
- * must occur before the write of x = 42).
- *
- * Note that the atomic_int y is simply used to aid in forcing a particularly
- * interesting scheduling. It is superfluous.
- */
-#include <stdio.h>
-#include <threads.h>
-#include <stdatomic.h>
-
-#include "librace.h"
-
-atomic_int x;
-atomic_int y;
-
-static void a(void *obj)
-{
-	int r1 = atomic_load_explicit(&x, memory_order_relaxed);
-	int r2 = atomic_load_explicit(&x, memory_order_relaxed);
-	printf("r1 = %d, r2 = %d\n", r1, r2);
-}
-
-static void b(void *obj)
-{
-	atomic_store_explicit(&y, 43, memory_order_relaxed);
-	atomic_store_explicit(&x, 42, memory_order_relaxed);
-}
-
-int user_main(int argc, char **argv)
-{
-	thrd_t t1, t2;
-
-	atomic_init(&x, 0);
-	atomic_init(&y, 0);
-
-	printf("Main thread: creating 2 threads\n");
-	thrd_create(&t1, (thrd_start_t)&a, NULL);
-	thrd_create(&t2, (thrd_start_t)&b, NULL);
-
-	thrd_join(t1);
-	thrd_join(t2);
-	printf("Main thread is finished\n");
-
-	return 0;
-}
diff --git a/test/double-relseq.c b/test/double-relseq.c
deleted file mode 100644
index 2ad1987a..00000000
--- a/test/double-relseq.c
+++ /dev/null
@@ -1,59 +0,0 @@
-/*
- * This test performs some relaxed, release, acquire opeations on a single
- * atomic variable. It can give some rough idea of release sequence support but
- * probably should be improved to give better information.
- *
- * This test tries to establish two release sequences, where we should always
- * either establish both or establish neither. (Note that this is only true for
- * a few executions of interest, where both load-acquire's read from the same
- * write.)
- */
-
-#include <stdio.h>
-#include <threads.h>
-#include <stdatomic.h>
-
-#include "librace.h"
-
-atomic_int x;
-int var = 0;
-
-static void a(void *obj)
-{
-	store_32(&var, 1);
-	atomic_store_explicit(&x, 1, memory_order_release);
-	atomic_store_explicit(&x, 42, memory_order_relaxed);
-}
-
-static void b(void *obj)
-{
-	int r = atomic_load_explicit(&x, memory_order_acquire);
-	printf("r = %d\n", r);
-	printf("load %d\n", load_32(&var));
-}
-
-static void c(void *obj)
-{
-	atomic_store_explicit(&x, 2, memory_order_relaxed);
-}
-
-int user_main(int argc, char **argv)
-{
-	thrd_t t1, t2, t3, t4;
-
-	atomic_init(&x, 0);
-
-	printf("Main thread: creating 4 threads\n");
-	thrd_create(&t1, (thrd_start_t)&a, NULL);
-	thrd_create(&t2, (thrd_start_t)&b, NULL);
-	thrd_create(&t3, (thrd_start_t)&b, NULL);
-	thrd_create(&t4, (thrd_start_t)&c, NULL);
-
-	thrd_join(t1);
-	thrd_join(t2);
-	thrd_join(t3);
-	thrd_join(t4);
-	printf("Main thread is finished\n");
-
-	return 0;
-}
diff --git a/test/fences.c b/test/fences.c
deleted file mode 100644
index 4d0328fd..00000000
--- a/test/fences.c
+++ /dev/null
@@ -1,42 +0,0 @@
-#include <stdio.h>
-#include <threads.h>
-#include <stdatomic.h>
-
-#include "librace.h"
-
-atomic_int x;
-atomic_int y;
-
-static void a(void *obj)
-{
-	atomic_store_explicit(&x, 1, memory_order_relaxed);
-	atomic_store_explicit(&x, 2, memory_order_relaxed);
-	atomic_thread_fence(memory_order_seq_cst);
-	printf("Thread A reads: %d\n", atomic_load_explicit(&y, memory_order_relaxed));
-}
-
-static void b(void *obj)
-{
-	atomic_store_explicit(&y, 1, memory_order_relaxed);
-	atomic_store_explicit(&y, 2, memory_order_relaxed);
-	atomic_thread_fence(memory_order_seq_cst);
-	printf("Thread B reads: %d\n", atomic_load_explicit(&x, memory_order_relaxed));
-}
-
-int user_main(int argc, char **argv)
-{
-	thrd_t t1, t2;
-
-	atomic_init(&x, 0);
-	atomic_init(&y, 0);
-
-	printf("Main thread: creating 2 threads\n");
-	thrd_create(&t1, (thrd_start_t)&a, NULL);
-	thrd_create(&t2, (thrd_start_t)&b, NULL);
-
-	thrd_join(t1);
-	thrd_join(t2);
-	printf("Main thread is finishing\n");
-
-	return 0;
-}
diff --git a/test/fences2.c b/test/fences2.c
deleted file mode 100644
index 2c80d617..00000000
--- a/test/fences2.c
+++ /dev/null
@@ -1,46 +0,0 @@
-#include <stdio.h>
-#include <threads.h>
-#include <stdatomic.h>
-
-#include "librace.h"
-#include "model-assert.h"
-
-atomic_int x;
-atomic_int y;
-
-static void a(void *obj)
-{
-	atomic_store_explicit(&x, 1, memory_order_relaxed);
-	atomic_thread_fence(memory_order_release);
-	atomic_store_explicit(&x, 2, memory_order_relaxed);
-}
-
-static void b(void *obj)
-{
-	int r1, r2;
-	r1 = atomic_load_explicit(&x, memory_order_relaxed);
-	atomic_thread_fence(memory_order_acquire);
-	r2 = atomic_load_explicit(&x, memory_order_relaxed);
-
-	printf("FENCES: r1 = %d, r2 = %d\n", r1, r2);
-	if (r1 == 2)
-		MODEL_ASSERT(r2 != 1);
-}
-
-int user_main(int argc, char **argv)
-{
-	thrd_t t1, t2;
-
-	atomic_init(&x, 0);
-	atomic_init(&y, 0);
-
-	printf("Main thread: creating 2 threads\n");
-	thrd_create(&t1, (thrd_start_t)&a, NULL);
-	thrd_create(&t2, (thrd_start_t)&b, NULL);
-
-	thrd_join(t1);
-	thrd_join(t2);
-	printf("Main thread is finishing\n");
-
-	return 0;
-}
diff --git a/test/insanesync.cc b/test/insanesync.cc
deleted file mode 100644
index 60fbc8dc..00000000
--- a/test/insanesync.cc
+++ /dev/null
@@ -1,69 +0,0 @@
-#include <stdlib.h>
-#include <stdio.h>
-#include <threads.h>
-#include <atomic>
-
-#include "librace.h"
-#include "model-assert.h"
-
-using namespace std;
-
-atomic_int x, y;
-atomic_intptr_t z, z2;
-
-int r1, r2, r3;	/* "local" variables */
-
-/**
-                This example illustrates a self-satisfying cycle involving
-                synchronization.  A failed synchronization creates the store that
-                causes the synchronization to fail.
-
-                The C++11 memory model nominally allows r1=0, r2=1, r3=5.
-
-                This example is insane, we don't support that behavior.
- */
-
-
-static void a(void *obj)
-{
-	z.store((intptr_t)&y, memory_order_relaxed);
-	r1 = y.fetch_add(1, memory_order_release);
-	z.store((intptr_t)&x, memory_order_relaxed);
-	r2 = y.fetch_add(1, memory_order_release);
-}
-
-
-static void b(void *obj)
-{
-	r3 = y.fetch_add(1, memory_order_acquire);
-	intptr_t ptr = z.load(memory_order_relaxed);
-	z2.store(ptr, memory_order_relaxed);
-}
-
-static void c(void *obj)
-{
-	atomic_int *ptr2 = (atomic_int *)z2.load(memory_order_relaxed);
-	(*ptr2).store(5, memory_order_relaxed);
-}
-
-int user_main(int argc, char **argv)
-{
-	thrd_t t1, t2, t3;
-
-	atomic_init(&x, 0);
-	atomic_init(&y, 0);
-	atomic_init(&z, (intptr_t) &x);
-	atomic_init(&z2, (intptr_t) &x);
-
-	thrd_create(&t1, (thrd_start_t)&a, NULL);
-	thrd_create(&t2, (thrd_start_t)&b, NULL);
-	thrd_create(&t3, (thrd_start_t)&c, NULL);
-
-	thrd_join(t1);
-	thrd_join(t2);
-	thrd_join(t3);
-
-	printf("r1=%d, r2=%d, r3=%d\n", r1, r2, r3);
-
-	return 0;
-}
diff --git a/test/iriw.cc b/test/iriw.cc
deleted file mode 100644
index 61463657..00000000
--- a/test/iriw.cc
+++ /dev/null
@@ -1,66 +0,0 @@
-/**
- * @file iriw.cc
- * @brief Independent read and independent write test
- */
-
-#include <atomic>
-#include <threads.h>
-#include <stdio.h>
-
-#include "wildcard.h"
-#include "model-assert.h"
-
-using namespace std;
-
-atomic_int x, y;
-int r1, r2, r3, r4;	/* "local" variables */
-
-static void a(void *obj)
-{
-	x.store(1, memory_order_seq_cst);
-}
-
-static void b(void *obj)
-{
-	y.store(1, memory_order_seq_cst);
-}
-
-static void c(void *obj)
-{
-	r1 = x.load(memory_order_acquire);
-	r2 = y.load(memory_order_seq_cst);
-}
-
-static void d(void *obj)
-{
-	r3 = y.load(memory_order_acquire);
-	r4 = x.load(memory_order_seq_cst);
-}
-
-
-int user_main(int argc, char **argv)
-{
-	thrd_t t1, t2, t3, t4;
-
-	atomic_init(&x, 0);
-	atomic_init(&y, 0);
-
-	printf("Main thread: creating 4 threads\n");
-	thrd_create(&t1, (thrd_start_t)&a, NULL);
-	thrd_create(&t2, (thrd_start_t)&b, NULL);
-	thrd_create(&t3, (thrd_start_t)&c, NULL);
-	thrd_create(&t4, (thrd_start_t)&d, NULL);
-
-	thrd_join(t1);
-	thrd_join(t2);
-	thrd_join(t3);
-	thrd_join(t4);
-	printf("Main thread is finished\n");
-
-	/*
-	 * This condition should not be hit if the execution is SC */
-	bool sc = (r1 == 1 && r2 == 0 && r3 == 1 && r4 == 0);
-	printf("r1 = %d, r2 = %d, r3 = %d and r4 = %d\n", r1, r2, r3, r4);
-	MODEL_ASSERT(!sc);
-	return 0;
-}
diff --git a/test/iriw_wildcard.cc b/test/iriw_wildcard.cc
deleted file mode 100644
index 0d68b6ef..00000000
--- a/test/iriw_wildcard.cc
+++ /dev/null
@@ -1,66 +0,0 @@
-/**
- * @file iriw.cc
- * @brief Independent read and independent write test
- */
-
-#include <atomic>
-#include <threads.h>
-#include <stdio.h>
-
-#include "wildcard.h"
-#include "model-assert.h"
-
-using namespace std;
-
-atomic_int x, y;
-int r1, r2, r3, r4;	/* "local" variables */
-
-static void a(void *obj)
-{
-	x.store(1, wildcard(1));
-}
-
-static void b(void *obj)
-{
-	y.store(1, wildcard(2));
-}
-
-static void c(void *obj)
-{
-	r1 = x.load(wildcard(3));
-	r2 = y.load(wildcard(4));
-}
-
-static void d(void *obj)
-{
-	r3 = y.load(wildcard(5));
-	r4 = x.load(wildcard(6));
-}
-
-
-int user_main(int argc, char **argv)
-{
-	thrd_t t1, t2, t3, t4;
-
-	atomic_init(&x, 0);
-	atomic_init(&y, 0);
-
-	printf("Main thread: creating 4 threads\n");
-	thrd_create(&t1, (thrd_start_t)&a, NULL);
-	thrd_create(&t2, (thrd_start_t)&b, NULL);
-	thrd_create(&t3, (thrd_start_t)&c, NULL);
-	thrd_create(&t4, (thrd_start_t)&d, NULL);
-
-	thrd_join(t1);
-	thrd_join(t2);
-	thrd_join(t3);
-	thrd_join(t4);
-	printf("Main thread is finished\n");
-
-	/*
-	 * This condition should not be hit if the execution is SC */
-	bool sc = (r1 == 1 && r2 == 0 && r3 == 1 && r4 == 0);
-	//MODEL_ASSERT(!sc);
-
-	return 0;
-}
diff --git a/test/linuxrwlocks.c b/test/linuxrwlocks.c
deleted file mode 100644
index 3d075aa8..00000000
--- a/test/linuxrwlocks.c
+++ /dev/null
@@ -1,112 +0,0 @@
-#include <stdio.h>
-#include <threads.h>
-#include <stdatomic.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);
-		do {
-			priorvalue = atomic_load_explicit(&rw->lock, memory_order_relaxed);
-		} while (priorvalue <= 0);
-		priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
-	}
-}
-
-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);
-		do {
-			priorvalue = atomic_load_explicit(&rw->lock, memory_order_relaxed);
-		} while (priorvalue != RW_LOCK_BIAS);
-		priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
-	}
-}
-
-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;
-
-static void a(void *obj)
-{
-	int i;
-	for(i = 0;i < 2;i++) {
-		if ((i % 2) == 0) {
-			read_lock(&mylock);
-			load_32(&shareddata);
-			read_unlock(&mylock);
-		} else {
-			write_lock(&mylock);
-			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);
-
-	thrd_create(&t1, (thrd_start_t)&a, NULL);
-	thrd_create(&t2, (thrd_start_t)&a, NULL);
-
-	thrd_join(t1);
-	thrd_join(t2);
-
-	return 0;
-}
diff --git a/test/linuxrwlocksyield.c b/test/linuxrwlocksyield.c
deleted file mode 100644
index e3a4a605..00000000
--- a/test/linuxrwlocksyield.c
+++ /dev/null
@@ -1,112 +0,0 @@
-#include <stdio.h>
-#include <threads.h>
-#include <stdatomic.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_acquire);
-	}
-}
-
-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_acquire);
-	}
-}
-
-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;
-
-static void a(void *obj)
-{
-	int i;
-	for(i = 0;i < 2;i++) {
-		if ((i % 2) == 0) {
-			read_lock(&mylock);
-			load_32(&shareddata);
-			read_unlock(&mylock);
-		} else {
-			write_lock(&mylock);
-			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);
-
-	thrd_create(&t1, (thrd_start_t)&a, NULL);
-	thrd_create(&t2, (thrd_start_t)&a, NULL);
-
-	thrd_join(t1);
-	thrd_join(t2);
-
-	return 0;
-}
diff --git a/test/litmus/Makefile b/test/litmus/Makefile
deleted file mode 100644
index a4a19b7b..00000000
--- a/test/litmus/Makefile
+++ /dev/null
@@ -1,4 +0,0 @@
-D := $(DIR)
-
-OBJECTS += $(patsubst %.c, %.o, $(wildcard $(D)/*.c))
-OBJECTS += $(patsubst %.cc, %.o, $(wildcard $(D)/*.cc))
diff --git a/test/litmus/iriw.cc b/test/litmus/iriw.cc
deleted file mode 100644
index fa4a0341..00000000
--- a/test/litmus/iriw.cc
+++ /dev/null
@@ -1,57 +0,0 @@
-#include <stdio.h>
-#include <threads.h>
-#include <atomic>
-
-std::atomic_int x;
-std::atomic_int y;
-
-std::memory_order store_mo = std::memory_order_release;
-std::memory_order load_mo = std::memory_order_acquire;
-
-static void a(void *obj)
-{
-	x.store(1, store_mo);
-}
-
-static void b(void *obj)
-{
-	y.store(1, store_mo);
-}
-
-static void c(void *obj)
-{
-	printf("x1: %d\n", x.load(load_mo));
-	printf("y1: %d\n", y.load(load_mo));
-}
-
-static void d(void *obj)
-{
-	printf("y2: %d\n", y.load(load_mo));
-	printf("x2: %d\n", x.load(load_mo));
-}
-
-int user_main(int argc, char **argv)
-{
-	thrd_t t1, t2, t3, t4;
-
-	/* Command-line argument 's' enables seq_cst test */
-	if (argc > 1 && *argv[1] == 's')
-		store_mo = load_mo = std::memory_order_seq_cst;
-
-	atomic_init(&x, 0);
-	atomic_init(&y, 0);
-
-	printf("Main thread: creating 4 threads\n");
-	thrd_create(&t1, (thrd_start_t)&a, NULL);
-	thrd_create(&t2, (thrd_start_t)&b, NULL);
-	thrd_create(&t3, (thrd_start_t)&c, NULL);
-	thrd_create(&t4, (thrd_start_t)&d, NULL);
-
-	thrd_join(t1);
-	thrd_join(t2);
-	thrd_join(t3);
-	thrd_join(t4);
-	printf("Main thread is finished\n");
-
-	return 0;
-}
diff --git a/test/litmus/load-buffer.cc b/test/litmus/load-buffer.cc
deleted file mode 100644
index 9c9923cc..00000000
--- a/test/litmus/load-buffer.cc
+++ /dev/null
@@ -1,36 +0,0 @@
-#include <stdio.h>
-#include <threads.h>
-#include <atomic>
-
-std::atomic_int x;
-std::atomic_int y;
-
-static void a(void *obj)
-{
-	printf("x: %d\n", x.load(std::memory_order_relaxed));
-	y.store(1, std::memory_order_relaxed);
-}
-
-static void b(void *obj)
-{
-	printf("y: %d\n", y.load(std::memory_order_relaxed));
-	x.store(1, std::memory_order_relaxed);
-}
-
-int user_main(int argc, char **argv)
-{
-	thrd_t t1, t2;
-
-	atomic_init(&x, 0);
-	atomic_init(&y, 0);
-
-	printf("Main thread: creating 2 threads\n");
-	thrd_create(&t1, (thrd_start_t)&a, NULL);
-	thrd_create(&t2, (thrd_start_t)&b, NULL);
-
-	thrd_join(t1);
-	thrd_join(t2);
-	printf("Main thread is finished\n");
-
-	return 0;
-}
diff --git a/test/litmus/message-passing.cc b/test/litmus/message-passing.cc
deleted file mode 100644
index 6ef41eb4..00000000
--- a/test/litmus/message-passing.cc
+++ /dev/null
@@ -1,44 +0,0 @@
-#include <stdio.h>
-#include <threads.h>
-#include <atomic>
-
-std::atomic_int x;
-std::atomic_int y;
-
-static void a(void *obj)
-{
-	x.store(1, std::memory_order_relaxed);
-	y.store(1, std::memory_order_relaxed);
-}
-
-static void b(void *obj)
-{
-	printf("y1: %d\n", y.load(std::memory_order_relaxed));
-	printf("x1: %d\n", x.load(std::memory_order_relaxed));
-}
-
-static void c(void *obj)
-{
-	printf("x2: %d\n", x.load(std::memory_order_relaxed));
-	printf("y2: %d\n", y.load(std::memory_order_relaxed));
-}
-
-int user_main(int argc, char **argv)
-{
-	thrd_t t1, t2, t3;
-
-	atomic_init(&x, 0);
-	atomic_init(&y, 0);
-
-	printf("Main thread: creating 3 threads\n");
-	thrd_create(&t1, (thrd_start_t)&a, NULL);
-	thrd_create(&t2, (thrd_start_t)&b, NULL);
-	thrd_create(&t3, (thrd_start_t)&c, NULL);
-
-	thrd_join(t1);
-	thrd_join(t2);
-	thrd_join(t3);
-	printf("Main thread is finished\n");
-
-	return 0;
-}
diff --git a/test/litmus/seq-lock.cc b/test/litmus/seq-lock.cc
deleted file mode 100644
index 03724e6f..00000000
--- a/test/litmus/seq-lock.cc
+++ /dev/null
@@ -1,67 +0,0 @@
-#include <stdlib.h>
-#include <stdio.h>
-#include <threads.h>
-#include <atomic>
-
-#include "model-assert.h"
-
-/*
- * This 'seqlock' example should never trigger the MODEL_ASSERT() for
- * release/acquire; it may trigger the MODEL_ASSERT() for release/consume
- */
-
-std::atomic_int x;
-std::atomic_int y;
-std::atomic_int z;
-
-static int N = 1;
-
-static void a(void *obj)
-{
-	for (int i = 0; i < N; i++) {
-		x.store(2 * i + 1, std::memory_order_release);
-		y.store(i + 1, std::memory_order_release);
-		z.store(i + 1, std::memory_order_release);
-		x.store(2 * i + 2, std::memory_order_release);
-	}
-}
-
-static void b(void *obj)
-{
-	int x1, y1, z1, x2;
-	x1 = x.load(std::memory_order_acquire);
-	y1 = y.load(std::memory_order_acquire);
-	z1 = z.load(std::memory_order_acquire);
-	x2 = x.load(std::memory_order_acquire);
-	printf("x: %d\n", x1);
-	printf("y: %d\n", y1);
-	printf("z: %d\n", z1);
-	printf("x: %d\n", x2);
-
-	/* If x1 and x2 are the same, even value, then y1 must equal z1 */
-	MODEL_ASSERT(x1 != x2 || x1 & 0x1 || y1 == z1);
-}
-
-int user_main(int argc, char **argv)
-{
-	thrd_t t1, t2;
-
-	if (argc > 1)
-		N = atoi(argv[1]);
-
-	printf("N: %d\n", N);
-
-	atomic_init(&x, 0);
-	atomic_init(&y, 0);
-	atomic_init(&z, 0);
-
-	printf("Main thread: creating 2 threads\n");
-	thrd_create(&t1, (thrd_start_t)&a, NULL);
-	thrd_create(&t2, (thrd_start_t)&b, NULL);
-
-	thrd_join(t1);
-	thrd_join(t2);
-	printf("Main thread is finished\n");
-
-	return 0;
-}
diff --git a/test/litmus/store-buffer.cc b/test/litmus/store-buffer.cc
deleted file mode 100644
index eb43d44e..00000000
--- a/test/litmus/store-buffer.cc
+++ /dev/null
@@ -1,36 +0,0 @@
-#include <stdio.h>
-#include <threads.h>
-#include <atomic>
-
-std::atomic_int x;
-std::atomic_int y;
-
-static void a(void *obj)
-{
-	x.store(1, std::memory_order_relaxed);
-	printf("y: %d\n", y.load(std::memory_order_relaxed));
-}
-
-static void b(void *obj)
-{
-	y.store(1, std::memory_order_relaxed);
-	printf("x: %d\n", x.load(std::memory_order_relaxed));
-}
-
-int user_main(int argc, char **argv)
-{
-	thrd_t t1, t2;
-
-	atomic_init(&x, 0);
-	atomic_init(&y, 0);
-
-	printf("Main thread: creating 2 threads\n");
-	thrd_create(&t1, (thrd_start_t)&a, NULL);
-	thrd_create(&t2, (thrd_start_t)&b, NULL);
-
-	thrd_join(t1);
-	thrd_join(t2);
-	printf("Main thread is finished\n");
-
-	return 0;
-}
diff --git a/test/litmus/wrc.cc b/test/litmus/wrc.cc
deleted file mode 100644
index 7d295fe1..00000000
--- a/test/litmus/wrc.cc
+++ /dev/null
@@ -1,57 +0,0 @@
-#include <stdlib.h>
-#include <stdio.h>
-#include <threads.h>
-#include <atomic>
-
-static int N = 2;
-
-/* Can be tested for different behavior with relaxed vs. release/acquire/seq-cst */
-#define load_mo std::memory_order_relaxed
-#define store_mo std::memory_order_relaxed
-
-static std::atomic_int *x;
-
-static void a(void *obj)
-{
-	int idx = *((int *)obj);
-
-	if (idx > 0)
-		x[idx - 1].load(load_mo);
-
-	if (idx < N)
-		x[idx].store(1, store_mo);
-	else
-		x[0].load(load_mo);
-}
-
-int user_main(int argc, char **argv)
-{
-	thrd_t *threads;
-	int *indexes;
-
-	if (argc > 1)
-		N = atoi(argv[1]);
-	if (N < 2) {
-		printf("Error: must have N >= 2\n");
-		return 1;
-	}
-	printf("N: %d\n", N);
-
-	threads = (thrd_t *)malloc((N + 1) * sizeof(thrd_t));
-	x = (std::atomic_int *)malloc(N * sizeof(std::atomic_int));
-	indexes = (int *)malloc((N + 1) * sizeof(int));
-	
-	for (int i = 0; i < N + 1; i++)
-		indexes[i] = i;
-
-	for (int i = 0; i < N; i++)
-		atomic_init(&x[i], 0);
-
-	for (int i = 0; i < N + 1; i++)
-		thrd_create(&threads[i], (thrd_start_t)&a, (void *)&indexes[i]);
-
-	for (int i = 0; i < N + 1; i++)
-		thrd_join(threads[i]);
-
-        return 0;
-}
diff --git a/test/memo/double-read-fv b/test/memo/double-read-fv
deleted file mode 100755
index eb48204d..00000000
Binary files a/test/memo/double-read-fv and /dev/null differ
diff --git a/test/memo/fences b/test/memo/fences
deleted file mode 100755
index 31963619..00000000
Binary files a/test/memo/fences and /dev/null differ
diff --git a/test/memo/rmw2prog b/test/memo/rmw2prog
deleted file mode 100755
index 6fbf4dd7..00000000
Binary files a/test/memo/rmw2prog and /dev/null differ
diff --git a/test/memo/script.sh b/test/memo/script.sh
deleted file mode 100755
index a97c7022..00000000
--- a/test/memo/script.sh
+++ /dev/null
@@ -1,19 +0,0 @@
-#!/bin/sh
-
-clang -Xclang -load -Xclang /scratch/llvm/build/lib/libSkeletonPass.so -c -I/scratch/random-fuzzer/include/  /scratch/random-fuzzer/test/userprog.c
-
-gcc -o userprog userprog.o -L/scratch/random-fuzzer -lmodel
-
-#clang -Xclang -load -Xclang /scratch/llvm/build/lib/libSkeletonPass.so -c -I/scratch/random-fuzzer/include/  /scratch/random-fuzzer/test/double-read-fv.c
-
-#gcc -o double-read-fv double-read-fv.o -L/scratch/random-fuzzer -lmodel
-
-#clang -Xclang -load -Xclang /scratch/llvm/build/lib/libSkeletonPass.so -c -I/scratch/random-fuzzer/include/  /scratch/random-fuzzer/test/rmw2prog.c
-
-#gcc -o rmw2prog rmw2prog.o -L/scratch/random-fuzzer -lmodel
-
-#clang -Xclang -load -Xclang /scratch/llvm/build/lib/libSkeletonPass.so -c -I/scratch/random-fuzzer/include/  /scratch/random-fuzzer/test/fences.c
-
-#gcc -o fences fences.o -L/scratch/random-fuzzer -lmodel
-
-export LD_LIBRARY_PATH=/scratch/random-fuzzer
diff --git a/test/memo/userprog b/test/memo/userprog
deleted file mode 100755
index 67443eaa..00000000
Binary files a/test/memo/userprog and /dev/null differ
diff --git a/test/mo-satcycle.cc b/test/mo-satcycle.cc
deleted file mode 100644
index f94f23f8..00000000
--- a/test/mo-satcycle.cc
+++ /dev/null
@@ -1,68 +0,0 @@
-/**
- * @file mo-satcycle.cc
- * @brief MO satisfaction cycle test
- *
- * This program has a peculiar behavior which is technically legal under the
- * current C++ memory model but which is a result of a type of satisfaction
- * cycle. We use this as justification for part of our modifications to the
- * memory model when proving our model-checker's correctness.
- */
-
-#include <atomic>
-#include <threads.h>
-#include <stdio.h>
-
-#include "model-assert.h"
-
-using namespace std;
-
-atomic_int x, y;
-int r0, r1, r2, r3;	/* "local" variables */
-
-static void a(void *obj)
-{
-	y.store(10, memory_order_relaxed);
-	x.store(1, memory_order_release);
-}
-
-static void b(void *obj)
-{
-	r0 = x.load(memory_order_relaxed);
-	r1 = x.load(memory_order_acquire);
-	y.store(11, memory_order_relaxed);
-}
-
-static void c(void *obj)
-{
-	r2 = y.load(memory_order_relaxed);
-	r3 = y.load(memory_order_relaxed);
-	if (r2 == 11 && r3 == 10)
-		x.store(0, memory_order_relaxed);
-}
-
-int user_main(int argc, char **argv)
-{
-	thrd_t t1, t2, t3;
-
-	atomic_init(&x, 0);
-	atomic_init(&y, 0);
-
-	printf("Main thread: creating 3 threads\n");
-	thrd_create(&t1, (thrd_start_t)&a, NULL);
-	thrd_create(&t2, (thrd_start_t)&b, NULL);
-	thrd_create(&t3, (thrd_start_t)&c, NULL);
-
-	thrd_join(t1);
-	thrd_join(t2);
-	thrd_join(t3);
-	printf("Main thread is finished\n");
-
-	/*
-	 * This condition should not be hit because it only occurs under a
-	 * satisfaction cycle
-	 */
-	bool cycle = (r0 == 1 && r1 == 0 && r2 == 11 && r3 == 10);
-	MODEL_ASSERT(!cycle);
-
-	return 0;
-}
diff --git a/test/mutextest.cc b/test/mutextest.cc
deleted file mode 100644
index c1767a29..00000000
--- a/test/mutextest.cc
+++ /dev/null
@@ -1,38 +0,0 @@
-#include <stdio.h>
-
-#include "threads.h"
-#include "librace.h"
-#include "stdatomic2.h"
-#include <mutex>
-std::mutex * m;
-int shareddata;
-
-static void a(void *obj)
-{
-	int i;
-	for(i=0;i<2;i++) {
-		if ((i%2)==0) {
-			m->lock();
-			store_32(&shareddata,(unsigned int)i);
-			m->unlock();
-		} else {
-			while(!m->try_lock())
-				thrd_yield();
-			store_32(&shareddata,(unsigned int)i);
-			m->unlock();
-		}
-	}
-}
-
-int user_main(int argc, char **argv)
-{
-	thrd_t t1, t2;
-	m=new std::mutex();
-
-	thrd_create(&t1, (thrd_start_t)&a, NULL);
-	thrd_create(&t2, (thrd_start_t)&a, NULL);
-
-	thrd_join(t1);
-	thrd_join(t2);
-	return 0;
-}
diff --git a/test/nestedpromise.c b/test/nestedpromise.c
deleted file mode 100644
index 9e514732..00000000
--- a/test/nestedpromise.c
+++ /dev/null
@@ -1,42 +0,0 @@
-#include <stdlib.h>
-#include <stdio.h>
-#include <threads.h>
-#include <stdatomic.h>
-
-#include "librace.h"
-#include "model-assert.h"
-
-atomic_int x;
-atomic_int y;
-atomic_int z;
-static void a(void *obj)
-{
-	(void)atomic_load_explicit(&z, memory_order_relaxed);				// this is only for schedule control
-	int t1=atomic_load_explicit(&x, memory_order_relaxed);
-	atomic_store_explicit(&y, 1, memory_order_relaxed);
-	printf("t1=%d\n",t1);
-}
-
-static void b(void *obj)
-{
-	int t2=atomic_load_explicit(&y, memory_order_relaxed);
-	atomic_store_explicit(&x, t2, memory_order_relaxed);
-}
-
-int user_main(int argc, char **argv)
-{
-	thrd_t t1, t2;
-
-
-	atomic_init(&x, 0);
-	atomic_init(&y, 0);
-	atomic_init(&z, 0);
-	thrd_create(&t1, (thrd_start_t)&a, NULL);
-	thrd_create(&t2, (thrd_start_t)&b, NULL);
-
-	thrd_join(t1);
-	thrd_join(t2);
-
-
-	return 0;
-}
diff --git a/test/pending-release.c b/test/pending-release.c
deleted file mode 100644
index a68f24df..00000000
--- a/test/pending-release.c
+++ /dev/null
@@ -1,65 +0,0 @@
-/*
- * This test performs some relaxes, release, acquire opeations on a single
- * atomic variable. It is designed for creating a difficult set of pending
- * release sequences to resolve at the end of an execution. However, it
- * utilizes 6 threads, so it blows up into a lot of executions quickly.
- */
-
-#include <stdio.h>
-#include <threads.h>
-#include <stdatomic.h>
-
-#include "librace.h"
-
-atomic_int x;
-int var = 0;
-
-static void a(void *obj)
-{
-	store_32(&var, 1);
-	atomic_store_explicit(&x, *((int *)obj), memory_order_release);
-	atomic_store_explicit(&x, *((int *)obj) + 1, memory_order_relaxed);
-}
-
-static void b2(void *obj)
-{
-	int r = atomic_load_explicit(&x, memory_order_acquire);
-	printf("r = %d\n", r);
-	store_32(&var, 3);
-}
-
-static void b1(void *obj)
-{
-	thrd_t t3, t4;
-	int i = 7;
-	int r = atomic_load_explicit(&x, memory_order_acquire);
-	printf("r = %d\n", r);
-	store_32(&var, 2);
-	thrd_create(&t3, (thrd_start_t)&a, &i);
-	thrd_create(&t4, (thrd_start_t)&b2, NULL);
-	thrd_join(t3);
-	thrd_join(t4);
-}
-
-static void c(void *obj)
-{
-	atomic_store_explicit(&x, 22, memory_order_relaxed);
-}
-
-int user_main(int argc, char **argv)
-{
-	thrd_t t1, t2, t5;
-	int i = 4;
-
-	atomic_init(&x, 0);
-
-	thrd_create(&t1, (thrd_start_t)&a, &i);
-	thrd_create(&t2, (thrd_start_t)&b1, NULL);
-	thrd_create(&t5, (thrd_start_t)&c, NULL);
-
-	thrd_join(t1);
-	thrd_join(t2);
-	thrd_join(t5);
-
-	return 0;
-}
diff --git a/test/releaseseq.c b/test/releaseseq.c
deleted file mode 100644
index 548f0a82..00000000
--- a/test/releaseseq.c
+++ /dev/null
@@ -1,52 +0,0 @@
-/*
- * This test performs some relaxes, release, acquire opeations on a single
- * atomic variable. It can give some rough idea of release sequence support but
- * probably should be improved to give better information.
- */
-
-#include <stdio.h>
-#include <threads.h>
-#include <stdatomic.h>
-
-#include "librace.h"
-
-atomic_int x;
-int var = 0;
-
-static void a(void *obj)
-{
-	store_32(&var, 1);
-	atomic_store_explicit(&x, 1, memory_order_release);
-	atomic_store_explicit(&x, 42, memory_order_relaxed);
-}
-
-static void b(void *obj)
-{
-	int r = atomic_load_explicit(&x, memory_order_acquire);
-	printf("r = %d\n", r);
-	printf("load %d\n", load_32(&var));
-}
-
-static void c(void *obj)
-{
-	atomic_store_explicit(&x, 2, memory_order_relaxed);
-}
-
-int user_main(int argc, char **argv)
-{
-	thrd_t t1, t2, t3;
-
-	atomic_init(&x, 0);
-
-	printf("Main thread: creating 3 threads\n");
-	thrd_create(&t1, (thrd_start_t)&a, NULL);
-	thrd_create(&t2, (thrd_start_t)&b, NULL);
-	thrd_create(&t3, (thrd_start_t)&c, NULL);
-
-	thrd_join(t1);
-	thrd_join(t2);
-	thrd_join(t3);
-	printf("Main thread is finished\n");
-
-	return 0;
-}
diff --git a/test/rmw2prog.c b/test/rmw2prog.c
deleted file mode 100644
index e1ec2faa..00000000
--- a/test/rmw2prog.c
+++ /dev/null
@@ -1,50 +0,0 @@
-#include <stdio.h>
-#include <threads.h>
-#include <stdatomic.h>
-
-#include "librace.h"
-
-atomic_short x;
-atomic_short y;
-
-static void a(void *obj)
-{
-	short desire = 315;
-	short expected = 0;
-	short * pt = &expected;
-
-	printf("expected was %d, but x is %d\n", expected, x);
-
-	short v1 = atomic_compare_exchange_weak_explicit(&x, pt, desire, memory_order_relaxed, memory_order_acquire);
-	printf("Then v1 = %d, x = %d\n", v1, x);
-	printf("expected: %d\n", expected);
-/*
-        short v1 = atomic_exchange_explicit(&x, 8, memory_order_relaxed);
-        short v2 = atomic_exchange_explicit(&x, -10, memory_order_relaxed);
-        short v3 = atomic_load_explicit(&x, memory_order_relaxed);
-        printf("v1 = %d, v2 = %d, v3 = %d\n", v1, v2, v3);
- */
-}
-
-static void b(void *obj)
-{
-	int v3=atomic_fetch_add_explicit(&y, 2, memory_order_relaxed);
-	int v4=atomic_fetch_add_explicit(&x, -5, memory_order_relaxed);
-	printf("v3 = %d, v4=%d\n", v3, v4);
-}
-
-int user_main(int argc, char **argv)
-{
-	thrd_t t1, t2;
-
-	atomic_init(&x, 0);
-	atomic_init(&y, 0);
-
-	thrd_create(&t1, (thrd_start_t)&a, NULL);
-//	thrd_create(&t2, (thrd_start_t)&b, NULL);
-
-	thrd_join(t1);
-//	thrd_join(t2);
-
-	return 0;
-}
diff --git a/test/rmwprog.c b/test/rmwprog.c
deleted file mode 100644
index f515628e..00000000
--- a/test/rmwprog.c
+++ /dev/null
@@ -1,36 +0,0 @@
-#include <stdlib.h>
-#include <stdio.h>
-#include <threads.h>
-#include <stdatomic.h>
-
-#include "librace.h"
-#include "model-assert.h"
-
-atomic_int x;
-static int N = 2;
-
-static void a(void *obj)
-{
-	int i;
-	for (i = 0;i < N;i++)
-		atomic_fetch_add_explicit(&x, 1, memory_order_relaxed);
-}
-
-int user_main(int argc, char **argv)
-{
-	thrd_t t1, t2;
-
-	if (argc > 1)
-		N = atoi(argv[1]);
-
-	atomic_init(&x, 0);
-	thrd_create(&t1, (thrd_start_t)&a, NULL);
-	thrd_create(&t2, (thrd_start_t)&a, NULL);
-
-	thrd_join(t1);
-	thrd_join(t2);
-
-	MODEL_ASSERT(atomic_load(&x) == N * 2);
-
-	return 0;
-}
diff --git a/test/sctest.c b/test/sctest.c
deleted file mode 100644
index 2ddb953b..00000000
--- a/test/sctest.c
+++ /dev/null
@@ -1,59 +0,0 @@
-#include <stdio.h>
-#include <threads.h>
-#include <stdatomic.h>
-
-#include "librace.h"
-
-atomic_int x;
-atomic_int y;
-atomic_int z;
-
-static int r1, r2, r3;
-
-static void a(void *obj)
-{
-	atomic_store_explicit(&z, 1, memory_order_relaxed);
-}
-
-static void b(void *obj)
-{
-	atomic_store_explicit(&x, 1, memory_order_relaxed);
-	atomic_store_explicit(&y, 1, memory_order_relaxed);
-	r1=atomic_load_explicit(&z, memory_order_relaxed);
-}
-static void c(void *obj)
-{
-	atomic_store_explicit(&z, 2, memory_order_relaxed);
-	atomic_store_explicit(&x, 2, memory_order_relaxed);
-	r2=atomic_load_explicit(&y, memory_order_relaxed);
-}
-
-static void d(void *obj)
-{
-	atomic_store_explicit(&z, 3, memory_order_relaxed);
-	atomic_store_explicit(&y, 2, memory_order_relaxed);
-	r3=atomic_load_explicit(&x, memory_order_relaxed);
-}
-
-int user_main(int argc, char **argv)
-{
-	thrd_t t1, t2,t3, t4;
-
-	atomic_init(&x, 0);
-	atomic_init(&y, 0);
-	atomic_init(&z, 0);
-
-	thrd_create(&t1, (thrd_start_t)&a, NULL);
-	thrd_create(&t2, (thrd_start_t)&b, NULL);
-	thrd_create(&t3, (thrd_start_t)&c, NULL);
-	thrd_create(&t4, (thrd_start_t)&d, NULL);
-
-	thrd_join(t1);
-	thrd_join(t2);
-	thrd_join(t3);
-	thrd_join(t4);
-
-	/* Check and/or print r1, r2, r3? */
-
-	return 0;
-}
diff --git a/test/thinair.c b/test/thinair.c
deleted file mode 100644
index 2f4f5805..00000000
--- a/test/thinair.c
+++ /dev/null
@@ -1,41 +0,0 @@
-#include <stdio.h>
-#include <threads.h>
-#include <stdatomic.h>
-
-#include "librace.h"
-
-atomic_int x;
-atomic_int y;
-
-static void a(void *obj)
-{
-	int r1=atomic_load_explicit(&x, memory_order_relaxed);
-	atomic_store_explicit(&y, r1, memory_order_relaxed);
-	printf("r1=%d\n",r1);
-}
-
-static void b(void *obj)
-{
-	int r2=atomic_load_explicit(&y, memory_order_relaxed);
-	atomic_store_explicit(&x, r2, memory_order_relaxed);
-	atomic_store_explicit(&x, r2 + 1, memory_order_relaxed);
-	printf("r2=%d\n",r2);
-}
-
-int user_main(int argc, char **argv)
-{
-	thrd_t t1, t2;
-
-	atomic_init(&x, -1);
-	atomic_init(&y, 0);
-
-	printf("Main thread: creating 2 threads\n");
-	thrd_create(&t1, (thrd_start_t)&a, NULL);
-	thrd_create(&t2, (thrd_start_t)&b, NULL);
-
-	thrd_join(t1);
-	thrd_join(t2);
-	printf("Main thread is finished\n");
-
-	return 0;
-}
diff --git a/test/uninit.cc b/test/uninit.cc
deleted file mode 100644
index b3a10261..00000000
--- a/test/uninit.cc
+++ /dev/null
@@ -1,54 +0,0 @@
-/**
- * @file uninit.cc
- * @brief Uninitialized loads test
- *
- * This is a test of the "uninitialized loads" code. While we don't explicitly
- * initialize y, this example's synchronization pattern should guarantee we
- * never see it uninitialized.
- */
-#include <stdio.h>
-#include <threads.h>
-#include <atomic>
-
-#include "librace.h"
-
-std::atomic_int x;
-std::atomic_int y;
-
-static void a(void *obj)
-{
-	int flag = x.load(std::memory_order_acquire);
-	printf("flag: %d\n", flag);
-	if (flag == 2)
-		printf("Load: %d\n", y.load(std::memory_order_relaxed));
-}
-
-static void b(void *obj)
-{
-	printf("fetch_add: %d\n", x.fetch_add(1, std::memory_order_relaxed));
-}
-
-static void c(void *obj)
-{
-	y.store(3, std::memory_order_relaxed);
-	x.store(1, std::memory_order_release);
-}
-
-int user_main(int argc, char **argv)
-{
-	thrd_t t1, t2, t3;
-
-	std::atomic_init(&x, 0);
-
-	printf("Main thread: creating 3 threads\n");
-	thrd_create(&t1, (thrd_start_t)&a, NULL);
-	thrd_create(&t2, (thrd_start_t)&b, NULL);
-	thrd_create(&t3, (thrd_start_t)&c, NULL);
-
-	thrd_join(t1);
-	thrd_join(t2);
-	thrd_join(t3);
-	printf("Main thread is finished\n");
-
-	return 0;
-}
diff --git a/test/userprog.c b/test/userprog.c
deleted file mode 100644
index 415eb248..00000000
--- a/test/userprog.c
+++ /dev/null
@@ -1,43 +0,0 @@
-#include <stdio.h>
-#include <threads.h>
-#include <stdatomic.h>
-
-#include "librace.h"
-
-atomic_int x;
-atomic_int y;
-int z;
-
-static void a(void *obj)
-{
-	int r1=atomic_load_explicit(&y, memory_order_relaxed);
-	atomic_store_explicit(&x, r1, memory_order_relaxed);
-//	z = 1;
-	printf("r1=%d\n",r1);
-}
-
-static void b(void *obj)
-{
-	int r2=atomic_load_explicit(&x, memory_order_relaxed);
-	atomic_store_explicit(&y, 42, memory_order_relaxed);
-//	z = 2;
-	printf("r2=%d\n",r2);
-}
-
-int user_main(int argc, char **argv)
-{
-	thrd_t t1, t2;
-
-	atomic_init(&x, 30);
-	atomic_init(&y, 0);
-
-	printf("Main thread: creating 2 threads\n");
-	thrd_create(&t1, (thrd_start_t)&a, NULL);
-	thrd_create(&t2, (thrd_start_t)&b, NULL);
-
-	thrd_join(t1);
-	thrd_join(t2);
-	printf("Main thread is finished\n");
-
-	return 0;
-}
diff --git a/test/wrc.c b/test/wrc.c
deleted file mode 100644
index 21198253..00000000
--- a/test/wrc.c
+++ /dev/null
@@ -1,89 +0,0 @@
-#include <stdio.h>
-#include <threads.h>
-#include <stdatomic.h>
-#include "librace.h"
-atomic_int x1;
-atomic_int x2;
-atomic_int x3;
-atomic_int x4;
-atomic_int x5;
-atomic_int x6;
-atomic_int x7;
-static void a(void *obj)
-{
-	atomic_store_explicit(&x1, 1,memory_order_relaxed);
-}
-
-static void b(void *obj)
-{
-	(void)atomic_load_explicit(&x1, memory_order_relaxed);
-	atomic_store_explicit(&x2, 1,memory_order_relaxed);
-}
-
-static void c(void *obj)
-{
-	(void)atomic_load_explicit(&x2, memory_order_relaxed);
-	atomic_store_explicit(&x3, 1,memory_order_relaxed);
-}
-
-static void d(void *obj)
-{
-	(void)atomic_load_explicit(&x3, memory_order_relaxed);
-	atomic_store_explicit(&x4, 1,memory_order_relaxed);
-}
-
-static void e(void *obj)
-{
-	(void)atomic_load_explicit(&x4, memory_order_relaxed);
-	atomic_store_explicit(&x5, 1,memory_order_relaxed);
-}
-
-static void f(void *obj)
-{
-	(void)atomic_load_explicit(&x5, memory_order_relaxed);
-	atomic_store_explicit(&x6, 1,memory_order_relaxed);
-}
-
-static void g(void *obj)
-{
-	(void)atomic_load_explicit(&x6, memory_order_relaxed);
-	atomic_store_explicit(&x7, 1,memory_order_relaxed);
-}
-static void h(void *obj)
-{
-	(void)atomic_load_explicit(&x7, memory_order_relaxed);
-	(void)atomic_load_explicit(&x1, memory_order_relaxed);
-}
-
-int user_main(int argc, char **argv)
-{
-	thrd_t t1, t2, t3, t4, t5, t6, t7, t8;
-	atomic_init(&x1, 0);
-	atomic_init(&x2, 0);
-	atomic_init(&x3, 0);
-	atomic_init(&x4, 0);
-	atomic_init(&x5, 0);
-	atomic_init(&x6, 0);
-	atomic_init(&x7, 0);
-
-
-	thrd_create(&t1, (thrd_start_t)&a, NULL);
-	thrd_create(&t2, (thrd_start_t)&b, NULL);
-	thrd_create(&t3, (thrd_start_t)&c, NULL);
-	thrd_create(&t4, (thrd_start_t)&d, NULL);
-	thrd_create(&t5, (thrd_start_t)&e, NULL);
-	thrd_create(&t6, (thrd_start_t)&f, NULL);
-	thrd_create(&t7, (thrd_start_t)&g, NULL);
-	thrd_create(&t8, (thrd_start_t)&h, NULL);
-
-	thrd_join(t1);
-	thrd_join(t2);
-	thrd_join(t3);
-	thrd_join(t4);
-	thrd_join(t5);
-	thrd_join(t6);
-	thrd_join(t7);
-	thrd_join(t8);
-
-	return 0;
-}
diff --git a/test/wrcs.c b/test/wrcs.c
deleted file mode 100644
index ddcf4f1a..00000000
--- a/test/wrcs.c
+++ /dev/null
@@ -1,89 +0,0 @@
-#include <stdio.h>
-#include <threads.h>
-#include <stdatomic.h>
-#include "librace.h"
-atomic_int x1;
-atomic_int x2;
-atomic_int x3;
-atomic_int x4;
-atomic_int x5;
-atomic_int x6;
-atomic_int x7;
-static void a(void *obj)
-{
-	atomic_store_explicit(&x1, 1,memory_order_seq_cst);
-}
-
-static void b(void *obj)
-{
-	(void)atomic_load_explicit(&x1, memory_order_seq_cst);
-	atomic_store_explicit(&x2, 1,memory_order_seq_cst);
-}
-
-static void c(void *obj)
-{
-	(void)atomic_load_explicit(&x2, memory_order_seq_cst);
-	atomic_store_explicit(&x3, 1,memory_order_seq_cst);
-}
-
-static void d(void *obj)
-{
-	(void)atomic_load_explicit(&x3, memory_order_seq_cst);
-	atomic_store_explicit(&x4, 1,memory_order_seq_cst);
-}
-
-static void e(void *obj)
-{
-	(void)atomic_load_explicit(&x4, memory_order_seq_cst);
-	atomic_store_explicit(&x5, 1,memory_order_seq_cst);
-}
-
-static void f(void *obj)
-{
-	(void)atomic_load_explicit(&x5, memory_order_seq_cst);
-	atomic_store_explicit(&x6, 1,memory_order_seq_cst);
-}
-
-static void g(void *obj)
-{
-	(void)atomic_load_explicit(&x6, memory_order_seq_cst);
-	atomic_store_explicit(&x7, 1,memory_order_seq_cst);
-}
-static void h(void *obj)
-{
-	(void)atomic_load_explicit(&x7, memory_order_seq_cst);
-	(void)atomic_load_explicit(&x1, memory_order_seq_cst);
-}
-
-int user_main(int argc, char **argv)
-{
-	thrd_t t1, t2, t3, t4, t5, t6, t7, t8;
-	atomic_init(&x1, 0);
-	atomic_init(&x2, 0);
-	atomic_init(&x3, 0);
-	atomic_init(&x4, 0);
-	atomic_init(&x5, 0);
-	atomic_init(&x6, 0);
-	atomic_init(&x7, 0);
-
-
-	thrd_create(&t1, (thrd_start_t)&a, NULL);
-	thrd_create(&t2, (thrd_start_t)&b, NULL);
-	thrd_create(&t3, (thrd_start_t)&c, NULL);
-	thrd_create(&t4, (thrd_start_t)&d, NULL);
-	thrd_create(&t5, (thrd_start_t)&e, NULL);
-	thrd_create(&t6, (thrd_start_t)&f, NULL);
-	thrd_create(&t7, (thrd_start_t)&g, NULL);
-	thrd_create(&t8, (thrd_start_t)&h, NULL);
-
-	thrd_join(t1);
-	thrd_join(t2);
-	thrd_join(t3);
-	thrd_join(t4);
-	thrd_join(t5);
-	thrd_join(t6);
-	thrd_join(t7);
-	thrd_join(t8);
-
-	return 0;
-}
diff --git a/threads.cc b/threads.cc
index 17b76863..8b55a91b 100644
--- a/threads.cc
+++ b/threads.cc
@@ -59,11 +59,9 @@ Thread * thread_current(void)
 	return model->get_current_thread();
 }
 
-#ifdef TLS
 void modelexit() {
 	model->switch_to_master(new ModelAction(THREAD_FINISH, std::memory_order_seq_cst, thread_current()));
 }
-#endif
 
 void initMainThread() {
 	atexit(modelexit);