Version that finds the bug of iris

diff --git a/cmodelint.cc b/cmodelint.cc
index 3c59fa01a68277cdbb74fc0a6af55698530b1b9a..8774c5b3f6a0124cbc3079d7de5bfcee79b5505d 100644 (file)
--- a/cmodelint.cc
+++ b/cmodelint.cc
@@ -335,6 +335,7 @@ void cds_atomic_thread_fence(int atomic_index, const char * position) {
 
 void cds_func_entry(const char * funcName) {
        ensureModel();
 
 void cds_func_entry(const char * funcName) {
        ensureModel();

+       /*

        Thread * th = thread_current();
        uint32_t func_id;
 
        Thread * th = thread_current();
        uint32_t func_id;
 


@@ -355,22 +356,25 @@ void cds_func_entry(const char * funcName) {
        }
 
        history->enter_function(func_id, th->get_id());
        }
 
        history->enter_function(func_id, th->get_id());

+*/

 }
 
 void cds_func_exit(const char * funcName) {
        ensureModel();
 }
 
 void cds_func_exit(const char * funcName) {
        ensureModel();

-       Thread * th = thread_current();
+
+/*     Thread * th = thread_current();

        uint32_t func_id;
 
        ModelHistory *history = model->get_history();
        func_id = history->getFuncMap()->get(funcName);
 
        uint32_t func_id;
 
        ModelHistory *history = model->get_history();
        func_id = history->getFuncMap()->get(funcName);
 

-       /* func_id not found; this could happen in the case where a function calls cds_func_entry
+        * func_id not found; this could happen in the case where a function calls cds_func_entry

         * when the model has been defined yet, but then an atomic inside the function initializes
         * the model. And then cds_func_exit is called upon the function exiting.
         * when the model has been defined yet, but then an atomic inside the function initializes
         * the model. And then cds_func_exit is called upon the function exiting.

-        */
+        *

        if (func_id == 0)
                return;
 
        history->exit_function(func_id, th->get_id());
        if (func_id == 0)
                return;
 
        history->exit_function(func_id, th->get_id());

+*/

 }
 }

diff --git a/execution.cc b/execution.cc
index 5449c4802170680346b714c30df0d52b8cf3ffaf..606b9642ebb6ba39bc50581df6c86f6d70bd61af 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -282,7 +282,7 @@ ModelAction * ModelExecution::convertNonAtomicStore(void * location) {
        add_normal_write_to_lists(act);
        add_write_to_lists(act);
        w_modification_order(act);
        add_normal_write_to_lists(act);
        add_write_to_lists(act);
        w_modification_order(act);

-       model->get_history()->process_action(act, act->get_tid());
+//     model->get_history()->process_action(act, act->get_tid());

        return act;
 }
 
        return act;
 }
 


@@ -302,13 +302,14 @@ bool ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> *
        }
 
        // Remove writes that violate read modification order
        }
 
        // Remove writes that violate read modification order

