Get GDAX working.
authorBrian Demsky <bdemsky@uci.edu>
Thu, 1 Aug 2019 04:15:34 +0000 (21:15 -0700)
committerBrian Demsky <bdemsky@uci.edu>
Thu, 1 Aug 2019 04:15:34 +0000 (21:15 -0700)
main.cc
model.cc
model.h
params.h
snapshot.cc
threads.cc

diff --git a/main.cc b/main.cc
index 5396823..5349507 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;
index b054069..66af988 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 2f137a3..82d9bc8 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. */
index 7f749ca..9a2cf3b 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;
index 2402bbd..24e8d07 100644 (file)
@@ -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 {
index 8d078b5..0da9282 100644 (file)
@@ -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