X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=execution.cc;h=f6b59cd9bda059c194c473bf376564c0ee343b9d;hp=e04b672a28d1a08e9e5991bacc3aa25826d3dbc9;hb=0229244d21ca78bf781e41684810e9fb6d5ca56c;hpb=1f817417cb820f356fb2afa7ac9e18d7ef054198 diff --git a/execution.cc b/execution.cc index e04b672a..f6b59cd9 100644 --- a/execution.cc +++ b/execution.cc @@ -1,6 +1,5 @@ #include #include -#include #include #include @@ -30,9 +29,11 @@ struct model_snapshot_members { next_backtrack(NULL), bugs(), failed_promise(false), + hard_failed_promise(false), too_many_reads(false), no_valid_reads(false), bad_synchronization(false), + bad_sc_read(false), asserted(false) { } @@ -47,10 +48,12 @@ struct model_snapshot_members { ModelAction *next_backtrack; SnapVector bugs; bool failed_promise; + bool hard_failed_promise; bool too_many_reads; bool no_valid_reads; /** @brief Incorrectly-ordered synchronization was made */ bool bad_synchronization; + bool bad_sc_read; bool asserted; SNAPSHOTALLOC @@ -66,9 +69,12 @@ ModelExecution::ModelExecution(ModelChecker *m, scheduler(scheduler), action_trace(), thread_map(2), /* We'll always need at least 2 threads */ + pthread_map(0), + pthread_counter(0), obj_map(), condvar_waiters_map(), obj_thrd_map(), + mutex_map(), promises(), futurevalues(), pending_rel_seqs(), @@ -79,8 +85,8 @@ ModelExecution::ModelExecution(ModelChecker *m, mo_graph(new CycleGraph()) { /* Initialize a model-checker thread, for special ModelActions */ - model_thread = new Thread(get_next_id()); - add_thread(model_thread); + model_thread = new Thread(get_next_id()); // L: Create model thread + add_thread(model_thread); // L: Add model thread to scheduler scheduler->register_engine(this); node_stack->register_engine(this); } @@ -200,6 +206,13 @@ 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)); @@ -674,8 +687,8 @@ bool ModelExecution::process_read(ModelAction *curr) */ bool ModelExecution::process_mutex(ModelAction *curr) { - std::mutex *mutex = curr->get_mutex(); - struct std::mutex_state *state = NULL; + cdsc::mutex *mutex = curr->get_mutex(); + struct cdsc::mutex_state *state = NULL; if (mutex) state = mutex->get_state(); @@ -755,12 +768,13 @@ bool ModelExecution::process_mutex(ModelAction *curr) /** * @brief Check if the current pending promises allow a future value to be sent * - * If one of the following is true: - * (a) there are no pending promises - * (b) the reader and writer do not cross any promises - * Then, it is safe to pass a future value back now. + * It is unsafe to pass a future value back if there exists a pending promise Pr + * such that: + * + * reader --exec-> Pr --exec-> writer * - * Otherwise, we must save the pending future value until (a) or (b) is true + * If such Pr exists, we must save the pending future value until Pr is + * resolved. * * @param writer The operation which sends the future value. Must be a write. * @param reader The operation which will observe the value. Must be a read. @@ -769,8 +783,6 @@ bool ModelExecution::process_mutex(ModelAction *curr) bool ModelExecution::promises_may_allow(const ModelAction *writer, const ModelAction *reader) const { - if (promises.empty()) - return true; for (int i = promises.size() - 1; i >= 0; i--) { ModelAction *pr = promises[i]->get_reader(0); //reader is after promise...doesn't cross any promise @@ -937,6 +949,7 @@ bool ModelExecution::process_thread_action(ModelAction *curr) thrd_t *thrd = (thrd_t *)curr->get_location(); struct thread_params *params = (struct thread_params *)curr->get_value(); Thread *th = new Thread(get_next_id(), thrd, params->func, params->arg, get_thread(curr)); + curr->set_thread_operand(th); add_thread(th); th->set_creation(curr); /* Promises can be satisfied by children */ @@ -947,6 +960,28 @@ bool ModelExecution::process_thread_action(ModelAction *curr) } break; } + case PTHREAD_CREATE: { + (*(pthread_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)); + curr->set_thread_operand(th); + add_thread(th); + th->set_creation(curr); + + if ( pthread_map.size() < pthread_counter ) + pthread_map.resize( pthread_counter ); + pthread_map[ pthread_counter-1 ] = th; + + /* Promises can be satisfied by children */ + for (unsigned int i = 0; i < promises.size(); i++) { + Promise *promise = promises[i]; + if (promise->thread_is_available(curr->get_tid())) + promise->add_thread(th->get_id()); + } + + break; + } case THREAD_JOIN: { Thread *blocking = curr->get_thread_operand(); ModelAction *act = get_last_action(blocking->get_id()); @@ -954,6 +989,14 @@ bool ModelExecution::process_thread_action(ModelAction *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 THREAD_FINISH: { Thread *th = get_thread(curr); /* Wake up any joining threads */ @@ -1122,6 +1165,7 @@ bool ModelExecution::initialize_curr_action(ModelAction **curr) * * @return True if this read established synchronization */ + bool ModelExecution::read_from(ModelAction *act, const ModelAction *rf) { ASSERT(rf); @@ -1204,8 +1248,8 @@ void ModelExecution::thread_blocking_check_promises(Thread *blocker, Thread *wai */ bool ModelExecution::check_action_enabled(ModelAction *curr) { if (curr->is_lock()) { - std::mutex *lock = curr->get_mutex(); - struct std::mutex_state *state = lock->get_state(); + cdsc::mutex *lock = curr->get_mutex(); + struct cdsc::mutex_state *state = lock->get_state(); if (state->locked) return false; } else if (curr->is_thread_join()) { @@ -1305,6 +1349,12 @@ ModelAction * ModelExecution::check_current_action(ModelAction *curr) if (rf) { if (r_modification_order(act, rf)) updated = true; + if (act->is_seqcst()) { + ModelAction *last_sc_write = get_last_seq_cst_write(act); + if (last_sc_write != NULL && rf->happens_before(last_sc_write)) { + set_bad_sc_read(); + } + } } else if (promise) { if (r_modification_order(act, promise)) updated = true; @@ -1376,7 +1426,7 @@ void ModelExecution::print_infeasibility(const char *prefix) const char *ptr = buf; if (mo_graph->checkForCycles()) ptr += sprintf(ptr, "[mo cycle]"); - if (priv->failed_promise) + if (priv->failed_promise || priv->hard_failed_promise) ptr += sprintf(ptr, "[failed promise]"); if (priv->too_many_reads) ptr += sprintf(ptr, "[too many reads]"); @@ -1384,6 +1434,8 @@ void ModelExecution::print_infeasibility(const char *prefix) const 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 (promises_expired()) ptr += sprintf(ptr, "[promise expired]"); if (promises.size() != 0) @@ -1398,7 +1450,8 @@ void ModelExecution::print_infeasibility(const char *prefix) const */ bool ModelExecution::is_feasible_prefix_ignore_relseq() const { - return !is_infeasible() && promises.size() == 0; + return !is_infeasible() && promises.size() == 0 && ! priv->failed_promise; + } /** @@ -1411,9 +1464,10 @@ bool ModelExecution::is_infeasible() const { return mo_graph->checkForCycles() || priv->no_valid_reads || - priv->failed_promise || priv->too_many_reads || priv->bad_synchronization || + priv->bad_sc_read || + priv->hard_failed_promise || promises_expired(); } @@ -1614,12 +1668,6 @@ bool ModelExecution::r_modification_order(ModelAction *curr, const rf_type *rf) } } - /* C++, Section 29.3 statement 3 (second subpoint) */ - if (curr->is_seqcst() && last_sc_write && act == last_sc_write) { - added = mo_graph->addEdge(act, rf) || added; - break; - } - /* * Include at most one act per-thread that "happens * before" curr @@ -1751,9 +1799,10 @@ bool ModelExecution::w_modification_order(ModelAction *curr, ModelVectoraddEdge(act, curr) || added; else if (act->is_read()) { //if previous read accessed a null, just keep going - if (act->get_reads_from() == NULL) - continue; - added = mo_graph->addEdge(act->get_reads_from(), curr) || added; + if (act->get_reads_from() == NULL) { + added = mo_graph->addEdge(act->get_reads_from_promise(), curr) || added; + } else + added = mo_graph->addEdge(act->get_reads_from(), curr) || added; } break; } else if (act->is_read() && !act->could_synchronize_with(curr) && @@ -1770,7 +1819,8 @@ bool ModelExecution::w_modification_order(ModelAction *curr, ModelVectorpush_back(act); else if (curr->is_rmw() && act->is_rmw() && curr->get_reads_from() && curr->get_reads_from() == act->get_reads_from()) @@ -1792,6 +1842,50 @@ bool ModelExecution::w_modification_order(ModelAction *curr, ModelVectorget_tid(); + for(unsigned int i = promises.size(); i>0; i--) { + Promise *pr=promises[i-1]; + if (!pr->same_location(write)) + continue; + //the reading thread is the only thread that can resolve the promise + if (pr->get_num_was_available_threads()==1 && pr->thread_was_available(read->get_tid())) { + for(unsigned int j=0;jget_num_readers();j++) { + ModelAction *prreader=pr->get_reader(j); + //the writing thread reads from the promise before the write + if (prreader->get_tid()==write_tid && + (*prreader)<(*write)) { + if ((*read)>(*prreader)) { + //check that we don't have a read between the read and promise + //from the same thread as read + bool okay=false; + for(const ModelAction *tmp=read;tmp!=prreader;) { + tmp=tmp->get_node()->get_parent()->get_action(); + if (tmp->is_read() && tmp->same_thread(read)) { + okay=true; + break; + } + } + if (okay) + continue; + } + return false; + } + } + } + } + return true; +} + + /** Arbitrary reads from the future are not allowed. Section 29.3 * part 9 places some constraints. This method checks one result of constraint * constraint. Others require compiler support. */ @@ -2287,6 +2381,7 @@ ModelAction * ModelExecution::get_last_seq_cst_fence(thread_id_t tid, const Mode ModelAction * ModelExecution::get_last_unlock(ModelAction *curr) const { void *location = curr->get_location(); + 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; @@ -2354,7 +2449,7 @@ bool ModelExecution::resolve_promise(ModelAction *write, Promise *promise, /* Make sure the promise's value matches the write's value */ ASSERT(promise->is_compatible(write) && promise->same_value(write)); if (!mo_graph->resolvePromise(promise, write)) - priv->failed_promise = true; + priv->hard_failed_promise = true; /** * @todo It is possible to end up in an inconsistent state, where a @@ -2466,7 +2561,7 @@ void ModelExecution::mo_check_promises(const ModelAction *act, bool is_read_chec if (!pread->happens_before(act)) continue; if (mo_graph->checkPromise(write, promise)) { - priv->failed_promise = true; + priv->hard_failed_promise = true; return; } break; @@ -2478,7 +2573,7 @@ void ModelExecution::mo_check_promises(const ModelAction *act, bool is_read_chec if (mo_graph->checkReachable(promise, write)) { if (mo_graph->checkPromise(write, promise)) { - priv->failed_promise = true; + priv->hard_failed_promise = true; return; } } @@ -2632,7 +2727,7 @@ static void print_list(const action_list_t *list) action_list_t::const_iterator it; model_print("------------------------------------------------------------------------------------\n"); - model_print("# t Action type MO Location Value Rf CV\n"); + model_print("# t Action type MO Location Value Rf CV\n"); model_print("------------------------------------------------------------------------------------\n"); unsigned int hash = 0; @@ -2761,6 +2856,16 @@ Thread * ModelExecution::get_thread(const ModelAction *act) const return get_thread(act->get_tid()); } +/** + * @brief Get a Thread reference by its pthread ID + * @param index The pthread's ID + * @return A Thread reference + */ +Thread * ModelExecution::get_pthread(pthread_t pid) { + if (pid < pthread_counter + 1) return pthread_map[pid]; + else return NULL; +} + /** * @brief Get a Promise's "promise number" * @@ -2817,9 +2922,26 @@ 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); +// defalut: +// return NULL; +// } + 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(); + if (curr->get_type() == PTHREAD_CREATE) { return curr->get_thread_operand(); + } return NULL; }