X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=execution.cc;h=c6962bc07aeeea50c693c02c78a3aaf5ed3fbe84;hp=c07db8e9a7d21a555c789a3053c6bcb2b3846491;hb=a46421375ee025acad83cf7cd612902d486987cb;hpb=4ba296a6fe70c95fefa999b0dd488a95070ac6f4 diff --git a/execution.cc b/execution.cc index c07db8e9..c6962bc0 100644 --- a/execution.cc +++ b/execution.cc @@ -66,7 +66,8 @@ ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) : mo_graph(new CycleGraph()), fuzzer(new Fuzzer()), thrd_func_list(), - thrd_func_inst_lists() + thrd_func_act_lists(), + isfinished(false) { /* Initialize a model-checker thread, for special ModelActions */ model_thread = new Thread(get_next_id()); @@ -152,6 +153,11 @@ bool ModelExecution::should_wake_up(const ModelAction *curr, const Thread *threa if (fence_release && *(get_last_action(thread->get_id())) < *fence_release) return true; } + if (asleep->is_sleep()) { + if (fuzzer->shouldWake(asleep)) + return true; + } + return false; } @@ -274,10 +280,10 @@ 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()); return act; } - /** * Processes a read model action. * @param curr is the read model action to process. @@ -390,8 +396,8 @@ bool ModelExecution::process_mutex(ModelAction *curr) case ATOMIC_NOTIFY_ALL: { action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location()); //activate all the waiting threads - for (action_list_t::iterator rit = waiters->begin();rit != waiters->end();rit++) { - scheduler->wake(get_thread(*rit)); + for (sllnode * rit = waiters->begin();rit != NULL;rit=rit->getNext()) { + scheduler->wake(get_thread(rit->getVal())); } waiters->clear(); break; @@ -440,10 +446,10 @@ bool ModelExecution::process_fence(ModelAction *curr) bool updated = false; if (curr->is_acquire()) { action_list_t *list = &action_trace; - action_list_t::reverse_iterator rit; + sllnode * rit; /* Find X : is_read(X) && X --sb-> curr */ - for (rit = list->rbegin();rit != list->rend();rit++) { - ModelAction *act = *rit; + for (rit = list->end();rit != NULL;rit=rit->getPrev()) { + ModelAction *act = rit->getVal(); if (act == curr) continue; if (act->get_tid() != curr->get_tid()) @@ -480,10 +486,8 @@ bool ModelExecution::process_fence(ModelAction *curr) * @param curr The current action * @return True if synchronization was updated or a thread completed */ -bool ModelExecution::process_thread_action(ModelAction *curr) +void ModelExecution::process_thread_action(ModelAction *curr) { - bool updated = false; - switch (curr->get_type()) { case THREAD_CREATE: { thrd_t *thrd = (thrd_t *)curr->get_location(); @@ -513,19 +517,25 @@ bool ModelExecution::process_thread_action(ModelAction *curr) Thread *blocking = curr->get_thread_operand(); ModelAction *act = get_last_action(blocking->get_id()); synchronize(act, curr); - updated = true; /* trigger rel-seq checks */ break; } case PTHREAD_JOIN: { Thread *blocking = curr->get_thread_operand(); ModelAction *act = get_last_action(blocking->get_id()); synchronize(act, curr); - updated = true; /* trigger rel-seq checks */ break; // WL: to be add (modified) } + case THREADONLY_FINISH: case THREAD_FINISH: { Thread *th = get_thread(curr); + if (curr->get_type() == THREAD_FINISH && + th == model->getInitThread()) { + th->complete(); + setFinished(); + break; + } + /* Wake up any joining threads */ for (unsigned int i = 0;i < get_num_threads();i++) { Thread *waiting = get_thread(int_to_id(i)); @@ -534,7 +544,6 @@ bool ModelExecution::process_thread_action(ModelAction *curr) scheduler->wake(waiting); } th->complete(); - updated = true; /* trigger rel-seq checks */ break; } case THREAD_START: { @@ -543,8 +552,6 @@ bool ModelExecution::process_thread_action(ModelAction *curr) default: break; } - - return updated; } /** @@ -649,6 +656,9 @@ bool ModelExecution::check_action_enabled(ModelAction *curr) { if (!blocking->is_complete()) { return false; } + } else if (curr->is_sleep()) { + if (!fuzzer->shouldSleep(curr)) + return false; } return true; @@ -803,9 +813,9 @@ bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction * /* Iterate over actions in thread, starting from most recent */ action_list_t *list = &(*thrd_lists)[tid]; - action_list_t::reverse_iterator rit; - for (rit = list->rbegin();rit != list->rend();rit++) { - ModelAction *act = *rit; + sllnode * rit; + for (rit = list->end();rit != NULL;rit=rit->getPrev()) { + ModelAction *act = rit->getVal(); /* Skip curr */ if (act == curr) @@ -919,6 +929,8 @@ void ModelExecution::w_modification_order(ModelAction *curr) if (last_seq_cst != NULL) { edgeset.push_back(last_seq_cst); } + //update map for next query + obj_last_sc_map.put(curr->get_location(), curr); } /* Last SC fence in the current thread */ @@ -933,9 +945,9 @@ void ModelExecution::w_modification_order(ModelAction *curr) /* Iterate over actions in thread, starting from most recent */ action_list_t *list = &(*thrd_lists)[i]; - action_list_t::reverse_iterator rit; - for (rit = list->rbegin();rit != list->rend();rit++) { - ModelAction *act = *rit; + sllnode* rit; + for (rit = list->end();rit != NULL;rit=rit->getPrev()) { + ModelAction *act = rit->getVal(); if (act == curr) { /* * 1) If RMW and it actually read from something, then we @@ -1007,9 +1019,9 @@ bool ModelExecution::mo_may_allow(const ModelAction *writer, const ModelAction * /* Iterate over actions in thread, starting from most recent */ action_list_t *list = &(*thrd_lists)[i]; - action_list_t::reverse_iterator rit; - for (rit = list->rbegin();rit != list->rend();rit++) { - ModelAction *act = *rit; + sllnode* rit; + for (rit = list->end();rit != NULL;rit=rit->getPrev()) { + ModelAction *act = rit->getVal(); /* Don't disallow due to act == reader */ if (!reader->happens_before(act) || reader == act) @@ -1098,8 +1110,13 @@ void ModelExecution::add_action_to_lists(ModelAction *act) uninit_id = id_to_int(uninit->get_tid()); list->push_front(uninit); SnapVector *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, act->get_location()); - if (uninit_id >= (int)vec->size()) + if (uninit_id >= (int)vec->size()) { + int oldsize = (int) vec->size(); vec->resize(uninit_id + 1); + for(int i=oldsize;ipush_back(act); @@ -1111,8 +1128,12 @@ void ModelExecution::add_action_to_lists(ModelAction *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()) + if (tid >= (int)vec->size()) { + uint oldsize =vec->size(); vec->resize(priv->next_thread_id); + for(uint i=oldsize;inext_thread_id;i++) + new (&(*vec)[i]) action_list_t(); + } (*vec)[tid].push_back(act); if (uninit) (*vec)[uninit_id].push_front(uninit); @@ -1136,22 +1157,25 @@ void ModelExecution::add_action_to_lists(ModelAction *act) get_safe_ptr_action(&obj_map, mutex_loc)->push_back(act); SnapVector *vec = get_safe_ptr_vect_action(&obj_thrd_map, mutex_loc); - if (tid >= (int)vec->size()) + if (tid >= (int)vec->size()) { + uint oldsize = vec->size(); vec->resize(priv->next_thread_id); + for(uint i=oldsize;inext_thread_id;i++) + new (&(*vec)[i]) action_list_t(); + } (*vec)[tid].push_back(act); } } void insertIntoActionList(action_list_t *list, ModelAction *act) { - action_list_t::reverse_iterator rit = list->rbegin(); + sllnode * rit = list->end(); modelclock_t next_seq = act->get_seq_number(); - if (rit == list->rend() || (*rit)->get_seq_number() == next_seq) + if (rit == NULL || (rit->getVal()->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); + for(;rit != NULL;rit=rit->getPrev()) { + if (rit->getVal()->get_seq_number() == next_seq) { + list->insertAfter(rit, act); break; } } @@ -1159,19 +1183,18 @@ void insertIntoActionList(action_list_t *list, ModelAction *act) { } void insertIntoActionListAndSetCV(action_list_t *list, ModelAction *act) { - action_list_t::reverse_iterator rit = list->rbegin(); + sllnode * rit = list->end(); modelclock_t next_seq = act->get_seq_number(); - if (rit == list->rend()) { + if (rit == NULL) { act->create_cv(NULL); - } else if ((*rit)->get_seq_number() == next_seq) { - act->create_cv((*rit)); + } else if (rit->getVal()->get_seq_number() == next_seq) { + act->create_cv(rit->getVal()); 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); + for(;rit != NULL;rit=rit->getPrev()) { + if (rit->getVal()->get_seq_number() == next_seq) { + act->create_cv(rit->getVal()); + list->insertAfter(rit, act); break; } } @@ -1196,8 +1219,12 @@ void ModelExecution::add_normal_write_to_lists(ModelAction *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()) + if (tid >= (int)vec->size()) { + uint oldsize =vec->size(); vec->resize(priv->next_thread_id); + for(uint i=oldsize;inext_thread_id;i++) + new (&(*vec)[i]) action_list_t(); + } insertIntoActionList(&(*vec)[tid],act); // Update thrd_last_action, the last action taken by each thrad @@ -1207,14 +1234,14 @@ void ModelExecution::add_normal_write_to_lists(ModelAction *act) void ModelExecution::add_write_to_lists(ModelAction *write) { - // Update seq_cst map - if (write->is_seqcst()) - obj_last_sc_map.put(write->get_location(), write); - SnapVector *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, write->get_location()); int tid = id_to_int(write->get_tid()); - if (tid >= (int)vec->size()) + if (tid >= (int)vec->size()) { + uint oldsize =vec->size(); vec->resize(priv->next_thread_id); + for(uint i=oldsize;inext_thread_id;i++) + new (&(*vec)[i]) action_list_t(); + } (*vec)[tid].push_back(write); } @@ -1276,20 +1303,22 @@ ModelAction * ModelExecution::get_last_seq_cst_fence(thread_id_t tid, const Mode if (!list) return NULL; - action_list_t::reverse_iterator rit = list->rbegin(); + sllnode* rit = list->end(); if (before_fence) { - for (;rit != list->rend();rit++) - if (*rit == before_fence) + for (;rit != NULL;rit=rit->getPrev()) + if (rit->getVal() == before_fence) break; - ASSERT(*rit == before_fence); - rit++; + ASSERT(rit->getVal() == before_fence); + rit=rit->getPrev(); } - for (;rit != list->rend();rit++) - if ((*rit)->is_fence() && (tid == (*rit)->get_tid()) && (*rit)->is_seqcst()) - return *rit; + for (;rit != NULL;rit=rit->getPrev()) { + ModelAction *act = rit->getVal(); + if (act->is_fence() && (tid == act->get_tid()) && act->is_seqcst()) + return act; + } return NULL; } @@ -1307,10 +1336,10 @@ ModelAction * ModelExecution::get_last_unlock(ModelAction *curr) const action_list_t *list = obj_map.get(location); /* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */ - action_list_t::reverse_iterator rit; - for (rit = list->rbegin();rit != list->rend();rit++) - if ((*rit)->is_unlock() || (*rit)->is_wait()) - return *rit; + sllnode* rit; + for (rit = list->end();rit != NULL;rit=rit->getPrev()) + if (rit->getVal()->is_unlock() || rit->getVal()->is_wait()) + return rit->getVal(); return NULL; } @@ -1373,9 +1402,9 @@ SnapVector * ModelExecution::build_may_read_from(ModelAction *cu for (i = 0;i < thrd_lists->size();i++) { /* Iterate over actions in thread, starting from most recent */ action_list_t *list = &(*thrd_lists)[i]; - action_list_t::reverse_iterator rit; - for (rit = list->rbegin();rit != list->rend();rit++) { - ModelAction *act = *rit; + sllnode * rit; + for (rit = list->end();rit != NULL;rit=rit->getPrev()) { + ModelAction *act = rit->getVal(); if (act == curr) continue; @@ -1438,9 +1467,9 @@ ModelAction * ModelExecution::get_uninitialized_action(ModelAction *curr) const return act; } -static void print_list(const action_list_t *list) +static void print_list(action_list_t *list) { - action_list_t::const_iterator it; + sllnode *it; model_print("------------------------------------------------------------------------------------\n"); model_print("# t Action type MO Location Value Rf CV\n"); @@ -1448,18 +1477,18 @@ static void print_list(const action_list_t *list) unsigned int hash = 0; - for (it = list->begin();it != list->end();it++) { - const ModelAction *act = *it; + for (it = list->begin();it != NULL;it=it->getNext()) { + const ModelAction *act = it->getVal(); if (act->get_seq_number() > 0) act->print(); - hash = hash^(hash<<3)^((*it)->hash()); + hash = hash^(hash<<3)^(it->getVal()->hash()); } model_print("HASH %u\n", hash); model_print("------------------------------------------------------------------------------------\n"); } #if SUPPORT_MOD_ORDER_DUMP -void ModelExecution::dumpGraph(char *filename) const +void ModelExecution::dumpGraph(char *filename) { char buffer[200]; sprintf(buffer, "%s.dot", filename); @@ -1468,8 +1497,8 @@ void ModelExecution::dumpGraph(char *filename) const mo_graph->dumpNodes(file); ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *) * get_num_threads()); - for (action_list_t::const_iterator it = action_trace.begin();it != action_trace.end();it++) { - ModelAction *act = *it; + for (sllnode* it = action_trace.begin();it != NULL;it=it->getNext()) { + ModelAction *act = it->getVal(); if (act->is_read()) { mo_graph->dot_print_node(file, act); mo_graph->dot_print_edge(file, @@ -1493,7 +1522,7 @@ void ModelExecution::dumpGraph(char *filename) const #endif /** @brief Prints an execution trace summary. */ -void ModelExecution::print_summary() const +void ModelExecution::print_summary() { #if SUPPORT_MOD_ORDER_DUMP char buffername[100]; @@ -1633,8 +1662,8 @@ Thread * ModelExecution::take_step(ModelAction *curr) curr = check_current_action(curr); ASSERT(curr); - /* Process this action in ModelHistory for records*/ - model->get_history()->process_action( 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);