Small changes; slightly faster than tsan11rec in jsbench now
authorweiyu <weiyuluo1232@gmail.com>
Wed, 2 Sep 2020 22:41:39 +0000 (15:41 -0700)
committerweiyu <weiyuluo1232@gmail.com>
Wed, 2 Sep 2020 22:41:39 +0000 (15:41 -0700)
datarace.cc
execution.cc
execution.h
model.cc
model.h
schedule.cc
schedule.h

index 544fced..da5fa8c 100644 (file)
@@ -558,9 +558,9 @@ struct DataRace * fullRaceCheckRead(thread_id_t thread, const void *location, ui
                if (clock_may_race(currClock, thread, readClock, readThread)) {
                        /* Still need this read in vector */
                        if (copytoindex != i) {
-                               ASSERT(record->thread[i] >= 0);
-                               record->readClock[copytoindex] = record->readClock[i];
-                               record->thread[copytoindex] = record->thread[i];
+                               ASSERT(readThread >= 0);
+                               record->readClock[copytoindex] = readClock;
+                               record->thread[copytoindex] = readThread;
                        }
                        copytoindex++;
                }
index c1a5308..c329b8c 100644 (file)
@@ -277,8 +277,9 @@ bool ModelExecution::should_wake_up(const ModelAction *curr, const Thread *threa
 void ModelExecution::wake_up_sleeping_actions(ModelAction *curr)
 {
        for (unsigned int i = 0;i < get_num_threads();i++) {
-               Thread *thr = get_thread(int_to_id(i));
-               if (scheduler->is_sleep_set(thr)) {
+               thread_id_t tid = int_to_id(i);
+               Thread *thr = get_thread(tid);
+               if (scheduler->is_sleep_set(tid)) {
                        if (should_wake_up(curr, thr)) {
                                /* Remove this thread from sleep set */
                                scheduler->remove_sleep(thr);
@@ -808,7 +809,6 @@ bool ModelExecution::check_action_enabled(ModelAction *curr) {
 ModelAction * ModelExecution::check_current_action(ModelAction *curr)
 {
        ASSERT(curr);
-       bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
        bool newly_explored = initialize_curr_action(&curr);
 
        DBG();
@@ -816,20 +816,17 @@ ModelAction * ModelExecution::check_current_action(ModelAction *curr)
        wake_up_sleeping_actions(curr);
 
        SnapVector<ModelAction *> * rf_set = NULL;
+       bool canprune = false;
        /* Build may_read_from set for newly-created actions */
-       if (newly_explored && curr->is_read())
+       if (curr->is_read() && newly_explored) {
                rf_set = build_may_read_from(curr);
-
-       bool canprune = false;
-
-       if (curr->is_read() && !second_part_of_rmw) {
                canprune = process_read(curr, rf_set);
                delete rf_set;
        } else
                ASSERT(rf_set == NULL);
 
-       /* Add the action to lists */
-       if (!second_part_of_rmw) {
+       /* Add the action to lists if not the second part of a rmw */
+       if (newly_explored) {
 #ifdef COLLECT_STAT
                record_atomic_stats(curr);
 #endif
@@ -884,7 +881,7 @@ ModelAction * ModelExecution::process_rmw(ModelAction *act) {
  */
 
 bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf,
-                                                                                                                                                                       SnapVector<ModelAction *> * priorset, bool * canprune, bool check_only)
+                                                                                                                                                                       SnapVector<ModelAction *> * priorset, bool * canprune)
 {
        SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
        ASSERT(curr->is_read());
@@ -947,8 +944,7 @@ bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *
                                                *act < *last_sc_fence_thread_local) {
                                        if (mo_graph->checkReachable(rf, act))
                                                return false;
-                                       if (!check_only)
-                                               priorset->push_back(act);
+                                       priorset->push_back(act);
                                        break;
                                }
                                /* C++, Section 29.3 statement 4 */
@@ -956,8 +952,7 @@ bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *
                                                                 *act < *last_sc_fence_local) {
                                        if (mo_graph->checkReachable(rf, act))
                                                return false;
-                                       if (!check_only)
-                                               priorset->push_back(act);
+                                       priorset->push_back(act);
                                        break;
                                }
                                /* C++, Section 29.3 statement 6 */
@@ -965,8 +960,7 @@ bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *
                                                                 *act < *last_sc_fence_thread_before) {
                                        if (mo_graph->checkReachable(rf, act))
                                                return false;
-                                       if (!check_only)
-                                               priorset->push_back(act);
+                                       priorset->push_back(act);
                                        break;
                                }
                        }
@@ -985,20 +979,17 @@ bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *
                                if (act->is_write()) {
                                        if (mo_graph->checkReachable(rf, act))
                                                return false;
-                                       if (!check_only)
-                                               priorset->push_back(act);
+                                       priorset->push_back(act);
                                } else {
                                        ModelAction *prevrf = act->get_reads_from();
                                        if (!prevrf->equals(rf)) {
                                                if (mo_graph->checkReachable(rf, prevrf))
                                                        return false;
-                                               if (!check_only)
-                                                       priorset->push_back(prevrf);
+                                               priorset->push_back(prevrf);
                                        } else {
                                                if (act->get_tid() == curr->get_tid()) {
                                                        //Can prune curr from obj list
-                                                       if (!check_only)
-                                                               *canprune = true;
+                                                       *canprune = true;
                                                }
                                        }
                                }
index 5158b2a..76f0e4e 100644 (file)
@@ -121,7 +121,7 @@ private:
        ModelAction * get_last_unlock(ModelAction *curr) const;
        SnapVector<ModelAction *> * build_may_read_from(ModelAction *curr);
        ModelAction * process_rmw(ModelAction *curr);
-       bool r_modification_order(ModelAction *curr, const ModelAction *rf, SnapVector<ModelAction *> *priorset, bool *canprune, bool check_only = false);
+       bool r_modification_order(ModelAction *curr, const ModelAction *rf, SnapVector<ModelAction *> *priorset, bool *canprune);
        void w_modification_order(ModelAction *curr);
        ClockVector * get_hb_from_write(ModelAction *rf) const;
        ModelAction * convertNonAtomicStore(void*);
index 5292b24..c022e9e 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -366,12 +366,31 @@ Thread* ModelChecker::getNextThread(Thread *old)
                        thr->freeResources();
                }
 
-               /* Don't schedule threads which should be disabled */
                ModelAction *act = thr->get_pending();
-               if (act && execution->is_enabled(thr) && !execution->check_action_enabled(act)) {
-                       scheduler->sleep(thr);
+               if (act && execution->is_enabled(tid)){
+                       /* Don't schedule threads which should be disabled */
+                       if (!execution->check_action_enabled(act)) {
+                               scheduler->sleep(thr);
+                       }
+
+                       /* Allow pending relaxed/release stores or thread actions to perform first */
+                       else if (!thread_chosen) {
+                               if (act->is_write()) {
+                                       std::memory_order order = act->get_mo();
+                                       if (order == std::memory_order_relaxed || \
+                                                       order == std::memory_order_release) {
+                                               chosen_thread = thr;
+                                               thread_chosen = true;
+                                       }
+                               } else if (act->get_type() == THREAD_CREATE || \
+                                                                        act->get_type() == PTHREAD_CREATE || \
+                                                                        act->get_type() == THREAD_START || \
+                                                                        act->get_type() == THREAD_FINISH) {
+                                       chosen_thread = thr;
+                                       thread_chosen = true;
+                               }
+                       }
                }
-               chooseThread(act, thr);
        }
        return nextThread;
 }
@@ -405,27 +424,6 @@ void ModelChecker::finishRunExecution(Thread *old)
        _Exit(0);
 }
 
-/* Allow pending relaxed/release stores or thread actions to perform first */
-void ModelChecker::chooseThread(ModelAction *act, Thread *thr)
-{
-       if (!thread_chosen && act && execution->is_enabled(thr) && (thr->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) {
-                               chosen_thread = thr;
-                               thread_chosen = true;
-                       }
-               } else if (act->get_type() == THREAD_CREATE || \
-                                                        act->get_type() == PTHREAD_CREATE || \
-                                                        act->get_type() == THREAD_START || \
-                                                        act->get_type() == THREAD_FINISH) {
-                       chosen_thread = thr;
-                       thread_chosen = true;
-               }
-       }
-}
-
 uint64_t ModelChecker::switch_thread(ModelAction *act)
 {
        if (modellock) {
diff --git a/model.h b/model.h
index 7763c56..7b8a9c9 100644 (file)
--- a/model.h
+++ b/model.h
@@ -77,7 +77,6 @@ private:
 
        void startRunExecution(Thread *old);
        void finishRunExecution(Thread *old);
-       void chooseThread(ModelAction *act, Thread *thr);
        Thread * getNextThread(Thread *old);
        bool handleChosenThread(Thread *old);
 
index 31db9c8..9bd8707 100644 (file)
@@ -102,7 +102,14 @@ bool Scheduler::is_enabled(thread_id_t tid) const
  */
 bool Scheduler::is_sleep_set(const Thread *t) const
 {
-       return get_enabled(t) == THREAD_SLEEP_SET;
+       return is_sleep_set(t->get_id());
+}
+
+bool Scheduler::is_sleep_set(thread_id_t tid) const
+{
+       int id = id_to_int(tid);
+       ASSERT(id < enabled_len);
+       return enabled[id] == THREAD_SLEEP_SET;
 }
 
 /**
index f966023..8e5554a 100644 (file)
@@ -39,6 +39,7 @@ public:
        bool is_enabled(const Thread *t) const;
        bool is_enabled(thread_id_t tid) const;
        bool is_sleep_set(const Thread *t) const;
+       bool is_sleep_set(thread_id_t tid) const;
        bool all_threads_sleeping() const;
        void set_scheduler_thread(thread_id_t tid);