X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=execution.cc;h=c6962bc07aeeea50c693c02c78a3aaf5ed3fbe84;hb=533aa98d0e7df1435defd4b0698aedf5300a1ad3;hp=2e7442515b4cf47556817f727ba3bd8a7e65b466;hpb=c44681494532fc9b3cec1e9148324025a635017b;p=c11tester.git diff --git a/execution.cc b/execution.cc index 2e744251..c6962bc0 100644 --- a/execution.cc +++ b/execution.cc @@ -6,7 +6,6 @@ #include "model.h" #include "execution.h" #include "action.h" -#include "nodestack.h" #include "schedule.h" #include "common.h" #include "clockvector.h" @@ -14,6 +13,7 @@ #include "datarace.h" #include "threads-model.h" #include "bugmessage.h" +#include "history.h" #include "fuzzer.h" #define INITIAL_THREAD_ID 0 @@ -48,30 +48,31 @@ struct model_snapshot_members { }; /** @brief Constructor */ -ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler, NodeStack *node_stack) : +ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) : model(m), params(NULL), scheduler(scheduler), action_trace(), thread_map(2), /* We'll always need at least 2 threads */ pthread_map(0), - pthread_counter(0), + pthread_counter(1), obj_map(), condvar_waiters_map(), obj_thrd_map(), mutex_map(), thrd_last_action(1), thrd_last_fence_release(), - node_stack(node_stack), priv(new struct model_snapshot_members ()), mo_graph(new CycleGraph()), - fuzzer(new Fuzzer()) + 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()); add_thread(model_thread); scheduler->register_engine(this); - node_stack->register_engine(this); } /** @brief Destructor */ @@ -99,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) { @@ -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; } @@ -191,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; @@ -253,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,13 +290,18 @@ bool ModelExecution::is_complete_execution() const * @param rf_set is the set of model actions we can possibly read from * @return True if processing this read updates the mo_graph. */ -void ModelExecution::process_read(ModelAction *curr, SnapVector * rf_set) +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); - const ModelAction *rf = (*rf_set)[index]; + ModelAction *rf = (*rf_set)[index]; ASSERT(rf); @@ -326,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 @@ -360,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; @@ -388,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); } @@ -413,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()) @@ -434,11 +467,8 @@ bool ModelExecution::process_fence(ModelAction *curr) continue; /* Establish hypothetical release sequences */ - rel_heads_list_t release_heads; - get_release_seq_heads(curr, act, &release_heads); - for (unsigned int i = 0;i < release_heads.size();i++) - synchronize(release_heads[i], curr); - if (release_heads.size() != 0) + ClockVector *cv = get_hb_from_write(act->get_reads_from()); + if (cv != NULL && curr->get_cv()->merge(cv)) updated = true; } } @@ -456,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(); @@ -489,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)); @@ -510,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: { @@ -519,14 +552,12 @@ bool ModelExecution::process_thread_action(ModelAction *curr) default: break; } - - return updated; } /** * Initialize the current action by performing one or more of the following - * actions, as appropriate: merging RMWR and RMWC/RMW actions, stepping forward - * in the NodeStack, manipulating backtracking sets, allocating and + * actions, as appropriate: merging RMWR and RMWC/RMW actions, + * manipulating backtracking sets, allocating and * initializing clock vectors, and computing the promises to fulfill. * * @param curr The current action, as passed from the user context; may be @@ -536,38 +567,16 @@ bool ModelExecution::process_thread_action(ModelAction *curr) */ bool ModelExecution::initialize_curr_action(ModelAction **curr) { - ModelAction *newcurr; - if ((*curr)->is_rmwc() || (*curr)->is_rmw()) { - newcurr = process_rmw(*curr); + ModelAction *newcurr = process_rmw(*curr); delete *curr; *curr = newcurr; return false; - } - - (*curr)->set_seq_number(get_next_seq_num()); - - newcurr = node_stack->explore_action(*curr); - if (newcurr) { - /* First restore type and order in case of RMW operation */ - if ((*curr)->is_rmwr()) - newcurr->copy_typeandorder(*curr); - - ASSERT((*curr)->get_location() == newcurr->get_location()); - newcurr->copy_from_new(*curr); - - /* Discard duplicate ModelAction; use action from NodeStack */ - delete *curr; - - /* Always compute new clock vector */ - newcurr->create_cv(get_parent_action(newcurr->get_tid())); - - *curr = newcurr; - return false; /* Action was explored previously */ } else { - newcurr = *curr; + ModelAction *newcurr = *curr; + newcurr->set_seq_number(get_next_seq_num()); /* Always compute new clock vector */ newcurr->create_cv(get_parent_action(newcurr->get_tid())); @@ -590,22 +599,18 @@ bool ModelExecution::initialize_curr_action(ModelAction **curr) * @return True if this read established synchronization */ -bool ModelExecution::read_from(ModelAction *act, const ModelAction *rf) +void ModelExecution::read_from(ModelAction *act, ModelAction *rf) { ASSERT(rf); ASSERT(rf->is_write()); act->set_read_from(rf); if (act->is_acquire()) { - rel_heads_list_t release_heads; - get_release_seq_heads(act, act, &release_heads); - int num_heads = release_heads.size(); - for (unsigned int i = 0;i < release_heads.size();i++) - if (!synchronize(release_heads[i], act)) - num_heads--; - return num_heads > 0; + ClockVector *cv = get_hb_from_write(rf); + if (cv == NULL) + return; + act->get_cv()->merge(cv); } - return false; } /** @@ -651,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; @@ -681,7 +689,10 @@ ModelAction * ModelExecution::check_current_action(ModelAction *curr) if (!second_part_of_rmw && curr->get_type() != NOOP) add_action_to_lists(curr); - SnapVector * rf_set = NULL; + 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()) rf_set = build_may_read_from(curr); @@ -802,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) @@ -851,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; } } @@ -909,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 */ @@ -930,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 @@ -946,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; @@ -959,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; } @@ -975,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); + } /** @@ -1019,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) @@ -1039,91 +1039,57 @@ bool ModelExecution::mo_may_allow(const ModelAction *writer, const ModelAction * } /** - * Finds the head(s) of the release sequence(s) containing a given ModelAction. - * The ModelAction under consideration is expected to be taking part in - * release/acquire synchronization as an object of the "reads from" relation. - * Note that this can only provide release sequence support for RMW chains - * which do not read from the future, as those actions cannot be traced until - * their "promise" is fulfilled. Similarly, we may not even establish the - * presence of a release sequence with certainty, as some modification order - * constraints may be decided further in the future. Thus, this function - * "returns" two pieces of data: a pass-by-reference vector of @a release_heads - * and a boolean representing certainty. + * Computes the clock vector that happens before propagates from this write. * * @param rf The action that might be part of a release sequence. Must be a * write. - * @param release_heads A pass-by-reference style return parameter. After - * execution of this function, release_heads will contain the heads of all the - * relevant release sequences, if any exists with certainty - * @return true, if the ModelExecution is certain that release_heads is complete; - * false otherwise + * @return ClockVector of happens before relation. */ -bool ModelExecution::release_seq_heads(const ModelAction *rf, rel_heads_list_t *release_heads) const -{ +ClockVector * ModelExecution::get_hb_from_write(ModelAction *rf) const { + SnapVector * processset = NULL; for ( ;rf != NULL;rf = rf->get_reads_from()) { ASSERT(rf->is_write()); + if (!rf->is_rmw() || (rf->is_acquire() && rf->is_release()) || rf->get_rfcv() != NULL) + break; + if (processset == NULL) + processset = new SnapVector(); + processset->push_back(rf); + } - if (rf->is_release()) - release_heads->push_back(rf); - else if (rf->get_last_fence_release()) - release_heads->push_back(rf->get_last_fence_release()); - if (!rf->is_rmw()) - break;/* End of RMW chain */ - - /** @todo Need to be smarter here... In the linux lock - * example, this will run to the beginning of the program for - * every acquire. */ - /** @todo The way to be smarter here is to keep going until 1 - * thread has a release preceded by an acquire and you've seen - * both. */ - - /* acq_rel RMW is a sufficient stopping condition */ - if (rf->is_acquire() && rf->is_release()) - return true;/* complete */ - }; - ASSERT(rf); // Needs to be real write - - if (rf->is_release()) - return true;/* complete */ - - /* else relaxed write - * - check for fence-release in the same thread (29.8, stmt. 3) - * - check modification order for contiguous subsequence - * -> rf must be same thread as release */ - - const ModelAction *fence_release = rf->get_last_fence_release(); - /* Synchronize with a fence-release unconditionally; we don't need to - * find any more "contiguous subsequence..." for it */ - if (fence_release) - release_heads->push_back(fence_release); - - return true; /* complete */ -} - -/** - * An interface for getting the release sequence head(s) with which a - * given ModelAction must synchronize. This function only returns a non-empty - * result when it can locate a release sequence head with certainty. Otherwise, - * it may mark the internal state of the ModelExecution so that it will handle - * the release sequence at a later time, causing @a acquire to update its - * synchronization at some later point in execution. - * - * @param acquire The 'acquire' action that may synchronize with a release - * sequence - * @param read The read action that may read from a release sequence; this may - * be the same as acquire, or else an earlier action in the same thread (i.e., - * when 'acquire' is a fence-acquire) - * @param release_heads A pass-by-reference return parameter. Will be filled - * with the head(s) of the release sequence(s), if they exists with certainty. - * @see ModelExecution::release_seq_heads - */ -void ModelExecution::get_release_seq_heads(ModelAction *acquire, - ModelAction *read, rel_heads_list_t *release_heads) -{ - const ModelAction *rf = read->get_reads_from(); + int i = (processset == NULL) ? 0 : processset->size(); - release_seq_heads(rf, release_heads); + ClockVector * vec = NULL; + while(true) { + if (rf->get_rfcv() != NULL) { + vec = rf->get_rfcv(); + } else if (rf->is_acquire() && rf->is_release()) { + vec = rf->get_cv(); + } else if (rf->is_release() && !rf->is_rmw()) { + vec = rf->get_cv(); + } else if (rf->is_release()) { + //have rmw that is release and doesn't have a rfcv + (vec = new ClockVector(vec, NULL))->merge(rf->get_cv()); + rf->set_rfcv(vec); + } else { + //operation that isn't release + if (rf->get_last_fence_release()) { + if (vec == NULL) + vec = rf->get_last_fence_release()->get_cv(); + else + (vec=new ClockVector(vec, NULL))->merge(rf->get_last_fence_release()->get_cv()); + } + rf->set_rfcv(vec); + } + i--; + if (i >= 0) { + rf = (*processset)[i]; + } else + break; + } + if (processset != NULL) + delete processset; + return vec; } /** @@ -1143,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()); @@ -1174,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 @@ -1219,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); } /** @@ -1247,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; } @@ -1278,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; } @@ -1300,7 +1358,8 @@ ModelAction * ModelExecution::get_parent_action(thread_id_t tid) const */ ClockVector * ModelExecution::get_cv(thread_id_t tid) const { - return get_parent_action(tid)->get_cv(); + ModelAction *firstaction=get_parent_action(tid); + return firstaction != NULL ? firstaction->get_cv() : NULL; } bool valequals(uint64_t val1, uint64_t val2, int size) { @@ -1326,9 +1385,9 @@ bool valequals(uint64_t val1, uint64_t val2, int size) { * @param curr is the current ModelAction that we are exploring; it must be a * 'read' operation. */ -SnapVector * ModelExecution::build_may_read_from(ModelAction *curr) +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()); @@ -1337,27 +1396,15 @@ SnapVector * ModelExecution::build_may_read_from(ModelActi if (curr->is_seqcst()) last_sc_write = get_last_seq_cst_write(curr); - SnapVector * rf_set = new SnapVector(); + SnapVector * rf_set = new SnapVector(); /* Iterate over all threads */ 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++) { - const ModelAction *act = *rit; - - /* Only consider 'write' actions */ - if (!act->is_write()) { - if (act != curr && act->is_read() && act->happens_before(curr)) { - const 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; @@ -1404,26 +1451,25 @@ SnapVector * ModelExecution::build_may_read_from(ModelActi /** * @brief Get an action representing an uninitialized atomic * - * This function may create a new one or try to retrieve one from the NodeStack + * This function may create a new one. * * @param curr The current action, which prompts the creation of an UNINIT action * @return A pointer to the UNINIT ModelAction */ -ModelAction * ModelExecution::get_uninitialized_action(const ModelAction *curr) const +ModelAction * ModelExecution::get_uninitialized_action(ModelAction *curr) const { - Node *node = curr->get_node(); - ModelAction *act = node->get_uninit_action(); + ModelAction *act = curr->get_uninit_action(); if (!act) { act = new ModelAction(ATOMIC_UNINIT, std::memory_order_relaxed, curr->get_location(), params->uninitvalue, model_thread); - node->set_uninit_action(act); + curr->set_uninit_action(act); } act->create_cv(NULL); 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"); @@ -1431,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); @@ -1451,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, @@ -1476,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]; @@ -1591,18 +1637,6 @@ Thread * ModelExecution::action_select_next_thread(const ModelAction *curr) cons /* Do not split atomic RMW */ if (curr->is_rmwr()) return get_thread(curr); - if (curr->is_write()) { - std::memory_order order = curr->get_mo(); - switch(order) { - case std::memory_order_relaxed: - return get_thread(curr); - case std::memory_order_release: - return get_thread(curr); - default: - return NULL; - } - } - /* Follow CREATE with the created thread */ /* which is not needed, because model.cc takes care of this */ if (curr->get_type() == THREAD_CREATE) @@ -1628,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);