ASSERT(curr->is_read());
+ ModelAction *last_seq_cst = NULL;
+
+ if (curr->is_seqcst())
+ last_seq_cst = get_last_seq_cst(curr->get_location());
+
/* Track whether this object has been initialized */
bool initialized = false;
+ /* Would each action synchronize if we read from it? */
+ bool all_synch = true;
+ /* Is the may_read_from set empty? (tracked locally) */
+ bool empty = true;
+ /* Iterate over all threads */
for (i = 0; i < thrd_lists->size(); i++) {
+ /* 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++) {
if (!act->is_write())
continue;
- DEBUG("Adding action to may_read_from:\n");
- if (DBG_ENABLED()) {
- act->print();
- curr->print();
+ /* Don't consider more than one seq_cst write */
+ if (!act->is_seqcst() || act == last_seq_cst) {
+ DEBUG("Adding action to may_read_from:\n");
+ if (DBG_ENABLED()) {
+ act->print();
+ curr->print();
+ }
+ curr->get_node()->add_read_from(act);
+ empty = false;
+
+ if (!(act->is_release() && curr->is_acquire())
+ && !act->same_thread(curr))
+ all_synch = false;
}
- curr->get_node()->add_read_from(act);
/* Include at most one act per-thread that "happens before" curr */
if (act->happens_before(curr)) {
}
}
+ if (!empty && all_synch)
+ initialized = true;
+
if (!initialized) {
/* TODO: need a more informative way of reporting errors */
printf("ERROR: may read from uninitialized atomic\n");
scheduler->remove_thread(t);
}
+/**
+ * Switch from a user-context to the "master thread" context (a.k.a. system
+ * context). This switch is made with the intention of exploring a particular
+ * model-checking action (described by a ModelAction object). Must be called
+ * from a user-thread context.
+ * @param act The current action that will be explored. May be NULL, although
+ * there is little reason to switch to the model-checker without an action to
+ * explore (note: act == NULL is sometimes used as a hack to allow a thread to
+ * yield control without performing any progress; see thrd_join()).
+ * @return Return status from the 'swap' call (i.e., success/fail, 0/-1)
+ */
int ModelChecker::switch_to_master(ModelAction *act)
{
Thread *old;