/* 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 */
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;
/* 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);
}
}
}
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;
}
}
// 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);
*
* @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 Only check if the current action satisfies read
- * modification order or not, without modifiying priorsetand canprune
+ * @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 check_only)
+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;
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);