X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=execution.cc;h=99f86195713523cb02791fb8ae75fcc309a1b0ec;hp=62a7346b56ee22055952bbf7f45bb367df3f117d;hb=e9992398715ddf04785b93a5a0e9b60e77a15b21;hpb=10e19f222985c1a2da41d3179643703d794faf57 diff --git a/execution.cc b/execution.cc index 62a7346b..99f86195 100644 --- a/execution.cc +++ b/execution.cc @@ -14,8 +14,9 @@ #include "datarace.h" #include "threads-model.h" #include "bugmessage.h" +#include "fuzzer.h" -#define INITIAL_THREAD_ID 0 +#define INITIAL_THREAD_ID 0 /** * Structure for holding small ModelChecker members that should be snapshotted @@ -25,45 +26,34 @@ struct model_snapshot_members { /* First thread created will have id INITIAL_THREAD_ID */ next_thread_id(INITIAL_THREAD_ID), used_sequence_numbers(0), - next_backtrack(NULL), bugs(), - too_many_reads(false), - no_valid_reads(false), bad_synchronization(false), - bad_sc_read(false), asserted(false) { } ~model_snapshot_members() { - for (unsigned int i = 0; i < bugs.size(); i++) + for (unsigned int i = 0;i < bugs.size();i++) delete bugs[i]; bugs.clear(); } unsigned int next_thread_id; modelclock_t used_sequence_numbers; - ModelAction *next_backtrack; SnapVector bugs; - bool too_many_reads; - bool no_valid_reads; /** @brief Incorrectly-ordered synchronization was made */ bool bad_synchronization; - bool bad_sc_read; bool asserted; SNAPSHOTALLOC }; /** @brief Constructor */ -ModelExecution::ModelExecution(ModelChecker *m, - const struct model_params *params, - Scheduler *scheduler, - NodeStack *node_stack) : +ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler, NodeStack *node_stack) : model(m), - params(params), + params(NULL), scheduler(scheduler), action_trace(), - thread_map(2), /* We'll always need at least 2 threads */ + thread_map(2), /* We'll always need at least 2 threads */ pthread_map(0), pthread_counter(0), obj_map(), @@ -73,8 +63,9 @@ ModelExecution::ModelExecution(ModelChecker *m, thrd_last_action(1), thrd_last_fence_release(), node_stack(node_stack), - priv(new struct model_snapshot_members()), - mo_graph(new CycleGraph()) + priv(new struct model_snapshot_members ()), + mo_graph(new CycleGraph()), + fuzzer(new Fuzzer()) { /* Initialize a model-checker thread, for special ModelActions */ model_thread = new Thread(get_next_id()); @@ -86,7 +77,7 @@ ModelExecution::ModelExecution(ModelChecker *m, /** @brief Destructor */ ModelExecution::~ModelExecution() { - for (unsigned int i = 0; i < get_num_threads(); i++) + for (unsigned int i = 0;i < get_num_threads();i++) delete get_thread(int_to_id(i)); delete mo_graph; @@ -178,7 +169,7 @@ bool ModelExecution::should_wake_up(const ModelAction *curr, const Thread *threa void ModelExecution::wake_up_sleeping_actions(ModelAction *curr) { - for (unsigned int i = 0; i < get_num_threads(); i++) { + for (unsigned int i = 0;i < get_num_threads();i++) { Thread *thr = get_thread(int_to_id(i)); if (scheduler->is_sleep_set(thr)) { if (should_wake_up(curr, thr)) @@ -195,13 +186,6 @@ void ModelExecution::set_bad_synchronization() priv->bad_synchronization = true; } -/** @brief Alert the model-checker that an incorrectly-ordered - * synchronization was made */ -void ModelExecution::set_bad_sc_read() -{ - priv->bad_sc_read = true; -} - bool ModelExecution::assert_bug(const char *msg) { priv->bugs.push_back(new bug_message(msg)); @@ -255,7 +239,7 @@ void ModelExecution::set_assert() bool ModelExecution::is_deadlocked() const { bool blocking_threads = false; - for (unsigned int i = 0; i < get_num_threads(); i++) { + for (unsigned int i = 0;i < get_num_threads();i++) { thread_id_t tid = int_to_id(i); if (is_enabled(tid)) return false; @@ -275,7 +259,7 @@ bool ModelExecution::is_deadlocked() const */ bool ModelExecution::is_complete_execution() const { - for (unsigned int i = 0; i < get_num_threads(); i++) + for (unsigned int i = 0;i < get_num_threads();i++) if (is_enabled(int_to_id(i))) return false; return true; @@ -288,21 +272,30 @@ 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. */ -bool ModelExecution::process_read(ModelAction *curr, ModelVector * rf_set) +void ModelExecution::process_read(ModelAction *curr, SnapVector * rf_set) { - int random_index = random() % rf_set->size(); - bool updated = false; - - const ModelAction *rf = (*rf_set)[random_index]; - ASSERT(rf); - - mo_graph->startChanges(); - - updated = r_modification_order(curr, rf); - read_from(curr, rf); - mo_graph->commitChanges(); - get_thread(curr)->set_return_value(curr->get_return_value()); - return updated; + SnapVector * priorset = new SnapVector(); + while(true) { + + int index = fuzzer->selectWrite(curr, rf_set); + const ModelAction *rf = (*rf_set)[index]; + + + ASSERT(rf); + + if (r_modification_order(curr, rf, priorset)) { + for(unsigned int i=0;isize();i++) { + mo_graph->addEdge((*priorset)[i], rf); + } + read_from(curr, rf); + get_thread(curr)->set_return_value(curr->get_return_value()); + delete priorset; + return; + } + priorset->clear(); + (*rf_set)[index] = rf_set->back(); + rf_set->pop_back(); + } } /** @@ -339,7 +332,7 @@ bool ModelExecution::process_mutex(ModelAction *curr) } get_thread(curr)->set_return_value(1); } - //otherwise fall into the lock case + //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"); @@ -355,7 +348,7 @@ bool ModelExecution::process_mutex(ModelAction *curr) case ATOMIC_WAIT: case ATOMIC_UNLOCK: { /* wake up the other threads */ - for (unsigned int i = 0; i < get_num_threads(); i++) { + for (unsigned int i = 0;i < get_num_threads();i++) { Thread *t = get_thread(int_to_id(i)); Thread *curr_thrd = get_thread(curr); if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock()) @@ -366,14 +359,14 @@ bool ModelExecution::process_mutex(ModelAction *curr) state->locked = NULL; if (!curr->is_wait()) - break; /* The rest is only for ATOMIC_WAIT */ + break;/* The rest is only for ATOMIC_WAIT */ break; } 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++) { + for (action_list_t::iterator rit = waiters->begin();rit != waiters->end();rit++) { scheduler->wake(get_thread(*rit)); } waiters->clear(); @@ -381,20 +374,8 @@ bool ModelExecution::process_mutex(ModelAction *curr) } case ATOMIC_NOTIFY_ONE: { action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location()); - - //BCD -- TOFIX FUZZER - //THIS SHOULD BE A RANDOM CHOICE - // int wakeupthread = curr->get_node()->get_misc(); - int wakeupthread = 0; - action_list_t::iterator it = waiters->begin(); - - // WL - if (it == waiters->end()) - break; - - advance(it, wakeupthread); - scheduler->wake(get_thread(*it)); - waiters->erase(it); + Thread * thread = fuzzer->selectNotify(waiters); + scheduler->wake(thread); break; } @@ -409,15 +390,13 @@ bool ModelExecution::process_mutex(ModelAction *curr) * @param curr The ModelAction to process * @return True if the mo_graph was updated or promises were resolved */ -bool ModelExecution::process_write(ModelAction *curr) +void ModelExecution::process_write(ModelAction *curr) { - bool updated_mod_order = w_modification_order(curr); + w_modification_order(curr); - mo_graph->commitChanges(); get_thread(curr)->set_return_value(VALUE_NONE); - return updated_mod_order; } /** @@ -440,7 +419,7 @@ bool ModelExecution::process_fence(ModelAction *curr) action_list_t *list = &action_trace; action_list_t::reverse_iterator rit; /* Find X : is_read(X) && X --sb-> curr */ - for (rit = list->rbegin(); rit != list->rend(); rit++) { + for (rit = list->rbegin();rit != list->rend();rit++) { ModelAction *act = *rit; if (act == curr) continue; @@ -461,7 +440,7 @@ bool ModelExecution::process_fence(ModelAction *curr) /* 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++) + for (unsigned int i = 0;i < release_heads.size();i++) synchronize(release_heads[i], curr); if (release_heads.size() != 0) updated = true; @@ -496,7 +475,7 @@ bool ModelExecution::process_thread_action(ModelAction *curr) break; } case PTHREAD_CREATE: { - (*(pthread_t *)curr->get_location()) = pthread_counter++; + (*(uint32_t *)curr->get_location()) = pthread_counter++; struct pthread_params *params = (struct pthread_params *)curr->get_value(); Thread *th = new Thread(get_next_id(), NULL, params->func, params->arg, get_thread(curr)); @@ -504,8 +483,8 @@ bool ModelExecution::process_thread_action(ModelAction *curr) add_thread(th); th->set_creation(curr); - if ( pthread_map.size() < pthread_counter ) - pthread_map.resize( pthread_counter ); + if ( pthread_map.size() < pthread_counter ) + pthread_map.resize( pthread_counter ); pthread_map[ pthread_counter-1 ] = th; break; @@ -514,28 +493,28 @@ 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 */ + 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) + updated = true; /* trigger rel-seq checks */ + break; // WL: to be add (modified) } case THREAD_FINISH: { Thread *th = get_thread(curr); /* Wake up any joining threads */ - for (unsigned int i = 0; i < get_num_threads(); i++) { + for (unsigned int i = 0;i < get_num_threads();i++) { Thread *waiting = get_thread(int_to_id(i)); if (waiting->waiting_on() == th && waiting->get_pending()->is_thread_join()) scheduler->wake(waiting); } th->complete(); - updated = true; /* trigger rel-seq checks */ + updated = true; /* trigger rel-seq checks */ break; } case THREAD_START: { @@ -589,7 +568,7 @@ bool ModelExecution::initialize_curr_action(ModelAction **curr) newcurr->create_cv(get_parent_action(newcurr->get_tid())); *curr = newcurr; - return false; /* Action was explored previously */ + return false; /* Action was explored previously */ } else { newcurr = *curr; @@ -599,7 +578,7 @@ bool ModelExecution::initialize_curr_action(ModelAction **curr) /* Assign most recent release fence */ newcurr->set_last_fence_release(get_last_fence_release(newcurr->get_tid())); - return true; /* This was a new ModelAction */ + return true; /* This was a new ModelAction */ } } @@ -625,7 +604,7 @@ bool ModelExecution::read_from(ModelAction *act, const ModelAction *rf) 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++) + for (unsigned int i = 0;i < release_heads.size();i++) if (!synchronize(release_heads[i], act)) num_heads--; return num_heads > 0; @@ -703,29 +682,31 @@ ModelAction * ModelExecution::check_current_action(ModelAction *curr) wake_up_sleeping_actions(curr); /* Add the action to lists before any other model-checking tasks */ - if (!second_part_of_rmw) + if (!second_part_of_rmw && curr->get_type() != NOOP) add_action_to_lists(curr); - ModelVector * rf_set = NULL; + 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); + rf_set = build_may_read_from(curr); process_thread_action(curr); - + if (curr->is_read() && !second_part_of_rmw) { - process_read(curr, rf_set); - delete rf_set; + process_read(curr, rf_set); + delete rf_set; + } else { + ASSERT(rf_set == NULL); } - + if (curr->is_write()) - process_write(curr); - + process_write(curr); + if (curr->is_fence()) - process_fence(curr); - + process_fence(curr); + if (curr->is_mutex_op()) - process_mutex(curr); + process_mutex(curr); return curr; } @@ -737,7 +718,7 @@ ModelAction * ModelExecution::check_current_action(ModelAction *curr) */ bool ModelExecution::isfeasibleprefix() const { - return !is_infeasible(); + return !is_infeasible(); } /** @@ -749,16 +730,8 @@ void ModelExecution::print_infeasibility(const char *prefix) const { char buf[100]; char *ptr = buf; - if (mo_graph->checkForCycles()) - ptr += sprintf(ptr, "[mo cycle]"); - if (priv->too_many_reads) - ptr += sprintf(ptr, "[too many reads]"); - if (priv->no_valid_reads) - ptr += sprintf(ptr, "[no valid reads-from]"); if (priv->bad_synchronization) ptr += sprintf(ptr, "[bad sw ordering]"); - if (priv->bad_sc_read) - ptr += sprintf(ptr, "[bad sc read]"); if (ptr != buf) model_print("%s: %s", prefix ? prefix : "Infeasible", buf); } @@ -771,11 +744,7 @@ void ModelExecution::print_infeasibility(const char *prefix) const */ bool ModelExecution::is_infeasible() const { - return mo_graph->checkForCycles() || - priv->no_valid_reads || - priv->too_many_reads || - priv->bad_synchronization || - priv->bad_sc_read; + return priv->bad_synchronization; } /** Close out a RMWR by converting previous RMWR into a RMW or READ. */ @@ -783,8 +752,7 @@ ModelAction * ModelExecution::process_rmw(ModelAction *act) { ModelAction *lastread = get_last_action(act->get_tid()); lastread->process_rmw(act); if (act->is_rmw()) { - mo_graph->addRMWEdge(lastread->get_reads_from(), lastread); - mo_graph->commitChanges(); + mo_graph->addRMWEdge(lastread->get_reads_from(), lastread); } return lastread; } @@ -805,12 +773,11 @@ ModelAction * ModelExecution::process_rmw(ModelAction *act) { * @param rf The ModelAction or Promise that curr reads from. Must be a write. * @return True if modification order edges were added; false otherwise */ -template -bool ModelExecution::r_modification_order(ModelAction *curr, const rf_type *rf) + +bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf, SnapVector * priorset) { SnapVector *thrd_lists = obj_thrd_map.get(curr->get_location()); unsigned int i; - bool added = false; ASSERT(curr->is_read()); /* Last SC fence in the current thread */ @@ -820,7 +787,7 @@ bool ModelExecution::r_modification_order(ModelAction *curr, const rf_type *rf) last_sc_write = get_last_seq_cst_write(curr); /* Iterate over all threads */ - for (i = 0; i < thrd_lists->size(); i++) { + for (i = 0;i < thrd_lists->size();i++) { /* Last SC fence in thread i */ ModelAction *last_sc_fence_thread_local = NULL; if (int_to_id((int)i) != curr->get_tid()) @@ -834,7 +801,7 @@ bool ModelExecution::r_modification_order(ModelAction *curr, const rf_type *rf) /* 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++) { + for (rit = list->rbegin();rit != list->rend();rit++) { ModelAction *act = *rit; /* Skip curr */ @@ -852,19 +819,25 @@ bool ModelExecution::r_modification_order(ModelAction *curr, const rf_type *rf) /* C++, Section 29.3 statement 5 */ if (curr->is_seqcst() && last_sc_fence_thread_local && *act < *last_sc_fence_thread_local) { - added = mo_graph->addEdge(act, rf) || added; + if (mo_graph->checkReachable(rf, act)) + return false; + priorset->push_back(act); break; } /* C++, Section 29.3 statement 4 */ else if (act->is_seqcst() && last_sc_fence_local && - *act < *last_sc_fence_local) { - added = mo_graph->addEdge(act, rf) || added; + *act < *last_sc_fence_local) { + if (mo_graph->checkReachable(rf, act)) + return false; + priorset->push_back(act); break; } /* C++, Section 29.3 statement 6 */ else if (last_sc_fence_thread_before && - *act < *last_sc_fence_thread_before) { - added = mo_graph->addEdge(act, rf) || added; + *act < *last_sc_fence_thread_before) { + if (mo_graph->checkReachable(rf, act)) + return false; + priorset->push_back(act); break; } } @@ -875,18 +848,22 @@ bool ModelExecution::r_modification_order(ModelAction *curr, const rf_type *rf) */ if (act->happens_before(curr)) { if (act->is_write()) { - added = mo_graph->addEdge(act, rf) || added; + if (mo_graph->checkReachable(rf, act)) + return false; + priorset->push_back(act); } else { const ModelAction *prevrf = act->get_reads_from(); - if (!prevrf->equals(rf)) - added = mo_graph->addEdge(prevrf, rf) || added; + if (!prevrf->equals(rf)) { + if (mo_graph->checkReachable(rf, prevrf)) + return false; + priorset->push_back(prevrf); + } } break; } } } - - return added; + return true; } /** @@ -913,19 +890,18 @@ bool ModelExecution::r_modification_order(ModelAction *curr, const rf_type *rf) * value. If NULL, then don't record any future values. * @return True if modification order edges were added; false otherwise */ -bool ModelExecution::w_modification_order(ModelAction *curr) +void ModelExecution::w_modification_order(ModelAction *curr) { SnapVector *thrd_lists = obj_thrd_map.get(curr->get_location()); unsigned int i; - bool added = false; ASSERT(curr->is_write()); if (curr->is_seqcst()) { /* We have to at least see the last sequentially consistent write, - so we are initialized. */ + so we are initialized. */ ModelAction *last_seq_cst = get_last_seq_cst_write(curr); if (last_seq_cst != NULL) { - added = mo_graph->addEdge(last_seq_cst, curr) || added; + mo_graph->addEdge(last_seq_cst, curr); } } @@ -933,7 +909,7 @@ bool ModelExecution::w_modification_order(ModelAction *curr) ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL); /* Iterate over all threads */ - for (i = 0; i < thrd_lists->size(); i++) { + for (i = 0;i < thrd_lists->size();i++) { /* Last SC fence in thread i, before last SC fence in current thread */ ModelAction *last_sc_fence_thread_before = NULL; if (last_sc_fence_local && int_to_id((int)i) != curr->get_tid()) @@ -942,7 +918,8 @@ bool 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++) { + bool force_edge = false; + for (rit = list->rbegin();rit != list->rend();rit++) { ModelAction *act = *rit; if (act == curr) { /* @@ -956,6 +933,7 @@ bool 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; @@ -968,7 +946,7 @@ bool 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) { - added = mo_graph->addEdge(act, curr) || added; + mo_graph->addEdge(act, curr, force_edge); break; } @@ -984,14 +962,14 @@ bool ModelExecution::w_modification_order(ModelAction *curr) * readfrom(act) --mo--> act */ if (act->is_write()) - added = mo_graph->addEdge(act, curr) || added; + mo_graph->addEdge(act, curr, force_edge); else if (act->is_read()) { //if previous read accessed a null, just keep going - added = mo_graph->addEdge(act->get_reads_from(), curr) || added; + mo_graph->addEdge(act->get_reads_from(), curr, force_edge); } break; } else if (act->is_read() && !act->could_synchronize_with(curr) && - !act->same_thread(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 @@ -1008,8 +986,6 @@ bool ModelExecution::w_modification_order(ModelAction *curr) } } } - - return added; } /** @@ -1025,13 +1001,13 @@ bool ModelExecution::mo_may_allow(const ModelAction *writer, const ModelAction * SnapVector *thrd_lists = obj_thrd_map.get(reader->get_location()); unsigned int i; /* Iterate over all threads */ - for (i = 0; i < thrd_lists->size(); i++) { + for (i = 0;i < thrd_lists->size();i++) { const ModelAction *write_after_read = NULL; /* 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++) { + for (rit = list->rbegin();rit != list->rend();rit++) { ModelAction *act = *rit; /* Don't disallow due to act == reader */ @@ -1069,14 +1045,10 @@ bool ModelExecution::mo_may_allow(const ModelAction *writer, const ModelAction * * @return true, if the ModelExecution is certain that release_heads is complete; * false otherwise */ -bool ModelExecution::release_seq_heads(const ModelAction *rf, - rel_heads_list_t *release_heads) const +bool ModelExecution::release_seq_heads(const ModelAction *rf, rel_heads_list_t *release_heads) const { - /* Only check for release sequences if there are no cycles */ - if (mo_graph->checkForCycles()) - return false; - for ( ; rf != NULL; rf = rf->get_reads_from()) { + for ( ;rf != NULL;rf = rf->get_reads_from()) { ASSERT(rf->is_write()); if (rf->is_release()) @@ -1084,7 +1056,7 @@ bool ModelExecution::release_seq_heads(const ModelAction *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 */ + 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 @@ -1095,12 +1067,12 @@ bool ModelExecution::release_seq_heads(const ModelAction *rf, /* acq_rel RMW is a sufficient stopping condition */ if (rf->is_acquire() && rf->is_release()) - return true; /* complete */ + return true;/* complete */ }; - ASSERT(rf); // Needs to be real write + ASSERT(rf); // Needs to be real write if (rf->is_release()) - return true; /* complete */ + return true;/* complete */ /* else relaxed write * - check for fence-release in the same thread (29.8, stmt. 3) @@ -1113,7 +1085,7 @@ bool ModelExecution::release_seq_heads(const ModelAction *rf, if (fence_release) release_heads->push_back(fence_release); - return true; /* complete */ + return true; /* complete */ } /** @@ -1134,7 +1106,7 @@ bool ModelExecution::release_seq_heads(const ModelAction *rf, * @see ModelExecution::release_seq_heads */ void ModelExecution::get_release_seq_heads(ModelAction *acquire, - ModelAction *read, rel_heads_list_t *release_heads) + ModelAction *read, rel_heads_list_t *release_heads) { const ModelAction *rf = read->get_reads_from(); @@ -1237,10 +1209,10 @@ ModelAction * ModelExecution::get_last_seq_cst_write(ModelAction *curr) const 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++) + for (rit = list->rbegin();(*rit) != curr;rit++) ; - rit++; /* Skip past curr */ - for ( ; rit != list->rend(); rit++) + rit++; /* Skip past curr */ + for ( ;rit != list->rend();rit++) if ((*rit)->is_write() && (*rit)->is_seqcst()) return *rit; return NULL; @@ -1265,7 +1237,7 @@ ModelAction * ModelExecution::get_last_seq_cst_fence(thread_id_t tid, const Mode action_list_t::reverse_iterator rit = list->rbegin(); if (before_fence) { - for (; rit != list->rend(); rit++) + for (;rit != list->rend();rit++) if (*rit == before_fence) break; @@ -1273,7 +1245,7 @@ ModelAction * ModelExecution::get_last_seq_cst_fence(thread_id_t tid, const Mode rit++; } - for (; rit != list->rend(); rit++) + for (;rit != list->rend();rit++) if ((*rit)->is_fence() && (tid == (*rit)->get_tid()) && (*rit)->is_seqcst()) return *rit; return NULL; @@ -1294,7 +1266,7 @@ 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++) + for (rit = list->rbegin();rit != list->rend();rit++) if ((*rit)->is_unlock() || (*rit)->is_wait()) return *rit; return NULL; @@ -1318,6 +1290,22 @@ ClockVector * ModelExecution::get_cv(thread_id_t tid) const return get_parent_action(tid)->get_cv(); } +bool valequals(uint64_t val1, uint64_t val2, int size) { + switch(size) { + case 1: + return ((uint8_t)val1) == ((uint8_t)val2); + case 2: + return ((uint16_t)val1) == ((uint16_t)val2); + case 4: + return ((uint32_t)val1) == ((uint32_t)val2); + case 8: + return val1==val2; + default: + ASSERT(0); + return false; + } +} + /** * Build up an initial set of all past writes that this 'read' action may read * from, as well as any previously-observed future values that must still be valid. @@ -1325,7 +1313,7 @@ ClockVector * ModelExecution::get_cv(thread_id_t tid) const * @param curr is the current ModelAction that we are exploring; it must be a * 'read' operation. */ -ModelVector * 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()); unsigned int i; @@ -1336,14 +1324,14 @@ ModelVector * ModelExecution::build_may_read_from(ModelAction *c if (curr->is_seqcst()) last_sc_write = get_last_seq_cst_write(curr); - ModelVector * rf_set = new ModelVector(); - + SnapVector * rf_set = new SnapVector(); + /* Iterate over all threads */ - for (i = 0; i < thrd_lists->size(); i++) { + 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++) { + for (rit = list->rbegin();rit != list->rend();rit++) { ModelAction *act = *rit; /* Only consider 'write' actions */ @@ -1356,13 +1344,23 @@ ModelVector * ModelExecution::build_may_read_from(ModelAction *c if (curr->is_seqcst() && (act->is_seqcst() || (last_sc_write != NULL && act->happens_before(last_sc_write))) && act != last_sc_write) allow_read = false; + /* Need to check whether we will have two RMW reading from the same value */ + if (curr->is_rmwr()) { + /* It is okay if we have a failing CAS */ + if (!curr->is_rmwrcas() || + valequals(curr->get_value(), act->get_value(), curr->getSize())) { + //Need to make sure we aren't the second RMW + CycleNode * node = mo_graph->getNode_noCreate(act); + if (node != NULL && node->getRMW() != NULL) { + //we are the second RMW + allow_read = false; + } + } + } + if (allow_read) { /* Only add feasible reads */ - mo_graph->startChanges(); - r_modification_order(curr, act); - if (!is_infeasible()) - rf_set->push_back(act); - mo_graph->rollbackChanges(); + rf_set->push_back(act); } /* Include at most one act per-thread that "happens before" curr */ @@ -1409,7 +1407,7 @@ static void print_list(const action_list_t *list) unsigned int hash = 0; - for (it = list->begin(); it != list->end(); it++) { + for (it = list->begin();it != list->end();it++) { const ModelAction *act = *it; if (act->get_seq_number() > 0) act->print(); @@ -1429,20 +1427,20 @@ 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++) { + for (action_list_t::const_iterator it = action_trace.begin();it != action_trace.end();it++) { ModelAction *act = *it; if (act->is_read()) { mo_graph->dot_print_node(file, act); mo_graph->dot_print_edge(file, - act->get_reads_from(), - act, - "label=\"rf\", color=red, weight=2"); + act->get_reads_from(), + act, + "label=\"rf\", color=red, weight=2"); } if (thread_array[act->get_tid()]) { mo_graph->dot_print_edge(file, - thread_array[id_to_int(act->get_tid())], - act, - "label=\"sb\", color=blue, weight=400"); + thread_array[id_to_int(act->get_tid())], + act, + "label=\"sb\", color=blue, weight=400"); } thread_array[act->get_tid()] = act; @@ -1523,8 +1521,14 @@ Thread * ModelExecution::get_thread(const ModelAction *act) const * @return A Thread reference */ Thread * ModelExecution::get_pthread(pthread_t pid) { - if (pid < pthread_counter + 1) return pthread_map[pid]; - else return NULL; + union { + pthread_t p; + uint32_t v; + } x; + x.p = pid; + uint32_t thread_id = x.v; + if (thread_id < pthread_counter + 1) return pthread_map[thread_id]; + else return NULL; } /** @@ -1564,33 +1568,27 @@ Thread * ModelExecution::action_select_next_thread(const ModelAction *curr) cons if (curr->is_rmwr()) return get_thread(curr); if (curr->is_write()) { - std::memory_order order = curr->get_mo(); + 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; - } + 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) - return curr->get_thread_operand(); + return curr->get_thread_operand(); if (curr->get_type() == PTHREAD_CREATE) { return curr->get_thread_operand(); } return NULL; } -/** @return True if the execution has taken too many steps */ -bool ModelExecution::too_many_steps() const -{ - return params->bound != 0 && priv->used_sequence_numbers > params->bound; -} - /** * Takes the next step in the execution, if possible. * @param curr The current step to take @@ -1602,7 +1600,7 @@ Thread * ModelExecution::take_step(ModelAction *curr) Thread *curr_thrd = get_thread(curr); ASSERT(curr_thrd->get_state() == THREAD_READY); - ASSERT(check_action_enabled(curr)); /* May have side effects? */ + ASSERT(check_action_enabled(curr)); /* May have side effects? */ curr = check_current_action(curr); ASSERT(curr); @@ -1612,3 +1610,6 @@ Thread * ModelExecution::take_step(ModelAction *curr) return action_select_next_thread(curr); } +Fuzzer * ModelExecution::getFuzzer() { + return fuzzer; +}