When an atomic read action cannot read from a desired write, make this thread sleep...
authorweiyu <weiyuluo1232@gmail.com>
Thu, 5 Sep 2019 00:49:56 +0000 (17:49 -0700)
committerweiyu <weiyuluo1232@gmail.com>
Thu, 5 Sep 2019 00:49:56 +0000 (17:49 -0700)
action.cc
action.h
execution.cc
execution.h
fuzzer.h
newfuzzer.cc
newfuzzer.h
schedule.cc

index 473d99f..f6d536e 100644 (file)
--- a/action.cc
+++ b/action.cc
@@ -219,6 +219,11 @@ void ModelAction::set_seq_number(modelclock_t num)
        seq_number = num;
 }
 
+void ModelAction::reset_seq_number()
+{
+       seq_number = 0;
+}
+
 bool ModelAction::is_thread_start() const
 {
        return type == THREAD_START;
index 0028935..21d46e5 100644 (file)
--- a/action.h
+++ b/action.h
@@ -122,6 +122,7 @@ public:
 
        void copy_from_new(ModelAction *newaction);
        void set_seq_number(modelclock_t num);
+       void reset_seq_number();
        void set_try_lock(bool obtainedlock);
        bool is_thread_start() const;
        bool is_thread_join() const;
index c3cb3bb..fe27e2f 100644 (file)
@@ -130,6 +130,12 @@ modelclock_t ModelExecution::get_next_seq_num()
        return ++priv->used_sequence_numbers;
 }
 
+/** Restore the last used sequence number when actions of a thread are postponed by Fuzzer */
+void ModelExecution::restore_last_seq_num()
+{
+       priv->used_sequence_numbers--;
+}
+
 /**
  * @brief Should the current action wake up a given thread?
  *
@@ -282,7 +288,7 @@ ModelAction * ModelExecution::convertNonAtomicStore(void * location) {
  * @param rf_set is the set of model actions we can possibly read from
  * @return True if processing this read updates the mo_graph.
  */
-void ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> * rf_set)
+bool ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> * rf_set)
 {
        SnapVector<const ModelAction *> * priorset = new SnapVector<const ModelAction *>();
        bool hasnonatomicstore = hasNonAtomicStore(curr->get_location());
@@ -294,7 +300,7 @@ void ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> *
        while(true) {
                int index = fuzzer->selectWrite(curr, rf_set);
                if (index == -1)        // no feasible write exists
-                       return;
+                       return false;
 
                ModelAction *rf = (*rf_set)[index];
 
@@ -311,7 +317,7 @@ void ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> *
                                int tid = id_to_int(curr->get_tid());
                                (*obj_thrd_map.get(curr->get_location()))[tid].pop_back();
                        }
-                       return;
+                       return true;
                }
                priorset->clear();
                (*rf_set)[index] = rf_set->back();
@@ -689,11 +695,12 @@ ModelAction * ModelExecution::check_current_action(ModelAction *curr)
                rf_set = build_may_read_from(curr);
 
        if (curr->is_read() && !second_part_of_rmw) {
-               process_read(curr, rf_set);
+               bool success = process_read(curr, rf_set);
                delete rf_set;
-       } else {
+               if (!success)
+                       return curr;    // Do not add action to lists
+       } else
                ASSERT(rf_set == NULL);
-       }
 
        /* Add the action to lists */
        if (!second_part_of_rmw && curr->get_type() != NOOP)
index f97832d..da3544a 100644 (file)
@@ -93,6 +93,8 @@ public:
        bool isFinished() {return isfinished;}
        void setFinished() {isfinished = true;}
 
+       void restore_last_seq_num();
+
        SNAPSHOTALLOC
 private:
        int get_execution_number() const;
@@ -112,7 +114,7 @@ private:
 
        bool next_execution();
        bool initialize_curr_action(ModelAction **curr);
-       void process_read(ModelAction *curr, SnapVector<ModelAction *> * rf_set);
+       bool process_read(ModelAction *curr, SnapVector<ModelAction *> * rf_set);
        void process_write(ModelAction *curr);
        bool process_fence(ModelAction *curr);
        bool process_mutex(ModelAction *curr);
index 348225c..29d31ed 100644 (file)
--- a/fuzzer.h
+++ b/fuzzer.h
@@ -10,7 +10,8 @@ public:
        Fuzzer() {}
        virtual int selectWrite(ModelAction *read, SnapVector<ModelAction *>* rf_set);
        virtual Predicate * get_selected_child_branch(thread_id_t tid) = 0;
-       Thread * selectThread(int * threadlist, int numthreads);
+       virtual bool has_paused_threads() { return false; }
+       virtual Thread * selectThread(int * threadlist, int numthreads);
        Thread * selectNotify(action_list_t * waiters);
        bool shouldSleep(const ModelAction *sleep);
        bool shouldWake(const ModelAction *sleep);
index e09175c..68efd37 100644 (file)
@@ -4,12 +4,14 @@
 #include "action.h"
 #include "execution.h"
 #include "funcnode.h"
+#include "schedule.h"
 
 NewFuzzer::NewFuzzer() :
        thrd_last_read_act(),
        thrd_curr_pred(),
        thrd_selected_child_branch(),
