Get GDAX working.

diff --git a/main.cc b/main.cc
index 5396823334df9a0b47f3077f3c352cc6774e7e1b..53495072e32d3c75f855d5cc82582a8dfc8e112b 100644 (file)
--- a/main.cc
+++ b/main.cc
@@ -23,6 +23,7 @@ void param_defaults(struct model_params *params)
        params->uninitvalue = 0;
        params->maxexecutions = 10;
        params->nofork = false;
+       params->threadsnocleanup = false;
 }
 
 static void print_usage(const char *program_name, struct model_params *params)
@@ -56,6 +57,9 @@ static void print_usage(const char *program_name, struct model_params *params)
                "                            Default: %u\n"
                "                            -o help for a list of options\n"
                "-n                          No fork\n"
+#ifdef TLS
+               "-d                          Don't allow threads to cleanup\n"
+#endif
                " --                         Program arguments follow.\n\n",
                program_name,
                params->verbose,
@@ -86,7 +90,7 @@ bool install_plugin(char * name) {
 
 static void parse_options(struct model_params *params, int argc, char **argv)
 {
-       const char *shortopts = "hnt:o:u:x:v::";
+       const char *shortopts = "hdnt:o:u:x:v::";
        const struct option longopts[] = {
                {"help", no_argument, NULL, 'h'},
                {"verbose", optional_argument, NULL, 'v'},
@@ -103,6 +107,9 @@ static void parse_options(struct model_params *params, int argc, char **argv)
                case 'h':
                        print_usage(argv[0], params);
                        break;
+               case 'd':
+                       params->threadsnocleanup = true;
+                       break;
                case 'n':
                        params->nofork = true;
                        break;

diff --git a/model.cc b/model.cc
index b0540699aee48bdca071ef1894d9690e7395c38e..66af988821af8ef491191a0cfb80151092ef38fd 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -392,20 +392,6 @@ void ModelChecker::startMainThread() {
        main_thread_startup();
 }
 
-static bool is_nonsc_write(const ModelAction *act) {
-       if (act->get_type() == ATOMIC_WRITE) {
-               std::memory_order order = act->get_mo();
-               switch(order) {
-               case std::memory_order_relaxed:
-               case std::memory_order_release:
-                       return true;
-               default:
-                       return false;
-               }
-       }
-       return false;
-}
-
 /** @brief Run ModelChecker for the user program */
 void ModelChecker::run()
 {

diff --git a/model.h b/model.h
index 2f137a3aea70bd3f8686cec759730d738996733c..82d9bc8c4fc9853f15ed3b2d2bef7e6e1f27cf83 100644 (file)
--- a/model.h
+++ b/model.h
@@ -68,6 +68,7 @@ public:
        void startMainThread();
        void startChecker();
        Thread * getInitThread() {return init_thread;}
+       Scheduler * getScheduler() {return scheduler;}
        MEMALLOC
 private:
        /** Flag indicates whether to restart the model checker. */

diff --git a/params.h b/params.h
index 7f749cae6fc082d1551fdfb86f0c5728cf176fbc..9a2cf3b96f99f5c864d4be1903b4eecb72c2fc71 100644 (file)
--- a/params.h
+++ b/params.h
@@ -9,6 +9,7 @@ struct model_params {
        unsigned int uninitvalue;
        int maxexecutions;
        bool nofork;
+       bool threadsnocleanup;
 
        /** @brief Verbosity (0 = quiet; 1 = noisy; 2 = noisier) */
        int verbose;

diff --git a/snapshot.cc b/snapshot.cc
index 2402bbde894f8a2134741636f24ebc8882aac306..24e8d073ca1330eb778b897955e500dab30f9c5e 100644 (file)
--- a/snapshot.cc
+++ b/snapshot.cc
@@ -14,6 +14,9 @@
 #include "context.h"
 #include "model.h"
 
+
+#if USE_MPROTECT_SNAPSHOT
+
 /** PageAlignedAdressUpdate return a page aligned address for the
  * address being added as a side effect the numBytes are also changed.
  */
@@ -22,8 +25,6 @@ static void * PageAlignAddressUpward(void *addr)
        return (void *)((((uintptr_t)addr) + PAGESIZE - 1) & ~(PAGESIZE - 1));
 }
 
-#if USE_MPROTECT_SNAPSHOT
-
 /* Each SnapShotRecord lists the firstbackingpage that must be written to
  * revert to that snapshot */
 struct SnapShotRecord {

diff --git a/threads.cc b/threads.cc
index 8d078b51bbfa1a8c0b4bc03b3176afa85f3a4d97..0da9282aa942bd2966bf939d6409636fa99049e5 100644 (file)
--- a/threads.cc
+++ b/threads.cc
@@ -13,6 +13,7 @@
 /* global "model" object */
 #include "model.h"
 #include "execution.h"
+#include "schedule.h"
 
 #ifdef TLS
 #include <dlfcn.h>
@@ -319,10 +320,15 @@ void Thread::complete()
        if (stack)
                stack_free(stack);
 #ifdef TLS
-       if (this != model->getInitThread()) {
+       if (this != model->getInitThread() && !model->getParams()->threadsnocleanup) {
                modellock = 1;
+               ASSERT(thread_current()==NULL);
+               Thread * curr_thread = model->getScheduler()->get_current_thread();
+               //Make any current_thread calls work in code to free
+               model->getScheduler()->set_current_thread(this);
                real_pthread_mutex_unlock(&mutex2);
                real_pthread_join(thread, NULL);
+               model->getScheduler()->set_current_thread(curr_thread);
                modellock = 0;
        }
 #endif