X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=execution.cc;h=48c73cfbeca2db10dd19148062bded4bfd9858e7;hp=8057aa99cfa97d82b95c3821ee0119981a6d579f;hb=8b57ab066a2b74a81c4261482ba9030465eb0dbe;hpb=1371ca80e0012e533ad450f955cb95d3d9dcc862 diff --git a/execution.cc b/execution.cc index 8057aa99..48c73cfb 100644 --- a/execution.cc +++ b/execution.cc @@ -53,12 +53,15 @@ ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) : scheduler(scheduler), thread_map(2), /* We'll always need at least 2 threads */ pthread_map(0), - pthread_counter(1), + pthread_counter(2), action_trace(), obj_map(), condvar_waiters_map(), obj_thrd_map(), + obj_wr_thrd_map(), + obj_last_sc_map(), mutex_map(), + cond_map(), thrd_last_action(1), thrd_last_fence_release(), priv(new struct model_snapshot_members ()), @@ -373,6 +376,8 @@ bool ModelExecution::process_mutex(ModelAction *curr) //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"); + + // TODO: lock count for recursive mutexes state->locked = get_thread(curr); ModelAction *unlock = get_last_unlock(curr); //synchronize with the previous unlock statement @@ -396,8 +401,17 @@ bool ModelExecution::process_mutex(ModelAction *curr) /* unlock the lock - after checking who was waiting on it */ state->locked = NULL; - /* disable this thread */ - get_safe_ptr_action(&condvar_waiters_map, curr->get_location())->push_back(curr); + /* remove old wait action and disable this thread */ + action_list_t * waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location()); + for (sllnode * it = waiters->begin(); it != NULL; it = it->getNext()) { + ModelAction * wait = it->getVal(); + if (wait->get_tid() == curr->get_tid()) { + waiters->erase(it); + break; + } + } + + waiters->push_back(curr); scheduler->sleep(get_thread(curr)); } @@ -414,6 +428,7 @@ bool ModelExecution::process_mutex(ModelAction *curr) //FAILS AND IN THE CASE IT DOESN'T... TIMED WAITS //MUST EVENMTUALLY RELEASE... + // TODO: lock count for recursive mutexes /* wake up the other threads */ for (unsigned int i = 0;i < get_num_threads();i++) { Thread *t = get_thread(int_to_id(i)); @@ -688,8 +703,15 @@ bool ModelExecution::check_action_enabled(ModelAction *curr) { if (curr->is_lock()) { cdsc::mutex *lock = curr->get_mutex(); struct cdsc::mutex_state *state = lock->get_state(); - if (state->locked) + if (state->locked) { + Thread *lock_owner = (Thread *)state->locked; + Thread *curr_thread = get_thread(curr); + if (lock_owner == curr_thread && state->type == PTHREAD_MUTEX_RECURSIVE) { + return true; + } + return false; + } } else if (curr->is_thread_join()) { Thread *blocking = curr->get_thread_operand(); if (!blocking->is_complete()) { @@ -1524,6 +1546,40 @@ void ModelExecution::print_summary() } +void ModelExecution::print_tail() +{ + model_print("Execution trace %d:\n", get_execution_number()); + + sllnode *it; + + model_print("------------------------------------------------------------------------------------\n"); + model_print("# t Action type MO Location Value Rf CV\n"); + model_print("------------------------------------------------------------------------------------\n"); + + unsigned int hash = 0; + + int length = 25; + int counter = 0; + SnapList list; + for (it = action_trace.end(); it != NULL; it = it->getPrev()) { + if (counter > length) + break; + + ModelAction * act = it->getVal(); + list.push_front(act); + counter++; + } + + 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->getVal()->hash()); + } + model_print("HASH %u\n", hash); + model_print("------------------------------------------------------------------------------------\n"); +} + /** * Add a Thread to the system for the first time. Should only be called once * per thread. @@ -1568,14 +1624,21 @@ Thread * ModelExecution::get_thread(const ModelAction *act) const * @return A Thread reference */ Thread * ModelExecution::get_pthread(pthread_t pid) { + // pid 1 is reserved for the main thread, pthread ids should start from 2 + if (pid == 1) + return get_thread(pid); + 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; + + if (thread_id < pthread_counter + 1) + return pthread_map[thread_id]; + else + return NULL; } /** @@ -1612,7 +1675,7 @@ bool ModelExecution::is_enabled(thread_id_t tid) const Thread * ModelExecution::action_select_next_thread(const ModelAction *curr) const { /* Do not split atomic RMW */ - if (curr->is_rmwr() && !paused_by_fuzzer(curr)) + if (curr->is_rmwr()) return get_thread(curr); /* Follow CREATE with the created thread */ /* which is not needed, because model.cc takes care of this */ @@ -1624,15 +1687,6 @@ Thread * ModelExecution::action_select_next_thread(const ModelAction *curr) cons return NULL; } -/** @param act A read atomic action */ -bool ModelExecution::paused_by_fuzzer(const ModelAction * act) const -{ - ASSERT(act->is_read()); - - // Actions paused by fuzzer have their sequence number reset to 0 - return act->get_seq_number() == 0; -} - /** * Takes the next step in the execution, if possible. * @param curr The current step to take @@ -1735,6 +1789,9 @@ void ModelExecution::fixupLastAct(ModelAction *act) { /** Compute which actions to free. */ void ModelExecution::collectActions() { + if (priv->used_sequence_numbers < params->traceminsize) + return; + //Compute minimal clock vector for all live threads ClockVector *cvmin = computeMinimalCV(); SnapVector * queue = new SnapVector(); @@ -1809,6 +1866,7 @@ void ModelExecution::collectActions() { if (islastact) { fixupLastAct(act); } + delete act; continue; }