X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=model.cc;h=a96a79c851ee83b5624df3bdafda7487802bf5b1;hp=f8482cbf7b9db9eb9689a213c5de18cf3b583ad9;hb=1b793f0683aff025afe2e19519572e3599575a19;hpb=b6f06ab2c626eb6e0f044fa9c7d1b74fbc82a09d diff --git a/model.cc b/model.cc index f8482cbf..a96a79c8 100644 --- a/model.cc +++ b/model.cc @@ -12,7 +12,7 @@ #include "promise.h" #include "datarace.h" #include "mutex.h" -#include "threads.h" +#include "threads-model.h" #define INITIAL_THREAD_ID 0 @@ -116,6 +116,10 @@ modelclock_t ModelChecker::get_next_seq_num() return ++priv->used_sequence_numbers; } +Node * ModelChecker::get_curr_node() { + return node_stack->get_head(); +} + /** * @brief Choose the next thread to execute. * @@ -260,7 +264,8 @@ bool ModelChecker::next_execution() DEBUG("Number of acquires waiting on pending release sequences: %zu\n", pending_rel_seqs->size()); - if (isfinalfeasible() || DBG_ENABLED()) + + if (isfinalfeasible() || (params.bound != 0 && priv->used_sequence_numbers > params.bound ) || DBG_ENABLED() ) print_summary(); if ((diverge = get_next_backtrack()) == NULL) @@ -519,7 +524,9 @@ bool ModelChecker::process_write(ModelAction *curr) if (promises->size() == 0) { for (unsigned int i = 0; i < futurevalues->size(); i++) { struct PendingFutureValue pfv = (*futurevalues)[i]; - if (pfv.act->get_node()->add_future_value(pfv.value, pfv.expiration) && + //Do more ambitious checks now that mo is more complete + if (mo_may_allow(pfv.writer, pfv.act)&& + pfv.act->get_node()->add_future_value(pfv.writer->get_value(), pfv.writer->get_seq_number()+params.maxfuturedelay) && (!priv->next_backtrack || *pfv.act > *priv->next_backtrack)) priv->next_backtrack = pfv.act; } @@ -555,26 +562,17 @@ bool ModelChecker::process_thread_action(ModelAction *curr) break; } case THREAD_JOIN: { - Thread *waiting, *blocking; - waiting = get_thread(curr); - blocking = (Thread *)curr->get_location(); - if (!blocking->is_complete()) { - blocking->push_wait_list(curr); - scheduler->sleep(waiting); - } else { - do_complete_join(curr); - updated = true; /* trigger rel-seq checks */ - } + Thread *blocking = (Thread *)curr->get_location(); + ModelAction *act = get_last_action(blocking->get_id()); + curr->synchronize_with(act); + updated = true; /* trigger rel-seq checks */ break; } case THREAD_FINISH: { Thread *th = get_thread(curr); while (!th->wait_list_empty()) { ModelAction *act = th->pop_wait_list(); - Thread *wake = get_thread(act); - scheduler->wake(wake); - do_complete_join(act); - updated = true; /* trigger rel-seq checks */ + scheduler->wake(get_thread(act)); } th->complete(); updated = true; /* trigger rel-seq checks */ @@ -719,9 +717,12 @@ ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr) } /** - * This method checks whether a model action is enabled at the given point. - * At this point, it checks whether a lock operation would be successful at this point. - * If not, it puts the thread in a waiter list. + * @brief Check whether a model action is enabled. + * + * Checks whether a lock or join operation would be successful (i.e., is the + * lock already locked, or is the joined thread already complete). If not, put + * the action in a waiter list. + * * @param curr is the ModelAction to check whether it is enabled. * @return a bool that indicates whether the action is enabled. */ @@ -734,6 +735,12 @@ bool ModelChecker::check_action_enabled(ModelAction *curr) { lock_waiters_map->get_safe_ptr(curr->get_location())->push_back(curr); return false; } + } else if (curr->get_type() == THREAD_JOIN) { + Thread *blocking = (Thread *)curr->get_location(); + if (!blocking->is_complete()) { + blocking->push_wait_list(curr); + return false; + } } return true; @@ -758,16 +765,15 @@ Thread * ModelChecker::check_current_action(ModelAction *curr) if (!check_action_enabled(curr)) { /* Make the execution look like we chose to run this action - * much later, when a lock is actually available to release */ + * much later, when a lock/join can succeed */ get_current_thread()->set_pending(curr); scheduler->sleep(get_current_thread()); return get_next_thread(NULL); } - wake_up_sleeping_actions(curr); - ModelAction *newcurr = initialize_curr_action(curr); + wake_up_sleeping_actions(curr); /* Add the action to lists before any other model-checking tasks */ if (!second_part_of_rmw) @@ -845,19 +851,6 @@ Thread * ModelChecker::check_current_action(ModelAction *curr) return get_next_thread(curr); } -/** - * Complete a THREAD_JOIN operation, by synchronizing with the THREAD_FINISH - * operation from the Thread it is joining with. Must be called after the - * completion of the Thread in question. - * @param join The THREAD_JOIN action - */ -void ModelChecker::do_complete_join(ModelAction *join) -{ - Thread *blocking = (Thread *)join->get_location(); - ModelAction *act = get_last_action(blocking->get_id()); - join->synchronize_with(act); -} - void ModelChecker::check_curr_backtracking(ModelAction * curr) { Node *currnode = curr->get_node(); Node *parnode = currnode->get_parent(); @@ -1248,12 +1241,16 @@ bool ModelChecker::w_modification_order(ModelAction *curr) (3) cannot synchronize with us (4) is in a different thread => - that read could potentially read from our write. + that read could potentially read from our write. Note that + these checks are overly conservative at this point, we'll + do more checks before actually removing the + pendingfuturevalue. + */ if (thin_air_constraint_may_allow(curr, act)) { if (isfeasible() || (curr->is_rmw() && act->is_rmw() && curr->get_reads_from() == act->get_reads_from() && isfeasibleotherthanRMW())) { - struct PendingFutureValue pfv = {curr->get_value(),curr->get_seq_number()+params.maxfuturedelay,act}; + struct PendingFutureValue pfv = {curr,act}; futurevalues->push_back(pfv); } } @@ -1285,6 +1282,33 @@ bool ModelChecker::thin_air_constraint_may_allow(const ModelAction * writer, con 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. */ +bool ModelChecker::mo_may_allow(const ModelAction * writer, const ModelAction *reader) { + std::vector *thrd_lists = obj_thrd_map->get_safe_ptr(reader->get_location()); + + //Get write that follows reader action + action_list_t *list = &(*thrd_lists)[id_to_int(reader->get_tid())]; + action_list_t::reverse_iterator rit; + ModelAction *first_write_after_read=NULL; + + for (rit = list->rbegin(); rit != list->rend(); rit++) { + ModelAction *act = *rit; + if (act==reader) + break; + if (act->is_write()) + first_write_after_read=act; + } + + if (first_write_after_read==NULL) + return true; + + return !mo_graph->checkReachable(first_write_after_read, writer); +} + + + /** * Finds the head(s) of the release sequence(s) containing a given ModelAction. * The ModelAction under consideration is expected to be taking part in @@ -1759,6 +1783,11 @@ void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write) //do we have a pwrite for the promise, if not, set it if (promise->get_write() == NULL ) { promise->set_write(write); + //The pwrite cannot happen before the promise + if (write->happens_before(act) && (write != act)) { + failed_promise = true; + return; + } } if (mo_graph->checkPromise(write, promise)) { failed_promise = true; @@ -1848,7 +1877,7 @@ void ModelChecker::build_reads_from_past(ModelAction *curr) curr->print(); } - if (curr->get_sleep_flag()) { + if (curr->get_sleep_flag() && ! curr->is_seqcst()) { if (sleep_can_read_from(curr, act)) curr->get_node()->add_read_from(act); } else @@ -1885,8 +1914,9 @@ bool ModelChecker::sleep_can_read_from(ModelAction * curr, const ModelAction *wr bool thread_sleep=prevnode->get_enabled_array()[id_to_int(curr->get_tid())]==THREAD_SLEEP_SET; if (write->is_release()&&thread_sleep) return true; - if (!write->is_rmw()) + if (!write->is_rmw()) { return false; + } if (write->get_reads_from()==NULL) return true; write=write->get_reads_from(); @@ -1899,10 +1929,13 @@ static void print_list(action_list_t *list) printf("---------------------------------------------------------------------\n"); printf("Trace:\n"); - + unsigned int hash=0; + for (it = list->begin(); it != list->end(); it++) { (*it)->print(); + hash=hash^(hash<<3)^((*it)->hash()); } + printf("HASH %u\n", hash); printf("---------------------------------------------------------------------\n"); } @@ -2044,6 +2077,12 @@ bool ModelChecker::take_step() { if (!isfeasible()) return false; + if (params.bound != 0) { + if (priv->used_sequence_numbers > params.bound) { + return false; + } + } + DEBUG("(%d, %d)\n", curr ? id_to_int(curr->get_id()) : -1, next ? id_to_int(next->get_id()) : -1);