- if (curr->is_write()) {
- bool updated_mod_order = w_modification_order(curr);
- bool updated_promises = resolve_promises(curr);
- updated = updated_mod_order|updated_promises;
-
- if (promises->size()==0) {
- for (unsigned int i = 0; i<futurevalues->size(); i++) {
- struct PendingFutureValue pfv=(*futurevalues)[i];
- if (pfv.act->get_node()->add_future_value(pfv.value, pfv.expiration) &&
- (!priv->next_backtrack || *pfv.act > *priv->next_backtrack))
- priv->next_backtrack = pfv.act;
- }
- futurevalues->resize(0);
+ 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()));
+ } 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);
+ }
+ return newcurr;
+}
+
+/**
+ * @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;