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: {
/* 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
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
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