+       /*

        for (uint i = 0; i < rf_set->size(); i++) {
                ModelAction * rf = (*rf_set)[i];
                if (!r_modification_order(curr, rf, NULL, NULL, true)) {
                        (*rf_set)[i] = rf_set->back();
                        rf_set->pop_back();
                }
        for (uint i = 0; i < rf_set->size(); i++) {
                ModelAction * rf = (*rf_set)[i];
                if (!r_modification_order(curr, rf, NULL, NULL, true)) {
                        (*rf_set)[i] = rf_set->back();
                        rf_set->pop_back();
                }

-       }
+       }*/

 
        while(true) {
                int index = fuzzer->selectWrite(curr, rf_set);
 
        while(true) {
                int index = fuzzer->selectWrite(curr, rf_set);


@@ -1757,7 +1758,7 @@ Thread * ModelExecution::take_step(ModelAction *curr)
        ASSERT(curr);
 
        /* Process this action in ModelHistory for records */
        ASSERT(curr);
 
        /* Process this action in ModelHistory for records */

-       model->get_history()->process_action( curr, curr->get_tid() );
+//     model->get_history()->process_action( curr, curr->get_tid() );

 
        if (curr_thrd->is_blocked() || curr_thrd->is_complete())
                scheduler->remove_thread(curr_thrd);
 
        if (curr_thrd->is_blocked() || curr_thrd->is_complete())
                scheduler->remove_thread(curr_thrd);

diff --git a/newfuzzer.cc b/newfuzzer.cc
index 9d061bbf9a857d41938bb7394d00d18e4bffed1b..e76d8961e47d3357360be5ee09270e4b0d75f01e 100644 (file)
--- a/newfuzzer.cc
+++ b/newfuzzer.cc
@@ -33,7 +33,7 @@ void NewFuzzer::register_engine(ModelHistory * history, ModelExecution *executio
 
 int NewFuzzer::selectWrite(ModelAction *read, SnapVector<ModelAction *> * rf_set)
 {
 
 int NewFuzzer::selectWrite(ModelAction *read, SnapVector<ModelAction *> * rf_set)
 {

-//     return random() % rf_set->size();
+       return random() % rf_set->size();

 
        thread_id_t tid = read->get_tid();
        int thread_id = id_to_int(tid);
 
        thread_id_t tid = read->get_tid();
        int thread_id = id_to_int(tid);


@@ -67,35 +67,6 @@ int NewFuzzer::selectWrite(ModelAction *read, SnapVector<ModelAction *> * rf_set
 
                //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());
 
 
                //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());
 

-/*--
-               Thread * read_thread = execution->get_thread(tid);
-               bool should_reselect_predicate = true;
-               bool should_sleep = should_conditional_sleep(selected_branch);
-               dist_info_vec.clear();
-
-               if (!find_threads(read)) {
-                       update_predicate_score(selected_branch, SLEEP_FAIL_TYPE1);
-                       should_reselect_predicate = true;
-               } else if (!should_sleep) {
-                       update_predicate_score(selected_branch, SLEEP_FAIL_TYPE2);
-                       should_reselect_predicate = true;
-               } else {
-                       for (uint i = 0; i < dist_info_vec.size(); i++) {
-                               struct node_dist_info info = dist_info_vec[i];
-                               history->add_waiting_thread(tid, info.tid, info.target, info.dist);
-                       }
-
-                       // 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;      
-               }
-*/
-

                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] );


@@ -182,11 +153,6 @@ Predicate * NewFuzzer::selectBranch(thread_id_t tid, Predicate * curr_pred, Func
                Predicate * child = (*children)[i];
                if (child->get_func_inst() == read_inst && !failed_predicates.contains(child)) {
                        branches.push_back(child);
                Predicate * child = (*children)[i];
                if (child->get_func_inst() == read_inst && !failed_predicates.contains(child)) {
                        branches.push_back(child);

-
-                       /*-- max of (exploration counts + 1)
-                       if (child->get_expl_count() + 1 > numerator)
-                               numerator = child->get_expl_count() + 1;
-                       */

                }
        }
 
                }
        }
 

diff --git a/newfuzzer.h b/newfuzzer.h
index ea08b74171a3fcae302679aad8182cccc8d05bd0..63d88de7318dd96cdce6c9e10ac781e9294f54d9 100644 (file)
--- a/newfuzzer.h
+++ b/newfuzzer.h
@@ -55,17 +55,17 @@ private:
 
        /* The set of Threads put to sleep by NewFuzzer because no writes in rf_set satisfies the selected predicate. Only used by selectWrite.
         */
 
        /* The set of Threads put to sleep by NewFuzzer because no writes in rf_set satisfies the selected predicate. Only used by selectWrite.
         */

-       SnapVector<Thread *> paused_thread_list;
-       HashTable<Thread *, int, uintptr_t, 0> paused_thread_table;
+       SnapVector<Thread *> paused_thread_list;        //-- (not in use)
+       HashTable<Thread *, int, uintptr_t, 0> paused_thread_table;     //--

        HashTable<Predicate *, bool, uintptr_t, 0> failed_predicates;
 
        HashTable<Predicate *, bool, uintptr_t, 0> failed_predicates;
 

-       SnapVector<struct node_dist_info> dist_info_vec;
+       SnapVector<struct node_dist_info> dist_info_vec;        //--

 
 

-       void conditional_sleep(Thread * thread);
+       void conditional_sleep(Thread * thread);        //--

        bool should_conditional_sleep(Predicate * predicate);
        bool should_conditional_sleep(Predicate * predicate);

-       void wake_up_paused_threads(int * threadlist, int * numthreads);
+       void wake_up_paused_threads(int * threadlist, int * numthreads);        //--

 
 

-       bool find_threads(ModelAction * pending_read);
+       bool find_threads(ModelAction * pending_read);  //--

        /*-- void update_predicate_score(Predicate * predicate, sleep_result_t type); */
 
        bool check_predicate_expressions(PredExprSet * pred_expressions, inst_act_map_t * inst_act_map, uint64_t write_val, bool * no_predicate);
        /*-- void update_predicate_score(Predicate * predicate, sleep_result_t type); */
 
        bool check_predicate_expressions(PredExprSet * pred_expressions, inst_act_map_t * inst_act_map, uint64_t write_val, bool * no_predicate);