X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=execution.cc;h=9ef071209cbefc9020b662a3ded0d8409b958bf1;hb=HEAD;hp=c329b8c48f00169dec9a945949e55b1ca38eba3c;hpb=bf698c32ac174a4dcfce69ad78cccf2a65e3bf92;p=c11tester.git diff --git a/execution.cc b/execution.cc index c329b8c4..9ef07120 100644 --- a/execution.cc +++ b/execution.cc @@ -2,6 +2,7 @@ #include #include #include +#include #include "model.h" #include "execution.h" @@ -13,11 +14,7 @@ #include "datarace.h" #include "threads-model.h" #include "bugmessage.h" -#include "history.h" #include "fuzzer.h" -#include "newfuzzer.h" - -#define INITIAL_THREAD_ID 0 #ifdef COLLECT_STAT static unsigned int atomic_load_count = 0; @@ -80,11 +77,7 @@ ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) : thrd_last_fence_release(), priv(new struct model_snapshot_members ()), mo_graph(new CycleGraph()), -#ifdef NEWFUZZER - fuzzer(new NewFuzzer()), -#else fuzzer(new Fuzzer()), -#endif isfinished(false) { /* Initialize a model-checker thread, for special ModelActions */ @@ -100,7 +93,7 @@ ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) : /** @brief Destructor */ ModelExecution::~ModelExecution() { - for (unsigned int i = 0;i < get_num_threads();i++) + for (unsigned int i = INITIAL_THREAD_ID;i < get_num_threads();i++) delete get_thread(int_to_id(i)); delete mo_graph; @@ -247,44 +240,54 @@ void ModelExecution::restore_last_seq_num() * @param thread The thread that we might wake up * @return True, if we should wake up the sleeping thread; false otherwise */ -bool ModelExecution::should_wake_up(const ModelAction *curr, const Thread *thread) const +bool ModelExecution::should_wake_up(const ModelAction * asleep) const { - const ModelAction *asleep = thread->get_pending(); - /* Don't allow partial RMW to wake anyone up */ - if (curr->is_rmwr()) - return false; - /* Synchronizing actions may have been backtracked */ - if (asleep->could_synchronize_with(curr)) - return true; - /* All acquire/release fences and fence-acquire/store-release */ - if (asleep->is_fence() && asleep->is_acquire() && curr->is_release()) - return true; - /* Fence-release + store can awake load-acquire on the same location */ - if (asleep->is_read() && asleep->is_acquire() && curr->same_var(asleep) && curr->is_write()) { - ModelAction *fence_release = get_last_fence_release(curr->get_tid()); - if (fence_release && *(get_last_action(thread->get_id())) < *fence_release) - return true; - } /* The sleep is literally sleeping */ - if (asleep->is_sleep()) { - if (fuzzer->shouldWake(asleep)) - return true; + switch (asleep->get_type()) { + case THREAD_SLEEP: + if (fuzzer->shouldWake(asleep)) + return true; + break; + case ATOMIC_WAIT: + case ATOMIC_TIMEDWAIT: + if (fuzzer->waitShouldWakeUp(asleep)) + return true; + break; + default: + return false; } return false; } -void ModelExecution::wake_up_sleeping_actions(ModelAction *curr) +void ModelExecution::wake_up_sleeping_actions() { - for (unsigned int i = 0;i < get_num_threads();i++) { + for (unsigned int i = MAIN_THREAD_ID;i < get_num_threads();i++) { thread_id_t tid = int_to_id(i); - Thread *thr = get_thread(tid); if (scheduler->is_sleep_set(tid)) { - if (should_wake_up(curr, thr)) { + Thread *thr = get_thread(tid); + ModelAction * pending = thr->get_pending(); + if (should_wake_up(pending)) { /* Remove this thread from sleep set */ scheduler->remove_sleep(thr); - if (thr->get_pending()->is_sleep()) + + if (pending->is_sleep()) { + thr->set_wakeup_state(true); + } else if (pending->is_wait()) { thr->set_wakeup_state(true); + /* Remove this thread from list of waiters */ + simple_action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, pending->get_location()); + for (sllnode * rit = waiters->begin();rit != NULL;rit=rit->getNext()) { + if (rit->getVal()->get_tid() == tid) { + waiters->erase(rit); + break; + } + } + + /* Set ETIMEDOUT error */ + if (pending->is_timedwait()) + thr->set_return_value(ETIMEDOUT); + } } } } @@ -338,7 +341,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 = MAIN_THREAD_ID;i < get_num_threads();i++) { thread_id_t tid = int_to_id(i); if (is_enabled(tid)) return false; @@ -358,7 +361,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 = MAIN_THREAD_ID;i < get_num_threads();i++) if (is_enabled(int_to_id(i))) return false; return true; @@ -375,9 +378,6 @@ ModelAction * ModelExecution::convertNonAtomicStore(void * location) { add_normal_write_to_lists(act); add_write_to_lists(act); w_modification_order(act); -#ifdef NEWFUZZER - model->get_history()->process_action(act, act->get_tid()); -#endif return act; } @@ -420,10 +420,10 @@ bool ModelExecution::process_read(ModelAction *curr, SnapVector * mo_graph->addEdge((*priorset)[i], rf); } read_from(curr, rf); - get_thread(curr)->set_return_value(curr->get_return_value()); + get_thread(curr)->set_return_value(rf->get_write_value()); delete priorset; //Update acquire fence clock vector - ClockVector * hbcv = get_hb_from_write(curr->get_reads_from()); + ClockVector * hbcv = get_hb_from_write(rf); if (hbcv != NULL) get_thread(curr)->get_acq_fence_cv()->merge(hbcv); return canprune && (curr->get_type() == ATOMIC_READ); @@ -485,51 +485,59 @@ bool ModelExecution::process_mutex(ModelAction *curr) break; } case ATOMIC_WAIT: { - //TODO: DOESN'T REALLY IMPLEMENT SPURIOUS WAKEUPS CORRECTLY - if (fuzzer->shouldWait(curr)) { - /* wake up the other threads */ - 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()) - scheduler->wake(t); - } + Thread *curr_thrd = get_thread(curr); + /* wake up the other threads */ + for (unsigned int i = MAIN_THREAD_ID;i < get_num_threads();i++) { + Thread *t = get_thread(int_to_id(i)); + if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock()) + scheduler->wake(t); + } - /* unlock the lock - after checking who was waiting on it */ - state->locked = NULL; + /* unlock the lock - after checking who was waiting on it */ + state->locked = NULL; - /* remove old wait action and disable this thread */ - simple_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; - } - } + /* disable this thread */ + simple_action_list_t * waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location()); + waiters->push_back(curr); + curr_thrd->set_pending(curr); // Forbid this thread to stash a new action + + if (fuzzer->waitShouldFail(curr)) // If wait should fail spuriously, + scheduler->add_sleep(curr_thrd); // place this thread into THREAD_SLEEP_SET + else + scheduler->sleep(curr_thrd); + + break; + } + case ATOMIC_TIMEDWAIT: { + Thread *curr_thrd = get_thread(curr); + if (!fuzzer->randomizeWaitTime(curr)) { + curr_thrd->set_return_value(ETIMEDOUT); + return false; + } - waiters->push_back(curr); - scheduler->sleep(get_thread(curr)); + /* wake up the other threads */ + for (unsigned int i = MAIN_THREAD_ID;i < get_num_threads();i++) { + Thread *t = get_thread(int_to_id(i)); + if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock()) + scheduler->wake(t); } + /* unlock the lock - after checking who was waiting on it */ + state->locked = NULL; + + /* disable this thread */ + simple_action_list_t * waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location()); + waiters->push_back(curr); + curr_thrd->set_pending(curr); // Forbid this thread to stash a new action + scheduler->add_sleep(curr_thrd); break; } - case ATOMIC_TIMEDWAIT: case ATOMIC_UNLOCK: { - //TODO: FIX WAIT SITUATION...WAITS CAN SPURIOUSLY - //FAIL...TIMED WAITS SHOULD PROBABLY JUST BE THE SAME - //AS NORMAL WAITS...THINK ABOUT PROBABILITIES - //THOUGH....AS IN TIMED WAIT MUST FAIL TO GUARANTEE - //PROGRESS...NORMAL WAIT MAY FAIL...SO NEED NORMAL - //WAIT TO WORK CORRECTLY IN THE CASE IT SPURIOUSLY - //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 *curr_thrd = get_thread(curr); + for (unsigned int i = MAIN_THREAD_ID;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()) scheduler->wake(t); } @@ -542,7 +550,10 @@ bool ModelExecution::process_mutex(ModelAction *curr) simple_action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location()); //activate all the waiting threads for (sllnode * rit = waiters->begin();rit != NULL;rit=rit->getNext()) { - scheduler->wake(get_thread(rit->getVal())); + Thread * thread = get_thread(rit->getVal()); + if (thread->get_state() != THREAD_COMPLETED) + scheduler->wake(thread); + thread->set_wakeup_state(true); } waiters->clear(); break; @@ -551,7 +562,9 @@ bool ModelExecution::process_mutex(ModelAction *curr) simple_action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location()); if (waiters->size() != 0) { Thread * thread = fuzzer->selectNotify(waiters); - scheduler->wake(thread); + if (thread->get_state() != THREAD_COMPLETED) + scheduler->wake(thread); + thread->set_wakeup_state(true); } break; } @@ -655,7 +668,7 @@ void ModelExecution::process_thread_action(ModelAction *curr) } /* Wake up any joining threads */ - for (unsigned int i = 0;i < get_num_threads();i++) { + for (unsigned int i = MAIN_THREAD_ID;i < get_num_threads();i++) { Thread *waiting = get_thread(int_to_id(i)); if (waiting->waiting_on() == th && waiting->get_pending()->is_thread_join()) @@ -770,7 +783,8 @@ bool ModelExecution::synchronize(const ModelAction *first, ModelAction *second) * @return a bool that indicates whether the action is enabled. */ bool ModelExecution::check_action_enabled(ModelAction *curr) { - if (curr->is_lock()) { + switch (curr->get_type()) { + case ATOMIC_LOCK: { cdsc::mutex *lock = curr->get_mutex(); struct cdsc::mutex_state *state = lock->get_state(); if (state->locked) { @@ -782,14 +796,23 @@ bool ModelExecution::check_action_enabled(ModelAction *curr) { return false; } - } else if (curr->is_thread_join()) { + break; + } + case THREAD_JOIN: + case PTHREAD_JOIN: { Thread *blocking = curr->get_thread_operand(); if (!blocking->is_complete()) { return false; } - } else if (curr->is_sleep()) { + break; + } + case THREAD_SLEEP: { if (!fuzzer->shouldSleep(curr)) return false; + break; + } + default: + return true; } return true; @@ -813,7 +836,7 @@ ModelAction * ModelExecution::check_current_action(ModelAction *curr) DBG(); - wake_up_sleeping_actions(curr); + wake_up_sleeping_actions(); SnapVector * rf_set = NULL; bool canprune = false; @@ -1111,43 +1134,6 @@ void ModelExecution::w_modification_order(ModelAction *curr) } -/** - * Arbitrary reads from the future are not allowed. Section 29.3 part 9 places - * some constraints. This method checks one the following constraint (others - * require compiler support): - * - * If X --hb-> Y --mo-> Z, then X should not read from Z. - * If X --hb-> Y, A --rf-> Y, and A --mo-> Z, then X should not read from Z. - */ -bool ModelExecution::mo_may_allow(const ModelAction *writer, const ModelAction *reader) -{ - 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++) { - const ModelAction *write_after_read = NULL; - - /* Iterate over actions in thread, starting from most recent */ - action_list_t *list = &(*thrd_lists)[i]; - 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) - break; - else if (act->is_write()) - write_after_read = act; - else if (act->is_read() && act->get_reads_from() != NULL) - write_after_read = act->get_reads_from(); - } - - if (write_after_read && write_after_read != writer && mo_graph->checkReachable(write_after_read, writer)) - return false; - } - return true; -} - /** * Computes the clock vector that happens before propagates from this write. * @@ -1755,9 +1741,6 @@ Thread * ModelExecution::take_step(ModelAction *curr) ASSERT(curr); /* Process this action in ModelHistory for records */ -#ifdef NEWFUZZER - model->get_history()->process_action( curr, curr->get_tid() ); -#endif if (curr_thrd->is_blocked() || curr_thrd->is_complete()) scheduler->remove_thread(curr_thrd);