futurevalues(new std::vector< struct PendingFutureValue, SnapshotAlloc<struct PendingFutureValue> >()),
pending_rel_seqs(new std::vector< struct release_seq *, SnapshotAlloc<struct release_seq *> >()),
thrd_last_action(new std::vector< ModelAction *, SnapshotAlloc<ModelAction *> >(1)),
+ thrd_last_fence_release(new std::vector< ModelAction *, SnapshotAlloc<ModelAction *> >()),
node_stack(new NodeStack()),
priv(new struct model_snapshot_members()),
mo_graph(new CycleGraph())
delete pending_rel_seqs;
delete thrd_last_action;
+ delete thrd_last_fence_release;
delete node_stack;
delete scheduler;
delete mo_graph;
ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
{
switch (act->get_type()) {
+ case ATOMIC_FENCE:
case ATOMIC_READ:
case ATOMIC_WRITE:
case ATOMIC_RMW: {
continue;
}
- curr->read_from(reads_from);
+ read_from(curr, reads_from);
mo_graph->commitChanges();
mo_check_promises(curr->get_tid(), reads_from);
/* Read from future value */
value = curr->get_node()->get_future_value();
modelclock_t expiration = curr->get_node()->get_future_value_expiration();
- curr->read_from(NULL);
+ read_from(curr, NULL);
Promise *valuepromise = new Promise(curr, value, expiration);
promises->push_back(valuepromise);
}
/* Always compute new clock vector */
newcurr->create_cv(get_parent_action(newcurr->get_tid()));
+
+ /* Assign most recent release fence */
+ newcurr->set_last_fence_release(get_last_fence_release(newcurr->get_tid()));
+
/*
* Perform one-time actions when pushing new ModelAction onto
* NodeStack
}
}
+/**
+ * @brief Establish reads-from relation between two actions
+ *
+ * Perform basic operations involved with establishing a concrete rf relation,
+ * including setting the ModelAction data and checking for release sequences.
+ *
+ * @param act The action that is reading (must be a read)
+ * @param rf The action from which we are reading (must be a write)
+ *
+ * @return True if this read established synchronization
+ */
+bool ModelChecker::read_from(ModelAction *act, const ModelAction *rf)
+{
+ act->set_read_from(rf);
+ if (rf != NULL && act->is_acquire()) {
+ rel_heads_list_t release_heads;
+ get_release_seq_heads(act, &release_heads);
+ int num_heads = release_heads.size();
+ for (unsigned int i = 0; i < release_heads.size(); i++)
+ if (!act->synchronize_with(release_heads[i])) {
+ set_bad_synchronization();
+ num_heads--;
+ }
+ return num_heads > 0;
+ }
+ return false;
+}
+
/**
* @brief Check whether a model action is enabled.
*
bool added = false;
ASSERT(curr->is_read());
+ /* Last SC fence in the current thread */
+ ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
+
/* Iterate over all threads */
for (i = 0; i < thrd_lists->size(); i++) {
+ /* Last SC fence in thread i */
+ ModelAction *last_sc_fence_thread_local = NULL;
+ if (int_to_id((int)i) != curr->get_tid())
+ last_sc_fence_thread_local = get_last_seq_cst_fence(int_to_id(i), NULL);
+
+ /* Last SC fence in thread i, before last SC fence in current thread */
+ ModelAction *last_sc_fence_thread_before = NULL;
+ if (last_sc_fence_local)
+ last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local);
+
/* Iterate over actions in thread, starting from most recent */
action_list_t *list = &(*thrd_lists)[i];
action_list_t::reverse_iterator rit;
for (rit = list->rbegin(); rit != list->rend(); rit++) {
ModelAction *act = *rit;
+ if (act->is_write() && act != rf && act != curr) {
+ /* C++, Section 29.3 statement 5 */
+ if (curr->is_seqcst() && last_sc_fence_thread_local &&
+ *act < *last_sc_fence_thread_local) {
+ mo_graph->addEdge(act, rf);
+ added = true;
+ }
+ /* C++, Section 29.3 statement 4 */
+ else if (act->is_seqcst() && last_sc_fence_local &&
+ *act < *last_sc_fence_local) {
+ mo_graph->addEdge(act, rf);
+ added = true;
+ }
+ /* C++, Section 29.3 statement 6 */
+ else if (last_sc_fence_thread_before &&
+ *act < *last_sc_fence_thread_before) {
+ mo_graph->addEdge(act, rf);
+ added = true;
+ }
+ }
+
/*
* Include at most one act per-thread that "happens
* before" curr. Don't consider reflexively.
}
}
+ /* Last SC fence in the current thread */
+ ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
+
/* Iterate over all threads */
for (i = 0; i < thrd_lists->size(); i++) {
+ /* Last SC fence in thread i, before last SC fence in current thread */
+ ModelAction *last_sc_fence_thread_before = NULL;
+ if (last_sc_fence_local && int_to_id((int)i) != curr->get_tid())
+ last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local);
+
/* Iterate over actions in thread, starting from most recent */
action_list_t *list = &(*thrd_lists)[i];
action_list_t::reverse_iterator rit;
continue;
}
+ /* C++, Section 29.3 statement 7 */
+ if (last_sc_fence_thread_before && act->is_write() &&
+ *act < *last_sc_fence_thread_before) {
+ mo_graph->addEdge(act, curr);
+ added = true;
+ }
+
/*
* Include at most one act per-thread that "happens
* before" curr
}
/**
- * A public interface for getting the release sequence head(s) with which a
+ * An 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
thrd_last_action->resize(get_num_threads());
(*thrd_last_action)[tid] = act;
+ if (act->is_fence() && act->is_release()) {
+ if ((int)thrd_last_fence_release->size() <= tid)
+ thrd_last_fence_release->resize(get_num_threads());
+ (*thrd_last_fence_release)[tid] = act;
+ }
+
if (act->is_wait()) {
void *mutex_loc=(void *) act->get_value();
get_safe_ptr_action(obj_map, mutex_loc)->push_back(act);
if (tid >= (int)vec->size())
vec->resize(priv->next_thread_id);
(*vec)[tid].push_back(act);
-
- if ((int)thrd_last_action->size() <= tid)
- thrd_last_action->resize(get_num_threads());
- (*thrd_last_action)[tid] = act;
}
}
return NULL;
}
+/**
+ * @brief Get the last fence release performed by a particular Thread
+ * @param tid The thread ID of the Thread in question
+ * @return The last fence release in the thread, if one exists; NULL otherwise
+ */
+ModelAction * ModelChecker::get_last_fence_release(thread_id_t tid) const
+{
+ int threadid = id_to_int(tid);
+ if (threadid < (int)thrd_last_fence_release->size())
+ return (*thrd_last_fence_release)[id_to_int(tid)];
+ else
+ return NULL;
+}
+
/**
* Gets the last memory_order_seq_cst write (in the total global sequence)
* performed on a particular object (i.e., memory location), not including the
if (read->is_rmw()) {
mo_graph->addRMWEdge(write, read);
}
- read->read_from(write);
+ read_from(read, write);
//First fix up the modification order for actions that happened
//before the read
r_modification_order(read, write);
projects / c11tester.git / blobdiff