From: Brian Demsky Date: Thu, 26 Jul 2012 05:59:41 +0000 (-0700) Subject: changes X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=5e4a7d161cba81152ddcf295ee72fbb25ba3afaa changes --- diff --git a/action.cc b/action.cc index 33c69656..33dbe75b 100644 --- a/action.cc +++ b/action.cc @@ -165,11 +165,22 @@ void ModelAction::create_cv(const ModelAction *parent) void ModelAction::read_from(const ModelAction *act) { ASSERT(cv); - if (act->is_release() && this->is_acquire()) + if (act->is_release() && this->is_acquire()) { + synchronized(act); cv->merge(act->cv); + } reads_from = act; } + +/** Synchronize the current thread with the thread corresponding to + * the ModelAction parameter. */ + +void ModelAction::synchronized(const ModelAction *act) { + model->check_promises(cv, act->cv); + cv->merge(act->cv); +} + /** * Check whether 'this' happens before act, according to the memory-model's * happens before relation. This is checked via the ClockVector constructs. diff --git a/action.h b/action.h index da22882c..7c457076 100644 --- a/action.h +++ b/action.h @@ -81,6 +81,8 @@ public: void create_cv(const ModelAction *parent = NULL); ClockVector * get_cv() const { return cv; } void read_from(const ModelAction *act); + void synchronized(const ModelAction *act); + bool happens_before(const ModelAction *act) const; diff --git a/model.cc b/model.cc index bfa3e029..29e16aa3 100644 --- a/model.cc +++ b/model.cc @@ -31,11 +31,12 @@ ModelChecker::ModelChecker() thread_map(new HashTable()), obj_map(new HashTable()), obj_thrd_map(new HashTable, uintptr_t, 4 >()), - promises(new std::vector(1)), + promises(new std::vector()), thrd_last_action(new std::vector(1)), node_stack(new NodeStack()), next_backtrack(NULL), - cyclegraph(new CycleGraph()) + cyclegraph(new CycleGraph()), + failed_promise(false) { } @@ -69,6 +70,7 @@ void ModelChecker::reset_to_initial_state() used_sequence_numbers = 0; nextThread = 0; next_backtrack = NULL; + failed_promise = false; snapshotObject->backTrackBeforeStep(0); } @@ -133,7 +135,11 @@ thread_id_t ModelChecker::get_next_replay_thread() Node *nextnode = next->get_node(); /* Reached divergence point */ if (nextnode->increment_read_from()) { - /* The next node will read from a different value */ + /* The next node will read from a different value. */ + tid = next->get_tid(); + node_stack->pop_restofstack(2); + } else if (nextnode->increment_future_values()) { + /* The next node will try to read from a different future value. */ tid = next->get_tid(); node_stack->pop_restofstack(2); } else { @@ -290,15 +296,28 @@ void ModelChecker::check_current_action(void) th->set_creation(curr); } + /* Deal with new thread */ + if (curr->get_type() == THREAD_START) { + check_promises(NULL, curr->get_cv()); + } + /* Assign reads_from values */ Thread *th = get_thread(curr->get_tid()); uint64_t value = VALUE_NONE; if (curr->is_read()) { const ModelAction *reads_from = curr->get_node()->get_read_from(); - value = reads_from->get_value(); - /* Assign reads_from, perform release/acquire synchronization */ - curr->read_from(reads_from); - r_modification_order(curr,reads_from); + if (reads_from!=NULL) { + value = reads_from->get_value(); + /* Assign reads_from, perform release/acquire synchronization */ + curr->read_from(reads_from); + r_modification_order(curr,reads_from); + } else { + /* Read from future value */ + value = curr->get_node()->get_future_value(); + curr->read_from(NULL); + Promise * valuepromise=new Promise(curr, value); + promises->push_back(valuepromise); + } } else if (curr->is_write()) { w_modification_order(curr); } @@ -323,16 +342,16 @@ void ModelChecker::check_current_action(void) Node *currnode = curr->get_node(); Node *parnode = currnode->get_parent(); - if (!parnode->backtrack_empty()||!currnode->readsfrom_empty()) + if (!parnode->backtrack_empty()||!currnode->readsfrom_empty()||!currnode->futurevalues_empty()) if (!next_backtrack || *curr > *next_backtrack) next_backtrack = curr; - + set_backtracking(curr); } /** @returns whether the current trace is feasible. */ bool ModelChecker::isfeasible() { - return !cyclegraph->checkForCycles(); + return !cyclegraph->checkForCycles() && !failed_promise; } /** Close out a RMWR by converting previous RMWR into a RMW or READ. */ @@ -410,6 +429,21 @@ void ModelChecker::w_modification_order(ModelAction * curr) { } else cyclegraph->addEdge(curr, act); break; + } else { + if (act->is_read()&&!act->is_synchronizing(curr)&&!act->same_thread(curr)) { + /* We have an action that: + (1) did not happen before us + (2) is a read and we are a write + (3) cannot synchronize with us + (4) is in a different thread + => + that read could potentially read from our write. + */ + + if (act->get_node()->add_future_value(curr->get_value())&& + (!next_backtrack || *act > * next_backtrack)) + next_backtrack = act; + } } } } @@ -481,6 +515,25 @@ ClockVector * ModelChecker::get_cv(thread_id_t tid) { return get_parent_action(tid)->get_cv(); } +/** Checks promises in response to change in ClockVector Threads. */ + +void ModelChecker::check_promises(ClockVector *old_cv, ClockVector * merge_cv) { + for(unsigned int i=0;isize();i++) { + Promise * promise=(*promises)[i]; + const ModelAction * act=promise->get_action(); + if ((old_cv==NULL||!old_cv->synchronized_since(act))&& + merge_cv->synchronized_since(act)) { + //This thread is no longer able to send values back to satisfy the promise + int num_synchronized_threads=promise->increment_threads(); + if (num_synchronized_threads==model->get_num_threads()) { + //Promise has failed + failed_promise = true; + return; + } + } + } +} + /** * Build up an initial set of all past writes that this 'read' action may read * from. This set is determined by the clock vector's "happens before" diff --git a/model.h b/model.h index 41ec97b5..e6dc06dd 100644 --- a/model.h +++ b/model.h @@ -57,6 +57,7 @@ public: ClockVector * get_cv(thread_id_t tid); bool next_execution(); bool isfeasible(); + void check_promises(ClockVector *old_cv, ClockVector * merge_cv); MEMALLOC private: @@ -86,8 +87,7 @@ private: ModelAction * process_rmw(ModelAction * curr); void r_modification_order(ModelAction * curr, const ModelAction *rf); void w_modification_order(ModelAction * curr); - - + ModelAction *current_action; ModelAction *diverge; thread_id_t nextThread; @@ -106,6 +106,7 @@ private: NodeStack *node_stack; ModelAction *next_backtrack; CycleGraph * cyclegraph; + bool failed_promise; }; extern ModelChecker *model; diff --git a/nodestack.cc b/nodestack.cc index 62954426..08283580 100644 --- a/nodestack.cc +++ b/nodestack.cc @@ -62,11 +62,12 @@ void Node::print_may_read_from() * @param value is the value to backtrack to. */ -void Node::add_future_value(uint64_t value) { +bool Node::add_future_value(uint64_t value) { for(int i=0;i