From: weiyu <weiyuluo1232@gmail.com>
Date: Tue, 8 Jan 2019 19:50:41 +0000 (-0800)
Subject: change cds checker to accomdate llvm pass
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=6e0d0a36ea0f00925308504a44c7b690a9a1d6b7

change cds checker to accomdate llvm pass
---

diff --git a/#cmodelint.cc# b/#cmodelint.cc#
new file mode 100644
index 00000000..b67194f2
--- /dev/null
+++ b/#cmodelint.cc#
@@ -0,0 +1,74 @@
+#include "model.h"
+#include "action.h"
+#include "cmodelint.h"
+#include "threads-model.h"
+
+memory_order orders[6] = {
+	memory_order_relaxed, memory_order_consume, memory_order_acquire,
+	memory_order_release, memory_order_acq_rel, memory_order_seq_cst
+};
+
+/** Performs a read action.*/
+uint64_t model_read_action(void * obj, memory_order ord) {
+	return model->switch_to_master(new ModelAction(ATOMIC_READ, ord, obj));
+}
+
+uint64_t model_read_action_helper(void * obj, int index) {
+	return model->switch_to_master(new ModelAction(ATOMIC_READ, orders[index], obj));
+}
+:q!
+
+/** Performs a write action.*/
+void model_write_action(void * obj, memory_order ord, uint64_t val) {
+	model->switch_to_master(new ModelAction(ATOMIC_WRITE, ord, obj, val));
+}
+
+void model_write_action_helper(void * obj, int index, uint64_t val) {
+	model->switch_to_master(new ModelAction(ATOMIC_WRITE, orders[index], obj, val));
+}
+
+/** Performs an init action. */
+void model_init_action(void * obj, uint64_t val) {
+	model->switch_to_master(new ModelAction(ATOMIC_INIT, memory_order_relaxed, obj, val));
+}
+// do not need a helper function
+
+/**
+ * Performs the read part of a RMW action. The next action must either be the
+ * write part of the RMW action or an explicit close out of the RMW action w/o
+ * a write.
+ */
+uint64_t model_rmwr_action(void *obj, memory_order ord) {
+	return model->switch_to_master(new ModelAction(ATOMIC_RMWR, ord, obj));
+}
+
+uint64_t model_rmwr_action_helper(void *obj, int index) {
+	return model->switch_to_master(new ModelAction(ATOMIC_RMWR, orders[index], obj));
+}
+
+/** Performs the write part of a RMW action. */
+void model_rmw_action(void *obj, memory_order ord, uint64_t val) {
+	model->switch_to_master(new ModelAction(ATOMIC_RMW, ord, obj, val));
+}
+
+void model_rmw_action_helper(void *obj, int index, uint64_t val) {
+	model->switch_to_master(new ModelAction(ATOMIC_RMW, orders[index], obj, val));
+}
+
+/** Closes out a RMW action without doing a write. */
+void model_rmwc_action(void *obj, memory_order ord) {
+	model->switch_to_master(new ModelAction(ATOMIC_RMWC, ord, obj));
+}
+
+void model_rmwc_action_helper(void *obj, int index) {
+	model->switch_to_master(new ModelAction(ATOMIC_RMWC, orders[index], obj));
+}
+
+/** Issues a fence operation. */
+void model_fence_action(memory_order ord) {
+	model->switch_to_master(new ModelAction(ATOMIC_FENCE, ord, FENCE_LOCATION));
+}
+
+void model_fence_action_helper(int index) {
+	model->switch_to_master(new ModelAction(ATOMIC_FENCE, orders[index], FENCE_LOCATION));
+}
diff --git a/#main.cc# b/#main.cc#
new file mode 100644
index 00000000..d4ab75bf
--- /dev/null
+++ b/#main.cc#
@@ -0,0 +1,288 @@
+/** @file main.cc
+ *  @brief Entry point for the model checker.
+ */
+
+#include <unistd.h>
+#include <getopt.h>
+#include <string.h>
+
+#include "common.h"
+#include "output.h"
+
+#include "datarace.h"
+
+/* global "model" object */
+#include "model.h"
+#include "params.h"
+#include "snapshot-interface.h"
+
+static void param_defaults(struct model_params *params)
+{
+	params->maxreads = 0;
+	params->maxfuturedelay = 6;
+	params->fairwindow = 0;
+	params->yieldon = false;
+	params->yieldblock = false;
+	params->enabledcount = 1;
+	params->bound = 0;
+	params->maxfuturevalues = 0;
+	params->expireslop = 4;
+	params->verbose = !!DBG_ENABLED();
+	params->uninitvalue = 0;
+	params->maxexecutions = 0;
+}
+
+static void print_usage(const char *program_name, struct model_params *params)
+{
+	ModelVector<TraceAnalysis *> * registeredanalysis=getRegisteredTraceAnalysis();
+	/* Reset defaults before printing */
+	param_defaults(params);
+
+	model_print(
+"Copyright (c) 2013 Regents of the University of California. All rights reserved.\n"
+"Distributed under the GPLv2\n"
+"Written by Brian Norris and Brian Demsky\n"
+"\n"
+"Usage: %s [MODEL-CHECKER OPTIONS] -- [PROGRAM ARGS]\n"
+"\n"
+"MODEL-CHECKER OPTIONS can be any of the model-checker options listed below. Arguments\n"
+"provided after the `--' (the PROGRAM ARGS) are passed to the user program.\n"
+"\n"
+"Model-checker options:\n"
+"-h, --help                  Display this help message and exit\n"
+"-m, --liveness=NUM          Maximum times a thread can read from the same write\n"
+"                              while other writes exist.\n"
+"                              Default: %d\n"
+"-M, --maxfv=NUM             Maximum number of future values that can be sent to\n"
+"                              the same read.\n"
+"                              Default: %d\n"
+"-s, --maxfvdelay=NUM        Maximum actions that the model checker will wait for\n"
+"                              a write from the future past the expected number\n"
+"                              of actions.\n"
+"                              Default: %d\n"
+"-S, --fvslop=NUM            Future value expiration sloppiness.\n"
+"                              Default: %u\n"
+"-y, --yield                 Enable CHESS-like yield-based fairness support\n"
+"                              (requires thrd_yield() in test program).\n"
+"                              Default: %s\n"
+"-Y, --yieldblock            Prohibit an execution from running a yield.\n"
+"                              Default: %s\n"
+"-f, --fairness=WINDOW       Specify a fairness window in which actions that are\n"
+"                              enabled sufficiently many times should receive\n"
+"                              priority for execution (not recommended).\n"
+"                              Default: %d\n"
+"-e, --enabled=COUNT         Enabled count.\n"
+"                              Default: %d\n"
+"-b, --bound=MAX             Upper length bound.\n"
+"                              Default: %d\n"
+"-v[NUM], --verbose[=NUM]    Print verbose execution information. NUM is optional:\n"
+"                              0 is quiet; 1 shows valid executions; 2 is noisy;\n"
+"                              3 is noisier.\n"
+"                              Default: %d\n"
+"-u, --uninitialized=VALUE   Return VALUE any load which may read from an\n"
+"                              uninitialized atomic.\n"
+"                              Default: %u\n"
+"-t, --analysis=NAME         Use Analysis Plugin.\n"
+"-o, --options=NAME          Option for previous analysis plugin.  \n"
+"-x, --maxexec=NUM           Maximum number of executions.\n"
+"                            Default: %u\n"
+"                            -o help for a list of options\n"
+" --                         Program arguments follow.\n\n",
+		program_name,
+		params->maxreads,
+		params->maxfuturevalues,
+		params->maxfuturedelay,
+		params->expireslop,
+		params->yieldon ? "enabled" : "disabled",
+		params->yieldblock ? "enabled" : "disabled",
+		params->fairwindow,
+		params->enabledcount,
+		params->bound,
+		params->verbose,
+    params->uninitvalue,
+		params->maxexecutions);
+	model_print("Analysis plugins:\n");
+	for(unsigned int i=0;i<registeredanalysis->size();i++) {
+		TraceAnalysis * analysis=(*registeredanalysis)[i];
+		model_print("%s\n", analysis->name());
+	}
+	exit(EXIT_SUCCESS);
+}
+
+bool install_plugin(char * name) {
+	ModelVector<TraceAnalysis *> * registeredanalysis=getRegisteredTraceAnalysis();
+	ModelVector<TraceAnalysis *> * installedanalysis=getInstalledTraceAnalysis();
+
+	for(unsigned int i=0;i<registeredanalysis->size();i++) {
+		TraceAnalysis * analysis=(*registeredanalysis)[i];
+		if (strcmp(name, analysis->name())==0) {
+			installedanalysis->push_back(analysis);
+			return false;
+		}
+	}
+	model_print("Analysis %s Not Found\n", name);
+	return true;
+}
+
+static void parse_options(struct model_params *params, int argc, char **argv)
+{
+	const char *shortopts = "hyYt:o:m:M:s:S:f:e:b:u:x:v::";
+	const struct option longopts[] = {
+		{"help", no_argument, NULL, 'h'},
+		{"liveness", required_argument, NULL, 'm'},
+		{"maxfv", required_argument, NULL, 'M'},
+		{"maxfvdelay", required_argument, NULL, 's'},
+		{"fvslop", required_argument, NULL, 'S'},
+		{"fairness", required_argument, NULL, 'f'},
+		{"yield", no_argument, NULL, 'y'},
+		{"yieldblock", no_argument, NULL, 'Y'},
+		{"enabled", required_argument, NULL, 'e'},
+		{"bound", required_argument, NULL, 'b'},
+		{"verbose", optional_argument, NULL, 'v'},
+		{"uninitialized", required_argument, NULL, 'u'},
+		{"analysis", required_argument, NULL, 't'},
+		{"options", required_argument, NULL, 'o'},
+		{"maxexecutions", required_argument, NULL, 'x'},
+		{0, 0, 0, 0} /* Terminator */
+	};
+	int opt, longindex;
+	bool error = false;
+	while (!error && (opt = getopt_long(argc, argv, shortopts, longopts, &longindex)) != -1) {
+		switch (opt) {
+		case 'h':
+			print_usage(argv[0], params);
+			break;
+		case 'x':
+			params->maxexecutions = atoi(optarg);
+			break;
+		case 's':
+			params->maxfuturedelay = atoi(optarg);
+			break;
+		case 'S':
+			params->expireslop = atoi(optarg);
+			break;
+		case 'f':
+			params->fairwindow = atoi(optarg);
+			break;
+		case 'e':
+			params->enabledcount = atoi(optarg);
+			break;
+		case 'b':
+			params->bound = atoi(optarg);
+			break;
+		case 'm':
+			params->maxreads = atoi(optarg);
+			break;
+		case 'M':
+			params->maxfuturevalues = atoi(optarg);
+			break;
+		case 'v':
+			params->verbose = optarg ? atoi(optarg) : 1;
+			break;
+		case 'u':
+			params->uninitvalue = atoi(optarg);
+			break;
+		case 'y':
+			params->yieldon = true;
+			break;
+		case 't':
+			if (install_plugin(optarg))
+				error = true;
+			break;
+		case 'o':
+			{
+				ModelVector<TraceAnalysis *> * analyses = getInstalledTraceAnalysis();
+				if ( analyses->size() == 0 || (*analyses)[analyses->size()-1]->option(optarg))
+					error = true;
+			}
+			break;
+		case 'Y':
+			params->yieldblock = true;
+			break;
+		default: /* '?' */
+			error = true;
+			break;
+		}
+	}
+
+	/* Pass remaining arguments to user program */
+	params->argc = argc - (optind - 1);
+	params->argv = argv + (optind - 1);
+
+	/* Reset program name */
+	params->argv[0] = argv[0];
+
+	/* Reset (global) optind for potential use by user program */
+	optind = 1;
+
+	if (error)
+		print_usage(argv[0], params);
+}
+
+int main_argc;
+char **main_argv;
+
+static void install_trace_analyses(ModelExecution *execution)
+{
+	ModelVector<TraceAnalysis *> * installedanalysis=getInstalledTraceAnalysis();
+	for(unsigned int i=0;i<installedanalysis->size();i++) {
+		TraceAnalysis * ta=(*installedanalysis)[i];
+		ta->setExecution(execution);
+		model->add_trace_analysis(ta);
+		/** Call the installation event for each installed plugin */
+		ta->actionAtInstallation();
+	}
+}
+
+/** The model_main function contains the main model checking loop. */
+static void model_main()
+{
+	struct model_params params;
+
+	param_defaults(&params);
+	register_plugins();
+
+	parse_options(&params, main_argc, main_argv);
+
+	//Initialize race detector
+	initRaceDetector();
+
+	snapshot_stack_init();
+
+	model = new ModelChecker(params);	// L: Model thread is created
+//	install_trace_analyses(model->get_execution()); 	L: disable plugin
+
+	snapshot_record(0);
+	model->run();
+	delete model;
+
+	DEBUG("Exiting\n");
+}
+
+/**
+ * Main function.  Just initializes snapshotting library and the
+ * snapshotting library calls the model_main function.
+ */
+int main(int argc, char **argv)
+{
+	main_argc = argc;
+	main_argv = argv;
+
+	/*
+	 * If this printf statement is removed, CDSChecker will fail on an
+	 * assert on some versions of glibc.  The first time printf is
+	 * called, it allocated internal buffers.  We can't easily snapshot
+	 * libc since we also use it.
+	 */
+
+	printf("CDSChecker\n"
+				 "Copyright (c) 2013 Regents of the University of California. All rights reserved.\n"
+				 "Distributed under the GPLv2\n"
+				 "Written by Brian Norris and Brian Demsky\n\n");
+
+	/* Configure output redirection for the model-checker */
+	redirect_output();
+
+	/* Let's jump in quickly and start running stuff */
+	snapshot_system_init(10000, 1024, 1024, 4000, &model_main);
+}
diff --git a/Makefile b/Makefile
index cf4a493b..3c512854 100644
--- a/Makefile
+++ b/Makefile
@@ -62,8 +62,7 @@ tags:
 	ctags -R
 
 PHONY += tests
-tests: $(LIB_SO)
-	$(MAKE) -C $(TESTS_DIR)
+tests: $(LIB_SO)	# $(MAKE) -C $(TESTS_DIR)
 
 BENCH_DIR := benchmarks
 
