+/**
+ * Processes a lock, trylock, or unlock model action. @param curr is
+ * the read model action to process.
+ *
+ * The try lock operation checks whether the lock is taken. If not,
+ * it falls to the normal lock operation case. If so, it returns
+ * fail.
+ *
+ * The lock operation has already been checked that it is enabled, so
+ * it just grabs the lock and synchronizes with the previous unlock.
+ *
+ * The unlock operation has to re-enable all of the threads that are
+ * waiting on the lock.
+ *
+ * @return True if synchronization was updated; false otherwise
+ */
+bool ModelChecker::process_mutex(ModelAction *curr) {
+ std::mutex *mutex=NULL;
+ struct std::mutex_state *state=NULL;
+
+ if (curr->is_trylock() || curr->is_lock() || curr->is_unlock()) {
+ mutex = (std::mutex *)curr->get_location();
+ state = mutex->get_state();
+ } else if(curr->is_wait()) {
+ mutex = (std::mutex *)curr->get_value();
+ state = mutex->get_state();
+ }
+
+ switch (curr->get_type()) {
+ case ATOMIC_TRYLOCK: {
+ bool success = !state->islocked;
+ curr->set_try_lock(success);
+ if (!success) {
+ get_thread(curr)->set_return_value(0);
+ break;
+ }
+ get_thread(curr)->set_return_value(1);
+ }
+ //otherwise fall into the lock case
+ case ATOMIC_LOCK: {
+ if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
+ assert_bug("Lock access before initialization");
+ state->islocked = true;
+ ModelAction *unlock = get_last_unlock(curr);
+ //synchronize with the previous unlock statement
+ if (unlock != NULL) {
+ curr->synchronize_with(unlock);
+ return true;
+ }
+ break;
+ }
+ case ATOMIC_UNLOCK: {
+ //unlock the lock
+ state->islocked = false;
+ //wake up the other threads
+ action_list_t *waiters = get_safe_ptr_action(lock_waiters_map, curr->get_location());
+ //activate all the waiting threads
+ for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) {
+ scheduler->wake(get_thread(*rit));
+ }
+ waiters->clear();
+ break;
+ }
+ case ATOMIC_WAIT: {
+ //unlock the lock
+ state->islocked = false;
+ //wake up the other threads
+ action_list_t *waiters = get_safe_ptr_action(lock_waiters_map, (void *) curr->get_value());
+ //activate all the waiting threads
+ for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) {
+ scheduler->wake(get_thread(*rit));
+ }
+ waiters->clear();
+ //check whether we should go to sleep or not...simulate spurious failures
+ if (curr->get_node()->get_misc()==0) {
+ get_safe_ptr_action(condvar_waiters_map, curr->get_location())->push_back(curr);
+ //disable us
+ scheduler->sleep(get_current_thread());
+ }
+ break;
+ }
+ case ATOMIC_NOTIFY_ALL: {
+ action_list_t *waiters = get_safe_ptr_action(condvar_waiters_map, curr->get_location());
+ //activate all the waiting threads
+ for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) {
+ scheduler->wake(get_thread(*rit));
+ }
+ waiters->clear();
+ break;
+ }
+ case ATOMIC_NOTIFY_ONE: {
+ action_list_t *waiters = get_safe_ptr_action(condvar_waiters_map, curr->get_location());
+ int wakeupthread=curr->get_node()->get_misc();
+ action_list_t::iterator it = waiters->begin();
+ advance(it, wakeupthread);
+ scheduler->wake(get_thread(*it));
+ waiters->erase(it);
+ break;
+ }
+
+ default:
+ ASSERT(0);
+ }
+ return false;
+}
+
+/**
+ * Process a write ModelAction
+ * @param curr The ModelAction to process
+ * @return True if the mo_graph was updated or promises were resolved
+ */
+bool ModelChecker::process_write(ModelAction *curr)
+{
+ bool updated_mod_order = w_modification_order(curr);
+ bool updated_promises = resolve_promises(curr);
+
+ if (promises->size() == 0) {
+ for (unsigned int i = 0; i < futurevalues->size(); i++) {
+ struct PendingFutureValue pfv = (*futurevalues)[i];
+ //Do more ambitious checks now that mo is more complete
+ if (mo_may_allow(pfv.writer, pfv.act)&&
+ pfv.act->get_node()->add_future_value(pfv.writer->get_value(), pfv.writer->get_seq_number()+params.maxfuturedelay) &&
+ (!priv->next_backtrack || *pfv.act > *priv->next_backtrack))
+ priv->next_backtrack = pfv.act;
+ }
+ futurevalues->resize(0);
+ }
+
+ mo_graph->commitChanges();
+ mo_check_promises(curr->get_tid(), curr);
+
+ get_thread(curr)->set_return_value(VALUE_NONE);
+ return updated_mod_order || updated_promises;
+}
+
+/**
+ * Process a fence ModelAction
+ * @param curr The ModelAction to process
+ * @return True if synchronization was updated
+ */
+bool ModelChecker::process_fence(ModelAction *curr)
+{
+ /*
+ * fence-relaxed: no-op
+ * fence-release: only log the occurence (not in this function), for
+ * use in later synchronization
+ * fence-acquire (this function): search for hypothetical release
+ * sequences
+ */
+ bool updated = false;
+ if (curr->is_acquire()) {
+ action_list_t *list = action_trace;
+ action_list_t::reverse_iterator rit;
+ /* Find X : is_read(X) && X --sb-> curr */
+ for (rit = list->rbegin(); rit != list->rend(); rit++) {
+ ModelAction *act = *rit;
+ if (act == curr)
+ continue;
+ if (act->get_tid() != curr->get_tid())
+ continue;
+ /* Stop at the beginning of the thread */
+ if (act->is_thread_start())
+ break;
+ /* Stop once we reach a prior fence-acquire */
+ if (act->is_fence() && act->is_acquire())
+ break;
+ if (!act->is_read())
+ continue;
+ /* read-acquire will find its own release sequences */
+ if (act->is_acquire())
+ continue;
+
+ /* Establish hypothetical release sequences */
+ rel_heads_list_t release_heads;
+ get_release_seq_heads(curr, act, &release_heads);
+ for (unsigned int i = 0; i < release_heads.size(); i++)
+ if (!curr->synchronize_with(release_heads[i]))
+ set_bad_synchronization();
+ if (release_heads.size() != 0)
+ updated = true;
+ }
+ }
+ return updated;
+}
+
+/**
+ * @brief Process the current action for thread-related activity
+ *
+ * Performs current-action processing for a THREAD_* ModelAction. Proccesses
+ * may include setting Thread status, completing THREAD_FINISH/THREAD_JOIN
+ * synchronization, etc. This function is a no-op for non-THREAD actions
+ * (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.)
+ *
+ * @param curr The current action
+ * @return True if synchronization was updated or a thread completed
+ */
+bool ModelChecker::process_thread_action(ModelAction *curr)
+{
+ bool updated = false;
+
+ switch (curr->get_type()) {
+ case THREAD_CREATE: {
+ Thread *th = (Thread *)curr->get_location();
+ th->set_creation(curr);
+ break;
+ }
+ case THREAD_JOIN: {
+ Thread *blocking = (Thread *)curr->get_location();
+ ModelAction *act = get_last_action(blocking->get_id());
+ curr->synchronize_with(act);
+ updated = true; /* trigger rel-seq checks */
+ break;
+ }
+ case THREAD_FINISH: {
+ Thread *th = get_thread(curr);
+ while (!th->wait_list_empty()) {
+ ModelAction *act = th->pop_wait_list();
+ scheduler->wake(get_thread(act));
+ }
+ th->complete();
+ updated = true; /* trigger rel-seq checks */
+ break;
+ }
+ case THREAD_START: {
+ check_promises(curr->get_tid(), NULL, curr->get_cv());
+ break;
+ }
+ default:
+ break;
+ }
+
+ return updated;
+}
+
+/**
+ * @brief Process the current action for release sequence fixup activity
+ *
+ * Performs model-checker release sequence fixups for the current action,
+ * forcing a single pending release sequence to break (with a given, potential
+ * "loose" write) or to complete (i.e., synchronize). If a pending release
+ * sequence forms a complete release sequence, then we must perform the fixup
+ * synchronization, mo_graph additions, etc.
+ *
+ * @param curr The current action; must be a release sequence fixup action
+ * @param work_queue The work queue to which to add work items as they are
+ * generated
+ */
+void ModelChecker::process_relseq_fixup(ModelAction *curr, work_queue_t *work_queue)
+{
+ const ModelAction *write = curr->get_node()->get_relseq_break();
+ struct release_seq *sequence = pending_rel_seqs->back();
+ pending_rel_seqs->pop_back();
+ ASSERT(sequence);
+ ModelAction *acquire = sequence->acquire;
+ const ModelAction *rf = sequence->rf;
+ const ModelAction *release = sequence->release;
+ ASSERT(acquire);
+ ASSERT(release);
+ ASSERT(rf);
+ ASSERT(release->same_thread(rf));
+
+ if (write == NULL) {
+ /**
+ * @todo Forcing a synchronization requires that we set
+ * modification order constraints. For instance, we can't allow
+ * a fixup sequence in which two separate read-acquire
+ * operations read from the same sequence, where the first one
+ * synchronizes and the other doesn't. Essentially, we can't
+ * allow any writes to insert themselves between 'release' and
+ * 'rf'
+ */
+
+ /* Must synchronize */
+ if (!acquire->synchronize_with(release)) {
+ set_bad_synchronization();
+ return;
+ }
+ /* Re-check all pending release sequences */
+ work_queue->push_back(CheckRelSeqWorkEntry(NULL));
+ /* Re-check act for mo_graph edges */
+ work_queue->push_back(MOEdgeWorkEntry(acquire));
+
+ /* propagate synchronization to later actions */
+ action_list_t::reverse_iterator rit = action_trace->rbegin();
+ for (; (*rit) != acquire; rit++) {
+ ModelAction *propagate = *rit;
+ if (acquire->happens_before(propagate)) {
+ propagate->synchronize_with(acquire);
+ /* Re-check 'propagate' for mo_graph edges */
+ work_queue->push_back(MOEdgeWorkEntry(propagate));
+ }
+ }
+ } else {
+ /* Break release sequence with new edges:
+ * release --mo--> write --mo--> rf */
+ mo_graph->addEdge(release, write);
+ mo_graph->addEdge(write, rf);