priv(new struct model_snapshot_members ()),
mo_graph(new CycleGraph()),
fuzzer(new NewFuzzer()),
- thrd_func_list(),
- thrd_func_act_lists(),
isfinished(false)
{
/* Initialize a model-checker thread, for special ModelActions */
add_thread(model_thread);
fuzzer->register_engine(m->get_history(), this);
scheduler->register_engine(this);
+#ifdef TLS
+ pthread_key_create(&pthreadkey, tlsdestructor);
+#endif
}
/** @brief Destructor */
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();
- }
- }*/
+ uint i = 0;
+ while (i < rf_set->size()) {
+ ModelAction * rf = (*rf_set)[i];
+ if (!r_modification_order(curr, rf, NULL, NULL, true)) {
+ (*rf_set)[i] = rf_set->back();
+ rf_set->pop_back();
+ } else
+ i++;
+ }
while(true) {
int index = fuzzer->selectWrite(curr, rf_set);
- if (index == -1)// no feasible write exists
- return false;
ModelAction *rf = (*rf_set)[index];
}
return true;
}
+
+ ASSERT(false);
+ /* TODO: Following code not needed anymore */
priorset->clear();
(*rf_set)[index] = rf_set->back();
rf_set->pop_back();
if (curr->is_read() && !second_part_of_rmw) {
process_read(curr, rf_set);
delete rf_set;
-
-/* bool success = process_read(curr, rf_set);
- delete rf_set;
- if (!success)
- return curr; // Do not add action to lists
- */
} else
ASSERT(rf_set == NULL);
int tid = id_to_int(act->get_tid());
ModelAction *uninit = NULL;
int uninit_id = -1;
- action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
- if (list->empty() && act->is_atomic_var()) {
+ SnapVector<action_list_t> *objvec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
+ if (objvec->empty() && act->is_atomic_var()) {
uninit = get_uninitialized_action(act);
uninit_id = id_to_int(uninit->get_tid());
- list->push_front(uninit);
SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, act->get_location());
if ((int)vec->size() <= uninit_id) {
int oldsize = (int) vec->size();
void ModelExecution::add_action_to_lists(ModelAction *act)
{
int tid = id_to_int(act->get_tid());
- action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
- list->push_back(act);
+ if ((act->is_fence() && act->is_seqcst()) || act->is_unlock()) {
+ action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
+ list->push_back(act);
+ }
// Update action trace, a total order of all actions
action_trace.push_back(act);
int tid = id_to_int(act->get_tid());
insertIntoActionListAndSetCV(&action_trace, act);
- action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
- insertIntoActionList(list, act);
-
// Update obj_thrd_map, a per location, per thread, order of actions
SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
if (tid >= (int)vec->size()) {
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);