Select a new predicate branch when the selected branch in the predicate tree fails...

diff --git a/newfuzzer.cc b/newfuzzer.cc
index 6810d022a990fc6f50765a653b21ce2de5bc2745..02666ed85ed88486f1a1cb6bfef6443cbcfdb7bc 100644 (file)
--- a/newfuzzer.cc
+++ b/newfuzzer.cc
@@ -14,11 +14,12 @@
 
 NewFuzzer::NewFuzzer() :
        thrd_last_read_act(),
-       thrd_curr_pred(),
+       thrd_last_func_inst(),
        thrd_selected_child_branch(),
        thrd_pruned_writes(),
        paused_thread_list(),
-       paused_thread_table(128)
+       paused_thread_table(128),
+       failed_predicates(32)
 {}
 
 /**
@@ -37,13 +38,13 @@ int NewFuzzer::selectWrite(ModelAction *read, SnapVector<ModelAction *> * rf_set
        thread_id_t tid = read->get_tid();
        int thread_id = id_to_int(tid);
 
-       if (thrd_last_read_act.size() <= (uint) thread_id)
+       if (thrd_last_read_act.size() <= (uint) thread_id) {
                thrd_last_read_act.resize(thread_id + 1);
+               thrd_last_func_inst.resize(thread_id + 1);
+       }
 
        // A new read action is encountered, select a random child branch of current predicate
        if (read != thrd_last_read_act[thread_id]) {
-               thrd_last_read_act[thread_id] = read;
-
                FuncNode * func_node = history->get_curr_func_node(tid);
                Predicate * curr_pred = func_node->get_predicate_tree_position(tid);
                FuncInst * read_inst = func_node->get_inst(read);
@@ -51,27 +52,49 @@ int NewFuzzer::selectWrite(ModelAction *read, SnapVector<ModelAction *> * rf_set
 
                inst_act_map_t * inst_act_map = func_node->get_inst_act_map(tid);
                prune_writes(tid, selected_branch, rf_set, inst_act_map);
+
+               if (!failed_predicates.isEmpty())
+                       failed_predicates.reset();
+
+               thrd_last_read_act[thread_id] = read;
+               thrd_last_func_inst[thread_id] = read_inst;
        }
 
        // No write satisfies the selected predicate, so pause this thread.
-       if ( rf_set->size() == 0 ) {
+       while ( rf_set->size() == 0 ) {
                Thread * read_thread = execution->get_thread(tid);
                model_print("the %d read action of thread %d at %p is unsuccessful\n", read->get_seq_number(), read_thread->get_id(), read->get_location());
 
-               // reset thread pending action and revert sequence numbers
-               read_thread->set_pending(read);
-               read->reset_seq_number();
-               execution->restore_last_seq_num();
+               if (find_threads(read)) {
+                       // reset thread pending action and revert sequence numbers
+                       read_thread->set_pending(read);
+                       read->reset_seq_number();
+                       execution->restore_last_seq_num();
+
+                       conditional_sleep(read_thread);
+
+                       // Returning -1 stops the while loop of ModelExecution::process_read
+                       return -1;
+               } else {
+                       Predicate * selected_branch = get_selected_child_branch(tid);
+                       failed_predicates.put(selected_branch, true);
+
+                       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] );
+                       }
+
+                       // Reselect a predicate and prune writes
+                       Predicate * curr_pred = selected_branch->get_parent();
+                       FuncInst * read_inst = thrd_last_func_inst[thread_id];
+                       selected_branch = selectBranch(tid, curr_pred, read_inst);
 
-               conditional_sleep(read_thread);
+                       FuncNode * func_node = history->get_curr_func_node(tid);
+                       inst_act_map_t * inst_act_map = func_node->get_inst_act_map(tid);
+                       prune_writes(tid, selected_branch, rf_set, inst_act_map);
 
-               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(selected_branch);
+               }
        }
 
        ASSERT(rf_set->size() != 0);
@@ -99,8 +122,9 @@ Predicate * NewFuzzer::selectBranch(thread_id_t tid, Predicate * curr_pred, Func
 
        for (uint i = 0; i < children->size(); i++) {
                Predicate * child = (*children)[i];
-               if (child->get_func_inst() == read_inst)
+               if (child->get_func_inst() == read_inst && !failed_predicates.contains(child)) {
                        branches.push_back(child);
+               }
        }
 
        // predicate children have not been generated
@@ -227,9 +251,7 @@ void NewFuzzer::conditional_sleep(Thread * thread)
        concrete->set_location(read->get_location());
 
        history->add_waiting_write(concrete);
-
-       /* history->add_waiting_thread is called in find_threads */
-       find_threads(read);
+       /* history->add_waiting_thread is already called in find_threads */
 }
 
 bool NewFuzzer::has_paused_threads()
