X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=execution.cc;h=01125bb2b0910b7e64fa3933afed1f1693e01c2a;hp=e0d49808f2bd14844a5cd9d72f916b1af55c13c7;hb=729acbffd2562f10dd1864b010c3623faa485513;hpb=ba484ecdbd0285d264e70ec6d9c0f3fab57b626f diff --git a/execution.cc b/execution.cc index e0d49808..01125bb2 100644 --- a/execution.cc +++ b/execution.cc @@ -27,7 +27,6 @@ struct model_snapshot_members { next_thread_id(INITIAL_THREAD_ID), used_sequence_numbers(0), bugs(), - dataraces(), bad_synchronization(false), asserted(false) { } @@ -35,16 +34,12 @@ struct model_snapshot_members { ~model_snapshot_members() { for (unsigned int i = 0;i < bugs.size();i++) delete bugs[i]; - for (unsigned int i = 0;i < dataraces.size(); i++) - delete dataraces[i]; bugs.clear(); - dataraces.clear(); } unsigned int next_thread_id; modelclock_t used_sequence_numbers; SnapVector bugs; - SnapVector dataraces; /** @brief Incorrectly-ordered synchronization was made */ bool bad_synchronization; bool asserted; @@ -190,22 +185,6 @@ bool ModelExecution::assert_bug(const char *msg) return false; } -/* @brief Put data races in a different list from other bugs. The purpose - * is to continue the program untill the number of data races exceeds a - * threshold */ - -/* TODO: check whether set_assert should be called */ -bool ModelExecution::assert_race(const char *msg) -{ - priv->dataraces.push_back(new bug_message(msg)); - - if (isfeasibleprefix()) { - set_assert(); - return true; - } - return false; -} - /** @return True, if any bugs have been reported for this execution */ bool ModelExecution::have_bug_reports() const { @@ -213,13 +192,13 @@ bool ModelExecution::have_bug_reports() const } /** @return True, if any fatal bugs have been reported for this execution. - * Any bug other than a data race is considered a fatal bug. Data races + * Any bug other than a data race is considered a fatal bug. Data races * are not considered fatal unless the number of races is exceeds - * a threshold (temporarily set as 15). + * a threshold (temporarily set as 15). */ bool ModelExecution::have_fatal_bug_reports() const { - return priv->bugs.size() != 0 || priv->dataraces.size() >= 15; + return priv->bugs.size() != 0; } SnapVector * ModelExecution::get_bugs() const @@ -284,6 +263,19 @@ bool ModelExecution::is_complete_execution() const return true; } +ModelAction * ModelExecution::convertNonAtomicStore(void * location) { + uint64_t value = *((const uint64_t *) location); + modelclock_t storeclock; + thread_id_t storethread; + getStoreThreadAndClock(location, &storethread, &storeclock); + setAtomicStoreFlag(location); + ModelAction * act = new ModelAction(NONATOMIC_WRITE, memory_order_relaxed, location, value, get_thread(storethread)); + act->set_seq_number(storeclock); + add_normal_write_to_lists(act); + add_write_to_lists(act); + w_modification_order(act); + return act; +} /** * Processes a read model action. @@ -294,8 +286,13 @@ bool ModelExecution::is_complete_execution() const void ModelExecution::process_read(ModelAction *curr, SnapVector * rf_set) { SnapVector * priorset = new SnapVector(); - while(true) { + bool hasnonatomicstore = hasNonAtomicStore(curr->get_location()); + if (hasnonatomicstore) { + ModelAction * nonatomicstore = convertNonAtomicStore(curr->get_location()); + rf_set->push_back(nonatomicstore); + } + while(true) { int index = fuzzer->selectWrite(curr, rf_set); ModelAction *rf = (*rf_set)[index]; @@ -1142,6 +1139,70 @@ void ModelExecution::add_action_to_lists(ModelAction *act) } } +void insertIntoActionList(action_list_t *list, ModelAction *act) { + action_list_t::reverse_iterator rit = list->rbegin(); + modelclock_t next_seq = act->get_seq_number(); + if (rit == list->rend() || (*rit)->get_seq_number() == next_seq) + list->push_back(act); + else { + for(;rit != list->rend();rit++) { + if ((*rit)->get_seq_number() == next_seq) { + action_list_t::iterator it = rit.base(); + list->insert(it, act); + break; + } + } + } +} + +void insertIntoActionListAndSetCV(action_list_t *list, ModelAction *act) { + action_list_t::reverse_iterator rit = list->rbegin(); + modelclock_t next_seq = act->get_seq_number(); + if (rit == list->rend()) { + act->create_cv(NULL); + } else if ((*rit)->get_seq_number() == next_seq) { + act->create_cv((*rit)); + list->push_back(act); + } else { + for(;rit != list->rend();rit++) { + if ((*rit)->get_seq_number() == next_seq) { + act->create_cv((*rit)); + action_list_t::iterator it = rit.base(); + list->insert(it, act); + break; + } + } + } +} + +/** + * Performs various bookkeeping operations for a normal write. The + * complication is that we are typically inserting a normal write + * lazily, so we need to insert it into the middle of lists. + * + * @param act is the ModelAction to add. + */ + +void ModelExecution::add_normal_write_to_lists(ModelAction *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 *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location()); + if (tid >= (int)vec->size()) + vec->resize(priv->next_thread_id); + insertIntoActionList(&(*vec)[tid],act); + + // Update thrd_last_action, the last action taken by each thrad + if (thrd_last_action[tid]->get_seq_number() == act->get_seq_number()) + thrd_last_action[tid] = act; +} + + void ModelExecution::add_write_to_lists(ModelAction *write) { // Update seq_cst map if (write->is_seqcst()) @@ -1569,8 +1630,8 @@ Thread * ModelExecution::take_step(ModelAction *curr) curr = check_current_action(curr); ASSERT(curr); - // model_print("poitner loc: %p, thread: %d, type: %d, order: %d, position: %s\n", curr, curr->get_tid(), curr->get_type(), curr->get_mo(), curr->get_position() ); - model->get_history()->add_func_atomic( curr, curr_thrd->get_id() ); + /* Process this action in ModelHistory for records*/ + model->get_history()->process_action( curr, curr->get_tid() ); if (curr_thrd->is_blocked() || curr_thrd->is_complete()) scheduler->remove_thread(curr_thrd);