Version that finds the bug of iris

[c11tester.git] / execution.cc

diff --git a/execution.cc b/execution.cc
index 870dcb1a9d06bd25614e4d872f6e6c9ae80045a4..606b9642ebb6ba39bc50581df6c86f6d70bd61af 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -73,8 +73,8 @@ ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) :
        /* Initialize a model-checker thread, for special ModelActions */
        model_thread = new Thread(get_next_id());
        add_thread(model_thread);
-       scheduler->register_engine(this);
        fuzzer->register_engine(m->get_history(), this);
+       scheduler->register_engine(this);
 }
 
 /** @brief Destructor */
@@ -161,6 +161,7 @@ bool ModelExecution::should_wake_up(const ModelAction *curr, const Thread *threa
                if (fence_release && *(get_last_action(thread->get_id())) < *fence_release)
                        return true;
        }
+       /* The sleep is literally sleeping */
        if (asleep->is_sleep()) {
                if (fuzzer->shouldWake(asleep))
                        return true;
@@ -178,7 +179,7 @@ void ModelExecution::wake_up_sleeping_actions(ModelAction *curr)
                                /* Remove this thread from sleep set */
                                scheduler->remove_sleep(thr);
                                if (thr->get_pending()->is_sleep())
-                                       thr->set_pending(NULL);
+                                       thr->set_wakeup_state(true);
                        }
                }
        }
@@ -281,7 +282,7 @@ ModelAction * ModelExecution::convertNonAtomicStore(void * location) {
        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;
 }
 
@@ -300,6 +301,16 @@ bool ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> *
                rf_set->push_back(nonatomicstore);
        }
 
+       // 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();
+               }
+       }*/
+
        while(true) {
                int index = fuzzer->selectWrite(curr, rf_set);
                if (index == -1)        // no feasible write exists
@@ -812,10 +823,14 @@ ModelAction * ModelExecution::process_rmw(ModelAction *act) {
  *
  * @param curr The current action. Must be a read.
  * @param rf The ModelAction or Promise that curr reads from. Must be a write.
+ * @param check_only If true, then only check whether the current action satisfies
+ *        read modification order or not, without modifiying priorset and canprune.
+ *        False by default.
  * @return True if modification order edges were added; false otherwise
  */
 
-bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf, SnapVector<const ModelAction *> * priorset, bool * canprune)
+bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf,
+       SnapVector<const ModelAction *> * priorset, bool * canprune, bool check_only)
 {
        SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
        unsigned int i;
@@ -868,7 +883,8 @@ bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *
                                                *act < *last_sc_fence_thread_local) {
                                        if (mo_graph->checkReachable(rf, act))
                                                return false;
-                                       priorset->push_back(act);
+                                       if (!check_only)
+                                               priorset->push_back(act);
                                        break;
                                }
                                /* C++, Section 29.3 statement 4 */
@@ -876,7 +892,8 @@ bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *
                                                                 *act < *last_sc_fence_local) {
                                        if (mo_graph->checkReachable(rf, act))
                                                return false;
-                                       priorset->push_back(act);
+                                       if (!check_only)
+                                               priorset->push_back(act);
                                        break;
                                }
                                /* C++, Section 29.3 statement 6 */
@@ -884,7 +901,8 @@ bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *
                                                                 *act < *last_sc_fence_thread_before) {
                                        if (mo_graph->checkReachable(rf, act))
                                                return false;
-                                       priorset->push_back(act);
+                                       if (!check_only)
+                                               priorset->push_back(act);
                                        break;
                                }
                        }
@@ -903,17 +921,20 @@ bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *
                                if (act->is_write()) {
                                        if (mo_graph->checkReachable(rf, act))
                                                return false;
-                                       priorset->push_back(act);
+                                       if (!check_only)
+                                               priorset->push_back(act);
                                } else {
                                        const ModelAction *prevrf = act->get_reads_from();
                                        if (!prevrf->equals(rf)) {
                                                if (mo_graph->checkReachable(rf, prevrf))
                                                        return false;
-                                               priorset->push_back(prevrf);
+                                               if (!check_only)
+                                                       priorset->push_back(prevrf);
                                        } else {
                                                if (act->get_tid() == curr->get_tid()) {
                                                        //Can prune curr from obj list
-                                                       *canprune = true;
+                                                       if (!check_only)
+                                                               *canprune = true;
                                                }
                                        }
                                }
@@ -1737,7 +1758,7 @@ Thread * ModelExecution::take_step(ModelAction *curr)
        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);