@@ -247,7 +269,7 @@ Thread * NewFuzzer::selectThread(int * threadlist, int numthreads)
        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);
+       return execution->get_thread(curr_tid);
 }
 
 /* Force waking up one of threads paused by Fuzzer, because otherwise
@@ -293,13 +315,16 @@ void NewFuzzer::notify_paused_thread(Thread * thread)
        history->remove_waiting_thread(tid);
 }
 
-/* Find threads that may write values that the pending read action is waiting for */
-void NewFuzzer::find_threads(ModelAction * pending_read)
+/* Find threads that may write values that the pending read action is waiting for
+ * @return True if any thread is found
+ */
+bool NewFuzzer::find_threads(ModelAction * pending_read)
 {
        ASSERT(pending_read->is_read());
 
        void * location = pending_read->get_location();
        thread_id_t self_id = pending_read->get_tid();
+       bool finds_waiting_for = false;
 
        SnapVector<FuncNode *> * func_node_list = history->getWrFuncNodes(location);
        for (uint i = 0; i < func_node_list->size(); i++) {
@@ -317,12 +342,13 @@ void NewFuzzer::find_threads(ModelAction * pending_read)
                        int distance = node->compute_distance(target_node);
                        if (distance != -1) {
                                history->add_waiting_thread(self_id, tid, target_node, distance);
+                               finds_waiting_for = true;
                                model_print("thread: %d; distance from node %d to node %d: %d\n", tid, node->get_func_id(), target_node->get_func_id(), distance);
-
                        }
-
                }
        }
+
+       return finds_waiting_for;
 }
 
 bool NewFuzzer::shouldWait(const ModelAction * act)

diff --git a/newfuzzer.h b/newfuzzer.h
index 6ce1e7f43eaddbe5d3422a70bb4dbefb3cdb2faf..d1037a61f5481378c46d5f317d0c071ba7afdb82 100644 (file)
--- a/newfuzzer.h
+++ b/newfuzzer.h
@@ -28,7 +28,8 @@ private:
        ModelExecution * execution;
 
        SnapVector<ModelAction *> thrd_last_read_act;
-       SnapVector<Predicate *> thrd_curr_pred;
+       SnapVector<FuncInst *> thrd_last_func_inst;
+
        SnapVector<Predicate *> thrd_selected_child_branch;
        SnapVector< SnapVector<ModelAction *> *> thrd_pruned_writes;
 
@@ -39,11 +40,12 @@ private:
         */
        SnapVector<Thread *> paused_thread_list;
        HashTable<Thread *, int, uintptr_t, 0> paused_thread_table;
+       HashTable<Predicate *, bool, uintptr_t, 0> failed_predicates;
 
        void conditional_sleep(Thread * thread);
        void wake_up_paused_threads(int * threadlist, int * numthreads);
 
-       void find_threads(ModelAction * pending_read);
+       bool find_threads(ModelAction * pending_read);
 };
 
 #endif /* end of __NEWFUZZER_H__ */

diff --git a/waitobj.cc b/waitobj.cc
index 692f0203fb2e1577c4b49efeefc78a64b4aefabc..39b47afc42e6a2fbc4889e2649406f19669a2b34 100644 (file)
--- a/waitobj.cc
+++ b/waitobj.cc
@@ -2,6 +2,8 @@
 #include "threads-model.h"
 #include "funcnode.h"
 
+#define COUNTER_THRESHOLD 1000
+
 WaitObj::WaitObj(thread_id_t tid) :
        tid(tid),
        waiting_for(32),
@@ -142,8 +144,10 @@ bool WaitObj::incr_counter(thread_id_t tid)
        }
 
        thrd_action_counters[thread_id]++;
-       if (thrd_action_counters[thread_id] > 1000)
+       if (thrd_action_counters[thread_id] > COUNTER_THRESHOLD) {
+               thrd_action_counters[thread_id] = 0;
                return true;
+       }
 
        return false;
 }