diff --git a/action.cc b/action.cc
index d4c6253c..c913b74c 100644
--- a/action.cc
+++ b/action.cc
@@ -482,13 +482,23 @@ Node * ModelAction::get_node() const
 void ModelAction::set_read_from(const ModelAction *act)
 {
 	ASSERT(act);
+
 	reads_from = act;
 	reads_from_promise = NULL;
-	if (act->is_uninitialized())
-		model->assert_bug("May read from uninitialized atomic:\n"
+
+	if (act->is_uninitialized()) { // WL
+		uint64_t val = *((uint64_t *) location);
+		ModelAction * act_initialized = (ModelAction *)act;
+		act_initialized->set_value(val);
+		reads_from = (const ModelAction *)act_initialized;
+
+// disabled by WL, because LLVM IR is unable to detect atomic init
+/*		model->assert_bug("May read from uninitialized atomic:\n"
 				"    action %d, thread %d, location %p (%s, %s)",
 				seq_number, id_to_int(tid), location,
 				get_type_str(), get_mo_str());
+*/
+	}
 }
 
 /**
diff --git a/action.h b/action.h
index c8ad85bc..d1f4fffd 100644
--- a/action.h
+++ b/action.h
@@ -23,6 +23,7 @@ namespace std {
 
 using std::memory_order;
 using std::memory_order_relaxed;
+using std::memory_order_consume;
 using std::memory_order_acquire;
 using std::memory_order_release;
 using std::memory_order_acq_rel;
@@ -185,6 +186,11 @@ public:
 	bool may_read_from(const ModelAction *write) const;
 	bool may_read_from(const Promise *promise) const;
 	MEMALLOC
+
+// Added by WL
+	void set_value(uint64_t val) {
+		value = val;
+	}
 private:
 
 	const char * get_type_str() const;
diff --git a/cmodelint.cc b/cmodelint.cc
index 16325811..15d6151b 100644
--- a/cmodelint.cc
+++ b/cmodelint.cc
@@ -1,8 +1,14 @@
+#include <stdio.h>
 #include "model.h"
 #include "action.h"
 #include "cmodelint.h"
 #include "threads-model.h"
 
+memory_order orders[6] = {
+	memory_order_relaxed, memory_order_consume, memory_order_acquire,
+	memory_order_release, memory_order_acq_rel, memory_order_seq_cst
+};
+
 /** Performs a read action.*/
 uint64_t model_read_action(void * obj, memory_order ord) {
 	return model->switch_to_master(new ModelAction(ATOMIC_READ, ord, obj));
@@ -41,3 +47,222 @@ void model_rmwc_action(void *obj, memory_order ord) {
 void model_fence_action(memory_order ord) {
 	model->switch_to_master(new ModelAction(ATOMIC_FENCE, ord, FENCE_LOCATION));
 }
+
+// --------------------- helper functions --------------------------------
+uint64_t model_rmwr_action_helper(void *obj, int atomic_index) {
+	return model->switch_to_master(new ModelAction(ATOMIC_RMWR, orders[atomic_index], obj));
+}
+
+void model_rmw_action_helper(void *obj, int atomic_index, uint64_t val) {
+	model->switch_to_master(new ModelAction(ATOMIC_RMW, orders[atomic_index], obj, val));
+}
+
+void model_rmwc_action_helper(void *obj, int atomic_index) {
+	model->switch_to_master(new ModelAction(ATOMIC_RMWC, orders[atomic_index], obj));
+}
+
+void model_fence_action_helper(int atomic_index) {
+	model->switch_to_master(new ModelAction(ATOMIC_FENCE, orders[atomic_index], FENCE_LOCATION));
+}
+
+// cds atomic loads
+uint8_t cds_atomic_load8(void * obj, int atomic_index) {	
+	return (uint8_t) ( model->switch_to_master(new ModelAction(ATOMIC_READ, orders[atomic_index], obj)) );
+}
+uint16_t cds_atomic_load16(void * obj, int atomic_index) {
+	return (uint16_t) ( model->switch_to_master(new ModelAction(ATOMIC_READ, orders[atomic_index], obj)) );
+}
+uint32_t cds_atomic_load32(void * obj, int atomic_index) {
+	return (uint32_t) ( model->switch_to_master(new ModelAction(ATOMIC_READ, orders[atomic_index], obj)) );
+}
+uint64_t cds_atomic_load64(void * obj, int atomic_index) {
+	return model->switch_to_master(new ModelAction(ATOMIC_READ, orders[atomic_index], obj));
+}
+
+// cds atomic stores
+void cds_atomic_store8(void * obj, int atomic_index, uint8_t val) {
+  model->switch_to_master(new ModelAction(ATOMIC_WRITE, orders[atomic_index], obj, (uint64_t) val));
+}
+void cds_atomic_store16(void * obj, int atomic_index, uint16_t val) {
+  model->switch_to_master(new ModelAction(ATOMIC_WRITE, orders[atomic_index], obj, (uint64_t) val));
+}
+void cds_atomic_store32(void * obj, int atomic_index, uint32_t val) {
+  model->switch_to_master(new ModelAction(ATOMIC_WRITE, orders[atomic_index], obj, (uint64_t) val));
+}
+void cds_atomic_store64(void * obj, int atomic_index, uint64_t val) {
+  model->switch_to_master(new ModelAction(ATOMIC_WRITE, orders[atomic_index], obj, val));
+}
+
+/*
+#define _ATOMIC_RMW_(__op__, size, addr, atomic_index, val )            \
+({                                                                      \
+  uint##size##_t _old = model_rmwr_action_helper(addr, atomic_index);   \
+  uint##size##_t _copy = _old;                                          \
+  _copy __op__ ( uint##size##_t ) _val;                                 \
+  model_rmw_action_helper(addr, atomic_index, (uint64_t) _copy);        \
+  return _old;                                                          \
+})*/
+
+#define _ATOMIC_RMW_(__op__, size, addr, atomic_index, val )            \
+({                                                                      \
+  uint##size##_t _old = model_rmwr_action_helper(addr, atomic_index);   \
+  uint##size##_t _copy = _old;                                          \
+  uint##size##_t _val = val;                                            \
+  _copy __op__ _val;                                                    \
+  model_rmw_action_helper(addr, atomic_index, (uint64_t) _copy);        \
+  return _old;                                                          \
+})
+
+// cds atomic exchange
+uint8_t cds_atomic_exchange8(void* addr, int atomic_index, uint8_t val) {
+  _ATOMIC_RMW_( = , 8, addr, atomic_index, val);
+}
+uint16_t cds_atomic_exchange16(void* addr, int atomic_index, uint16_t val) {
+  _ATOMIC_RMW_( = , 16, addr, atomic_index, val);
+}
+uint32_t cds_atomic_exchange32(void* addr, int atomic_index, uint32_t val) {
+  _ATOMIC_RMW_( = , 32, addr, atomic_index, val);
+}
+uint64_t cds_atomic_exchange64(void* addr, int atomic_index, uint64_t val) {
+  _ATOMIC_RMW_( = , 64, addr, atomic_index, val);
+}
+
+// cds atomic fetch add
+uint8_t cds_atomic_fetch_add8(void* addr, int atomic_index, uint8_t val) {
+  _ATOMIC_RMW_( += , 8, addr, atomic_index, val);
+}
+uint16_t cds_atomic_fetch_add16(void* addr, int atomic_index, uint16_t val) {
+  _ATOMIC_RMW_( += , 16, addr, atomic_index, val);
+}
+uint32_t cds_atomic_fetch_add32(void* addr, int atomic_index, uint32_t val) {
+  _ATOMIC_RMW_( += , 32, addr, atomic_index, val);
+}
+uint64_t cds_atomic_fetch_add64(void* addr, int atomic_index, uint64_t val) {
+  _ATOMIC_RMW_( += , 64, addr, atomic_index, val);
+}
+
+// cds atomic fetch sub
+uint8_t cds_atomic_fetch_sub8(void* addr, int atomic_index, uint8_t val) {
+  _ATOMIC_RMW_( -= , 8, addr, atomic_index, val);
+}
+uint16_t cds_atomic_fetch_sub16(void* addr, int atomic_index, uint16_t val) {
+  _ATOMIC_RMW_( -= , 16, addr, atomic_index, val);
+}
+uint32_t cds_atomic_fetch_sub32(void* addr, int atomic_index, uint32_t val) {
+  _ATOMIC_RMW_( -= , 32, addr, atomic_index, val);
+}
+uint64_t cds_atomic_fetch_sub64(void* addr, int atomic_index, uint64_t val) {
+  _ATOMIC_RMW_( -= , 64, addr, atomic_index, val);
+}
+
+// cds atomic fetch and
+uint8_t cds_atomic_fetch_and8(void* addr, int atomic_index, uint8_t val) {
+  _ATOMIC_RMW_( &= , 8, addr, atomic_index, val);
+}
+uint16_t cds_atomic_fetch_and16(void* addr, int atomic_index, uint16_t val) {
+  _ATOMIC_RMW_( &= , 16, addr, atomic_index, val);
+}
+uint32_t cds_atomic_fetch_and32(void* addr, int atomic_index, uint32_t val) {
+  _ATOMIC_RMW_( &= , 32, addr, atomic_index, val);
+}
+uint64_t cds_atomic_fetch_and64(void* addr, int atomic_index, uint64_t val) {
+  _ATOMIC_RMW_( &= , 64, addr, atomic_index, val);
+}
+
+// cds atomic fetch or
+uint8_t cds_atomic_fetch_or8(void* addr, int atomic_index, uint8_t val) {
+  _ATOMIC_RMW_( |= , 8, addr, atomic_index, val);
+}
+uint16_t cds_atomic_fetch_or16(void* addr, int atomic_index, uint16_t val) {
+  _ATOMIC_RMW_( |= , 16, addr, atomic_index, val);
+}
+uint32_t cds_atomic_fetch_or32(void* addr, int atomic_index, uint32_t val) {
+  _ATOMIC_RMW_( |= , 32, addr, atomic_index, val);
+}
+uint64_t cds_atomic_fetch_or64(void* addr, int atomic_index, uint64_t val) {
+  _ATOMIC_RMW_( |= , 64, addr, atomic_index, val);
+}
+
+// cds atomic fetch xor
+uint8_t cds_atomic_fetch_xor8(void* addr, int atomic_index, uint8_t val) {
+  _ATOMIC_RMW_( ^= , 8, addr, atomic_index, val);
+}
+uint16_t cds_atomic_fetch_xor16(void* addr, int atomic_index, uint16_t val) {
+  _ATOMIC_RMW_( ^= , 16, addr, atomic_index, val);
+}
+uint32_t cds_atomic_fetch_xor32(void* addr, int atomic_index, uint32_t val) {
+  _ATOMIC_RMW_( ^= , 32, addr, atomic_index, val);
+}
+uint64_t cds_atomic_fetch_xor64(void* addr, int atomic_index, uint64_t val) {
+  _ATOMIC_RMW_( ^= , 64, addr, atomic_index, val);
+}
+
+// cds atomic compare and exchange
+// In order to accomodate the LLVM PASS, the return values are not true or false. 
+
+#define _ATOMIC_CMPSWP_WEAK_ _ATOMIC_CMPSWP_
+#define _ATOMIC_CMPSWP_(size, addr, expected, desired, atomic_index)                            \
+({                                                                                              \
+  uint##size##_t _desired = desired;                                                            \
+  uint##size##_t _expected = expected;                                                          \
+  uint##size##_t _old = model_rmwr_action_helper(addr, atomic_index);                           \
+  if (_old == _expected  ) {                                                                    \
+    model_rmw_action_helper(addr, atomic_index, (uint64_t) _desired ); return _expected; }      \
+  else {                                                                                        \
+    model_rmwc_action_helper(addr, atomic_index); _expected = _old; return _old; }              \
+})
+
+// expected is supposed to be a pointer to an address, but the CmpOperand
+// extracted from LLVM IR is an integer type. 
+
+uint8_t cds_atomic_compare_exchange8(void* addr, uint8_t expected, 
+                uint8_t desired, int atomic_index_succ, int atomic_index_fail ) {
+  _ATOMIC_CMPSWP_(8, addr, expected, desired, atomic_index_succ );
+}
+uint16_t cds_atomic_compare_exchange16(void* addr, uint16_t expected,
+                uint16_t desired, int atomic_index_succ, int atomic_index_fail ) {
+  _ATOMIC_CMPSWP_(16, addr, expected, desired, atomic_index_succ );
+}
+uint32_t cds_atomic_compare_exchange32(void* addr, uint32_t expected, 
+                uint32_t desired, int atomic_index_succ, int atomic_index_fail ) {
+  _ATOMIC_CMPSWP_(32, addr, expected, desired, atomic_index_succ );
+}
+uint64_t cds_atomic_compare_exchange64(void* addr, uint64_t expected, 
+                uint64_t desired, int atomic_index_succ, int atomic_index_fail ) {
+  _ATOMIC_CMPSWP_(64, addr, expected, desired, atomic_index_succ );
+}
+
+// cds atomic thread fence
+
+void cds_atomic_thread_fence(int atomic_index) {
+	model->switch_to_master(new ModelAction(ATOMIC_FENCE, orders[atomic_index], FENCE_LOCATION));
+}
+
+/*
+#define _ATOMIC_CMPSWP_( __a__, __e__, __m__, __x__ )                         \
+        ({ volatile __typeof__((__a__)->__f__)* __p__ = & ((__a__)->__f__);   \
+                __typeof__(__e__) __q__ = (__e__);                            \
+                __typeof__(__m__) __v__ = (__m__);                            \
+                bool __r__;                                                   \
+                __typeof__((__a__)->__f__) __t__=(__typeof__((__a__)->__f__)) model_rmwr_action((void *)__p__, __x__); \
+                if (__t__ == * __q__ ) {                                      \
+                        model_rmw_action((void *)__p__, __x__, (uint64_t) __v__); __r__ = true; } \
+                else {  model_rmwc_action((void *)__p__, __x__); *__q__ = __t__;  __r__ = false;} \
+                __r__; })
+
+#define _ATOMIC_FENCE_( __x__ ) \
+        ({ model_fence_action(__x__);})
+*/
+
+/*
+
+#define _ATOMIC_MODIFY_( __a__, __o__, __m__, __x__ )                         \
+        ({ volatile __typeof__((__a__)->__f__)* __p__ = & ((__a__)->__f__);   \
+        __typeof__((__a__)->__f__) __old__=(__typeof__((__a__)->__f__)) model_rmwr_action((void *)__p__, __x__); \
+        __typeof__(__m__) __v__ = (__m__);                                    \
+        __typeof__((__a__)->__f__) __copy__= __old__;                         \
+        __copy__ __o__ __v__;                                                 \
+        model_rmw_action((void *)__p__, __x__, (uint64_t) __copy__);          \
+        __old__ = __old__;  Silence clang (-Wunused-value)                    \
+         })                           
+*/
diff --git a/execution.cc b/execution.cc
index 0fcf4e8d..869833c2 100644
--- a/execution.cc
+++ b/execution.cc
@@ -1132,6 +1132,7 @@ bool ModelExecution::initialize_curr_action(ModelAction **curr)
  *
  * @return True if this read established synchronization
  */
+
 bool ModelExecution::read_from(ModelAction *act, const ModelAction *rf)
 {
 	ASSERT(rf);
diff --git a/include/cmodelint.h b/include/cmodelint.h
index 24c5f6fb..1c456b89 100644
--- a/include/cmodelint.h
+++ b/include/cmodelint.h
@@ -20,6 +20,68 @@ void model_rmw_action(void *obj, memory_order ord, uint64_t val);
 void model_rmwc_action(void *obj, memory_order ord);
 void model_fence_action(memory_order ord);
 
+// void model_init_action_helper(void * obj, uint64_t val);
+uint64_t model_rmwr_action_helper(void *obj, int atomic_index);
+void model_rmw_action_helper(void *obj, int atomic_index, uint64_t val);
+void model_rmwc_action_helper(void *obj, int atomic_index);
+void model_fence_action_helper(int atomic_index);
+
+// WL
+uint8_t  cds_atomic_load8(void * obj, int atomic_index);
+uint16_t cds_atomic_load16(void * obj, int atomic_index);
+uint32_t cds_atomic_load32(void * obj, int atomic_index);
+uint64_t cds_atomic_load64(void * obj, int atomic_index);
+
+void cds_atomic_store8(void * obj, int atomic_index, uint8_t val);
+void cds_atomic_store16(void * obj, int atomic_index, uint16_t val);
+void cds_atomic_store32(void * obj, int atomic_index, uint32_t val);
+void cds_atomic_store64(void * obj, int atomic_index, uint64_t val);
+
+
+// cds atomic exchange
+uint8_t cds_atomic_exchange8(void* addr, int atomic_index, uint8_t val);
+uint16_t cds_atomic_exchange16(void* addr, int atomic_index, uint16_t val);
+uint32_t cds_atomic_exchange32(void* addr, int atomic_index, uint32_t val);
+uint64_t cds_atomic_exchange64(void* addr, int atomic_index, uint64_t val);
+// cds atomic fetch add
+uint8_t  cds_atomic_fetch_add8(void* addr, int atomic_index, uint8_t val);
+uint16_t cds_atomic_fetch_add16(void* addr, int atomic_index, uint16_t val);
+uint32_t cds_atomic_fetch_add32(void* addr, int atomic_index, uint32_t val);
+uint64_t cds_atomic_fetch_add64(void* addr, int atomic_index, uint64_t val);
+// cds atomic fetch sub
+uint8_t  cds_atomic_fetch_sub8(void* addr, int atomic_index, uint8_t val);
+uint16_t cds_atomic_fetch_sub16(void* addr, int atomic_index, uint16_t val);
+uint32_t cds_atomic_fetch_sub32(void* addr, int atomic_index, uint32_t val);
+uint64_t cds_atomic_fetch_sub64(void* addr, int atomic_index, uint64_t val);
+// cds atomic fetch and
+uint8_t cds_atomic_fetch_and8(void* addr, int atomic_index, uint8_t val);
+uint16_t cds_atomic_fetch_and16(void* addr, int atomic_index, uint16_t val);
+uint32_t cds_atomic_fetch_and32(void* addr, int atomic_index, uint32_t val);
+uint64_t cds_atomic_fetch_and64(void* addr, int atomic_index, uint64_t val);
+// cds atomic fetch or
+uint8_t cds_atomic_fetch_or8(void* addr, int atomic_index, uint8_t val);
+uint16_t cds_atomic_fetch_or16(void* addr, int atomic_index, uint16_t val);
+uint32_t cds_atomic_fetch_or32(void* addr, int atomic_index, uint32_t val);
+uint64_t cds_atomic_fetch_or64(void* addr, int atomic_index, uint64_t val);
+// cds atomic fetch xor
+uint8_t cds_atomic_fetch_xor8(void* addr, int atomic_index, uint8_t val);
+uint16_t cds_atomic_fetch_xor16(void* addr, int atomic_index, uint16_t val);
+uint32_t cds_atomic_fetch_xor32(void* addr, int atomic_index, uint32_t val);
+uint64_t cds_atomic_fetch_xor64(void* addr, int atomic_index, uint64_t val);
+
+// cds atomic compare and exchange (strong)
+
+uint8_t cds_atomic_compare_exchange8(void* addr, uint8_t expected, 
+                  uint8_t desire, int atomic_index_succ, int atomic_index_fail );
+uint16_t cds_atomic_compare_exchange16(void* addr, uint16_t expected,
+                  uint16_t desire, int atomic_index_succ, int atomic_index_fail );
+uint32_t cds_atomic_compare_exchange32(void* addr, uint32_t expected, 
+                  uint32_t desire, int atomic_index_succ, int atomic_index_fail );
+uint64_t cds_atomic_compare_exchange64(void* addr, uint64_t expected, 
+                  uint64_t desire, int atomic_index_succ, int atomic_index_fail );
+
+// cds atomic thread fence
+void cds_atomic_thread_fence(int atomic_index);
 
 #if __cplusplus
 }
diff --git a/include/impatomic.h b/include/impatomic.h
index b4273eee..100ad0d6 100644
--- a/include/impatomic.h
+++ b/include/impatomic.h
@@ -1,3 +1,4 @@
+#include <stdio.h>
 /**
  * @file impatomic.h
  * @brief Common header for C11/C++11 atomics
@@ -118,7 +119,7 @@ inline void atomic_flag::clear( memory_order __x__ ) volatile
                 __typeof__(__m__) __v__ = (__m__);                            \
                 bool __r__;                                                   \
                 __typeof__((__a__)->__f__) __t__=(__typeof__((__a__)->__f__)) model_rmwr_action((void *)__p__, __x__); \
-                if (__t__ == * __q__ ) {                                      \
+                if (__t__ == * __q__ ) {;                                     \
                         model_rmw_action((void *)__p__, __x__, (uint64_t) __v__); __r__ = true; } \
                 else {  model_rmwc_action((void *)__p__, __x__); *__q__ = __t__;  __r__ = false;} \
                 __r__; })
diff --git a/include/librace.h b/include/librace.h
index cabf0661..83e05d92 100644
--- a/include/librace.h
+++ b/include/librace.h
@@ -21,6 +21,16 @@ extern "C" {
 	uint32_t load_32(const void *addr);
 	uint64_t load_64(const void *addr);
 
+	void cds_store8(void *addr);
+	void cds_store16(void *addr);
+	void cds_store32(void *addr);
+	void cds_store64(void *addr);
+
+	void cds_load8(const void *addr);
+	void cds_load16(const void *addr);
+	void cds_load32(const void *addr);
+	void cds_load64(const void *addr);
+
 #ifdef __cplusplus
 }
 #endif
diff --git a/include/memoryorder.h b/include/memoryorder.h
index ba0dafd6..704d15e7 100644
--- a/include/memoryorder.h
+++ b/include/memoryorder.h
@@ -14,8 +14,8 @@ namespace std {
 
 
 typedef enum memory_order {
-    memory_order_relaxed, memory_order_acquire, memory_order_release,
-    memory_order_acq_rel, memory_order_seq_cst
+    memory_order_relaxed, memory_order_consume, memory_order_acquire, 
+    memory_order_release, memory_order_acq_rel, memory_order_seq_cst
 } memory_order;
 
 
diff --git a/include/stdatomic.h b/include/stdatomic.h
deleted file mode 100644
index d4d21984..00000000
--- a/include/stdatomic.h
+++ /dev/null
@@ -1,72 +0,0 @@
-/**
- * @file stdatomic.h
- * @brief C11 atomic interface header
- */
-
-#ifndef __STDATOMIC_H__
-#define __STDATOMIC_H__
-
-#include "impatomic.h"
-
-#ifdef __cplusplus
-
-
-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;
-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;
-
-#endif /* __cplusplus */
-
-#endif /* __STDATOMIC_H__ */
diff --git a/include/stdatomic2.h b/include/stdatomic2.h
new file mode 100644
index 00000000..d4d21984
--- /dev/null
+++ b/include/stdatomic2.h
@@ -0,0 +1,72 @@
+/**
+ * @file stdatomic.h
+ * @brief C11 atomic interface header
+ */
+
+#ifndef __STDATOMIC_H__
+#define __STDATOMIC_H__
+
+#include "impatomic.h"
+
+#ifdef __cplusplus
+
+
+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;
+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;
+
+#endif /* __cplusplus */
+
+#endif /* __STDATOMIC_H__ */
diff --git a/librace.cc b/librace.cc
index 2c36054b..5dafc6ff 100644
--- a/librace.cc
+++ b/librace.cc
@@ -92,3 +92,52 @@ uint64_t load_64(const void *addr)
 	raceCheckRead(tid, (const void *)(((uintptr_t)addr) + 7));
 	return *((uint64_t *)addr);
 }
+
+// helper functions used by CdsPass
+// The CdsPass implementation does not replace normal load/stores with cds load/stores,
+// but inserts cds load/stores to check dataraces. Thus, the cds load/stores do not
+// return anything. 
+
+void cds_store8(void *addr)
+{
+	DEBUG("addr = %p, val = %" PRIu8 "\n", addr, val);
+	thread_id_t tid = thread_current()->get_id();
+	raceCheckWrite(tid, addr);
+}
+
+void cds_store16(void *addr)
+{
+	DEBUG("addr = %p, val = %" PRIu16 "\n", addr, val);
+	thread_id_t tid = thread_current()->get_id();
+	raceCheckWrite(tid, addr);
+	raceCheckWrite(tid, (void *)(((uintptr_t)addr) + 1));
+}
+
+void cds_store32(void *addr)
+{
+	DEBUG("addr = %p, val = %" PRIu32 "\n", addr, val);
+	thread_id_t tid = thread_current()->get_id();
+	raceCheckWrite(tid, addr);
+	raceCheckWrite(tid, (void *)(((uintptr_t)addr) + 1));
+	raceCheckWrite(tid, (void *)(((uintptr_t)addr) + 2));
+	raceCheckWrite(tid, (void *)(((uintptr_t)addr) + 3));
+}
+
+void cds_store64(void *addr)
+{
+	DEBUG("addr = %p, val = %" PRIu64 "\n", addr, val);
+	thread_id_t tid = thread_current()->get_id();
+	raceCheckWrite(tid, addr);
+	raceCheckWrite(tid, (void *)(((uintptr_t)addr) + 1));
+	raceCheckWrite(tid, (void *)(((uintptr_t)addr) + 2));
+	raceCheckWrite(tid, (void *)(((uintptr_t)addr) + 3));
+	raceCheckWrite(tid, (void *)(((uintptr_t)addr) + 4));
+	raceCheckWrite(tid, (void *)(((uintptr_t)addr) + 5));
+	raceCheckWrite(tid, (void *)(((uintptr_t)addr) + 6));
+	raceCheckWrite(tid, (void *)(((uintptr_t)addr) + 7));
+}
+
+void cds_load8(const void *addr) { load_8(addr); }
+void cds_load16(const void *addr) { load_16(addr); }
+void cds_load32(const void *addr) { load_32(addr); }
+void cds_load64(const void *addr) { load_64(addr); }
\ No newline at end of file
diff --git a/model.cc b/model.cc
index bfb6d22f..ccc109a7 100644
--- a/model.cc
+++ b/model.cc
@@ -512,11 +512,14 @@ void ModelChecker::run()
 				if (act && execution->is_enabled(th) && (th->get_state() != THREAD_BLOCKED) ){
 					if (act->is_write()){
 						std::memory_order order = act->get_mo(); 
-				                if (order == std::memory_order_relaxed || order == std::memory_order_release) {
+				                if (order == std::memory_order_relaxed || \
+							order == std::memory_order_release) {
 							t = th;
 							break;
 						}
-					} else if (act->get_type() == THREAD_CREATE || act->get_type() == THREAD_START || act->get_type() == THREAD_FINISH) {
+					} else if (act->get_type() == THREAD_CREATE || \
+							act->get_type() == THREAD_START || \
+							act->get_type() == THREAD_FINISH) {
 						t = th;
 						break;
 					}				
@@ -539,7 +542,7 @@ void ModelChecker::run()
 
 		has_next = next_execution();
 		i++;
-	} while (i<250); // while (has_next);
+	} while (i<100); // while (has_next);
 
 	execution->fixup_release_sequences();
 
diff --git a/snapshot.cc b/snapshot.cc
index 66faacd8..7deaeff4 100644
--- a/snapshot.cc
+++ b/snapshot.cc
@@ -110,7 +110,7 @@ static void mprot_handle_pf(int sig, siginfo_t *si, void *unused)
 		model_print("For debugging, place breakpoint at: %s:%d\n",
 				__FILE__, __LINE__);
 		// print_trace(); // Trace printing may cause dynamic memory allocation
-		exit(EXIT_FAILURE);
+ 		exit(EXIT_FAILURE);
 	}
 	void* addr = ReturnPageAlignedAddress(si->si_addr);
 
diff --git a/test/memo/double-read-fv b/test/memo/double-read-fv
new file mode 100755
index 00000000..eb48204d
Binary files /dev/null and b/test/memo/double-read-fv differ
diff --git a/test/memo/fences b/test/memo/fences
new file mode 100755
index 00000000..31963619
Binary files /dev/null and b/test/memo/fences differ
diff --git a/test/memo/original b/test/memo/original
new file mode 100644
index 00000000..68f653ef
--- /dev/null
+++ b/test/memo/original
@@ -0,0 +1,737 @@
+Program output from execution 1:
+---- BEGIN PROGRAM OUTPUT ----
+CDSChecker
+Copyright (c) 2013 Regents of the University of California. All rights reserved.
+Distributed under the GPLv2
+Written by Brian Norris and Brian Demsky
+
+v3 = 0, v4=0
+v1 = 1, v2=1
+---- END PROGRAM OUTPUT   ----
+
+Execution trace 1:
+------------------------------------------------------------------------------------
+#    t    Action type     MO       Location         Value               Rf  CV
+------------------------------------------------------------------------------------
+1    1    thread start    seq_cst  0x7f91579ab7c0   0xdeadbeef              ( 0,  1)
+2    1    init atomic     relaxed        0x60106c   0                       ( 0,  2)
+3    1    init atomic     relaxed        0x601070   0                       ( 0,  3)
+4    1    thread create   seq_cst  0x7f9157aabb68   0x7f9157aabaf0          ( 0,  4)
+5    1    thread create   seq_cst  0x7f9157aabb60   0x7f9157aabaf0          ( 0,  5)
+6    2    thread start    seq_cst  0x7f9157aabbc8   0xdeadbeef              ( 0,  4,  6)
+7    3    thread start    seq_cst  0x7f9157babfd0   0xdeadbeef              ( 0,  5,  0,  7)
+8    3    atomic rmw      relaxed        0x601070   0                   3   ( 0,  5,  0,  8)
+9    3    atomic rmw      relaxed        0x60106c   0                   2   ( 0,  5,  0,  9)
+10   3    thread finish   seq_cst  0x7f9157babfd0   0xdeadbeef              ( 0,  5,  0, 10)
+11   2    atomic rmw      relaxed        0x60106c   0x1                 9   ( 0,  4, 11)
+12   2    atomic rmw      relaxed        0x601070   0x1                 8   ( 0,  4, 12)
+13   2    thread finish   seq_cst  0x7f9157aabbc8   0xdeadbeef              ( 0,  4, 13)
+14   1    thread join     seq_cst  0x7f9157aabbc8   0x2                     ( 0, 14, 13)
+15   1    thread join     seq_cst  0x7f9157babfd0   0x3                     ( 0, 15, 13, 10)
+16   1    thread finish   seq_cst  0x7f91579ab7c0   0xdeadbeef              ( 0, 16, 13, 10)
+HASH 3212361479
+------------------------------------------------------------------------------------
+
+Program output from execution 5:
+---- BEGIN PROGRAM OUTPUT ----
+v3 = 0, v4=1
+v1 = 0, v2=1
+---- END PROGRAM OUTPUT   ----
+
+Execution trace 5:
+------------------------------------------------------------------------------------
+#    t    Action type     MO       Location         Value               Rf  CV
+------------------------------------------------------------------------------------
+1    1    thread start    seq_cst  0x7f91579ab7c0   0xdeadbeef              ( 0,  1)
+2    1    init atomic     relaxed        0x60106c   0                       ( 0,  2)
+3    1    init atomic     relaxed        0x601070   0                       ( 0,  3)
+4    1    thread create   seq_cst  0x7f9157aabb68   0x7f9157aabaf0          ( 0,  4)
+5    1    thread create   seq_cst  0x7f9157aabb60   0x7f9157aabaf0          ( 0,  5)
+6    2    thread start    seq_cst  0x7f9157aabbc8   0xdeadbeef              ( 0,  4,  6)
+7    3    thread start    seq_cst  0x7f9157babfd0   0xdeadbeef              ( 0,  5,  0,  7)
+8    2    atomic rmw      relaxed        0x60106c   0                   2   ( 0,  4,  8)
+9    3    atomic rmw      relaxed        0x601070   0                   3   ( 0,  5,  0,  9)
+10   3    atomic rmw      relaxed        0x60106c   0x1                 8   ( 0,  5,  0, 10)
+11   3    thread finish   seq_cst  0x7f9157babfd0   0xdeadbeef              ( 0,  5,  0, 11)
+12   2    atomic rmw      relaxed        0x601070   0x1                 9   ( 0,  4, 12)
+13   2    thread finish   seq_cst  0x7f9157aabbc8   0xdeadbeef              ( 0,  4, 13)
+14   1    thread join     seq_cst  0x7f9157aabbc8   0x2                     ( 0, 14, 13)
+15   1    thread join     seq_cst  0x7f9157babfd0   0x3                     ( 0, 15, 13, 11)
+16   1    thread finish   seq_cst  0x7f91579ab7c0   0xdeadbeef              ( 0, 16, 13, 11)
+HASH 4275545527
+------------------------------------------------------------------------------------
+
+Program output from execution 8:
+---- BEGIN PROGRAM OUTPUT ----
+v3 = 0, v4=1
+v1 = 0, v2=1
+---- END PROGRAM OUTPUT   ----
+
+Execution trace 8:
+------------------------------------------------------------------------------------
+#    t    Action type     MO       Location         Value               Rf  CV
+------------------------------------------------------------------------------------
+1    1    thread start    seq_cst  0x7f91579ab7c0   0xdeadbeef              ( 0,  1)
+2    1    init atomic     relaxed        0x60106c   0                       ( 0,  2)
+3    1    init atomic     relaxed        0x601070   0                       ( 0,  3)
+4    1    thread create   seq_cst  0x7f9157aabb68   0x7f9157aabaf0          ( 0,  4)
+5    1    thread create   seq_cst  0x7f9157aabb60   0x7f9157aabaf0          ( 0,  5)
+6    2    thread start    seq_cst  0x7f9157aabbc8   0xdeadbeef              ( 0,  4,  6)
+7    3    thread start    seq_cst  0x7f9157babfd0   0xdeadbeef              ( 0,  5,  0,  7)
+8    3    atomic rmw      relaxed        0x601070   0                   3   ( 0,  5,  0,  8)
+9    2    atomic rmw      relaxed        0x60106c   0                   2   ( 0,  4,  9)
+10   3    atomic rmw      relaxed        0x60106c   0x1                 9   ( 0,  5,  0, 10)
+11   3    thread finish   seq_cst  0x7f9157babfd0   0xdeadbeef              ( 0,  5,  0, 11)
+12   2    atomic rmw      relaxed        0x601070   0x1                 8   ( 0,  4, 12)
+13   2    thread finish   seq_cst  0x7f9157aabbc8   0xdeadbeef              ( 0,  4, 13)
+14   1    thread join     seq_cst  0x7f9157aabbc8   0x2                     ( 0, 14, 13)
+15   1    thread join     seq_cst  0x7f9157babfd0   0x3                     ( 0, 15, 13, 11)
+16   1    thread finish   seq_cst  0x7f91579ab7c0   0xdeadbeef              ( 0, 16, 13, 11)
+HASH 3067323839
+------------------------------------------------------------------------------------
+
+Program output from execution 9:
+---- BEGIN PROGRAM OUTPUT ----
+v3 = 0, v4=1
+v1 = 0, v2=1
+---- END PROGRAM OUTPUT   ----
+
+Execution trace 9:
+------------------------------------------------------------------------------------
+#    t    Action type     MO       Location         Value               Rf  CV
+------------------------------------------------------------------------------------
+1    1    thread start    seq_cst  0x7f91579ab7c0   0xdeadbeef              ( 0,  1)
+2    1    init atomic     relaxed        0x60106c   0                       ( 0,  2)
+3    1    init atomic     relaxed        0x601070   0                       ( 0,  3)
+4    1    thread create   seq_cst  0x7f9157aabb68   0x7f9157aabaf0          ( 0,  4)
+5    1    thread create   seq_cst  0x7f9157aabb60   0x7f9157aabaf0          ( 0,  5)
+6    2    thread start    seq_cst  0x7f9157aabbc8   0xdeadbeef              ( 0,  4,  6)
+7    3    thread start    seq_cst  0x7f9157babfd0   0xdeadbeef              ( 0,  5,  0,  7)
+8    3    atomic rmw      relaxed        0x601070   0                   3   ( 0,  5,  0,  8)
+9    2    atomic rmw      relaxed        0x60106c   0                   2   ( 0,  4,  9)
+10   3    atomic rmw      relaxed        0x60106c   0x1                 9   ( 0,  5,  0, 10)
+11   3    thread finish   seq_cst  0x7f9157babfd0   0xdeadbeef              ( 0,  5,  0, 11)
+12   2    atomic rmw      relaxed        0x601070   0x1                 8   ( 0,  4, 12)
+13   2    thread finish   seq_cst  0x7f9157aabbc8   0xdeadbeef              ( 0,  4, 13)
+14   1    thread join     seq_cst  0x7f9157aabbc8   0x2                     ( 0, 14, 13)
+15   1    thread join     seq_cst  0x7f9157babfd0   0x3                     ( 0, 15, 13, 11)
+16   1    thread finish   seq_cst  0x7f91579ab7c0   0xdeadbeef              ( 0, 16, 13, 11)
+HASH 3067323839
+------------------------------------------------------------------------------------
+
+Program output from execution 13:
+---- BEGIN PROGRAM OUTPUT ----
+v1 = 0, v2=1
+v3 = 0, v4=1
+---- END PROGRAM OUTPUT   ----
+
+Execution trace 13:
+------------------------------------------------------------------------------------
+#    t    Action type     MO       Location         Value               Rf  CV
+------------------------------------------------------------------------------------
+1    1    thread start    seq_cst  0x7f91579ab7c0   0xdeadbeef              ( 0,  1)
+2    1    init atomic     relaxed        0x60106c   0                       ( 0,  2)
+3    1    init atomic     relaxed        0x601070   0                       ( 0,  3)
+4    1    thread create   seq_cst  0x7f9157aabb68   0x7f9157aabaf0          ( 0,  4)
+5    1    thread create   seq_cst  0x7f9157aabb60   0x7f9157aabaf0          ( 0,  5)
+6    2    thread start    seq_cst  0x7f9157aabbc8   0xdeadbeef              ( 0,  4,  6)
+7    3    thread start    seq_cst  0x7f9157babfd0   0xdeadbeef              ( 0,  5,  0,  7)
+8    3    atomic rmw      relaxed        0x601070   0                   3   ( 0,  5,  0,  8)
+9    2    atomic rmw      relaxed        0x60106c   0                   2   ( 0,  4,  9)
+10   2    atomic rmw      relaxed        0x601070   0x1                 8   ( 0,  4, 10)
+11   2    thread finish   seq_cst  0x7f9157aabbc8   0xdeadbeef              ( 0,  4, 11)
+12   3    atomic rmw      relaxed        0x60106c   0x1                 9   ( 0,  5,  0, 12)
+13   3    thread finish   seq_cst  0x7f9157babfd0   0xdeadbeef              ( 0,  5,  0, 13)
+14   1    thread join     seq_cst  0x7f9157aabbc8   0x2                     ( 0, 14, 11)
+15   1    thread join     seq_cst  0x7f9157babfd0   0x3                     ( 0, 15, 11, 13)
+16   1    thread finish   seq_cst  0x7f91579ab7c0   0xdeadbeef              ( 0, 16, 11, 13)
+HASH 3086165503
+------------------------------------------------------------------------------------
+
+Program output from execution 14:
+---- BEGIN PROGRAM OUTPUT ----
+v3 = 0, v4=1
+v1 = 0, v2=1
+---- END PROGRAM OUTPUT   ----
+
+Execution trace 14:
+------------------------------------------------------------------------------------
+#    t    Action type     MO       Location         Value               Rf  CV
+------------------------------------------------------------------------------------
+1    1    thread start    seq_cst  0x7f91579ab7c0   0xdeadbeef              ( 0,  1)
+2    1    init atomic     relaxed        0x60106c   0                       ( 0,  2)
+3    1    init atomic     relaxed        0x601070   0                       ( 0,  3)
+4    1    thread create   seq_cst  0x7f9157aabb68   0x7f9157aabaf0          ( 0,  4)
+5    1    thread create   seq_cst  0x7f9157aabb60   0x7f9157aabaf0          ( 0,  5)
+6    2    thread start    seq_cst  0x7f9157aabbc8   0xdeadbeef              ( 0,  4,  6)
+7    3    thread start    seq_cst  0x7f9157babfd0   0xdeadbeef              ( 0,  5,  0,  7)
+8    3    atomic rmw      relaxed        0x601070   0                   3   ( 0,  5,  0,  8)
+9    2    atomic rmw      relaxed        0x60106c   0                   2   ( 0,  4,  9)
+10   3    atomic rmw      relaxed        0x60106c   0x1                 9   ( 0,  5,  0, 10)
+11   3    thread finish   seq_cst  0x7f9157babfd0   0xdeadbeef              ( 0,  5,  0, 11)
+12   2    atomic rmw      relaxed        0x601070   0x1                 8   ( 0,  4, 12)
+13   2    thread finish   seq_cst  0x7f9157aabbc8   0xdeadbeef              ( 0,  4, 13)
+14   1    thread join     seq_cst  0x7f9157aabbc8   0x2                     ( 0, 14, 13)
+15   1    thread join     seq_cst  0x7f9157babfd0   0x3                     ( 0, 15, 13, 11)
+16   1    thread finish   seq_cst  0x7f91579ab7c0   0xdeadbeef              ( 0, 16, 13, 11)
+HASH 3067323839
+------------------------------------------------------------------------------------
+
+Program output from execution 16:
+---- BEGIN PROGRAM OUTPUT ----
+v1 = 0, v2=0
+v3 = 1, v4=1
+---- END PROGRAM OUTPUT   ----
+
+Execution trace 16:
+------------------------------------------------------------------------------------
+#    t    Action type     MO       Location         Value               Rf  CV
+------------------------------------------------------------------------------------
+1    1    thread start    seq_cst  0x7f91579ab7c0   0xdeadbeef              ( 0,  1)
+2    1    init atomic     relaxed        0x60106c   0                       ( 0,  2)
+3    1    init atomic     relaxed        0x601070   0                       ( 0,  3)
+4    1    thread create   seq_cst  0x7f9157aabb68   0x7f9157aabaf0          ( 0,  4)
+5    1    thread create   seq_cst  0x7f9157aabb60   0x7f9157aabaf0          ( 0,  5)
+6    2    thread start    seq_cst  0x7f9157aabbc8   0xdeadbeef              ( 0,  4,  6)
+7    3    thread start    seq_cst  0x7f9157babfd0   0xdeadbeef              ( 0,  5,  0,  7)
+8    2    atomic rmw      relaxed        0x60106c   0                   2   ( 0,  4,  8)
+9    2    atomic rmw      relaxed        0x601070   0                   3   ( 0,  4,  9)
+10   2    thread finish   seq_cst  0x7f9157aabbc8   0xdeadbeef              ( 0,  4, 10)
+11   1    thread join     seq_cst  0x7f9157aabbc8   0x2                     ( 0, 11, 10)
+12   3    atomic rmw      relaxed        0x601070   0x1                 9   ( 0,  5,  0, 12)
+13   3    atomic rmw      relaxed        0x60106c   0x1                 8   ( 0,  5,  0, 13)
+14   3    thread finish   seq_cst  0x7f9157babfd0   0xdeadbeef              ( 0,  5,  0, 14)
+15   1    thread join     seq_cst  0x7f9157babfd0   0x3                     ( 0, 15, 10, 14)
+16   1    thread finish   seq_cst  0x7f91579ab7c0   0xdeadbeef              ( 0, 16, 10, 14)
+HASH 4127308943
+------------------------------------------------------------------------------------
+
+Program output from execution 17:
+---- BEGIN PROGRAM OUTPUT ----
+v1 = 0, v2=0
+v3 = 1, v4=1
+---- END PROGRAM OUTPUT   ----
+
+Execution trace 17:
+------------------------------------------------------------------------------------
+#    t    Action type     MO       Location         Value               Rf  CV
+------------------------------------------------------------------------------------
+1    1    thread start    seq_cst  0x7f91579ab7c0   0xdeadbeef              ( 0,  1)
+2    1    init atomic     relaxed        0x60106c   0                       ( 0,  2)
+3    1    init atomic     relaxed        0x601070   0                       ( 0,  3)
+4    1    thread create   seq_cst  0x7f9157aabb68   0x7f9157aabaf0          ( 0,  4)
+5    1    thread create   seq_cst  0x7f9157aabb60   0x7f9157aabaf0          ( 0,  5)
+6    2    thread start    seq_cst  0x7f9157aabbc8   0xdeadbeef              ( 0,  4,  6)
+7    3    thread start    seq_cst  0x7f9157babfd0   0xdeadbeef              ( 0,  5,  0,  7)
+8    2    atomic rmw      relaxed        0x60106c   0                   2   ( 0,  4,  8)
+9    2    atomic rmw      relaxed        0x601070   0                   3   ( 0,  4,  9)
+10   2    thread finish   seq_cst  0x7f9157aabbc8   0xdeadbeef              ( 0,  4, 10)
+11   3    atomic rmw      relaxed        0x601070   0x1                 9   ( 0,  5,  0, 11)
+12   3    atomic rmw      relaxed        0x60106c   0x1                 8   ( 0,  5,  0, 12)
+13   3    thread finish   seq_cst  0x7f9157babfd0   0xdeadbeef              ( 0,  5,  0, 13)
+14   1    thread join     seq_cst  0x7f9157aabbc8   0x2                     ( 0, 14, 10)
+15   1    thread join     seq_cst  0x7f9157babfd0   0x3                     ( 0, 15, 10, 13)
+16   1    thread finish   seq_cst  0x7f91579ab7c0   0xdeadbeef              ( 0, 16, 10, 13)
+HASH 4133240655
+------------------------------------------------------------------------------------
+
+Program output from execution 22:
+---- BEGIN PROGRAM OUTPUT ----
+v3 = 0, v4=1
+v1 = 0, v2=1
+---- END PROGRAM OUTPUT   ----
+
+Execution trace 22:
+------------------------------------------------------------------------------------
+#    t    Action type     MO       Location         Value               Rf  CV
+------------------------------------------------------------------------------------
+1    1    thread start    seq_cst  0x7f91579ab7c0   0xdeadbeef              ( 0,  1)
+2    1    init atomic     relaxed        0x60106c   0                       ( 0,  2)
+3    1    init atomic     relaxed        0x601070   0                       ( 0,  3)
+4    1    thread create   seq_cst  0x7f9157aabb68   0x7f9157aabaf0          ( 0,  4)
+5    1    thread create   seq_cst  0x7f9157aabb60   0x7f9157aabaf0          ( 0,  5)
+6    2    thread start    seq_cst  0x7f9157aabbc8   0xdeadbeef              ( 0,  4,  6)
+7    3    thread start    seq_cst  0x7f9157babfd0   0xdeadbeef              ( 0,  5,  0,  7)
+8    3    atomic rmw      relaxed        0x601070   0                   3   ( 0,  5,  0,  8)
+9    2    atomic rmw      relaxed        0x60106c   0                   2   ( 0,  4,  9)
+10   3    atomic rmw      relaxed        0x60106c   0x1                 9   ( 0,  5,  0, 10)
+11   3    thread finish   seq_cst  0x7f9157babfd0   0xdeadbeef              ( 0,  5,  0, 11)
+12   2    atomic rmw      relaxed        0x601070   0x1                 8   ( 0,  4, 12)
+13   2    thread finish   seq_cst  0x7f9157aabbc8   0xdeadbeef              ( 0,  4, 13)
+14   1    thread join     seq_cst  0x7f9157aabbc8   0x2                     ( 0, 14, 13)
+15   1    thread join     seq_cst  0x7f9157babfd0   0x3                     ( 0, 15, 13, 11)
+16   1    thread finish   seq_cst  0x7f91579ab7c0   0xdeadbeef              ( 0, 16, 13, 11)
+HASH 3067323839
+------------------------------------------------------------------------------------
+
+Program output from execution 24:
+---- BEGIN PROGRAM OUTPUT ----
+v3 = 0, v4=0
+v1 = 1, v2=1
+---- END PROGRAM OUTPUT   ----
+
+Execution trace 24:
+------------------------------------------------------------------------------------
+#    t    Action type     MO       Location         Value               Rf  CV
+------------------------------------------------------------------------------------
+1    1    thread start    seq_cst  0x7f91579ab7c0   0xdeadbeef              ( 0,  1)
+2    1    init atomic     relaxed        0x60106c   0                       ( 0,  2)
+3    1    init atomic     relaxed        0x601070   0                       ( 0,  3)
+4    1    thread create   seq_cst  0x7f9157aabb68   0x7f9157aabaf0          ( 0,  4)
+5    1    thread create   seq_cst  0x7f9157aabb60   0x7f9157aabaf0          ( 0,  5)
+6    2    thread start    seq_cst  0x7f9157aabbc8   0xdeadbeef              ( 0,  4,  6)
+7    3    thread start    seq_cst  0x7f9157babfd0   0xdeadbeef              ( 0,  5,  0,  7)
+8    3    atomic rmw      relaxed        0x601070   0                   3   ( 0,  5,  0,  8)
+9    3    atomic rmw      relaxed        0x60106c   0                   2   ( 0,  5,  0,  9)
+10   3    thread finish   seq_cst  0x7f9157babfd0   0xdeadbeef              ( 0,  5,  0, 10)
+11   2    atomic rmw      relaxed        0x60106c   0x1                 9   ( 0,  4, 11)
+12   2    atomic rmw      relaxed        0x601070   0x1                 8   ( 0,  4, 12)
+13   2    thread finish   seq_cst  0x7f9157aabbc8   0xdeadbeef              ( 0,  4, 13)
+14   1    thread join     seq_cst  0x7f9157aabbc8   0x2                     ( 0, 14, 13)
+15   1    thread join     seq_cst  0x7f9157babfd0   0x3                     ( 0, 15, 13, 10)
+16   1    thread finish   seq_cst  0x7f91579ab7c0   0xdeadbeef              ( 0, 16, 13, 10)
+HASH 3212361479
+------------------------------------------------------------------------------------
+
+Program output from execution 37:
+---- BEGIN PROGRAM OUTPUT ----
+v3 = 0, v4=1
+v1 = 0, v2=1
+---- END PROGRAM OUTPUT   ----
+
+Execution trace 37:
+------------------------------------------------------------------------------------
+#    t    Action type     MO       Location         Value               Rf  CV
+------------------------------------------------------------------------------------
+1    1    thread start    seq_cst  0x7f91579ab7c0   0xdeadbeef              ( 0,  1)
+2    1    init atomic     relaxed        0x60106c   0                       ( 0,  2)
+3    1    init atomic     relaxed        0x601070   0                       ( 0,  3)
+4    1    thread create   seq_cst  0x7f9157aabb68   0x7f9157aabaf0          ( 0,  4)
+5    1    thread create   seq_cst  0x7f9157aabb60   0x7f9157aabaf0          ( 0,  5)
+6    2    thread start    seq_cst  0x7f9157aabbc8   0xdeadbeef              ( 0,  4,  6)
+7    3    thread start    seq_cst  0x7f9157babfd0   0xdeadbeef              ( 0,  5,  0,  7)
+8    3    atomic rmw      relaxed        0x601070   0                   3   ( 0,  5,  0,  8)
+9    2    atomic rmw      relaxed        0x60106c   0                   2   ( 0,  4,  9)
+10   3    atomic rmw      relaxed        0x60106c   0x1                 9   ( 0,  5,  0, 10)
+11   3    thread finish   seq_cst  0x7f9157babfd0   0xdeadbeef              ( 0,  5,  0, 11)
+12   2    atomic rmw      relaxed        0x601070   0x1                 8   ( 0,  4, 12)
+13   2    thread finish   seq_cst  0x7f9157aabbc8   0xdeadbeef              ( 0,  4, 13)
+14   1    thread join     seq_cst  0x7f9157aabbc8   0x2                     ( 0, 14, 13)
+15   1    thread join     seq_cst  0x7f9157babfd0   0x3                     ( 0, 15, 13, 11)
+16   1    thread finish   seq_cst  0x7f91579ab7c0   0xdeadbeef              ( 0, 16, 13, 11)
+HASH 3067323839
+------------------------------------------------------------------------------------
+
+Program output from execution 48:
+---- BEGIN PROGRAM OUTPUT ----
+v1 = 0, v2=1
+v3 = 0, v4=1
+---- END PROGRAM OUTPUT   ----
+
+Execution trace 48:
+------------------------------------------------------------------------------------
+#    t    Action type     MO       Location         Value               Rf  CV
+------------------------------------------------------------------------------------
+1    1    thread start    seq_cst  0x7f91579ab7c0   0xdeadbeef              ( 0,  1)
+2    1    init atomic     relaxed        0x60106c   0                       ( 0,  2)
+3    1    init atomic     relaxed        0x601070   0                       ( 0,  3)
+4    1    thread create   seq_cst  0x7f9157aabb68   0x7f9157aabaf0          ( 0,  4)
+5    1    thread create   seq_cst  0x7f9157aabb60   0x7f9157aabaf0          ( 0,  5)
+6    2    thread start    seq_cst  0x7f9157aabbc8   0xdeadbeef              ( 0,  4,  6)
+7    3    thread start    seq_cst  0x7f9157babfd0   0xdeadbeef              ( 0,  5,  0,  7)
+8    2    atomic rmw      relaxed        0x60106c   0                   2   ( 0,  4,  8)
+9    3    atomic rmw      relaxed        0x601070   0                   3   ( 0,  5,  0,  9)
+10   2    atomic rmw      relaxed        0x601070   0x1                 9   ( 0,  4, 10)
+11   2    thread finish   seq_cst  0x7f9157aabbc8   0xdeadbeef              ( 0,  4, 11)
+12   3    atomic rmw      relaxed        0x60106c   0x1                 8   ( 0,  5,  0, 12)
+13   3    thread finish   seq_cst  0x7f9157babfd0   0xdeadbeef              ( 0,  5,  0, 13)
+14   1    thread join     seq_cst  0x7f9157aabbc8   0x2                     ( 0, 14, 11)
+15   1    thread join     seq_cst  0x7f9157babfd0   0x3                     ( 0, 15, 11, 13)
+16   1    thread finish   seq_cst  0x7f91579ab7c0   0xdeadbeef              ( 0, 16, 11, 13)
+HASH 4294387191
+------------------------------------------------------------------------------------
+
+Program output from execution 49:
+---- BEGIN PROGRAM OUTPUT ----
+v1 = 0, v2=1
+v3 = 0, v4=1
+---- END PROGRAM OUTPUT   ----
+
+Execution trace 49:
+------------------------------------------------------------------------------------
+#    t    Action type     MO       Location         Value               Rf  CV
+------------------------------------------------------------------------------------
+1    1    thread start    seq_cst  0x7f91579ab7c0   0xdeadbeef              ( 0,  1)
+2    1    init atomic     relaxed        0x60106c   0                       ( 0,  2)
+3    1    init atomic     relaxed        0x601070   0                       ( 0,  3)
+4    1    thread create   seq_cst  0x7f9157aabb68   0x7f9157aabaf0          ( 0,  4)
+5    1    thread create   seq_cst  0x7f9157aabb60   0x7f9157aabaf0          ( 0,  5)
+6    2    thread start    seq_cst  0x7f9157aabbc8   0xdeadbeef              ( 0,  4,  6)
+7    3    thread start    seq_cst  0x7f9157babfd0   0xdeadbeef              ( 0,  5,  0,  7)
+8    2    atomic rmw      relaxed        0x60106c   0                   2   ( 0,  4,  8)
+9    3    atomic rmw      relaxed        0x601070   0                   3   ( 0,  5,  0,  9)
+10   2    atomic rmw      relaxed        0x601070   0x1                 9   ( 0,  4, 10)
+11   2    thread finish   seq_cst  0x7f9157aabbc8   0xdeadbeef              ( 0,  4, 11)
+12   3    atomic rmw      relaxed        0x60106c   0x1                 8   ( 0,  5,  0, 12)
+13   3    thread finish   seq_cst  0x7f9157babfd0   0xdeadbeef              ( 0,  5,  0, 13)
+14   1    thread join     seq_cst  0x7f9157aabbc8   0x2                     ( 0, 14, 11)
+15   1    thread join     seq_cst  0x7f9157babfd0   0x3                     ( 0, 15, 11, 13)
+16   1    thread finish   seq_cst  0x7f91579ab7c0   0xdeadbeef              ( 0, 16, 11, 13)
+HASH 4294387191
+------------------------------------------------------------------------------------
+
+Program output from execution 51:
+---- BEGIN PROGRAM OUTPUT ----
+v3 = 0, v4=1
+v1 = 0, v2=1
+---- END PROGRAM OUTPUT   ----
+
+Execution trace 51:
+------------------------------------------------------------------------------------
+#    t    Action type     MO       Location         Value               Rf  CV
+------------------------------------------------------------------------------------
+1    1    thread start    seq_cst  0x7f91579ab7c0   0xdeadbeef              ( 0,  1)
+2    1    init atomic     relaxed        0x60106c   0                       ( 0,  2)
+3    1    init atomic     relaxed        0x601070   0                       ( 0,  3)
+4    1    thread create   seq_cst  0x7f9157aabb68   0x7f9157aabaf0          ( 0,  4)
+5    1    thread create   seq_cst  0x7f9157aabb60   0x7f9157aabaf0          ( 0,  5)
+6    2    thread start    seq_cst  0x7f9157aabbc8   0xdeadbeef              ( 0,  4,  6)
+7    3    thread start    seq_cst  0x7f9157babfd0   0xdeadbeef              ( 0,  5,  0,  7)
+8    2    atomic rmw      relaxed        0x60106c   0                   2   ( 0,  4,  8)
+9    3    atomic rmw      relaxed        0x601070   0                   3   ( 0,  5,  0,  9)
+10   3    atomic rmw      relaxed        0x60106c   0x1                 8   ( 0,  5,  0, 10)
+11   3    thread finish   seq_cst  0x7f9157babfd0   0xdeadbeef              ( 0,  5,  0, 11)
+12   2    atomic rmw      relaxed        0x601070   0x1                 9   ( 0,  4, 12)
+13   2    thread finish   seq_cst  0x7f9157aabbc8   0xdeadbeef              ( 0,  4, 13)
+14   1    thread join     seq_cst  0x7f9157aabbc8   0x2                     ( 0, 14, 13)
+15   1    thread join     seq_cst  0x7f9157babfd0   0x3                     ( 0, 15, 13, 11)
+16   1    thread finish   seq_cst  0x7f91579ab7c0   0xdeadbeef              ( 0, 16, 13, 11)
+HASH 4275545527
+------------------------------------------------------------------------------------
+
+Program output from execution 57:
+---- BEGIN PROGRAM OUTPUT ----
+v1 = 0, v2=0
+v3 = 1, v4=1
+---- END PROGRAM OUTPUT   ----
+
+Execution trace 57:
+------------------------------------------------------------------------------------
+#    t    Action type     MO       Location         Value               Rf  CV
+------------------------------------------------------------------------------------
+1    1    thread start    seq_cst  0x7f91579ab7c0   0xdeadbeef              ( 0,  1)
+2    1    init atomic     relaxed        0x60106c   0                       ( 0,  2)
+3    1    init atomic     relaxed        0x601070   0                       ( 0,  3)
+4    1    thread create   seq_cst  0x7f9157aabb68   0x7f9157aabaf0          ( 0,  4)
+5    1    thread create   seq_cst  0x7f9157aabb60   0x7f9157aabaf0          ( 0,  5)
+6    2    thread start    seq_cst  0x7f9157aabbc8   0xdeadbeef              ( 0,  4,  6)
+7    3    thread start    seq_cst  0x7f9157babfd0   0xdeadbeef              ( 0,  5,  0,  7)
+8    2    atomic rmw      relaxed        0x60106c   0                   2   ( 0,  4,  8)
+9    2    atomic rmw      relaxed        0x601070   0                   3   ( 0,  4,  9)
+10   2    thread finish   seq_cst  0x7f9157aabbc8   0xdeadbeef              ( 0,  4, 10)
+11   1    thread join     seq_cst  0x7f9157aabbc8   0x2                     ( 0, 11, 10)
+12   3    atomic rmw      relaxed        0x601070   0x1                 9   ( 0,  5,  0, 12)
+13   3    atomic rmw      relaxed        0x60106c   0x1                 8   ( 0,  5,  0, 13)
+14   3    thread finish   seq_cst  0x7f9157babfd0   0xdeadbeef              ( 0,  5,  0, 14)
+15   1    thread join     seq_cst  0x7f9157babfd0   0x3                     ( 0, 15, 10, 14)
+16   1    thread finish   seq_cst  0x7f91579ab7c0   0xdeadbeef              ( 0, 16, 10, 14)
+HASH 4127308943
+------------------------------------------------------------------------------------
+
+Program output from execution 58:
+---- BEGIN PROGRAM OUTPUT ----
+v1 = 0, v2=0
+v3 = 1, v4=1
+---- END PROGRAM OUTPUT   ----
+
+Execution trace 58:
+------------------------------------------------------------------------------------
+#    t    Action type     MO       Location         Value               Rf  CV
+------------------------------------------------------------------------------------
+1    1    thread start    seq_cst  0x7f91579ab7c0   0xdeadbeef              ( 0,  1)
+2    1    init atomic     relaxed        0x60106c   0                       ( 0,  2)
+3    1    init atomic     relaxed        0x601070   0                       ( 0,  3)
+4    1    thread create   seq_cst  0x7f9157aabb68   0x7f9157aabaf0          ( 0,  4)
+5    1    thread create   seq_cst  0x7f9157aabb60   0x7f9157aabaf0          ( 0,  5)
+6    2    thread start    seq_cst  0x7f9157aabbc8   0xdeadbeef              ( 0,  4,  6)
+7    3    thread start    seq_cst  0x7f9157babfd0   0xdeadbeef              ( 0,  5,  0,  7)
+8    2    atomic rmw      relaxed        0x60106c   0                   2   ( 0,  4,  8)
+9    2    atomic rmw      relaxed        0x601070   0                   3   ( 0,  4,  9)
+10   2    thread finish   seq_cst  0x7f9157aabbc8   0xdeadbeef              ( 0,  4, 10)
+11   1    thread join     seq_cst  0x7f9157aabbc8   0x2                     ( 0, 11, 10)
+12   3    atomic rmw      relaxed        0x601070   0x1                 9   ( 0,  5,  0, 12)
+13   3    atomic rmw      relaxed        0x60106c   0x1                 8   ( 0,  5,  0, 13)
+14   3    thread finish   seq_cst  0x7f9157babfd0   0xdeadbeef              ( 0,  5,  0, 14)
+15   1    thread join     seq_cst  0x7f9157babfd0   0x3                     ( 0, 15, 10, 14)
+16   1    thread finish   seq_cst  0x7f91579ab7c0   0xdeadbeef              ( 0, 16, 10, 14)
+HASH 4127308943
+------------------------------------------------------------------------------------
+
+Program output from execution 67:
+---- BEGIN PROGRAM OUTPUT ----
+v3 = 0, v4=1
+v1 = 0, v2=1
+---- END PROGRAM OUTPUT   ----
+
+Execution trace 67:
+------------------------------------------------------------------------------------
+#    t    Action type     MO       Location         Value               Rf  CV
+------------------------------------------------------------------------------------
+1    1    thread start    seq_cst  0x7f91579ab7c0   0xdeadbeef              ( 0,  1)
+2    1    init atomic     relaxed        0x60106c   0                       ( 0,  2)
+3    1    init atomic     relaxed        0x601070   0                       ( 0,  3)
+4    1    thread create   seq_cst  0x7f9157aabb68   0x7f9157aabaf0          ( 0,  4)
+5    1    thread create   seq_cst  0x7f9157aabb60   0x7f9157aabaf0          ( 0,  5)
+6    2    thread start    seq_cst  0x7f9157aabbc8   0xdeadbeef              ( 0,  4,  6)
+7    3    thread start    seq_cst  0x7f9157babfd0   0xdeadbeef              ( 0,  5,  0,  7)
+8    2    atomic rmw      relaxed        0x60106c   0                   2   ( 0,  4,  8)
+9    3    atomic rmw      relaxed        0x601070   0                   3   ( 0,  5,  0,  9)
+10   3    atomic rmw      relaxed        0x60106c   0x1                 8   ( 0,  5,  0, 10)
+11   3    thread finish   seq_cst  0x7f9157babfd0   0xdeadbeef              ( 0,  5,  0, 11)
+12   2    atomic rmw      relaxed        0x601070   0x1                 9   ( 0,  4, 12)
+13   2    thread finish   seq_cst  0x7f9157aabbc8   0xdeadbeef              ( 0,  4, 13)
+14   1    thread join     seq_cst  0x7f9157aabbc8   0x2                     ( 0, 14, 13)
+15   1    thread join     seq_cst  0x7f9157babfd0   0x3                     ( 0, 15, 13, 11)
+16   1    thread finish   seq_cst  0x7f91579ab7c0   0xdeadbeef              ( 0, 16, 13, 11)
+HASH 4275545527
+------------------------------------------------------------------------------------
+
+Program output from execution 70:
+---- BEGIN PROGRAM OUTPUT ----
+v1 = 0, v2=0
+v3 = 1, v4=1
+---- END PROGRAM OUTPUT   ----
+
+Execution trace 70:
+------------------------------------------------------------------------------------
+#    t    Action type     MO       Location         Value               Rf  CV
+------------------------------------------------------------------------------------
+1    1    thread start    seq_cst  0x7f91579ab7c0   0xdeadbeef              ( 0,  1)
+2    1    init atomic     relaxed        0x60106c   0                       ( 0,  2)
+3    1    init atomic     relaxed        0x601070   0                       ( 0,  3)
+4    1    thread create   seq_cst  0x7f9157aabb68   0x7f9157aabaf0          ( 0,  4)
+5    1    thread create   seq_cst  0x7f9157aabb60   0x7f9157aabaf0          ( 0,  5)
+6    2    thread start    seq_cst  0x7f9157aabbc8   0xdeadbeef              ( 0,  4,  6)
+7    3    thread start    seq_cst  0x7f9157babfd0   0xdeadbeef              ( 0,  5,  0,  7)
+8    2    atomic rmw      relaxed        0x60106c   0                   2   ( 0,  4,  8)
+9    2    atomic rmw      relaxed        0x601070   0                   3   ( 0,  4,  9)
+10   2    thread finish   seq_cst  0x7f9157aabbc8   0xdeadbeef              ( 0,  4, 10)
+11   3    atomic rmw      relaxed        0x601070   0x1                 9   ( 0,  5,  0, 11)
+12   1    thread join     seq_cst  0x7f9157aabbc8   0x2                     ( 0, 12, 10)
+13   3    atomic rmw      relaxed        0x60106c   0x1                 8   ( 0,  5,  0, 13)
+14   3    thread finish   seq_cst  0x7f9157babfd0   0xdeadbeef              ( 0,  5,  0, 14)
+15   1    thread join     seq_cst  0x7f9157babfd0   0x3                     ( 0, 15, 10, 14)
+16   1    thread finish   seq_cst  0x7f91579ab7c0   0xdeadbeef              ( 0, 16, 10, 14)
+HASH 4132878847
+------------------------------------------------------------------------------------
+
+Program output from execution 73:
+---- BEGIN PROGRAM OUTPUT ----
+v3 = 0, v4=1
+v1 = 0, v2=1
+---- END PROGRAM OUTPUT   ----
+
+Execution trace 73:
+------------------------------------------------------------------------------------
+#    t    Action type     MO       Location         Value               Rf  CV
+------------------------------------------------------------------------------------
+1    1    thread start    seq_cst  0x7f91579ab7c0   0xdeadbeef              ( 0,  1)
+2    1    init atomic     relaxed        0x60106c   0                       ( 0,  2)
+3    1    init atomic     relaxed        0x601070   0                       ( 0,  3)
+4    1    thread create   seq_cst  0x7f9157aabb68   0x7f9157aabaf0          ( 0,  4)
+5    1    thread create   seq_cst  0x7f9157aabb60   0x7f9157aabaf0          ( 0,  5)
+6    2    thread start    seq_cst  0x7f9157aabbc8   0xdeadbeef              ( 0,  4,  6)
+7    3    thread start    seq_cst  0x7f9157babfd0   0xdeadbeef              ( 0,  5,  0,  7)
+8    2    atomic rmw      relaxed        0x60106c   0                   2   ( 0,  4,  8)
+9    3    atomic rmw      relaxed        0x601070   0                   3   ( 0,  5,  0,  9)
+10   3    atomic rmw      relaxed        0x60106c   0x1                 8   ( 0,  5,  0, 10)
+11   3    thread finish   seq_cst  0x7f9157babfd0   0xdeadbeef              ( 0,  5,  0, 11)
+12   2    atomic rmw      relaxed        0x601070   0x1                 9   ( 0,  4, 12)
+13   2    thread finish   seq_cst  0x7f9157aabbc8   0xdeadbeef              ( 0,  4, 13)
+14   1    thread join     seq_cst  0x7f9157aabbc8   0x2                     ( 0, 14, 13)
+15   1    thread join     seq_cst  0x7f9157babfd0   0x3                     ( 0, 15, 13, 11)
+16   1    thread finish   seq_cst  0x7f91579ab7c0   0xdeadbeef              ( 0, 16, 13, 11)
+HASH 4275545527
+------------------------------------------------------------------------------------
+
+Program output from execution 74:
+---- BEGIN PROGRAM OUTPUT ----
+v1 = 0, v2=0
+v3 = 1, v4=1
+---- END PROGRAM OUTPUT   ----
+
+Execution trace 74:
+------------------------------------------------------------------------------------
+#    t    Action type     MO       Location         Value               Rf  CV
+------------------------------------------------------------------------------------
+1    1    thread start    seq_cst  0x7f91579ab7c0   0xdeadbeef              ( 0,  1)
+2    1    init atomic     relaxed        0x60106c   0                       ( 0,  2)
+3    1    init atomic     relaxed        0x601070   0                       ( 0,  3)
+4    1    thread create   seq_cst  0x7f9157aabb68   0x7f9157aabaf0          ( 0,  4)
+5    1    thread create   seq_cst  0x7f9157aabb60   0x7f9157aabaf0          ( 0,  5)
+6    2    thread start    seq_cst  0x7f9157aabbc8   0xdeadbeef              ( 0,  4,  6)
+7    3    thread start    seq_cst  0x7f9157babfd0   0xdeadbeef              ( 0,  5,  0,  7)
+8    2    atomic rmw      relaxed        0x60106c   0                   2   ( 0,  4,  8)
+9    2    atomic rmw      relaxed        0x601070   0                   3   ( 0,  4,  9)
+10   2    thread finish   seq_cst  0x7f9157aabbc8   0xdeadbeef              ( 0,  4, 10)
+11   1    thread join     seq_cst  0x7f9157aabbc8   0x2                     ( 0, 11, 10)
+12   3    atomic rmw      relaxed        0x601070   0x1                 9   ( 0,  5,  0, 12)
+13   3    atomic rmw      relaxed        0x60106c   0x1                 8   ( 0,  5,  0, 13)
+14   3    thread finish   seq_cst  0x7f9157babfd0   0xdeadbeef              ( 0,  5,  0, 14)
+15   1    thread join     seq_cst  0x7f9157babfd0   0x3                     ( 0, 15, 10, 14)
+16   1    thread finish   seq_cst  0x7f91579ab7c0   0xdeadbeef              ( 0, 16, 10, 14)
+HASH 4127308943
+------------------------------------------------------------------------------------
+
+Program output from execution 94:
+---- BEGIN PROGRAM OUTPUT ----
+v1 = 0, v2=1
+v3 = 0, v4=1
+---- END PROGRAM OUTPUT   ----
+
+Execution trace 94:
+------------------------------------------------------------------------------------
+#    t    Action type     MO       Location         Value               Rf  CV
+------------------------------------------------------------------------------------
+1    1    thread start    seq_cst  0x7f91579ab7c0   0xdeadbeef              ( 0,  1)
+2    1    init atomic     relaxed        0x60106c   0                       ( 0,  2)
+3    1    init atomic     relaxed        0x601070   0                       ( 0,  3)
+4    1    thread create   seq_cst  0x7f9157aabb68   0x7f9157aabaf0          ( 0,  4)
+5    1    thread create   seq_cst  0x7f9157aabb60   0x7f9157aabaf0          ( 0,  5)
+6    2    thread start    seq_cst  0x7f9157aabbc8   0xdeadbeef              ( 0,  4,  6)
+7    3    thread start    seq_cst  0x7f9157babfd0   0xdeadbeef              ( 0,  5,  0,  7)
+8    3    atomic rmw      relaxed        0x601070   0                   3   ( 0,  5,  0,  8)
+9    2    atomic rmw      relaxed        0x60106c   0                   2   ( 0,  4,  9)
+10   2    atomic rmw      relaxed        0x601070   0x1                 8   ( 0,  4, 10)
+11   2    thread finish   seq_cst  0x7f9157aabbc8   0xdeadbeef              ( 0,  4, 11)
+12   3    atomic rmw      relaxed        0x60106c   0x1                 9   ( 0,  5,  0, 12)
+13   3    thread finish   seq_cst  0x7f9157babfd0   0xdeadbeef              ( 0,  5,  0, 13)
+14   1    thread join     seq_cst  0x7f9157aabbc8   0x2                     ( 0, 14, 11)
+15   1    thread join     seq_cst  0x7f9157babfd0   0x3                     ( 0, 15, 11, 13)
+16   1    thread finish   seq_cst  0x7f91579ab7c0   0xdeadbeef              ( 0, 16, 11, 13)
+HASH 3086165503
+------------------------------------------------------------------------------------
+
+Program output from execution 95:
+---- BEGIN PROGRAM OUTPUT ----
+v3 = 0, v4=0
+v1 = 1, v2=1
+---- END PROGRAM OUTPUT   ----
+
+Execution trace 95:
+------------------------------------------------------------------------------------
+#    t    Action type     MO       Location         Value               Rf  CV
+------------------------------------------------------------------------------------
+1    1    thread start    seq_cst  0x7f91579ab7c0   0xdeadbeef              ( 0,  1)
+2    1    init atomic     relaxed        0x60106c   0                       ( 0,  2)
+3    1    init atomic     relaxed        0x601070   0                       ( 0,  3)
+4    1    thread create   seq_cst  0x7f9157aabb68   0x7f9157aabaf0          ( 0,  4)
+5    1    thread create   seq_cst  0x7f9157aabb60   0x7f9157aabaf0          ( 0,  5)
+6    2    thread start    seq_cst  0x7f9157aabbc8   0xdeadbeef              ( 0,  4,  6)
+7    3    thread start    seq_cst  0x7f9157babfd0   0xdeadbeef              ( 0,  5,  0,  7)
+8    3    atomic rmw      relaxed        0x601070   0                   3   ( 0,  5,  0,  8)
+9    3    atomic rmw      relaxed        0x60106c   0                   2   ( 0,  5,  0,  9)
+10   3    thread finish   seq_cst  0x7f9157babfd0   0xdeadbeef              ( 0,  5,  0, 10)
+11   2    atomic rmw      relaxed        0x60106c   0x1                 9   ( 0,  4, 11)
+12   2    atomic rmw      relaxed        0x601070   0x1                 8   ( 0,  4, 12)
+13   2    thread finish   seq_cst  0x7f9157aabbc8   0xdeadbeef              ( 0,  4, 13)
+14   1    thread join     seq_cst  0x7f9157aabbc8   0x2                     ( 0, 14, 13)
+15   1    thread join     seq_cst  0x7f9157babfd0   0x3                     ( 0, 15, 13, 10)
+16   1    thread finish   seq_cst  0x7f91579ab7c0   0xdeadbeef              ( 0, 16, 13, 10)
+HASH 3212361479
+------------------------------------------------------------------------------------
+
+Program output from execution 96:
+---- BEGIN PROGRAM OUTPUT ----
+v3 = 0, v4=1
+v1 = 0, v2=1
+---- END PROGRAM OUTPUT   ----
+
+Execution trace 96:
+------------------------------------------------------------------------------------
+#    t    Action type     MO       Location         Value               Rf  CV
+------------------------------------------------------------------------------------
+1    1    thread start    seq_cst  0x7f91579ab7c0   0xdeadbeef              ( 0,  1)
+2    1    init atomic     relaxed        0x60106c   0                       ( 0,  2)
+3    1    init atomic     relaxed        0x601070   0                       ( 0,  3)
+4    1    thread create   seq_cst  0x7f9157aabb68   0x7f9157aabaf0          ( 0,  4)
+5    1    thread create   seq_cst  0x7f9157aabb60   0x7f9157aabaf0          ( 0,  5)
+6    2    thread start    seq_cst  0x7f9157aabbc8   0xdeadbeef              ( 0,  4,  6)
+7    3    thread start    seq_cst  0x7f9157babfd0   0xdeadbeef              ( 0,  5,  0,  7)
+8    2    atomic rmw      relaxed        0x60106c   0                   2   ( 0,  4,  8)
+9    3    atomic rmw      relaxed        0x601070   0                   3   ( 0,  5,  0,  9)
+10   3    atomic rmw      relaxed        0x60106c   0x1                 8   ( 0,  5,  0, 10)
+11   3    thread finish   seq_cst  0x7f9157babfd0   0xdeadbeef              ( 0,  5,  0, 11)
+12   2    atomic rmw      relaxed        0x601070   0x1                 9   ( 0,  4, 12)
+13   2    thread finish   seq_cst  0x7f9157aabbc8   0xdeadbeef              ( 0,  4, 13)
+14   1    thread join     seq_cst  0x7f9157aabbc8   0x2                     ( 0, 14, 13)
+15   1    thread join     seq_cst  0x7f9157babfd0   0x3                     ( 0, 15, 13, 11)
+16   1    thread finish   seq_cst  0x7f91579ab7c0   0xdeadbeef              ( 0, 16, 13, 11)
+HASH 4275545527
+------------------------------------------------------------------------------------
+
+Program output from execution 98:
+---- BEGIN PROGRAM OUTPUT ----
+v3 = 0, v4=0
+v1 = 1, v2=1
+---- END PROGRAM OUTPUT   ----
+
+Execution trace 98:
+------------------------------------------------------------------------------------
+#    t    Action type     MO       Location         Value               Rf  CV
+------------------------------------------------------------------------------------
+1    1    thread start    seq_cst  0x7f91579ab7c0   0xdeadbeef              ( 0,  1)
+2    1    init atomic     relaxed        0x60106c   0                       ( 0,  2)
+3    1    init atomic     relaxed        0x601070   0                       ( 0,  3)
+4    1    thread create   seq_cst  0x7f9157aabb68   0x7f9157aabaf0          ( 0,  4)
+5    1    thread create   seq_cst  0x7f9157aabb60   0x7f9157aabaf0          ( 0,  5)
+6    2    thread start    seq_cst  0x7f9157aabbc8   0xdeadbeef              ( 0,  4,  6)
+7    3    thread start    seq_cst  0x7f9157babfd0   0xdeadbeef              ( 0,  5,  0,  7)
+8    3    atomic rmw      relaxed        0x601070   0                   3   ( 0,  5,  0,  8)
+9    3    atomic rmw      relaxed        0x60106c   0                   2   ( 0,  5,  0,  9)
+10   3    thread finish   seq_cst  0x7f9157babfd0   0xdeadbeef              ( 0,  5,  0, 10)
+11   2    atomic rmw      relaxed        0x60106c   0x1                 9   ( 0,  4, 11)
+12   2    atomic rmw      relaxed        0x601070   0x1                 8   ( 0,  4, 12)
+13   2    thread finish   seq_cst  0x7f9157aabbc8   0xdeadbeef              ( 0,  4, 13)
+14   1    thread join     seq_cst  0x7f9157aabbc8   0x2                     ( 0, 14, 13)
+15   1    thread join     seq_cst  0x7f9157babfd0   0x3                     ( 0, 15, 13, 10)
+16   1    thread finish   seq_cst  0x7f91579ab7c0   0xdeadbeef              ( 0, 16, 13, 10)
+HASH 3212361479
+------------------------------------------------------------------------------------
+
+Program output from execution 100:
+---- BEGIN PROGRAM OUTPUT ----
+v1 = 0, v2=1
+v3 = 0, v4=1
+---- END PROGRAM OUTPUT   ----
+
+Execution trace 100:
+------------------------------------------------------------------------------------
+#    t    Action type     MO       Location         Value               Rf  CV
+------------------------------------------------------------------------------------
+1    1    thread start    seq_cst  0x7f91579ab7c0   0xdeadbeef              ( 0,  1)
+2    1    init atomic     relaxed        0x60106c   0                       ( 0,  2)
+3    1    init atomic     relaxed        0x601070   0                       ( 0,  3)
+4    1    thread create   seq_cst  0x7f9157aabb68   0x7f9157aabaf0          ( 0,  4)
+5    1    thread create   seq_cst  0x7f9157aabb60   0x7f9157aabaf0          ( 0,  5)
+6    2    thread start    seq_cst  0x7f9157aabbc8   0xdeadbeef              ( 0,  4,  6)
+7    3    thread start    seq_cst  0x7f9157babfd0   0xdeadbeef              ( 0,  5,  0,  7)
+8    3    atomic rmw      relaxed        0x601070   0                   3   ( 0,  5,  0,  8)
+9    2    atomic rmw      relaxed        0x60106c   0                   2   ( 0,  4,  9)
+10   2    atomic rmw      relaxed        0x601070   0x1                 8   ( 0,  4, 10)
+11   2    thread finish   seq_cst  0x7f9157aabbc8   0xdeadbeef              ( 0,  4, 11)
+12   1    thread join     seq_cst  0x7f9157aabbc8   0x2                     ( 0, 12, 11)
+13   3    atomic rmw      relaxed        0x60106c   0x1                 9   ( 0,  5,  0, 13)
+14   3    thread finish   seq_cst  0x7f9157babfd0   0xdeadbeef              ( 0,  5,  0, 14)
+15   1    thread join     seq_cst  0x7f9157babfd0   0x3                     ( 0, 15, 11, 14)
+16   1    thread finish   seq_cst  0x7f91579ab7c0   0xdeadbeef              ( 0, 16, 11, 14)
+HASH 3086594311
+------------------------------------------------------------------------------------
+
+******* Model-checking complete: *******
+Number of complete, bug-free executions: 25
+Number of redundant executions: 0
+Number of buggy executions: 0
+Number of infeasible executions: 75
+Total executions: 100
+Total nodes created: 1135
diff --git a/test/memo/output b/test/memo/output
new file mode 100644
index 00000000..3e8204e4
--- /dev/null
+++ b/test/memo/output
@@ -0,0 +1,687 @@
+Program output from execution 1:
+---- BEGIN PROGRAM OUTPUT ----
+CDSChecker
+Copyright (c) 2013 Regents of the University of California. All rights reserved.
+Distributed under the GPLv2
+Written by Brian Norris and Brian Demsky
+
+v3 = 0, v4=0
+v1 = 1, v2=1
+---- END PROGRAM OUTPUT   ----
+
+Execution trace 1:
+------------------------------------------------------------------------------------
+#    t    Action type     MO       Location         Value               Rf  CV
+------------------------------------------------------------------------------------
+1    1    thread start    seq_cst  0x7efc241ab7c0   0xdeadbeef              ( 0,  1)
+2    1    thread create   seq_cst  0x7efc242abb68   0x7efc242abb10          ( 0,  2)
+3    1    thread create   seq_cst  0x7efc242abb60   0x7efc242abb10          ( 0,  3)
+4    2    thread start    seq_cst  0x7efc242abbc8   0xdeadbeef              ( 0,  2,  4)
+5    3    thread start    seq_cst  0x7efc243abfd0   0xdeadbeef              ( 0,  3,  0,  5)
+6    3    atomic rmw      relaxed        0x601060   0                   0   ( 0,  3,  0,  6)
+7    3    atomic rmw      relaxed        0x60105c   0                   0   ( 0,  3,  0,  7)
+8    3    thread finish   seq_cst  0x7efc243abfd0   0xdeadbeef              ( 0,  3,  0,  8)
+9    2    atomic rmw      relaxed        0x60105c   0x1                 7   ( 0,  2,  9)
+10   2    atomic rmw      relaxed        0x601060   0x1                 6   ( 0,  2, 10)
+11   2    thread finish   seq_cst  0x7efc242abbc8   0xdeadbeef              ( 0,  2, 11)
+12   1    thread join     seq_cst  0x7efc242abbc8   0x2                     ( 0, 12, 11)
+13   1    thread join     seq_cst  0x7efc243abfd0   0x3                     ( 0, 13, 11,  8)
+14   1    thread finish   seq_cst  0x7efc241ab7c0   0xdeadbeef              ( 0, 14, 11,  8)
+HASH 3127311590
+------------------------------------------------------------------------------------
+
+Program output from execution 5:
+---- BEGIN PROGRAM OUTPUT ----
+v3 = 0, v4=1
+v1 = 0, v2=1
+---- END PROGRAM OUTPUT   ----
+
+Execution trace 5:
+------------------------------------------------------------------------------------
+#    t    Action type     MO       Location         Value               Rf  CV
+------------------------------------------------------------------------------------
+1    1    thread start    seq_cst  0x7efc241ab7c0   0xdeadbeef              ( 0,  1)
+2    1    thread create   seq_cst  0x7efc242abb68   0x7efc242abb10          ( 0,  2)
+3    1    thread create   seq_cst  0x7efc242abb60   0x7efc242abb10          ( 0,  3)
+4    2    thread start    seq_cst  0x7efc242abbc8   0xdeadbeef              ( 0,  2,  4)
+5    3    thread start    seq_cst  0x7efc243abfd0   0xdeadbeef              ( 0,  3,  0,  5)
+6    2    atomic rmw      relaxed        0x60105c   0                   0   ( 0,  2,  6)
+7    3    atomic rmw      relaxed        0x601060   0                   0   ( 0,  3,  0,  7)
+8    3    atomic rmw      relaxed        0x60105c   0x1                 6   ( 0,  3,  0,  8)
+9    3    thread finish   seq_cst  0x7efc243abfd0   0xdeadbeef              ( 0,  3,  0,  9)
+10   2    atomic rmw      relaxed        0x601060   0x1                 7   ( 0,  2, 10)
+11   2    thread finish   seq_cst  0x7efc242abbc8   0xdeadbeef              ( 0,  2, 11)
+12   1    thread join     seq_cst  0x7efc242abbc8   0x2                     ( 0, 12, 11)
+13   1    thread join     seq_cst  0x7efc243abfd0   0x3                     ( 0, 13, 11,  9)
+14   1    thread finish   seq_cst  0x7efc241ab7c0   0xdeadbeef              ( 0, 14, 11,  9)
+HASH 4208097262
+------------------------------------------------------------------------------------
+
+Program output from execution 8:
+---- BEGIN PROGRAM OUTPUT ----
+v3 = 0, v4=1
+v1 = 0, v2=1
+---- END PROGRAM OUTPUT   ----
+
+Execution trace 8:
+------------------------------------------------------------------------------------
+#    t    Action type     MO       Location         Value               Rf  CV
+------------------------------------------------------------------------------------
+1    1    thread start    seq_cst  0x7efc241ab7c0   0xdeadbeef              ( 0,  1)
+2    1    thread create   seq_cst  0x7efc242abb68   0x7efc242abb10          ( 0,  2)
+3    1    thread create   seq_cst  0x7efc242abb60   0x7efc242abb10          ( 0,  3)
+4    2    thread start    seq_cst  0x7efc242abbc8   0xdeadbeef              ( 0,  2,  4)
+5    3    thread start    seq_cst  0x7efc243abfd0   0xdeadbeef              ( 0,  3,  0,  5)
+6    3    atomic rmw      relaxed        0x601060   0                   0   ( 0,  3,  0,  6)
+7    2    atomic rmw      relaxed        0x60105c   0                   0   ( 0,  2,  7)
+8    3    atomic rmw      relaxed        0x60105c   0x1                 7   ( 0,  3,  0,  8)
+9    3    thread finish   seq_cst  0x7efc243abfd0   0xdeadbeef              ( 0,  3,  0,  9)
+10   2    atomic rmw      relaxed        0x601060   0x1                 6   ( 0,  2, 10)
+11   2    thread finish   seq_cst  0x7efc242abbc8   0xdeadbeef              ( 0,  2, 11)
+12   1    thread join     seq_cst  0x7efc242abbc8   0x2                     ( 0, 12, 11)
+13   1    thread join     seq_cst  0x7efc243abfd0   0x3                     ( 0, 13, 11,  9)
+14   1    thread finish   seq_cst  0x7efc241ab7c0   0xdeadbeef              ( 0, 14, 11,  9)
+HASH 3019040174
+------------------------------------------------------------------------------------
+
+Program output from execution 9:
+---- BEGIN PROGRAM OUTPUT ----
+v3 = 0, v4=1
+v1 = 0, v2=1
+---- END PROGRAM OUTPUT   ----
+
+Execution trace 9:
+------------------------------------------------------------------------------------
+#    t    Action type     MO       Location         Value               Rf  CV
+------------------------------------------------------------------------------------
+1    1    thread start    seq_cst  0x7efc241ab7c0   0xdeadbeef              ( 0,  1)
+2    1    thread create   seq_cst  0x7efc242abb68   0x7efc242abb10          ( 0,  2)
+3    1    thread create   seq_cst  0x7efc242abb60   0x7efc242abb10          ( 0,  3)
+4    2    thread start    seq_cst  0x7efc242abbc8   0xdeadbeef              ( 0,  2,  4)
+5    3    thread start    seq_cst  0x7efc243abfd0   0xdeadbeef              ( 0,  3,  0,  5)
+6    3    atomic rmw      relaxed        0x601060   0                   0   ( 0,  3,  0,  6)
+7    2    atomic rmw      relaxed        0x60105c   0                   0   ( 0,  2,  7)
+8    3    atomic rmw      relaxed        0x60105c   0x1                 7   ( 0,  3,  0,  8)
+9    3    thread finish   seq_cst  0x7efc243abfd0   0xdeadbeef              ( 0,  3,  0,  9)
+10   2    atomic rmw      relaxed        0x601060   0x1                 6   ( 0,  2, 10)
+11   2    thread finish   seq_cst  0x7efc242abbc8   0xdeadbeef              ( 0,  2, 11)
+12   1    thread join     seq_cst  0x7efc242abbc8   0x2                     ( 0, 12, 11)
+13   1    thread join     seq_cst  0x7efc243abfd0   0x3                     ( 0, 13, 11,  9)
+14   1    thread finish   seq_cst  0x7efc241ab7c0   0xdeadbeef              ( 0, 14, 11,  9)
+HASH 3019040174
+------------------------------------------------------------------------------------
+
+Program output from execution 13:
+---- BEGIN PROGRAM OUTPUT ----
+v1 = 0, v2=1
+v3 = 0, v4=1
+---- END PROGRAM OUTPUT   ----
+
+Execution trace 13:
+------------------------------------------------------------------------------------
+#    t    Action type     MO       Location         Value               Rf  CV
+------------------------------------------------------------------------------------
+1    1    thread start    seq_cst  0x7efc241ab7c0   0xdeadbeef              ( 0,  1)
+2    1    thread create   seq_cst  0x7efc242abb68   0x7efc242abb10          ( 0,  2)
+3    1    thread create   seq_cst  0x7efc242abb60   0x7efc242abb10          ( 0,  3)
+4    2    thread start    seq_cst  0x7efc242abbc8   0xdeadbeef              ( 0,  2,  4)
+5    3    thread start    seq_cst  0x7efc243abfd0   0xdeadbeef              ( 0,  3,  0,  5)
+6    3    atomic rmw      relaxed        0x601060   0                   0   ( 0,  3,  0,  6)
+7    2    atomic rmw      relaxed        0x60105c   0                   0   ( 0,  2,  7)
+8    2    atomic rmw      relaxed        0x601060   0x1                 6   ( 0,  2,  8)
+9    2    thread finish   seq_cst  0x7efc242abbc8   0xdeadbeef              ( 0,  2,  9)
+10   3    atomic rmw      relaxed        0x60105c   0x1                 7   ( 0,  3,  0, 10)
+11   3    thread finish   seq_cst  0x7efc243abfd0   0xdeadbeef              ( 0,  3,  0, 11)
+12   1    thread join     seq_cst  0x7efc242abbc8   0x2                     ( 0, 12,  9)
+13   1    thread join     seq_cst  0x7efc243abfd0   0x3                     ( 0, 13,  9, 11)
+14   1    thread finish   seq_cst  0x7efc241ab7c0   0xdeadbeef              ( 0, 14,  9, 11)
+HASH 3000133102
+------------------------------------------------------------------------------------
+
+Program output from execution 14:
+---- BEGIN PROGRAM OUTPUT ----
+v3 = 0, v4=1
+v1 = 0, v2=1
+---- END PROGRAM OUTPUT   ----
+
+Execution trace 14:
+------------------------------------------------------------------------------------
+#    t    Action type     MO       Location         Value               Rf  CV
+------------------------------------------------------------------------------------
+1    1    thread start    seq_cst  0x7efc241ab7c0   0xdeadbeef              ( 0,  1)
+2    1    thread create   seq_cst  0x7efc242abb68   0x7efc242abb10          ( 0,  2)
+3    1    thread create   seq_cst  0x7efc242abb60   0x7efc242abb10          ( 0,  3)
+4    2    thread start    seq_cst  0x7efc242abbc8   0xdeadbeef              ( 0,  2,  4)
+5    3    thread start    seq_cst  0x7efc243abfd0   0xdeadbeef              ( 0,  3,  0,  5)
+6    3    atomic rmw      relaxed        0x601060   0                   0   ( 0,  3,  0,  6)
+7    2    atomic rmw      relaxed        0x60105c   0                   0   ( 0,  2,  7)
+8    3    atomic rmw      relaxed        0x60105c   0x1                 7   ( 0,  3,  0,  8)
+9    3    thread finish   seq_cst  0x7efc243abfd0   0xdeadbeef              ( 0,  3,  0,  9)
+10   2    atomic rmw      relaxed        0x601060   0x1                 6   ( 0,  2, 10)
+11   2    thread finish   seq_cst  0x7efc242abbc8   0xdeadbeef              ( 0,  2, 11)
+12   1    thread join     seq_cst  0x7efc242abbc8   0x2                     ( 0, 12, 11)
+13   1    thread join     seq_cst  0x7efc243abfd0   0x3                     ( 0, 13, 11,  9)
+14   1    thread finish   seq_cst  0x7efc241ab7c0   0xdeadbeef              ( 0, 14, 11,  9)
+HASH 3019040174
+------------------------------------------------------------------------------------
+
+Program output from execution 16:
+---- BEGIN PROGRAM OUTPUT ----
+v1 = 0, v2=0
+v3 = 1, v4=1
+---- END PROGRAM OUTPUT   ----
+
+Execution trace 16:
+------------------------------------------------------------------------------------
+#    t    Action type     MO       Location         Value               Rf  CV
+------------------------------------------------------------------------------------
+1    1    thread start    seq_cst  0x7efc241ab7c0   0xdeadbeef              ( 0,  1)
+2    1    thread create   seq_cst  0x7efc242abb68   0x7efc242abb10          ( 0,  2)
+3    1    thread create   seq_cst  0x7efc242abb60   0x7efc242abb10          ( 0,  3)
+4    2    thread start    seq_cst  0x7efc242abbc8   0xdeadbeef              ( 0,  2,  4)
+5    3    thread start    seq_cst  0x7efc243abfd0   0xdeadbeef              ( 0,  3,  0,  5)
+6    2    atomic rmw      relaxed        0x60105c   0                   0   ( 0,  2,  6)
+7    2    atomic rmw      relaxed        0x601060   0                   0   ( 0,  2,  7)
+8    2    thread finish   seq_cst  0x7efc242abbc8   0xdeadbeef              ( 0,  2,  8)
+9    1    thread join     seq_cst  0x7efc242abbc8   0x2                     ( 0,  9,  8)
+10   3    atomic rmw      relaxed        0x601060   0x1                 7   ( 0,  3,  0, 10)
+11   3    atomic rmw      relaxed        0x60105c   0x1                 6   ( 0,  3,  0, 11)
+12   3    thread finish   seq_cst  0x7efc243abfd0   0xdeadbeef              ( 0,  3,  0, 12)
+13   1    thread join     seq_cst  0x7efc243abfd0   0x3                     ( 0, 13,  8, 12)
+14   1    thread finish   seq_cst  0x7efc241ab7c0   0xdeadbeef              ( 0, 14,  8, 12)
+HASH 4064055974
+------------------------------------------------------------------------------------
+
+Program output from execution 17:
+---- BEGIN PROGRAM OUTPUT ----
+v1 = 0, v2=0
+v3 = 1, v4=1
+---- END PROGRAM OUTPUT   ----
+
+Execution trace 17:
+------------------------------------------------------------------------------------
+#    t    Action type     MO       Location         Value               Rf  CV
+------------------------------------------------------------------------------------
+1    1    thread start    seq_cst  0x7efc241ab7c0   0xdeadbeef              ( 0,  1)
+2    1    thread create   seq_cst  0x7efc242abb68   0x7efc242abb10          ( 0,  2)
+3    1    thread create   seq_cst  0x7efc242abb60   0x7efc242abb10          ( 0,  3)
+4    2    thread start    seq_cst  0x7efc242abbc8   0xdeadbeef              ( 0,  2,  4)
+5    3    thread start    seq_cst  0x7efc243abfd0   0xdeadbeef              ( 0,  3,  0,  5)
+6    2    atomic rmw      relaxed        0x60105c   0                   0   ( 0,  2,  6)
+7    2    atomic rmw      relaxed        0x601060   0                   0   ( 0,  2,  7)
+8    2    thread finish   seq_cst  0x7efc242abbc8   0xdeadbeef              ( 0,  2,  8)
+9    3    atomic rmw      relaxed        0x601060   0x1                 7   ( 0,  3,  0,  9)
+10   3    atomic rmw      relaxed        0x60105c   0x1                 6   ( 0,  3,  0, 10)
+11   3    thread finish   seq_cst  0x7efc243abfd0   0xdeadbeef              ( 0,  3,  0, 11)
+12   1    thread join     seq_cst  0x7efc242abbc8   0x2                     ( 0, 12,  8)
+13   1    thread join     seq_cst  0x7efc243abfd0   0x3                     ( 0, 13,  8, 11)
+14   1    thread finish   seq_cst  0x7efc241ab7c0   0xdeadbeef              ( 0, 14,  8, 11)
+HASH 4066832102
+------------------------------------------------------------------------------------
+
+Program output from execution 22:
+---- BEGIN PROGRAM OUTPUT ----
+v3 = 0, v4=1
+v1 = 0, v2=1
+---- END PROGRAM OUTPUT   ----
+
+Execution trace 22:
+------------------------------------------------------------------------------------
+#    t    Action type     MO       Location         Value               Rf  CV
+------------------------------------------------------------------------------------
+1    1    thread start    seq_cst  0x7efc241ab7c0   0xdeadbeef              ( 0,  1)
+2    1    thread create   seq_cst  0x7efc242abb68   0x7efc242abb10          ( 0,  2)
+3    1    thread create   seq_cst  0x7efc242abb60   0x7efc242abb10          ( 0,  3)
+4    2    thread start    seq_cst  0x7efc242abbc8   0xdeadbeef              ( 0,  2,  4)
+5    3    thread start    seq_cst  0x7efc243abfd0   0xdeadbeef              ( 0,  3,  0,  5)
+6    3    atomic rmw      relaxed        0x601060   0                   0   ( 0,  3,  0,  6)
+7    2    atomic rmw      relaxed        0x60105c   0                   0   ( 0,  2,  7)
+8    3    atomic rmw      relaxed        0x60105c   0x1                 7   ( 0,  3,  0,  8)
+9    3    thread finish   seq_cst  0x7efc243abfd0   0xdeadbeef              ( 0,  3,  0,  9)
+10   2    atomic rmw      relaxed        0x601060   0x1                 6   ( 0,  2, 10)
+11   2    thread finish   seq_cst  0x7efc242abbc8   0xdeadbeef              ( 0,  2, 11)
+12   1    thread join     seq_cst  0x7efc242abbc8   0x2                     ( 0, 12, 11)
+13   1    thread join     seq_cst  0x7efc243abfd0   0x3                     ( 0, 13, 11,  9)
+14   1    thread finish   seq_cst  0x7efc241ab7c0   0xdeadbeef              ( 0, 14, 11,  9)
+HASH 3019040174
+------------------------------------------------------------------------------------
+
+Program output from execution 24:
+---- BEGIN PROGRAM OUTPUT ----
+v3 = 0, v4=0
+v1 = 1, v2=1
+---- END PROGRAM OUTPUT   ----
+
+Execution trace 24:
+------------------------------------------------------------------------------------
+#    t    Action type     MO       Location         Value               Rf  CV
+------------------------------------------------------------------------------------
+1    1    thread start    seq_cst  0x7efc241ab7c0   0xdeadbeef              ( 0,  1)
+2    1    thread create   seq_cst  0x7efc242abb68   0x7efc242abb10          ( 0,  2)
+3    1    thread create   seq_cst  0x7efc242abb60   0x7efc242abb10          ( 0,  3)
+4    2    thread start    seq_cst  0x7efc242abbc8   0xdeadbeef              ( 0,  2,  4)
+5    3    thread start    seq_cst  0x7efc243abfd0   0xdeadbeef              ( 0,  3,  0,  5)
+6    3    atomic rmw      relaxed        0x601060   0                   0   ( 0,  3,  0,  6)
+7    3    atomic rmw      relaxed        0x60105c   0                   0   ( 0,  3,  0,  7)
+8    3    thread finish   seq_cst  0x7efc243abfd0   0xdeadbeef              ( 0,  3,  0,  8)
+9    2    atomic rmw      relaxed        0x60105c   0x1                 7   ( 0,  2,  9)
+10   2    atomic rmw      relaxed        0x601060   0x1                 6   ( 0,  2, 10)
+11   2    thread finish   seq_cst  0x7efc242abbc8   0xdeadbeef              ( 0,  2, 11)
+12   1    thread join     seq_cst  0x7efc242abbc8   0x2                     ( 0, 12, 11)
+13   1    thread join     seq_cst  0x7efc243abfd0   0x3                     ( 0, 13, 11,  8)
+14   1    thread finish   seq_cst  0x7efc241ab7c0   0xdeadbeef              ( 0, 14, 11,  8)
+HASH 3127311590
+------------------------------------------------------------------------------------
+
+Program output from execution 37:
+---- BEGIN PROGRAM OUTPUT ----
+v3 = 0, v4=1
+v1 = 0, v2=1
+---- END PROGRAM OUTPUT   ----
+
+Execution trace 37:
+------------------------------------------------------------------------------------
+#    t    Action type     MO       Location         Value               Rf  CV
+------------------------------------------------------------------------------------
+1    1    thread start    seq_cst  0x7efc241ab7c0   0xdeadbeef              ( 0,  1)
+2    1    thread create   seq_cst  0x7efc242abb68   0x7efc242abb10          ( 0,  2)
+3    1    thread create   seq_cst  0x7efc242abb60   0x7efc242abb10          ( 0,  3)
+4    2    thread start    seq_cst  0x7efc242abbc8   0xdeadbeef              ( 0,  2,  4)
+5    3    thread start    seq_cst  0x7efc243abfd0   0xdeadbeef              ( 0,  3,  0,  5)
+6    3    atomic rmw      relaxed        0x601060   0                   0   ( 0,  3,  0,  6)
+7    2    atomic rmw      relaxed        0x60105c   0                   0   ( 0,  2,  7)
+8    3    atomic rmw      relaxed        0x60105c   0x1                 7   ( 0,  3,  0,  8)
+9    3    thread finish   seq_cst  0x7efc243abfd0   0xdeadbeef              ( 0,  3,  0,  9)
+10   2    atomic rmw      relaxed        0x601060   0x1                 6   ( 0,  2, 10)
+11   2    thread finish   seq_cst  0x7efc242abbc8   0xdeadbeef              ( 0,  2, 11)
+12   1    thread join     seq_cst  0x7efc242abbc8   0x2                     ( 0, 12, 11)
+13   1    thread join     seq_cst  0x7efc243abfd0   0x3                     ( 0, 13, 11,  9)
+14   1    thread finish   seq_cst  0x7efc241ab7c0   0xdeadbeef              ( 0, 14, 11,  9)
+HASH 3019040174
+------------------------------------------------------------------------------------
+
+Program output from execution 48:
+---- BEGIN PROGRAM OUTPUT ----
+v1 = 0, v2=1
+v3 = 0, v4=1
+---- END PROGRAM OUTPUT   ----
+
+Execution trace 48:
+------------------------------------------------------------------------------------
+#    t    Action type     MO       Location         Value               Rf  CV
+------------------------------------------------------------------------------------
+1    1    thread start    seq_cst  0x7efc241ab7c0   0xdeadbeef              ( 0,  1)
+2    1    thread create   seq_cst  0x7efc242abb68   0x7efc242abb10          ( 0,  2)
+3    1    thread create   seq_cst  0x7efc242abb60   0x7efc242abb10          ( 0,  3)
+4    2    thread start    seq_cst  0x7efc242abbc8   0xdeadbeef              ( 0,  2,  4)
+5    3    thread start    seq_cst  0x7efc243abfd0   0xdeadbeef              ( 0,  3,  0,  5)
+6    2    atomic rmw      relaxed        0x60105c   0                   0   ( 0,  2,  6)
+7    3    atomic rmw      relaxed        0x601060   0                   0   ( 0,  3,  0,  7)
+8    2    atomic rmw      relaxed        0x601060   0x1                 7   ( 0,  2,  8)
+9    2    thread finish   seq_cst  0x7efc242abbc8   0xdeadbeef              ( 0,  2,  9)
+10   3    atomic rmw      relaxed        0x60105c   0x1                 6   ( 0,  3,  0, 10)
+11   3    thread finish   seq_cst  0x7efc243abfd0   0xdeadbeef              ( 0,  3,  0, 11)
+12   1    thread join     seq_cst  0x7efc242abbc8   0x2                     ( 0, 12,  9)
+13   1    thread join     seq_cst  0x7efc243abfd0   0x3                     ( 0, 13,  9, 11)
+14   1    thread finish   seq_cst  0x7efc241ab7c0   0xdeadbeef              ( 0, 14,  9, 11)
+HASH 4227004334
+------------------------------------------------------------------------------------
+
+Program output from execution 49:
+---- BEGIN PROGRAM OUTPUT ----
+v1 = 0, v2=1
+v3 = 0, v4=1
+---- END PROGRAM OUTPUT   ----
+
+Execution trace 49:
+------------------------------------------------------------------------------------
+#    t    Action type     MO       Location         Value               Rf  CV
+------------------------------------------------------------------------------------
+1    1    thread start    seq_cst  0x7efc241ab7c0   0xdeadbeef              ( 0,  1)
+2    1    thread create   seq_cst  0x7efc242abb68   0x7efc242abb10          ( 0,  2)
+3    1    thread create   seq_cst  0x7efc242abb60   0x7efc242abb10          ( 0,  3)
+4    2    thread start    seq_cst  0x7efc242abbc8   0xdeadbeef              ( 0,  2,  4)
+5    3    thread start    seq_cst  0x7efc243abfd0   0xdeadbeef              ( 0,  3,  0,  5)
+6    2    atomic rmw      relaxed        0x60105c   0                   0   ( 0,  2,  6)
+7    3    atomic rmw      relaxed        0x601060   0                   0   ( 0,  3,  0,  7)
+8    2    atomic rmw      relaxed        0x601060   0x1                 7   ( 0,  2,  8)
+9    2    thread finish   seq_cst  0x7efc242abbc8   0xdeadbeef              ( 0,  2,  9)
+10   3    atomic rmw      relaxed        0x60105c   0x1                 6   ( 0,  3,  0, 10)
+11   3    thread finish   seq_cst  0x7efc243abfd0   0xdeadbeef              ( 0,  3,  0, 11)
+12   1    thread join     seq_cst  0x7efc242abbc8   0x2                     ( 0, 12,  9)
+13   1    thread join     seq_cst  0x7efc243abfd0   0x3                     ( 0, 13,  9, 11)
+14   1    thread finish   seq_cst  0x7efc241ab7c0   0xdeadbeef              ( 0, 14,  9, 11)
+HASH 4227004334
+------------------------------------------------------------------------------------
+
+Program output from execution 51:
+---- BEGIN PROGRAM OUTPUT ----
+v3 = 0, v4=1
+v1 = 0, v2=1
+---- END PROGRAM OUTPUT   ----
+
+Execution trace 51:
+------------------------------------------------------------------------------------
+#    t    Action type     MO       Location         Value               Rf  CV
+------------------------------------------------------------------------------------
+1    1    thread start    seq_cst  0x7efc241ab7c0   0xdeadbeef              ( 0,  1)
+2    1    thread create   seq_cst  0x7efc242abb68   0x7efc242abb10          ( 0,  2)
+3    1    thread create   seq_cst  0x7efc242abb60   0x7efc242abb10          ( 0,  3)
+4    2    thread start    seq_cst  0x7efc242abbc8   0xdeadbeef              ( 0,  2,  4)
+5    3    thread start    seq_cst  0x7efc243abfd0   0xdeadbeef              ( 0,  3,  0,  5)
+6    2    atomic rmw      relaxed        0x60105c   0                   0   ( 0,  2,  6)
+7    3    atomic rmw      relaxed        0x601060   0                   0   ( 0,  3,  0,  7)
+8    3    atomic rmw      relaxed        0x60105c   0x1                 6   ( 0,  3,  0,  8)
+9    3    thread finish   seq_cst  0x7efc243abfd0   0xdeadbeef              ( 0,  3,  0,  9)
+10   2    atomic rmw      relaxed        0x601060   0x1                 7   ( 0,  2, 10)
+11   2    thread finish   seq_cst  0x7efc242abbc8   0xdeadbeef              ( 0,  2, 11)
+12   1    thread join     seq_cst  0x7efc242abbc8   0x2                     ( 0, 12, 11)
+13   1    thread join     seq_cst  0x7efc243abfd0   0x3                     ( 0, 13, 11,  9)
+14   1    thread finish   seq_cst  0x7efc241ab7c0   0xdeadbeef              ( 0, 14, 11,  9)
+HASH 4208097262
+------------------------------------------------------------------------------------
+
+Program output from execution 57:
+---- BEGIN PROGRAM OUTPUT ----
+v1 = 0, v2=0
+v3 = 1, v4=1
+---- END PROGRAM OUTPUT   ----
+
+Execution trace 57:
+------------------------------------------------------------------------------------
+#    t    Action type     MO       Location         Value               Rf  CV
+------------------------------------------------------------------------------------
+1    1    thread start    seq_cst  0x7efc241ab7c0   0xdeadbeef              ( 0,  1)
+2    1    thread create   seq_cst  0x7efc242abb68   0x7efc242abb10          ( 0,  2)
+3    1    thread create   seq_cst  0x7efc242abb60   0x7efc242abb10          ( 0,  3)
+4    2    thread start    seq_cst  0x7efc242abbc8   0xdeadbeef              ( 0,  2,  4)
+5    3    thread start    seq_cst  0x7efc243abfd0   0xdeadbeef              ( 0,  3,  0,  5)
+6    2    atomic rmw      relaxed        0x60105c   0                   0   ( 0,  2,  6)
+7    2    atomic rmw      relaxed        0x601060   0                   0   ( 0,  2,  7)
+8    2    thread finish   seq_cst  0x7efc242abbc8   0xdeadbeef              ( 0,  2,  8)
+9    1    thread join     seq_cst  0x7efc242abbc8   0x2                     ( 0,  9,  8)
+10   3    atomic rmw      relaxed        0x601060   0x1                 7   ( 0,  3,  0, 10)
+11   3    atomic rmw      relaxed        0x60105c   0x1                 6   ( 0,  3,  0, 11)
+12   3    thread finish   seq_cst  0x7efc243abfd0   0xdeadbeef              ( 0,  3,  0, 12)
+13   1    thread join     seq_cst  0x7efc243abfd0   0x3                     ( 0, 13,  8, 12)
+14   1    thread finish   seq_cst  0x7efc241ab7c0   0xdeadbeef              ( 0, 14,  8, 12)
+HASH 4064055974
+------------------------------------------------------------------------------------
+
+Program output from execution 58:
+---- BEGIN PROGRAM OUTPUT ----
+v1 = 0, v2=0
+v3 = 1, v4=1
+---- END PROGRAM OUTPUT   ----
+
+Execution trace 58:
+------------------------------------------------------------------------------------
+#    t    Action type     MO       Location         Value               Rf  CV
+------------------------------------------------------------------------------------
+1    1    thread start    seq_cst  0x7efc241ab7c0   0xdeadbeef              ( 0,  1)
+2    1    thread create   seq_cst  0x7efc242abb68   0x7efc242abb10          ( 0,  2)
+3    1    thread create   seq_cst  0x7efc242abb60   0x7efc242abb10          ( 0,  3)
+4    2    thread start    seq_cst  0x7efc242abbc8   0xdeadbeef              ( 0,  2,  4)
+5    3    thread start    seq_cst  0x7efc243abfd0   0xdeadbeef              ( 0,  3,  0,  5)
+6    2    atomic rmw      relaxed        0x60105c   0                   0   ( 0,  2,  6)
+7    2    atomic rmw      relaxed        0x601060   0                   0   ( 0,  2,  7)
+8    2    thread finish   seq_cst  0x7efc242abbc8   0xdeadbeef              ( 0,  2,  8)
+9    1    thread join     seq_cst  0x7efc242abbc8   0x2                     ( 0,  9,  8)
+10   3    atomic rmw      relaxed        0x601060   0x1                 7   ( 0,  3,  0, 10)
+11   3    atomic rmw      relaxed        0x60105c   0x1                 6   ( 0,  3,  0, 11)
+12   3    thread finish   seq_cst  0x7efc243abfd0   0xdeadbeef              ( 0,  3,  0, 12)
+13   1    thread join     seq_cst  0x7efc243abfd0   0x3                     ( 0, 13,  8, 12)
+14   1    thread finish   seq_cst  0x7efc241ab7c0   0xdeadbeef              ( 0, 14,  8, 12)
+HASH 4064055974
+------------------------------------------------------------------------------------
+
+Program output from execution 67:
+---- BEGIN PROGRAM OUTPUT ----
+v3 = 0, v4=1
+v1 = 0, v2=1
+---- END PROGRAM OUTPUT   ----
+
+Execution trace 67:
+------------------------------------------------------------------------------------
+#    t    Action type     MO       Location         Value               Rf  CV
+------------------------------------------------------------------------------------
+1    1    thread start    seq_cst  0x7efc241ab7c0   0xdeadbeef              ( 0,  1)
+2    1    thread create   seq_cst  0x7efc242abb68   0x7efc242abb10          ( 0,  2)
+3    1    thread create   seq_cst  0x7efc242abb60   0x7efc242abb10          ( 0,  3)
+4    2    thread start    seq_cst  0x7efc242abbc8   0xdeadbeef              ( 0,  2,  4)
+5    3    thread start    seq_cst  0x7efc243abfd0   0xdeadbeef              ( 0,  3,  0,  5)
+6    2    atomic rmw      relaxed        0x60105c   0                   0   ( 0,  2,  6)
+7    3    atomic rmw      relaxed        0x601060   0                   0   ( 0,  3,  0,  7)
+8    3    atomic rmw      relaxed        0x60105c   0x1                 6   ( 0,  3,  0,  8)
+9    3    thread finish   seq_cst  0x7efc243abfd0   0xdeadbeef              ( 0,  3,  0,  9)
+10   2    atomic rmw      relaxed        0x601060   0x1                 7   ( 0,  2, 10)
+11   2    thread finish   seq_cst  0x7efc242abbc8   0xdeadbeef              ( 0,  2, 11)
+12   1    thread join     seq_cst  0x7efc242abbc8   0x2                     ( 0, 12, 11)
+13   1    thread join     seq_cst  0x7efc243abfd0   0x3                     ( 0, 13, 11,  9)
+14   1    thread finish   seq_cst  0x7efc241ab7c0   0xdeadbeef              ( 0, 14, 11,  9)
+HASH 4208097262
+------------------------------------------------------------------------------------
+
+Program output from execution 70:
+---- BEGIN PROGRAM OUTPUT ----
+v1 = 0, v2=0
+v3 = 1, v4=1
+---- END PROGRAM OUTPUT   ----
+
+Execution trace 70:
+------------------------------------------------------------------------------------
+#    t    Action type     MO       Location         Value               Rf  CV
+------------------------------------------------------------------------------------
+1    1    thread start    seq_cst  0x7efc241ab7c0   0xdeadbeef              ( 0,  1)
+2    1    thread create   seq_cst  0x7efc242abb68   0x7efc242abb10          ( 0,  2)
+3    1    thread create   seq_cst  0x7efc242abb60   0x7efc242abb10          ( 0,  3)
+4    2    thread start    seq_cst  0x7efc242abbc8   0xdeadbeef              ( 0,  2,  4)
+5    3    thread start    seq_cst  0x7efc243abfd0   0xdeadbeef              ( 0,  3,  0,  5)
+6    2    atomic rmw      relaxed        0x60105c   0                   0   ( 0,  2,  6)
+7    2    atomic rmw      relaxed        0x601060   0                   0   ( 0,  2,  7)
+8    2    thread finish   seq_cst  0x7efc242abbc8   0xdeadbeef              ( 0,  2,  8)
+9    3    atomic rmw      relaxed        0x601060   0x1                 7   ( 0,  3,  0,  9)
+10   1    thread join     seq_cst  0x7efc242abbc8   0x2                     ( 0, 10,  8)
+11   3    atomic rmw      relaxed        0x60105c   0x1                 6   ( 0,  3,  0, 11)
+12   3    thread finish   seq_cst  0x7efc243abfd0   0xdeadbeef              ( 0,  3,  0, 12)
+13   1    thread join     seq_cst  0x7efc243abfd0   0x3                     ( 0, 13,  8, 12)
+14   1    thread finish   seq_cst  0x7efc241ab7c0   0xdeadbeef              ( 0, 14,  8, 12)
+HASH 4067202982
+------------------------------------------------------------------------------------
+
+Program output from execution 73:
+---- BEGIN PROGRAM OUTPUT ----
+v3 = 0, v4=1
+v1 = 0, v2=1
+---- END PROGRAM OUTPUT   ----
+
+Execution trace 73:
+------------------------------------------------------------------------------------
+#    t    Action type     MO       Location         Value               Rf  CV
+------------------------------------------------------------------------------------
+1    1    thread start    seq_cst  0x7efc241ab7c0   0xdeadbeef              ( 0,  1)
+2    1    thread create   seq_cst  0x7efc242abb68   0x7efc242abb10          ( 0,  2)
+3    1    thread create   seq_cst  0x7efc242abb60   0x7efc242abb10          ( 0,  3)
+4    2    thread start    seq_cst  0x7efc242abbc8   0xdeadbeef              ( 0,  2,  4)
+5    3    thread start    seq_cst  0x7efc243abfd0   0xdeadbeef              ( 0,  3,  0,  5)
+6    2    atomic rmw      relaxed        0x60105c   0                   0   ( 0,  2,  6)
+7    3    atomic rmw      relaxed        0x601060   0                   0   ( 0,  3,  0,  7)
+8    3    atomic rmw      relaxed        0x60105c   0x1                 6   ( 0,  3,  0,  8)
+9    3    thread finish   seq_cst  0x7efc243abfd0   0xdeadbeef              ( 0,  3,  0,  9)
+10   2    atomic rmw      relaxed        0x601060   0x1                 7   ( 0,  2, 10)
+11   2    thread finish   seq_cst  0x7efc242abbc8   0xdeadbeef              ( 0,  2, 11)
+12   1    thread join     seq_cst  0x7efc242abbc8   0x2                     ( 0, 12, 11)
+13   1    thread join     seq_cst  0x7efc243abfd0   0x3                     ( 0, 13, 11,  9)
+14   1    thread finish   seq_cst  0x7efc241ab7c0   0xdeadbeef              ( 0, 14, 11,  9)
+HASH 4208097262
+------------------------------------------------------------------------------------
+
+Program output from execution 74:
+---- BEGIN PROGRAM OUTPUT ----
+v1 = 0, v2=0
+v3 = 1, v4=1
+---- END PROGRAM OUTPUT   ----
+
+Execution trace 74:
+------------------------------------------------------------------------------------
+#    t    Action type     MO       Location         Value               Rf  CV
+------------------------------------------------------------------------------------
+1    1    thread start    seq_cst  0x7efc241ab7c0   0xdeadbeef              ( 0,  1)
+2    1    thread create   seq_cst  0x7efc242abb68   0x7efc242abb10          ( 0,  2)
+3    1    thread create   seq_cst  0x7efc242abb60   0x7efc242abb10          ( 0,  3)
+4    2    thread start    seq_cst  0x7efc242abbc8   0xdeadbeef              ( 0,  2,  4)
+5    3    thread start    seq_cst  0x7efc243abfd0   0xdeadbeef              ( 0,  3,  0,  5)
+6    2    atomic rmw      relaxed        0x60105c   0                   0   ( 0,  2,  6)
+7    2    atomic rmw      relaxed        0x601060   0                   0   ( 0,  2,  7)
+8    2    thread finish   seq_cst  0x7efc242abbc8   0xdeadbeef              ( 0,  2,  8)
+9    1    thread join     seq_cst  0x7efc242abbc8   0x2                     ( 0,  9,  8)
+10   3    atomic rmw      relaxed        0x601060   0x1                 7   ( 0,  3,  0, 10)
+11   3    atomic rmw      relaxed        0x60105c   0x1                 6   ( 0,  3,  0, 11)
+12   3    thread finish   seq_cst  0x7efc243abfd0   0xdeadbeef              ( 0,  3,  0, 12)
+13   1    thread join     seq_cst  0x7efc243abfd0   0x3                     ( 0, 13,  8, 12)
+14   1    thread finish   seq_cst  0x7efc241ab7c0   0xdeadbeef              ( 0, 14,  8, 12)
+HASH 4064055974
+------------------------------------------------------------------------------------
+
+Program output from execution 94:
+---- BEGIN PROGRAM OUTPUT ----
+v1 = 0, v2=1
+v3 = 0, v4=1
+---- END PROGRAM OUTPUT   ----
+
+Execution trace 94:
+------------------------------------------------------------------------------------
+#    t    Action type     MO       Location         Value               Rf  CV
+------------------------------------------------------------------------------------
+1    1    thread start    seq_cst  0x7efc241ab7c0   0xdeadbeef              ( 0,  1)
+2    1    thread create   seq_cst  0x7efc242abb68   0x7efc242abb10          ( 0,  2)
+3    1    thread create   seq_cst  0x7efc242abb60   0x7efc242abb10          ( 0,  3)
+4    2    thread start    seq_cst  0x7efc242abbc8   0xdeadbeef              ( 0,  2,  4)
+5    3    thread start    seq_cst  0x7efc243abfd0   0xdeadbeef              ( 0,  3,  0,  5)
+6    3    atomic rmw      relaxed        0x601060   0                   0   ( 0,  3,  0,  6)
+7    2    atomic rmw      relaxed        0x60105c   0                   0   ( 0,  2,  7)
+8    2    atomic rmw      relaxed        0x601060   0x1                 6   ( 0,  2,  8)
+9    2    thread finish   seq_cst  0x7efc242abbc8   0xdeadbeef              ( 0,  2,  9)
+10   3    atomic rmw      relaxed        0x60105c   0x1                 7   ( 0,  3,  0, 10)
+11   3    thread finish   seq_cst  0x7efc243abfd0   0xdeadbeef              ( 0,  3,  0, 11)
+12   1    thread join     seq_cst  0x7efc242abbc8   0x2                     ( 0, 12,  9)
+13   1    thread join     seq_cst  0x7efc243abfd0   0x3                     ( 0, 13,  9, 11)
+14   1    thread finish   seq_cst  0x7efc241ab7c0   0xdeadbeef              ( 0, 14,  9, 11)
+HASH 3000133102
+------------------------------------------------------------------------------------
+
+Program output from execution 95:
+---- BEGIN PROGRAM OUTPUT ----
+v3 = 0, v4=0
+v1 = 1, v2=1
+---- END PROGRAM OUTPUT   ----
+
+Execution trace 95:
+------------------------------------------------------------------------------------
+#    t    Action type     MO       Location         Value               Rf  CV
+------------------------------------------------------------------------------------
+1    1    thread start    seq_cst  0x7efc241ab7c0   0xdeadbeef              ( 0,  1)
+2    1    thread create   seq_cst  0x7efc242abb68   0x7efc242abb10          ( 0,  2)
+3    1    thread create   seq_cst  0x7efc242abb60   0x7efc242abb10          ( 0,  3)
+4    2    thread start    seq_cst  0x7efc242abbc8   0xdeadbeef              ( 0,  2,  4)
+5    3    thread start    seq_cst  0x7efc243abfd0   0xdeadbeef              ( 0,  3,  0,  5)
+6    3    atomic rmw      relaxed        0x601060   0                   0   ( 0,  3,  0,  6)
+7    3    atomic rmw      relaxed        0x60105c   0                   0   ( 0,  3,  0,  7)
+8    3    thread finish   seq_cst  0x7efc243abfd0   0xdeadbeef              ( 0,  3,  0,  8)
+9    2    atomic rmw      relaxed        0x60105c   0x1                 7   ( 0,  2,  9)
+10   2    atomic rmw      relaxed        0x601060   0x1                 6   ( 0,  2, 10)
+11   2    thread finish   seq_cst  0x7efc242abbc8   0xdeadbeef              ( 0,  2, 11)
+12   1    thread join     seq_cst  0x7efc242abbc8   0x2                     ( 0, 12, 11)
+13   1    thread join     seq_cst  0x7efc243abfd0   0x3                     ( 0, 13, 11,  8)
+14   1    thread finish   seq_cst  0x7efc241ab7c0   0xdeadbeef              ( 0, 14, 11,  8)
+HASH 3127311590
+------------------------------------------------------------------------------------
+
+Program output from execution 96:
+---- BEGIN PROGRAM OUTPUT ----
+v3 = 0, v4=1
+v1 = 0, v2=1
+---- END PROGRAM OUTPUT   ----
+
+Execution trace 96:
+------------------------------------------------------------------------------------
+#    t    Action type     MO       Location         Value               Rf  CV
+------------------------------------------------------------------------------------
+1    1    thread start    seq_cst  0x7efc241ab7c0   0xdeadbeef              ( 0,  1)
+2    1    thread create   seq_cst  0x7efc242abb68   0x7efc242abb10          ( 0,  2)
+3    1    thread create   seq_cst  0x7efc242abb60   0x7efc242abb10          ( 0,  3)
+4    2    thread start    seq_cst  0x7efc242abbc8   0xdeadbeef              ( 0,  2,  4)
+5    3    thread start    seq_cst  0x7efc243abfd0   0xdeadbeef              ( 0,  3,  0,  5)
+6    2    atomic rmw      relaxed        0x60105c   0                   0   ( 0,  2,  6)
+7    3    atomic rmw      relaxed        0x601060   0                   0   ( 0,  3,  0,  7)
+8    3    atomic rmw      relaxed        0x60105c   0x1                 6   ( 0,  3,  0,  8)
+9    3    thread finish   seq_cst  0x7efc243abfd0   0xdeadbeef              ( 0,  3,  0,  9)
+10   2    atomic rmw      relaxed        0x601060   0x1                 7   ( 0,  2, 10)
+11   2    thread finish   seq_cst  0x7efc242abbc8   0xdeadbeef              ( 0,  2, 11)
+12   1    thread join     seq_cst  0x7efc242abbc8   0x2                     ( 0, 12, 11)
+13   1    thread join     seq_cst  0x7efc243abfd0   0x3                     ( 0, 13, 11,  9)
+14   1    thread finish   seq_cst  0x7efc241ab7c0   0xdeadbeef              ( 0, 14, 11,  9)
+HASH 4208097262
+------------------------------------------------------------------------------------
+
+Program output from execution 98:
+---- BEGIN PROGRAM OUTPUT ----
+v3 = 0, v4=0
+v1 = 1, v2=1
+---- END PROGRAM OUTPUT   ----
+
+Execution trace 98:
+------------------------------------------------------------------------------------
+#    t    Action type     MO       Location         Value               Rf  CV
+------------------------------------------------------------------------------------
+1    1    thread start    seq_cst  0x7efc241ab7c0   0xdeadbeef              ( 0,  1)
+2    1    thread create   seq_cst  0x7efc242abb68   0x7efc242abb10          ( 0,  2)
+3    1    thread create   seq_cst  0x7efc242abb60   0x7efc242abb10          ( 0,  3)
+4    2    thread start    seq_cst  0x7efc242abbc8   0xdeadbeef              ( 0,  2,  4)
+5    3    thread start    seq_cst  0x7efc243abfd0   0xdeadbeef              ( 0,  3,  0,  5)
+6    3    atomic rmw      relaxed        0x601060   0                   0   ( 0,  3,  0,  6)
+7    3    atomic rmw      relaxed        0x60105c   0                   0   ( 0,  3,  0,  7)
+8    3    thread finish   seq_cst  0x7efc243abfd0   0xdeadbeef              ( 0,  3,  0,  8)
+9    2    atomic rmw      relaxed        0x60105c   0x1                 7   ( 0,  2,  9)
+10   2    atomic rmw      relaxed        0x601060   0x1                 6   ( 0,  2, 10)
+11   2    thread finish   seq_cst  0x7efc242abbc8   0xdeadbeef              ( 0,  2, 11)
+12   1    thread join     seq_cst  0x7efc242abbc8   0x2                     ( 0, 12, 11)
+13   1    thread join     seq_cst  0x7efc243abfd0   0x3                     ( 0, 13, 11,  8)
+14   1    thread finish   seq_cst  0x7efc241ab7c0   0xdeadbeef              ( 0, 14, 11,  8)
+HASH 3127311590
+------------------------------------------------------------------------------------
+
+Program output from execution 100:
+---- BEGIN PROGRAM OUTPUT ----
+v1 = 0, v2=1
+v3 = 0, v4=1
+---- END PROGRAM OUTPUT   ----
+
+Execution trace 100:
+------------------------------------------------------------------------------------
+#    t    Action type     MO       Location         Value               Rf  CV
+------------------------------------------------------------------------------------
+1    1    thread start    seq_cst  0x7efc241ab7c0   0xdeadbeef              ( 0,  1)
+2    1    thread create   seq_cst  0x7efc242abb68   0x7efc242abb10          ( 0,  2)
+3    1    thread create   seq_cst  0x7efc242abb60   0x7efc242abb10          ( 0,  3)
+4    2    thread start    seq_cst  0x7efc242abbc8   0xdeadbeef              ( 0,  2,  4)
+5    3    thread start    seq_cst  0x7efc243abfd0   0xdeadbeef              ( 0,  3,  0,  5)
+6    3    atomic rmw      relaxed        0x601060   0                   0   ( 0,  3,  0,  6)
+7    2    atomic rmw      relaxed        0x60105c   0                   0   ( 0,  2,  7)
+8    2    atomic rmw      relaxed        0x601060   0x1                 6   ( 0,  2,  8)
+9    2    thread finish   seq_cst  0x7efc242abbc8   0xdeadbeef              ( 0,  2,  9)
+10   1    thread join     seq_cst  0x7efc242abbc8   0x2                     ( 0, 10,  9)
+11   3    atomic rmw      relaxed        0x60105c   0x1                 7   ( 0,  3,  0, 11)
+12   3    thread finish   seq_cst  0x7efc243abfd0   0xdeadbeef              ( 0,  3,  0, 12)
+13   1    thread join     seq_cst  0x7efc243abfd0   0x3                     ( 0, 13,  9, 12)
+14   1    thread finish   seq_cst  0x7efc241ab7c0   0xdeadbeef              ( 0, 14,  9, 12)
+HASH 3000504038
+------------------------------------------------------------------------------------
+
+******* Model-checking complete: *******
+Number of complete, bug-free executions: 25
+Number of redundant executions: 0
+Number of buggy executions: 0
+Number of infeasible executions: 75
+Total executions: 100
+Total nodes created: 935
diff --git a/test/memo/rmw2prog b/test/memo/rmw2prog
new file mode 100755
index 00000000..6fbf4dd7
Binary files /dev/null and b/test/memo/rmw2prog differ
diff --git a/test/memo/script.sh b/test/memo/script.sh
new file mode 100755
index 00000000..a97c7022
--- /dev/null
+++ b/test/memo/script.sh
@@ -0,0 +1,19 @@
+#!/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
new file mode 100755
index 00000000..67443eaa
Binary files /dev/null and b/test/memo/userprog differ
diff --git a/test/rmw2prog.c b/test/rmw2prog.c
index 0d03b028..f5c3f108 100644
--- a/test/rmw2prog.c
+++ b/test/rmw2prog.c
@@ -4,20 +4,32 @@
 
 #include "librace.h"
 
-atomic_int x;
-atomic_int y;
+atomic_short x;
+atomic_short y;
 
 static void a(void *obj)
 {
-	int v1=atomic_fetch_add_explicit(&x, 1, memory_order_relaxed);
-	int v2=atomic_fetch_add_explicit(&y, 1, memory_order_relaxed);
-	printf("v1 = %d, v2=%d\n", v1, v2);
+	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, 1, memory_order_relaxed);
-	int v4=atomic_fetch_add_explicit(&x, 1, memory_order_relaxed);
+	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);
 }
 
@@ -27,11 +39,12 @@ int user_main(int argc, char **argv)
 
 	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_create(&t2, (thrd_start_t)&b, NULL);
 
 	thrd_join(t1);
-	thrd_join(t2);
+//	thrd_join(t2);
 
 	return 0;
 }
diff --git a/test/userprog.c b/test/userprog.c
index 02a83b4b..0ff8f125 100644
--- a/test/userprog.c
+++ b/test/userprog.c
@@ -6,11 +6,13 @@
 
 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);
 }
 
@@ -18,14 +20,15 @@ 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)
+int main(int argc, char **argv)
 {
 	thrd_t t1, t2;
 
-	atomic_init(&x, 0);
+	atomic_init(&x, 30);
 	atomic_init(&y, 0);
 
 	printf("Main thread: creating 2 threads\n");