X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=execution.cc;h=5aaabbcf00060a1ffe55cb77ad11f049037d7648;hp=3a73e353358d52a8a1f307f809d117a746c31545;hb=98e8ab95688324f8d0c0e77392c375c89c562c08;hpb=17b49f10df170ee8e6aca7401e014e8658971cdb diff --git a/execution.cc b/execution.cc index 3a73e353..5aaabbcf 100644 --- a/execution.cc +++ b/execution.cc @@ -51,10 +51,10 @@ 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(1), + action_trace(), obj_map(), condvar_waiters_map(), obj_thrd_map(), @@ -64,8 +64,6 @@ ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) : priv(new struct model_snapshot_members ()), mo_graph(new CycleGraph()), fuzzer(new NewFuzzer()), - thrd_func_list(), - thrd_func_act_lists(), isfinished(false) { /* Initialize a model-checker thread, for special ModelActions */ @@ -73,6 +71,9 @@ ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) : add_thread(model_thread); fuzzer->register_engine(m->get_history(), this); scheduler->register_engine(this); +#ifdef TLS + pthread_key_create(&pthreadkey, tlsdestructor); +#endif } /** @brief Destructor */ @@ -280,7 +281,7 @@ ModelAction * ModelExecution::convertNonAtomicStore(void * location) { */ bool ModelExecution::process_read(ModelAction *curr, SnapVector * rf_set) { - SnapVector * priorset = new SnapVector(); + SnapVector * priorset = new SnapVector(); bool hasnonatomicstore = hasNonAtomicStore(curr->get_location()); if (hasnonatomicstore) { ModelAction * nonatomicstore = convertNonAtomicStore(curr->get_location()); @@ -300,8 +301,6 @@ bool ModelExecution::process_read(ModelAction *curr, SnapVector * while(true) { int index = fuzzer->selectWrite(curr, rf_set); - if (index == -1)// no feasible write exists - return false; ModelAction *rf = (*rf_set)[index]; @@ -317,6 +316,7 @@ bool ModelExecution::process_read(ModelAction *curr, SnapVector * if (canprune && curr->get_type() == ATOMIC_READ) { int tid = id_to_int(curr->get_tid()); (*obj_thrd_map.get(curr->get_location()))[tid].pop_back(); + curr->setThrdMapRef(NULL); } return true; } @@ -711,10 +711,6 @@ ModelAction * ModelExecution::check_current_action(ModelAction *curr) wake_up_sleeping_actions(curr); - /* Add uninitialized actions to lists */ - if (!second_part_of_rmw) - add_uninit_action_to_lists(curr); - SnapVector * rf_set = NULL; /* Build may_read_from set for newly-created actions */ if (newly_explored && curr->is_read()) @@ -723,12 +719,6 @@ ModelAction * ModelExecution::check_current_action(ModelAction *curr) if (curr->is_read() && !second_part_of_rmw) { process_read(curr, rf_set); delete rf_set; - -/* bool success = process_read(curr, rf_set); - delete rf_set; - if (!success) - return curr; // Do not add action to lists - */ } else ASSERT(rf_set == NULL); @@ -784,7 +774,7 @@ ModelAction * ModelExecution::process_rmw(ModelAction *act) { */ bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf, - SnapVector * priorset, bool * canprune, bool check_only) + SnapVector * priorset, bool * canprune, bool check_only) { SnapVector *thrd_lists = obj_thrd_map.get(curr->get_location()); unsigned int i; @@ -878,7 +868,7 @@ bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction * if (!check_only) priorset->push_back(act); } else { - const ModelAction *prevrf = act->get_reads_from(); + ModelAction *prevrf = act->get_reads_from(); if (!prevrf->equals(rf)) { if (mo_graph->checkReachable(rf, prevrf)) return false; @@ -1101,59 +1091,6 @@ ClockVector * ModelExecution::get_hb_from_write(ModelAction *rf) const { return vec; } -/** - * Performs various bookkeeping operations for the current ModelAction when it is - * the first atomic action occurred at its memory location. - * - * For instance, adds uninitialized action to the per-object, per-thread action vector - * and to the action trace list of all thread actions. - * - * @param act is the ModelAction to process. - */ -void ModelExecution::add_uninit_action_to_lists(ModelAction *act) -{ - int tid = id_to_int(act->get_tid()); - ModelAction *uninit = NULL; - int uninit_id = -1; - action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location()); - if (list->empty() && act->is_atomic_var()) { - 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 ((int)vec->size() <= uninit_id) { - int oldsize = (int) vec->size(); - vec->resize(uninit_id + 1); - for(int i = oldsize;i < uninit_id + 1;i++) { - new (&(*vec)[i]) action_list_t(); - } - } - (*vec)[uninit_id].push_front(uninit); - } - - // Update action trace, a total order of all actions - 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 ((int)vec->size() <= tid) { - uint oldsize = vec->size(); - vec->resize(priv->next_thread_id); - for(uint i = oldsize;i < priv->next_thread_id;i++) - new (&(*vec)[i]) action_list_t(); - } - 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()); - if (uninit) - thrd_last_action[uninit_id] = uninit; -} - - /** * Performs various bookkeeping operations for the current ModelAction. For * instance, adds action to the per-object, per-thread action vector and to the @@ -1164,11 +1101,14 @@ void ModelExecution::add_uninit_action_to_lists(ModelAction *act) void ModelExecution::add_action_to_lists(ModelAction *act) { int tid = id_to_int(act->get_tid()); - action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location()); - list->push_back(act); + if ((act->is_fence() && act->is_seqcst()) || act->is_unlock()) { + action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location()); + act->setActionRef(list->add_back(act)); + } // Update action trace, a total order of all actions - action_trace.push_back(act); + act->setTraceRef(action_trace.add_back(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()); @@ -1178,9 +1118,9 @@ void ModelExecution::add_action_to_lists(ModelAction *act) for(uint i = oldsize;i < priv->next_thread_id;i++) new (&(*vec)[i]) action_list_t(); } - (*vec)[tid].push_back(act); + act->setThrdMapRef((*vec)[tid].add_back(act)); - // Update thrd_last_action, the last action taken by each thrad + // Update thrd_last_action, the last action taken by each thread if ((int)thrd_last_action.size() <= tid) thrd_last_action.resize(get_num_threads()); thrd_last_action[tid] = act; @@ -1194,7 +1134,7 @@ void ModelExecution::add_action_to_lists(ModelAction *act) if (act->is_wait()) { void *mutex_loc = (void *) act->get_value(); - get_safe_ptr_action(&obj_map, mutex_loc)->push_back(act); + act->setActionRef(get_safe_ptr_action(&obj_map, mutex_loc)->add_back(act)); SnapVector *vec = get_safe_ptr_vect_action(&obj_thrd_map, mutex_loc); if ((int)vec->size() <= tid) { @@ -1203,41 +1143,42 @@ void ModelExecution::add_action_to_lists(ModelAction *act) for(uint i = oldsize;i < priv->next_thread_id;i++) new (&(*vec)[i]) action_list_t(); } - (*vec)[tid].push_back(act); + act->setThrdMapRef((*vec)[tid].add_back(act)); } } -void insertIntoActionList(action_list_t *list, ModelAction *act) { +sllnode* 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); + return list->add_back(act); else { for(;rit != NULL;rit=rit->getPrev()) { if (rit->getVal()->get_seq_number() == next_seq) { - list->insertAfter(rit, act); - break; + return list->insertAfter(rit, act); } } + return NULL; } } -void insertIntoActionListAndSetCV(action_list_t *list, ModelAction *act) { +sllnode* 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); + return NULL; } else if (rit->getVal()->get_seq_number() == next_seq) { act->create_cv(rit->getVal()); - list->push_back(act); + return list->add_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; + return list->insertAfter(rit, act); } } + return NULL; } } @@ -1252,10 +1193,7 @@ void insertIntoActionListAndSetCV(action_list_t *list, ModelAction *act) { 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); + act->setTraceRef(insertIntoActionListAndSetCV(&action_trace, 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()); @@ -1265,7 +1203,7 @@ void ModelExecution::add_normal_write_to_lists(ModelAction *act) for(uint i=oldsize;inext_thread_id;i++) new (&(*vec)[i]) action_list_t(); } - insertIntoActionList(&(*vec)[tid],act); + act->setThrdMapRef(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()) @@ -1282,7 +1220,7 @@ void ModelExecution::add_write_to_lists(ModelAction *write) { for(uint i=oldsize;inext_thread_id;i++) new (&(*vec)[i]) action_list_t(); } - (*vec)[tid].push_back(write); + write->setActionRef((*vec)[tid].add_back(write)); } /** @@ -1375,6 +1313,9 @@ ModelAction * ModelExecution::get_last_unlock(ModelAction *curr) const void *location = curr->get_location(); action_list_t *list = obj_map.get(location); + if (list == NULL) + return NULL; + /* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */ sllnode* rit; for (rit = list->end();rit != NULL;rit=rit->getPrev()) @@ -1488,25 +1429,6 @@ SnapVector * ModelExecution::build_may_read_from(ModelAction *cu return rf_set; } -/** - * @brief Get an action representing an uninitialized atomic - * - * 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(ModelAction *curr) const -{ - ModelAction *act = curr->get_uninit_action(); - if (!act) { - act = new ModelAction(ATOMIC_UNINIT, std::memory_order_relaxed, curr->get_location(), params->uninitvalue, model_thread); - curr->set_uninit_action(act); - } - act->create_cv(NULL); - return act; -} - static void print_list(action_list_t *list) { sllnode *it; @@ -1718,6 +1640,150 @@ Thread * ModelExecution::take_step(ModelAction *curr) return action_select_next_thread(curr); } +void ModelExecution::removeAction(ModelAction *act) { + { + sllnode * listref = act->getTraceRef(); + if (listref != NULL) { + action_trace.erase(listref); + } + } + { + sllnode * listref = act->getThrdMapRef(); + if (listref != NULL) { + SnapVector *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location()); + (*vec)[act->get_tid()].erase(listref); + } + } + if ((act->is_fence() && act->is_seqcst()) || act->is_unlock()) { + sllnode * listref = act->getActionRef(); + if (listref != NULL) { + action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location()); + list->erase(listref); + } + } else if (act->is_wait()) { + sllnode * listref = act->getActionRef(); + if (listref != NULL) { + void *mutex_loc = (void *) act->get_value(); + get_safe_ptr_action(&obj_map, mutex_loc)->erase(listref); + } + } else if (act->is_write()) { + sllnode * listref = act->getActionRef(); + if (listref != NULL) { + SnapVector *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, act->get_location()); + (*vec)[act->get_tid()].erase(listref); + } + //Remove from Cyclegraph + mo_graph->freeAction(act); + } +} + +ClockVector * ModelExecution::computeMinimalCV() { + ClockVector *cvmin = NULL; + for(unsigned int i = 0;i < thread_map.size();i++) { + Thread * t = thread_map[i]; + if (t->get_state() == THREAD_COMPLETED) + continue; + thread_id_t tid = int_to_id(i); + ClockVector * cv = get_cv(tid); + if (cvmin == NULL) + cvmin = new ClockVector(cv, NULL); + else + cvmin->minmerge(cv); + } + return cvmin; +} + +void ModelExecution::collectActions() { + //Compute minimal clock vector for all live threads + ClockVector *cvmin = computeMinimalCV(); + SnapVector * queue = new SnapVector(); + //walk action trace... When we hit an action, see if it is + //invisible (e.g., earlier than the first before the minimum + //clock for the thread... if so erase it and all previous + //actions in cyclegraph + for (sllnode* it = action_trace.begin();it != NULL;it=it->getNext()) { + ModelAction *act = it->getVal(); + modelclock_t actseq = act->get_seq_number(); + thread_id_t act_tid = act->get_tid(); + modelclock_t tid_clock = cvmin->getClock(act_tid); + if (actseq <= tid_clock) { + ModelAction * write; + if (act->is_write()) { + write = act; + } else if (act->is_read()) { + write = act->get_reads_from(); + } else + continue; + + //Mark everything earlier in MO graph to be freed + queue->push_back(mo_graph->getNode_noCreate(write)); + while(!queue->empty()) { + CycleNode * node = queue->back(); + queue->pop_back(); + for(unsigned int i=0;igetNumInEdges();i++) { + CycleNode * prevnode = node->getInEdge(i); + ModelAction * prevact = prevnode->getAction(); + if (prevact->get_type() != READY_FREE) { + prevact->set_free(); + queue->push_back(prevnode); + } + } + } + } + } + for (sllnode* it = action_trace.end();it != NULL;it=it->getPrev()) { + ModelAction *act = it->getVal(); + if (act->is_free()) { + removeAction(act); + delete act; + } else if (act->is_read()) { + if (act->get_reads_from()->is_free()) { + removeAction(act); + delete act; + } else { + const ModelAction *rel_fence =act->get_last_fence_release(); + if (rel_fence != NULL) { + modelclock_t relfenceseq = rel_fence->get_seq_number(); + thread_id_t relfence_tid = rel_fence->get_tid(); + modelclock_t tid_clock = cvmin->getClock(relfence_tid); + //Remove references to irrelevant release fences + if (relfenceseq <= tid_clock) + act->set_last_fence_release(NULL); + } + } + } else if (act->is_fence()) { + //Note that acquire fences can always be safely + //removed, but could incur extra overheads in + //traversals. Removing them before the cvmin seems + //like a good compromise. + + //Release fences before the cvmin don't do anything + //because everyone has already synchronized. + + //Sequentially fences before cvmin are redundant + //because happens-before will enforce same + //orderings. + + modelclock_t actseq = act->get_seq_number(); + thread_id_t act_tid = act->get_tid(); + modelclock_t tid_clock = cvmin->getClock(act_tid); + if (actseq <= tid_clock) { + removeAction(act); + delete act; + } + } else { + //need to deal with lock, annotation, wait, notify, thread create, start, join, yield, finish + //lock, notify thread create, thread finish, yield, finish are dead as soon as they are in the trace + //need to keep most recent unlock/wait for each lock + } + } + + delete cvmin; + delete queue; +} + + + Fuzzer * ModelExecution::getFuzzer() { return fuzzer; }