+/**
+ * This method checks whether a model action is enabled at the given point.
+ * At this point, it checks whether a lock operation would be successful at this point.
+ * If not, it puts the thread 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;
+ }
+ }
+
+ 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 is actually available to release */
+ get_current_thread()->set_pending(curr);
+ remove_thread(get_current_thread());
+ return get_next_thread(NULL);