+/**
+ * Initialize the current action by performing one or more of the following
+ * actions, as appropriate: merging RMWR and RMWC/RMW actions, stepping forward
+ * in the NodeStack, manipulating backtracking sets, allocating and
+ * initializing clock vectors, and computing the promises to fulfill.
+ *
+ * @param curr The current action, as passed from the user context; may be
+ * freed/invalidated after the execution of this function, with a different
+ * action "returned" its place (pass-by-reference)
+ * @return True if curr is a newly-explored action; false otherwise
+ */
+bool ModelChecker::initialize_curr_action(ModelAction **curr)
+{
+ ModelAction *newcurr;
+
+ 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(get_safe_ptr_action(condvar_waiters_map, 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
+ get_safe_ptr_action(lock_waiters_map, 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;
+}
+
+/**
+ * Stores the ModelAction for the current thread action. Call this
+ * immediately before switching from user- to system-context to pass
+ * data between them.
+ * @param act The ModelAction created by the user-thread action
+ */
+void ModelChecker::set_current_action(ModelAction *act) {
+ priv->current_action = act;
+}
+
+/**
+ * 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));
+ while (!work_queue.empty() && !has_asserted()) {
+ WorkQueueEntry work = work_queue.front();
+ work_queue.pop_front();
+
+ switch (work.type) {
+ case WORK_CHECK_CURR_ACTION: {
+ ModelAction *act = work.action;
+ bool update = false; /* update this location's release seq's */
+ bool update_all = false; /* update all release seq's */
+
+ if (process_thread_action(curr))
+ update_all = true;
+
+ if (act->is_read() && process_read(act, second_part_of_rmw))
+ update = true;
+
+ if (act->is_write() && process_write(act))
+ update = true;
+
+ if (act->is_mutex_op() && process_mutex(act))
+ update_all = true;
+
+ if (act->is_relseq_fixup())
+ process_relseq_fixup(curr, &work_queue);
+
+ if (update_all)
+ work_queue.push_back(CheckRelSeqWorkEntry(NULL));
+ else if (update)
+ work_queue.push_back(CheckRelSeqWorkEntry(act->get_location()));
+ break;
+ }
+ case WORK_CHECK_RELEASE_SEQ:
+ resolve_release_sequences(work.location, &work_queue);
+ break;
+ case WORK_CHECK_MO_EDGES: {
+ /** @todo Complete verification of work_queue */
+ ModelAction *act = work.action;
+ bool updated = false;
+
+ if (act->is_read()) {
+ const ModelAction *rf = act->get_reads_from();
+ if (rf != NULL && r_modification_order(act, rf))
+ updated = true;
+ }
+ if (act->is_write()) {
+ if (w_modification_order(act))
+ updated = true;