+ if ((*curr)->is_rmwc() || (*curr)->is_rmw()) {
+ newcurr = process_rmw(*curr);
+ delete *curr;
+
+ if (newcurr->is_rmw())
+ compute_promises(newcurr);
+
+ *curr = newcurr;
+ return false;
+ }
+
+ (*curr)->set_seq_number(get_next_seq_num());
+
+ newcurr = node_stack->explore_action(*curr, scheduler->get_enabled());
+ if (newcurr) {
+ /* First restore type and order in case of RMW operation */
+ if ((*curr)->is_rmwr())
+ newcurr->copy_typeandorder(*curr);
+
+ ASSERT((*curr)->get_location() == newcurr->get_location());
+ newcurr->copy_from_new(*curr);
+
+ /* Discard duplicate ModelAction; use action from NodeStack */
+ delete *curr;
+
+ /* Always compute new clock vector */
+ newcurr->create_cv(get_parent_action(newcurr->get_tid()));
+
+ *curr = newcurr;
+ return false; /* Action was explored previously */
+ } else {
+ newcurr = *curr;
+
+ /* Always compute new clock vector */
+ newcurr->create_cv(get_parent_action(newcurr->get_tid()));
+ /*
+ * Perform one-time actions when pushing new ModelAction onto
+ * NodeStack
+ */
+ if (newcurr->is_write())
+ compute_promises(newcurr);
+ else if (newcurr->is_relseq_fixup())
+ compute_relseq_breakwrites(newcurr);
+ else if (newcurr->is_wait())
+ newcurr->get_node()->set_misc_max(2);
+ else if (newcurr->is_notify_one()) {
+ newcurr->get_node()->set_misc_max(condvar_waiters_map->get_safe_ptr(newcurr->get_location())->size());
+ }
+ return true; /* This was a new ModelAction */
+ }
+}
+
+/**
+ * @brief Check whether a model action is enabled.
+ *
+ * Checks whether a lock or join operation would be successful (i.e., is the
+ * lock already locked, or is the joined thread already complete). If not, put
+ * the action in a waiter list.
+ *
+ * @param curr is the ModelAction to check whether it is enabled.
+ * @return a bool that indicates whether the action is enabled.
+ */
+bool ModelChecker::check_action_enabled(ModelAction *curr) {
+ if (curr->is_lock()) {
+ std::mutex * lock = (std::mutex *)curr->get_location();
+ struct std::mutex_state * state = lock->get_state();
+ if (state->islocked) {
+ //Stick the action in the appropriate waiting queue
+ lock_waiters_map->get_safe_ptr(curr->get_location())->push_back(curr);
+ return false;
+ }
+ } else if (curr->get_type() == THREAD_JOIN) {
+ Thread *blocking = (Thread *)curr->get_location();
+ if (!blocking->is_complete()) {
+ blocking->push_wait_list(curr);
+ return false;
+ }
+ }
+
+ return true;
+}
+
+/**
+ * This is the heart of the model checker routine. It performs model-checking
+ * actions corresponding to a given "current action." Among other processes, it
+ * calculates reads-from relationships, updates synchronization clock vectors,
+ * forms a memory_order constraints graph, and handles replay/backtrack
+ * execution when running permutations of previously-observed executions.
+ *
+ * @param curr The current action to process
+ * @return The next Thread that must be executed. May be NULL if ModelChecker
+ * makes no choice (e.g., according to replay execution, combining RMW actions,
+ * etc.)
+ */
+Thread * ModelChecker::check_current_action(ModelAction *curr)
+{
+ ASSERT(curr);
+ bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
+
+ if (!check_action_enabled(curr)) {
+ /* Make the execution look like we chose to run this action
+ * much later, when a lock/join can succeed */
+ get_current_thread()->set_pending(curr);
+ scheduler->sleep(get_current_thread());
+ return get_next_thread(NULL);
+ }
+
+ bool newly_explored = initialize_curr_action(&curr);
+
+ wake_up_sleeping_actions(curr);
+
+ /* Add the action to lists before any other model-checking tasks */
+ if (!second_part_of_rmw)
+ add_action_to_lists(curr);
+
+ /* Build may_read_from set for newly-created actions */
+ if (newly_explored && curr->is_read())
+ build_reads_from_past(curr);
+
+ /* Initialize work_queue with the "current action" work */
+ work_queue_t work_queue(1, CheckCurrWorkEntry(curr));