-       thrd_pruned_writes()
+       thrd_pruned_writes(),
+       paused_thread_set()
 {}
 
 /**
@@ -47,9 +49,21 @@ int NewFuzzer::selectWrite(ModelAction *read, SnapVector<ModelAction *> * rf_set
        // TODO: make this thread sleep if no write satisfies the chosen predicate
        // if no read satisfies the selected predicate
        if ( rf_set->size() == 0 ) {
+               Thread * read_thread = execution->get_thread(tid);
+               model_print("the %d read action of thread %d is unsuccessful\n", read->get_seq_number(), read_thread->get_id());
+
+               read_thread->set_pending(read);
+               read->reset_seq_number();       // revert some operations
+               execution->restore_last_seq_num();
+               
+               conditional_sleep(read_thread);
+               return -1;
+/*
                SnapVector<ModelAction *> * pruned_writes = thrd_pruned_writes[thread_id];
                for (uint i = 0; i < pruned_writes->size(); i++)
                        rf_set->push_back( (*pruned_writes)[i] );
+               pruned_writes->clear();
+*/
        }
 
        ASSERT(rf_set->size() != 0);
@@ -186,3 +200,46 @@ bool NewFuzzer::prune_writes(thread_id_t tid, Predicate * pred,
 
        return pruned;
 }
+
+/* @brief Put a thread to sleep because no writes in rf_set satisfies the selected predicate. 
+ *
+ * @param thread A thread whose last action is a read
+ */
+void NewFuzzer::conditional_sleep(Thread * thread)
+{
+       model->getScheduler()->add_sleep(thread);
+       paused_thread_set.push_back(thread);
+}
+
+bool NewFuzzer::has_paused_threads()
+{
+       return paused_thread_set.size() != 0;
+}
+
+Thread * NewFuzzer::selectThread(int * threadlist, int numthreads)
+{
+       if (numthreads == 0 && has_paused_threads()) {
+               wake_up_paused_threads(threadlist, &numthreads);
+               model_print("list size: %d\n", numthreads);
+               model_print("active t id: %d\n", threadlist[0]);
+       }
+
+       int random_index = random() % numthreads;
+       int thread = threadlist[random_index];
+       thread_id_t curr_tid = int_to_id(thread);
+       return model->get_thread(curr_tid);
+}
+
+void NewFuzzer::wake_up_paused_threads(int * threadlist, int * numthreads)
+{
+       int random_index = random() % paused_thread_set.size();
+       Thread * thread = paused_thread_set[random_index];
+       model->getScheduler()->remove_sleep(thread);
+
+       paused_thread_set[random_index] = paused_thread_set.back();
+       paused_thread_set.pop_back();
+
+       model_print("thread %d is woken up\n", thread->get_id());
+       threadlist[*numthreads] = thread->get_id();
+       (*numthreads)++;
+}
index c956935..7de4cd7 100644 (file)
@@ -12,9 +12,10 @@ class NewFuzzer : public Fuzzer {
 public:
        NewFuzzer();
        int selectWrite(ModelAction *read, SnapVector<ModelAction *>* rf_set);
-       Predicate * selectBranch(thread_id_t tid, Predicate * curr_pred, FuncInst * read_inst);
        Predicate * get_selected_child_branch(thread_id_t tid);
-       bool prune_writes(thread_id_t tid, Predicate * pred, SnapVector<ModelAction *> * rf_set, inst_act_map_t * inst_act_map);
+       void conditional_sleep(Thread * thread);
+       bool has_paused_threads();
+       void wake_up_paused_threads(int * threadlist, int * numthreads);
 
        Thread * selectThread(int * threadlist, int numthreads);
        Thread * selectNotify(action_list_t * waiters);
@@ -32,6 +33,14 @@ private:
        SnapVector<Predicate *> thrd_curr_pred;
        SnapVector<Predicate *> thrd_selected_child_branch;
        SnapVector< SnapVector<ModelAction *> *> thrd_pruned_writes;
+
+       bool prune_writes(thread_id_t tid, Predicate * pred, SnapVector<ModelAction *> * rf_set, inst_act_map_t * inst_act_map);
+       Predicate * selectBranch(thread_id_t tid, Predicate * curr_pred, FuncInst * read_inst);
+
+       /* Threads put to sleep by NewFuzzer because no writes in rf_set satisfies the selected predicate.
+        * Only used by selectWrite;
+        */
+       SnapVector<Thread *> paused_thread_set;
 };
 
 #endif /* end of __NEWFUZZER_H__ */
index cb97d5b..4a9752a 100644 (file)
@@ -208,8 +208,8 @@ Thread * Scheduler::select_next_thread()
                        thread_list[avail_threads++] = i;
        }
 
-       if (avail_threads == 0)
-               return NULL;// No threads availablex
+       if (avail_threads == 0 && !execution->getFuzzer()->has_paused_threads())
+               return NULL;    // No threads available
 
        Thread * thread = execution->getFuzzer()->selectThread(thread_list, avail_threads);
        curr_thread_index = id_to_int(thread->get_id());