return THREAD_ID_T_NONE;
/* Else, we are trying to replay an execution */
- ModelAction * next = node_stack->get_next()->get_action();
+ ModelAction *next = node_stack->get_next()->get_action();
if (next == diverge) {
Node *nextnode = next->get_node();
delete curr;
curr = tmp;
} else {
- ModelAction * tmp = node_stack->explore_action(curr);
+ ModelAction *tmp = node_stack->explore_action(curr);
if (tmp) {
/* Discard duplicate ModelAction; use action from NodeStack */
/* First restore type and order in case of RMW operation */
/* Read from future value */
value = curr->get_node()->get_future_value();
curr->read_from(NULL);
- Promise * valuepromise = new Promise(curr, value);
+ Promise *valuepromise = new Promise(curr, value);
promises->push_back(valuepromise);
}
} else if (curr->is_write()) {
}
/** Close out a RMWR by converting previous RMWR into a RMW or READ. */
-ModelAction * ModelChecker::process_rmw(ModelAction * act) {
+ModelAction * ModelChecker::process_rmw(ModelAction *act) {
int tid = id_to_int(act->get_tid());
ModelAction *lastread = get_last_action(tid);
lastread->process_rmw(act);
/* Include at most one act per-thread that "happens before" curr */
if (act->happens_before(curr)) {
if (act->is_read()) {
- const ModelAction * prevreadfrom = act->get_reads_from();
+ const ModelAction *prevreadfrom = act->get_reads_from();
if (prevreadfrom != NULL && rf != prevreadfrom)
mo_graph->addEdge(prevreadfrom, rf);
} else if (rf != act) {
}
/** Updates the mo_graph with the constraints imposed from the current read. */
-void ModelChecker::post_r_modification_order(ModelAction * curr, const ModelAction *rf) {
+void ModelChecker::post_r_modification_order(ModelAction *curr, const ModelAction *rf)
+{
std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
unsigned int i;
ASSERT(curr->is_read());
/* Include at most one act per-thread that "happens before" curr */
if (lastact != NULL) {
if (lastact->is_read()) {
- const ModelAction * postreadfrom = lastact->get_reads_from();
+ const ModelAction *postreadfrom = lastact->get_reads_from();
if (postreadfrom != NULL&&rf != postreadfrom)
mo_graph->addEdge(rf, postreadfrom);
} else if (rf != lastact) {
if (curr->is_seqcst()) {
/* We have to at least see the last sequentially consistent write,
so we are initialized. */
- ModelAction * last_seq_cst = get_last_seq_cst(curr->get_location());
+ ModelAction *last_seq_cst = get_last_seq_cst(curr->get_location());
if (last_seq_cst != NULL)
mo_graph->addEdge(last_seq_cst, curr);
}
}
}
+/**
+ * Finds the head(s) of the release sequence(s) containing a given ModelAction.
+ * The ModelAction under consideration is expected to be taking part in
+ * release/acquire synchronization as an object of the "reads from" relation.
+ * Note that this can only provide release sequence support for RMW chains
+ * which do not read from the future, as those actions cannot be traced until
+ * their "promise" is fulfilled. Similarly, we may not even establish the
+ * presence of a release sequence with certainty, as some modification order
+ * constraints may be decided further in the future. Thus, this function
+ * "returns" two pieces of data: a pass-by-reference vector of @a release_heads
+ * and a boolean representing certainty.
+ *
+ * @todo Finish lazy updating, when promises are fulfilled in the future
+ * @param rf The action that might be part of a release sequence. Must be a
+ * write.
+ * @param release_heads A pass-by-reference style return parameter. After
+ * execution of this function, release_heads will contain the heads of all the
+ * relevant release sequences, if any exists
+ * @return true, if the ModelChecker is certain that release_heads is complete;
+ * false otherwise
+ */
+bool ModelChecker::release_seq_head(const ModelAction *rf,
+ std::vector<const ModelAction *> *release_heads) const
+{
+ ASSERT(rf->is_write());
+ if (!rf) {
+ /* read from future: need to settle this later */
+ return false; /* incomplete */
+ }
+ if (rf->is_release())
+ release_heads->push_back(rf);
+ if (rf->is_rmw()) {
+ if (rf->is_acquire())
+ return true; /* complete */
+ return release_seq_head(rf->get_reads_from(), release_heads);
+ }
+ if (rf->is_release())
+ return true; /* complete */
+
+ /* else relaxed write; check modification order for contiguous subsequence
+ * -> rf must be same thread as release */
+ int tid = id_to_int(rf->get_tid());
+ std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(rf->get_location());
+ action_list_t *list = &(*thrd_lists)[tid];
+ action_list_t::const_reverse_iterator rit;
+
+ /* Find rf in the thread list */
+ for (rit = list->rbegin(); rit != list->rend(); rit++)
+ if (*rit == rf)
+ break;
+
+ /* Find the last write/release */
+ for (; rit != list->rend(); rit++)
+ if ((*rit)->is_release())
+ break;
+ if (rit == list->rend()) {
+ /* No write-release in this thread */
+ return true; /* complete */
+ }
+ ModelAction *release = *rit;
+
+ ASSERT(rf->same_thread(release));
+
+ bool certain = true;
+ for (unsigned int i = 0; i < thrd_lists->size(); i++) {
+ if (id_to_int(rf->get_tid()) == (int)i)
+ continue;
+ list = &(*thrd_lists)[i];
+ for (rit = list->rbegin(); rit != list->rend(); rit++) {
+ const ModelAction *act = *rit;
+ if (!act->is_write())
+ continue;
+ /* Reach synchronization -> this thread is complete */
+ if (act->happens_before(release))
+ break;
+ if (rf->happens_before(act))
+ continue;
+
+ /* Check modification order */
+ if (mo_graph->checkReachable(rf, act))
+ /* rf --mo--> act */
+ continue;
+ if (mo_graph->checkReachable(act, release))
+ /* act --mo--> release */
+ break;
+ if (mo_graph->checkReachable(release, act) &&
+ mo_graph->checkReachable(act, rf)) {
+ /* release --mo-> act --mo--> rf */
+ return true; /* complete */
+ }
+ certain = false;
+ }
+ }
+
+ if (certain)
+ release_heads->push_back(release);
+ return certain;
+}
+
+/**
+ * A public interface for getting the release sequence head(s) with which a
+ * given ModelAction must synchronize. This function only returns a non-empty
+ * result when it can locate a release sequence head with certainty. Otherwise,
+ * it may mark the internal state of the ModelChecker so that it will handle
+ * the release sequence at a later time, causing @a act to update its
+ * synchronization at some later point in execution.
+ * @param act The 'acquire' action that may read from a release sequence
+ * @param release_heads A pass-by-reference return parameter. Will be filled
+ * with the head(s) of the release sequence(s), if they exists with certainty.
+ * @see ModelChecker::release_seq_head
+ */
+void ModelChecker::get_release_seq_heads(ModelAction *act,
+ std::vector<const ModelAction *> *release_heads)
+{
+ const ModelAction *rf = act->get_reads_from();
+ bool complete;
+ complete = release_seq_head(rf, release_heads);
+ if (!complete) {
+ /** @todo complete lazy checking */
+ }
+}
+
/**
* Performs various bookkeeping operations for the current ModelAction. For
* instance, adds action to the per-object, per-thread action vector and to the
* @param tid The thread whose clock vector we want
* @return Desired clock vector
*/
-ClockVector * ModelChecker::get_cv(thread_id_t tid) {
+ClockVector * ModelChecker::get_cv(thread_id_t tid)
+{
return get_parent_action(tid)->get_cv();
}
-
-/** Resolve the given promises. */
-
-void ModelChecker::resolve_promises(ModelAction *write) {
- for (unsigned int i = 0, promise_index = 0;promise_index<promises->size(); i++) {
- Promise * promise = (*promises)[promise_index];
+/**
+ * Resolve a set of Promises with a current write. The set is provided in the
+ * Node corresponding to @a write.
+ * @param write The ModelAction that is fulfilling Promises
+ */
+void ModelChecker::resolve_promises(ModelAction *write)
+{
+ for (unsigned int i = 0, promise_index = 0; promise_index < promises->size(); i++) {
+ Promise *promise = (*promises)[promise_index];
if (write->get_node()->get_promise(i)) {
- ModelAction * read = promise->get_action();
+ ModelAction *read = promise->get_action();
read->read_from(write);
r_modification_order(read, write);
post_r_modification_order(read, write);
- promises->erase(promises->begin()+promise_index);
+ promises->erase(promises->begin() + promise_index);
} else
promise_index++;
}
}
-/** Compute the set of promises that could potentially be satisfied by
- * this action. */
-
-void ModelChecker::compute_promises(ModelAction *curr) {
- for (unsigned int i = 0;i<promises->size();i++) {
- Promise * promise = (*promises)[i];
- const ModelAction * act = promise->get_action();
- if (!act->happens_before(curr)&&
- act->is_read()&&
- !act->is_synchronizing(curr)&&
- !act->same_thread(curr)&&
+/**
+ * Compute the set of promises that could potentially be satisfied by this
+ * action. Note that the set computation actually appears in the Node, not in
+ * ModelChecker.
+ * @param curr The ModelAction that may satisfy promises
+ */
+void ModelChecker::compute_promises(ModelAction *curr)
+{
+ for (unsigned int i = 0; i < promises->size(); i++) {
+ Promise *promise = (*promises)[i];
+ const ModelAction *act = promise->get_action();
+ if (!act->happens_before(curr) &&
+ act->is_read() &&
+ !act->is_synchronizing(curr) &&
+ !act->same_thread(curr) &&
promise->get_value() == curr->get_value()) {
curr->get_node()->set_promise(i);
}
}
/** Checks promises in response to change in ClockVector Threads. */
-
-void ModelChecker::check_promises(ClockVector *old_cv, ClockVector * merge_cv) {
- for (unsigned int i = 0;i<promises->size();i++) {
- Promise * promise = (*promises)[i];
- const ModelAction * act = promise->get_action();
- if ((old_cv == NULL||!old_cv->synchronized_since(act))&&
+void ModelChecker::check_promises(ClockVector *old_cv, ClockVector *merge_cv)
+{
+ for (unsigned int i = 0; i < promises->size(); 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();
int ModelChecker::switch_to_master(ModelAction *act)
{
DBG();
- Thread * old = thread_current();
+ Thread *old = thread_current();
set_current_action(act);
old->set_state(THREAD_READY);
return Thread::swap(old, &system_context);
projects / c11tester.git / blobdiff