When an atomic read action cannot read from a desired write, make this thread sleep...

diff --git a/action.cc b/action.cc
index 473d99f72899f4c0866719b5629767b4053e0c38..f6d536ee77072feaa1db4f0aa6e6a0771ea6244f 100644 (file)
--- a/action.cc
+++ b/action.cc
@@ -219,6 +219,11 @@ void ModelAction::set_seq_number(modelclock_t num)
        seq_number = num;
 }
 
        seq_number = num;
 }
 

+void ModelAction::reset_seq_number()
+{
+       seq_number = 0;
+}
+

 bool ModelAction::is_thread_start() const
 {
        return type == THREAD_START;
 bool ModelAction::is_thread_start() const
 {
        return type == THREAD_START;

diff --git a/action.h b/action.h
index 00289355be9db60dd14c4cec2eace3381ac2e79a..21d46e5bac789ec34f93340d6fa973f2eb49be52 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 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;
        void set_try_lock(bool obtainedlock);
        bool is_thread_start() const;
        bool is_thread_join() const;

diff --git a/execution.cc b/execution.cc
index c3cb3bbd2d78e5d28ca5c6a465a5e3a89c14d4fa..fe27e2ff70ee41c0aa193179ae007cab673d90fc 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -130,6 +130,12 @@ modelclock_t ModelExecution::get_next_seq_num()
        return ++priv->used_sequence_numbers;
 }
 
        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?
  *
 /**
  * @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.
  */
  * @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());
 {
        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
        while(true) {
                int index = fuzzer->selectWrite(curr, rf_set);
                if (index == -1)        // no feasible write exists

-                       return;
+                       return false;

 
                ModelAction *rf = (*rf_set)[index];
 
 
                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();
                        }
                                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();
                }
                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) {
                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;
                delete rf_set;

-       } else {
+               if (!success)
+                       return curr;    // Do not add action to lists
+       } else

                ASSERT(rf_set == NULL);
                ASSERT(rf_set == NULL);

-       }

 
        /* Add the action to lists */
        if (!second_part_of_rmw && curr->get_type() != NOOP)
 
        /* Add the action to lists */
        if (!second_part_of_rmw && curr->get_type() != NOOP)

diff --git a/execution.h b/execution.h
index f97832d8a7d063af8e251dfc1ba7e87980b13b6a..da3544ab210332c4bb10dbb08c5cb4e4b68c36c2 100644 (file)
--- a/execution.h
+++ b/execution.h
@@ -93,6 +93,8 @@ public:
        bool isFinished() {return isfinished;}
        void setFinished() {isfinished = true;}
 
        bool isFinished() {return isfinished;}
        void setFinished() {isfinished = true;}
 

+       void restore_last_seq_num();
+

        SNAPSHOTALLOC
 private:
        int get_execution_number() const;
        SNAPSHOTALLOC
 private:
        int get_execution_number() const;


@@ -112,7 +114,7 @@ private:
 
        bool next_execution();
        bool initialize_curr_action(ModelAction **curr);
 
        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);
        void process_write(ModelAction *curr);
        bool process_fence(ModelAction *curr);
        bool process_mutex(ModelAction *curr);

diff --git a/fuzzer.h b/fuzzer.h
index 348225c8f60184d90701b63df36767761bf0129e..29d31edaac7456412c7269c3c6a891ee895b5697 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;
        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);
        Thread * selectNotify(action_list_t * waiters);
        bool shouldSleep(const ModelAction *sleep);
        bool shouldWake(const ModelAction *sleep);

diff --git a/newfuzzer.cc b/newfuzzer.cc
index e09175ce227ce1e17f87204ad08a686c743e1d1b..68efd37d437a47d4a6ad064f90d67d4f0f181719 100644 (file)
--- a/newfuzzer.cc
+++ b/newfuzzer.cc
@@ -4,12 +4,14 @@
 #include "action.h"
 #include "execution.h"
 #include "funcnode.h"
 #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(),
 
 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 ) {
        // 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] );
                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);
        }
 
        ASSERT(rf_set->size() != 0);


@@ -186,3 +200,46 @@ bool NewFuzzer::prune_writes(thread_id_t tid, Predicate * pred,
 
        return pruned;
 }
 
        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)++;
+}

diff --git a/newfuzzer.h b/newfuzzer.h
index c956935e8cef70b354302e83449722148a34bc31..7de4cd7696f5afdeea7404df697c140018edda9e 100644 (file)
--- a/newfuzzer.h
+++ b/newfuzzer.h
@@ -12,9 +12,10 @@ class NewFuzzer : public Fuzzer {
 public:
        NewFuzzer();
        int selectWrite(ModelAction *read, SnapVector<ModelAction *>* rf_set);
 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);
        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);
 
        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;
        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__ */
 };
 
 #endif /* end of __NEWFUZZER_H__ */

diff --git a/schedule.cc b/schedule.cc
index cb97d5bdba2efdbd95f44e1d4a355f9499140826..4a9752a761ee105472e79543ec0fd89fbdd2f114 100644 (file)
--- a/schedule.cc
+++ b/schedule.cc
@@ -208,8 +208,8 @@ Thread * Scheduler::select_next_thread()
                        thread_list[avail_threads++] = i;
        }
 
                        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());
 
        Thread * thread = execution->getFuzzer()->selectThread(thread_list, avail_threads);
        curr_thread_index = id_to_int(thread->get_id());