change cds checker to accomdate llvm pass

diff --git a/#cmodelint.cc# b/#cmodelint.cc#
new file mode 100644 (file)
index 0000000..b67194f
--- /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 (file)
index 0000000..d4ab75b
--- /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 cf4a493b2a523fed3ed327509d69a396657f8cc9..3c5128545481c917983c17750d421590f5520bc8 100644 (file)
--- 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 d4c6253caf20c23411c60ba350a91760c386e6fc..c913b74c80daa134f4e1140c1b4ffb292d2882aa 100644 (file)
--- 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 c8ad85bcc99bf1e051771d7a6779b99f58f0dae7..d1f4fffde77b5f96600f45e1c1dbaea8b6a98b85 100644 (file)
--- 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 1632581101e0c5801f8ba14c05d3d12e1fa4c94c..15d6151b9f1bc7b7030539e656ef209f19c6eb09 100644 (file)
--- 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 0fcf4e8d10b206e5a07062849e038c12915264a9..869833c21ccda7949c1c655bb85f62828175fa26 100644 (file)
--- 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 24c5f6fb67353b97d24351ef9e8f32c08e437155..1c456b89f7ec82260d6f6bcf5106449b5eba5add 100644 (file)
--- 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 b4273eee4a5984ce47c3b0ae922700fcad1f9e11..100ad0d6c6a43902abe9a51949b8524807f80b84 100644 (file)
--- 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 cabf0661ae32832efde74da04fe5ba6257552241..83e05d92cd88325555b82aeabfb95dcc1d3ae491 100644 (file)
--- 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 ba0dafd652410e4eac17189f0d7fe54ce2b22928..704d15e723bb5152bbda603b58bb3024031e516c 100644 (file)
--- 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 (file)
index d4d2198..0000000
--- 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 (file)
index 0000000..d4d2198
--- /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 2c36054bad8000fe4231ce822a215f291163d5fb..5dafc6ffcbb33a5893310f117822738202fd2fa9 100644 (file)
--- 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 bfb6d22f85009e61e0d4fbad5926764328a4a8fd..ccc109a7be96594f395c2ccd0f6ab56cf230a88f 100644 (file)
--- 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 66faacd8e445510f57c7714ce9ccd60a1ee95f3c..7deaeff4339a0dcdd6e6d535bf4cc67245cab08e 100644 (file)
--- 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 (executable)
index 0000000..eb48204
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 (executable)
index 0000000..3196361
Binary files /dev/null and b/test/memo/fences differ

diff --git a/test/memo/original b/test/memo/original
new file mode 100644 (file)
index 0000000..68f653e
--- /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 (file)
index 0000000..3e8204e
--- /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 (executable)
index 0000000..6fbf4dd
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 (executable)
index 0000000..a97c702
--- /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 (executable)
index 0000000..67443ea
Binary files /dev/null and b/test/memo/userprog differ

diff --git a/test/rmw2prog.c b/test/rmw2prog.c
index 0d03b028d8d8432d160cf6724cd327294cff6e73..f5c3f108e595ac0c6be8004ad74fe836b14592ab 100644 (file)
--- 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 02a83b4b2f2469f6af1f59c77038ed95c7878998..0ff8f125f79e6fb67ac44fea04a5e59cfd759873 100644 (file)
--- 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");