Get gdax to not crash
authorBrian Demsky <bdemsky@uci.edu>
Wed, 26 Jun 2019 23:29:31 +0000 (16:29 -0700)
committerBrian Demsky <bdemsky@uci.edu>
Wed, 26 Jun 2019 23:29:31 +0000 (16:29 -0700)
1  2 
Makefile
action.h
cmodelint.cc
execution.cc
history.cc
history.h
include/cmodelint.h
model.cc
model.h

diff --cc Makefile
+++ b/Makefile
@@@ -5,7 -5,7 +5,7 @@@ OBJECTS := libthreads.o schedule.o mode
           datarace.o impatomic.o cmodelint.o \
           snapshot.o malloc.o mymemory.o common.o mutex.o conditionvariable.o \
           context.o execution.o libannotate.o plugins.o pthread.o futex.o fuzzer.o \
--         sleeps.o
++         sleeps.o history.o
  
  CPPFLAGS += -Iinclude -I.
  LDFLAGS := -ldl -lrt -rdynamic
diff --cc action.h
Simple merge
diff --cc cmodelint.cc
@@@ -2,8 -4,8 +4,9 @@@
  #include "model.h"
  #include "execution.h"
  #include "action.h"
+ #include "history.h"
  #include "cmodelint.h"
 +#include "snapshot-interface.h"
  #include "threads-model.h"
  
  memory_order orders[6] = {
@@@ -86,7 -64,9 +89,9 @@@ void model_fence_action(memory_order or
  
  /* ---  helper functions --- */
  uint64_t model_rmwrcas_action_helper(void *obj, int atomic_index, uint64_t oldval, int size, const char *position) {
-       ensureModelValue(new ModelAction(ATOMIC_RMWRCAS, position, orders[atomic_index], obj), uint64_t);
 -      return model->switch_to_master(
 -              new ModelAction(ATOMIC_RMWRCAS, position, orders[atomic_index], obj, oldval, size)
++      ensureModelValue(
++              new ModelAction(ATOMIC_RMWRCAS, position, orders[atomic_index], obj, oldval, size), uint64_t
+               );
  }
  
  uint64_t model_rmwr_action_helper(void *obj, int atomic_index, const char *position) {
@@@ -373,3 -362,34 +378,34 @@@ void cds_atomic_thread_fence(int atomic
          __old__ = __old__;  Silence clang (-Wunused-value)                    \
           })
   */
 -        Thread * th = thread_current();
+ void cds_func_entry(const char * funcName) {
+       if (!model) return;
 -        Thread * th = thread_current();
++      Thread * th = thread_current();
+       uint32_t func_id;
+       ModelHistory *history = model->get_history();
+       if ( !history->getFuncMap()->contains(funcName) ) {
+               func_id = history->get_func_counter();
+               history->incr_func_counter();
+               history->getFuncMap()->put(funcName, func_id);
+       } else {
+               func_id = history->getFuncMap()->get(funcName);
+       }
+       history->enter_function(func_id, th->get_id());
+ }
+ void cds_func_exit(const char * funcName) {
+       if (!model) return;
++      Thread * th = thread_current();
+       uint32_t func_id;
+       ModelHistory *history = model->get_history();
+       func_id = history->getFuncMap()->get(funcName);
+       history->exit_function(func_id, th->get_id());
+ }
diff --cc execution.cc
@@@ -64,7 -64,7 +64,7 @@@ ModelExecution::ModelExecution(ModelChe
        thrd_last_fence_release(),
        node_stack(node_stack),
        priv(new struct model_snapshot_members ()),
--                       mo_graph(new CycleGraph()),
++      mo_graph(new CycleGraph()),
        fuzzer(new Fuzzer())
  {
        /* Initialize a model-checker thread, for special ModelActions */
diff --cc history.cc
index 0000000,ca52209..e0560ba
mode 000000,100644..100644
--- /dev/null
@@@ -1,0 -1,36 +1,36 @@@
 -      func_id(1), /* function id starts with 1 */
+ #include <inttypes.h>
+ #include "history.h"
+ #include "action.h"
+ ModelHistory::ModelHistory() :
++      func_id(1),     /* function id starts with 1 */
+       func_map(),
+       func_history(),
+       work_list()
+ {}
+ void ModelHistory::enter_function(const uint32_t func_id, thread_id_t tid)
+ {
+       if ( !work_list.contains(tid) ) {
+               // This thread has not been pushed to work_list
+               SnapList<uint32_t> * func_list = new SnapList<uint32_t>();
+               func_list->push_back(func_id);
+               work_list.put(tid, func_list);
+       } else {
+               SnapList<uint32_t> * func_list = work_list.get(tid);
+               func_list->push_back(func_id);
+       }
+ }
+ void ModelHistory::exit_function(const uint32_t func_id, thread_id_t tid)
+ {
+       SnapList<uint32_t> * func_list = work_list.get(tid);
+       uint32_t last_func_id = func_list->back();
+       if (last_func_id == func_id) {
+               func_list->pop_back();
+       } else {
+               model_print("trying to exit with a wrong function id\n");
+               model_print("--- last_func: %d, func_id: %d\n", last_func_id, func_id);
+       }
+ }
diff --cc history.h
index 0000000,fff5712..441a999
mode 000000,100644..100644
--- /dev/null
+++ b/history.h
@@@ -1,0 -1,39 +1,39 @@@
 -      
+ #include "stl-model.h"
+ #include "common.h"
+ #include "hashtable.h"
+ #include "modeltypes.h"
+ /* forward declaration */
+ class ModelAction;
+ typedef ModelList<ModelAction *> action_mlist_t;
+ class ModelHistory {
+ public:
+       ModelHistory();
 -        uint32_t get_func_counter() { return func_id; }
 -        void incr_func_counter() { func_id++; }
++
+       void enter_function(const uint32_t func_id, thread_id_t tid);
+       void exit_function(const uint32_t func_id, thread_id_t tid);
 -        HashTable<const char *, uint32_t, uintptr_t, 4> * getFuncMap() { return &func_map; }
++      uint32_t get_func_counter() { return func_id; }
++      void incr_func_counter() { func_id++; }
 -        /* map function names to integer ids */ 
 -        HashTable<const char *, uint32_t, uintptr_t, 4> func_map;
++      HashTable<const char *, uint32_t, uintptr_t, 4> * getFuncMap() { return &func_map; }
+       HashTable<uint32_t, action_mlist_t *, uintptr_t, 4> * getFuncHistory() { return &func_history; }
+       void print();
+ private:
+       uint32_t func_id;
 -       * the functions that thread i has entered and yet to exit from 
++      /* map function names to integer ids */
++      HashTable<const char *, uint32_t, uintptr_t, 4> func_map;
+       HashTable<uint32_t, action_mlist_t *, uintptr_t, 4> func_history;
+       /* work_list stores a list of function ids for each thread
+        * SnapList<uint32_t> is intended to be used as a stack storing
++       * the functions that thread i has entered and yet to exit from
+        */
+       HashTable<thread_id_t, SnapList<uint32_t> *, uintptr_t, 4> work_list;
+ };
Simple merge
diff --cc model.cc
+++ b/model.cc
  #include "output.h"
  #include "traceanalysis.h"
  #include "execution.h"
+ #include "history.h"
  #include "bugmessage.h"
 +#include "params.h"
  
 -ModelChecker *model;
 +ModelChecker *model = NULL;
 +bool modelchecker_started = false;
 +
 +/** Wrapper to run the user's main function, with appropriate arguments */
 +void user_main_wrapper(void *)
 +{
 +      user_main(model->params.argc, model->params.argv);
 +}
  
  /** @brief Constructor */
  ModelChecker::ModelChecker() :
@@@ -161,7 -153,7 +163,7 @@@ void ModelChecker::print_bugs() cons
                                                        bugs->size(),
                                                        bugs->size() > 1 ? "s" : "");
        for (unsigned int i = 0;i < bugs->size();i++)
--              (*bugs)[i]->print();
++              (*bugs)[i] -> print();
  }
  
  /**
   */
  void ModelChecker::record_stats()
  {
--      stats.num_total++;
++      stats.num_total ++;
        if (!execution->isfeasibleprefix())
--              stats.num_infeasible++;
++              stats.num_infeasible ++;
        else if (execution->have_bug_reports())
--              stats.num_buggy_executions++;
++              stats.num_buggy_executions ++;
        else if (execution->is_complete_execution())
--              stats.num_complete++;
++              stats.num_complete ++;
        else {
--              stats.num_redundant++;
++              stats.num_redundant ++;
  
                /**
                 * @todo We can violate this ASSERT() when fairness/sleep sets
@@@ -261,15 -253,16 +263,15 @@@ bool ModelChecker::next_execution(
                return true;
        }
  // test code
--      execution_number++;
++      execution_number ++;
        reset_to_initial_state();
 -      node_stack->full_reset();
        return false;
  }
  
  /** @brief Run trace analyses on complete trace */
  void ModelChecker::run_trace_analyses() {
--      for (unsigned int i = 0;i < trace_analyses.size();i++)
--              trace_analyses[i]->analyze(execution->get_action_trace());
++      for (unsigned int i = 0;i < trace_analyses.size();i ++)
++              trace_analyses[i] -> analyze(execution->get_action_trace());
  }
  
  /**
@@@ -369,9 -368,11 +371,9 @@@ void ModelChecker::run(
        char random_state[256];
        initstate(423121, random_state, sizeof(random_state));
  
--      for(int exec = 0;exec < params.maxexecutions;exec++) {
 -              thrd_t user_thread;
 -              Thread *t = new Thread(execution->get_next_id(), &user_thread, &user_main_wrapper, NULL, NULL); // L: user_main_wrapper passes the user program
 -              execution->add_thread(t);
 -              //Need to seed random number generator, otherwise its state gets reset
++      for(int exec = 0;exec < params.maxexecutions;exec ++) {
 +              Thread * t = init_thread;
 +
                do {
                        /*
                         * Stash next pending action(s) for thread(s). There
diff --cc model.h
+++ b/model.h
@@@ -72,7 -74,7 +74,8 @@@ private
        Scheduler * const scheduler;
        NodeStack * const node_stack;
        ModelExecution *execution;
 +      Thread * init_thread;
+       ModelHistory *history;
  
        int execution_number;