X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=execution.cc;h=c6962bc07aeeea50c693c02c78a3aaf5ed3fbe84;hp=d22f628d215bcc5f81704c058dea57d1480956d8;hb=a46421375ee025acad83cf7cd612902d486987cb;hpb=9e899821b7500371dbe61975ccbc64e42e82ef83 diff --git a/execution.cc b/execution.cc index d22f628d..c6962bc0 100644 --- a/execution.cc +++ b/execution.cc @@ -13,6 +13,7 @@ #include "datarace.h" #include "threads-model.h" #include "bugmessage.h" +#include "history.h" #include "fuzzer.h" #define INITIAL_THREAD_ID 0 @@ -62,8 +63,11 @@ ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) : thrd_last_action(1), thrd_last_fence_release(), priv(new struct model_snapshot_members ()), - mo_graph(new CycleGraph()), - fuzzer(new Fuzzer()) + mo_graph(new CycleGraph()), + fuzzer(new Fuzzer()), + thrd_func_list(), + thrd_func_act_lists(), + isfinished(false) { /* Initialize a model-checker thread, for special ModelActions */ model_thread = new Thread(get_next_id()); @@ -96,7 +100,7 @@ static action_list_t * get_safe_ptr_action(HashTable * get_safe_ptr_vect_action(HashTable *, uintptr_t, 4> * hash, void * ptr) +static SnapVector * get_safe_ptr_vect_action(HashTable *, uintptr_t, 4> * hash, void * ptr) { SnapVector *tmp = hash->get(ptr); if (tmp == NULL) { @@ -149,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; } @@ -188,6 +197,16 @@ bool ModelExecution::have_bug_reports() const return priv->bugs.size() != 0; } +/** @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 + * are not considered fatal unless the number of races is exceeds + * a threshold (temporarily set as 15). + */ +bool ModelExecution::have_fatal_bug_reports() const +{ + return priv->bugs.size() != 0; +} + SnapVector * ModelExecution::get_bugs() const { return &priv->bugs; @@ -250,6 +269,20 @@ 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); + model->get_history()->process_action(act, act->get_tid()); + return act; +} /** * Processes a read model action. @@ -260,8 +293,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]; @@ -323,8 +361,9 @@ bool ModelExecution::process_mutex(ModelAction *curr) } //otherwise fall into the lock case case ATOMIC_LOCK: { - if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock) - assert_bug("Lock access before initialization"); + //TODO: FIND SOME BETTER WAY TO CHECK LOCK INITIALIZED OR NOT + //if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock) + // assert_bug("Lock access before initialization"); state->locked = get_thread(curr); ModelAction *unlock = get_last_unlock(curr); //synchronize with the previous unlock statement @@ -357,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; @@ -385,10 +424,7 @@ bool ModelExecution::process_mutex(ModelAction *curr) */ void ModelExecution::process_write(ModelAction *curr) { - w_modification_order(curr); - - get_thread(curr)->set_return_value(VALUE_NONE); } @@ -410,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()) @@ -431,8 +467,8 @@ bool ModelExecution::process_fence(ModelAction *curr) continue; /* Establish hypothetical release sequences */ - ClockVector *cv = get_hb_from_write(act); - if (curr->get_cv()->merge(cv)) + ClockVector *cv = get_hb_from_write(act->get_reads_from()); + if (cv != NULL && curr->get_cv()->merge(cv)) updated = true; } } @@ -450,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(); @@ -483,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)); @@ -504,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: { @@ -513,8 +552,6 @@ bool ModelExecution::process_thread_action(ModelAction *curr) default: break; } - - return updated; } /** @@ -619,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; @@ -649,6 +689,9 @@ ModelAction * ModelExecution::check_current_action(ModelAction *curr) if (!second_part_of_rmw && curr->get_type() != NOOP) add_action_to_lists(curr); + if (curr->is_write()) + add_write_to_lists(curr); + SnapVector * rf_set = NULL; /* Build may_read_from set for newly-created actions */ if (newly_explored && curr->is_read()) @@ -770,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) @@ -819,7 +862,7 @@ bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction * if (act->happens_before(curr)) { if (i==0) { if (last_sc_fence_local == NULL || - (*last_sc_fence_local < *prev_same_thread)) { + (*last_sc_fence_local < *act)) { prev_same_thread = act; } } @@ -877,13 +920,17 @@ void ModelExecution::w_modification_order(ModelAction *curr) unsigned int i; ASSERT(curr->is_write()); + SnapList edgeset; + if (curr->is_seqcst()) { /* We have to at least see the last sequentially consistent write, so we are initialized. */ ModelAction *last_seq_cst = get_last_seq_cst_write(curr); if (last_seq_cst != NULL) { - mo_graph->addEdge(last_seq_cst, curr); + 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 */ @@ -898,10 +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; - bool force_edge = false; - 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 @@ -914,7 +960,6 @@ void ModelExecution::w_modification_order(ModelAction *curr) * 3) If normal write, we need to look at earlier actions, so * continue processing list. */ - force_edge = true; if (curr->is_rmw()) { if (curr->get_reads_from() != NULL) break; @@ -927,7 +972,7 @@ void ModelExecution::w_modification_order(ModelAction *curr) /* C++, Section 29.3 statement 7 */ if (last_sc_fence_thread_before && act->is_write() && *act < *last_sc_fence_thread_before) { - mo_graph->addEdge(act, curr, force_edge); + edgeset.push_back(act); break; } @@ -943,30 +988,17 @@ void ModelExecution::w_modification_order(ModelAction *curr) * readfrom(act) --mo--> act */ if (act->is_write()) - mo_graph->addEdge(act, curr, force_edge); + edgeset.push_back(act); else if (act->is_read()) { //if previous read accessed a null, just keep going - mo_graph->addEdge(act->get_reads_from(), curr, force_edge); + edgeset.push_back(act->get_reads_from()); } break; - } else if (act->is_read() && !act->could_synchronize_with(curr) && - !act->same_thread(curr)) { - /* We have an action that: - (1) did not happen before us - (2) is a read and we are a write - (3) cannot synchronize with us - (4) is in a different thread - => - that read could potentially read from our write. Note that - these checks are overly conservative at this point, we'll - do more checks before actually removing the - pendingfuturevalue. - - */ - } } } + mo_graph->addEdges(&edgeset, curr); + } /** @@ -987,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) @@ -1051,9 +1083,9 @@ ClockVector * ModelExecution::get_hb_from_write(ModelAction *rf) const { } i--; if (i >= 0) { - rf = (*processset)[i]; + rf = (*processset)[i]; } else - break; + break; } if (processset != NULL) delete processset; @@ -1077,26 +1109,43 @@ void ModelExecution::add_action_to_lists(ModelAction *act) uninit = get_uninitialized_action(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()) { + int oldsize = (int) vec->size(); + vec->resize(uninit_id + 1); + for(int i=oldsize;ipush_back(act); + // Update action trace, a total order of all actions action_trace.push_back(act); if (uninit) action_trace.push_front(uninit); + // 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); + // Update thrd_last_action, the last action taken by each thrad if ((int)thrd_last_action.size() <= tid) thrd_last_action.resize(get_num_threads()); thrd_last_action[tid] = act; if (uninit) thrd_last_action[uninit_id] = uninit; + // Update thrd_last_fence_release, the last release fence taken by each thread if (act->is_fence() && act->is_release()) { if ((int)thrd_last_fence_release.size() <= tid) thrd_last_fence_release.resize(get_num_threads()); @@ -1108,12 +1157,94 @@ 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) { + sllnode * rit = list->end(); + modelclock_t next_seq = act->get_seq_number(); + if (rit == NULL || (rit->getVal()->get_seq_number() == next_seq)) + list->push_back(act); + else { + for(;rit != NULL;rit=rit->getPrev()) { + if (rit->getVal()->get_seq_number() == next_seq) { + list->insertAfter(rit, act); + break; + } + } + } +} + +void insertIntoActionListAndSetCV(action_list_t *list, ModelAction *act) { + sllnode * rit = list->end(); + modelclock_t next_seq = act->get_seq_number(); + if (rit == NULL) { + act->create_cv(NULL); + } else if (rit->getVal()->get_seq_number() == next_seq) { + act->create_cv(rit->getVal()); + list->push_back(act); + } else { + for(;rit != NULL;rit=rit->getPrev()) { + if (rit->getVal()->get_seq_number() == next_seq) { + act->create_cv(rit->getVal()); + list->insertAfter(rit, 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()) { + 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 + 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) { + 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()) { + 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); +} + /** * @brief Get the last action performed by a particular Thread * @param tid The thread ID of the Thread in question @@ -1153,16 +1284,7 @@ ModelAction * ModelExecution::get_last_fence_release(thread_id_t tid) const ModelAction * ModelExecution::get_last_seq_cst_write(ModelAction *curr) const { void *location = curr->get_location(); - action_list_t *list = obj_map.get(location); - /* Find: max({i in dom(S) | seq_cst(t_i) && isWrite(t_i) && samevar(t_i, t)}) */ - action_list_t::reverse_iterator rit; - for (rit = list->rbegin();(*rit) != curr;rit++) - ; - rit++; /* Skip past curr */ - for ( ;rit != list->rend();rit++) - if ((*rit)->is_write() && (*rit)->is_seqcst()) - return *rit; - return NULL; + return obj_last_sc_map.get(location); } /** @@ -1181,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; } @@ -1212,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; } @@ -1263,7 +1387,7 @@ bool valequals(uint64_t val1, uint64_t val2, int size) { */ SnapVector * ModelExecution::build_may_read_from(ModelAction *curr) { - SnapVector *thrd_lists = obj_thrd_map.get(curr->get_location()); + SnapVector *thrd_lists = obj_wr_thrd_map.get(curr->get_location()); unsigned int i; ASSERT(curr->is_read()); @@ -1278,21 +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; - - /* Only consider 'write' actions */ - if (!act->is_write()) { - if (act != curr && act->is_read() && act->happens_before(curr)) { - ModelAction *tmp = act->get_reads_from(); - if (((unsigned int) id_to_int(tmp->get_tid()))==i) - act = tmp; - else - break; - } else - continue; - } + sllnode * rit; + for (rit = list->end();rit != NULL;rit=rit->getPrev()) { + ModelAction *act = rit->getVal(); if (act == curr) continue; @@ -1355,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"); @@ -1365,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); @@ -1385,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, @@ -1410,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]; @@ -1550,6 +1662,9 @@ 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->get_tid() ); + if (curr_thrd->is_blocked() || curr_thrd->is_complete()) scheduler->remove_thread(curr_thrd);