+ case ATOMIC_NOTIFY_ALL:
+ case ATOMIC_NOTIFY_ONE: {
+ /* linear search: from most recent to oldest */
+ action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
+ action_list_t::reverse_iterator rit;
+ for (rit = list->rbegin(); rit != list->rend(); rit++) {
+ ModelAction *prev = *rit;
+ if (!act->same_thread(prev) && prev->is_wait())
+ return prev;
+ }
+ break;
+ }
+ default:
+ break;
+ }
+ return NULL;
+}
+
+/** This method finds backtracking points where we should try to
+ * reorder the parameter ModelAction against.
+ *
+ * @param the ModelAction to find backtracking points for.
+ */
+void ModelChecker::set_backtracking(ModelAction *act)
+{
+ Thread *t = get_thread(act);
+ ModelAction *prev = get_last_conflict(act);
+ if (prev == NULL)
+ return;
+
+ Node *node = prev->get_node()->get_parent();
+
+ /* See Dynamic Partial Order Reduction (addendum), POPL '05 */
+ int low_tid, high_tid;
+ if (node->enabled_status(t->get_id()) == THREAD_ENABLED) {
+ low_tid = id_to_int(act->get_tid());
+ high_tid = low_tid + 1;
+ } else {
+ low_tid = 0;
+ high_tid = get_num_threads();
+ }
+
+ for (int i = low_tid; i < high_tid; i++) {
+ thread_id_t tid = int_to_id(i);
+
+ /* Make sure this thread can be enabled here. */
+ if (i >= node->get_num_threads())
+ break;
+
+ /* See Dynamic Partial Order Reduction (addendum), POPL '05 */
+ /* Don't backtrack into a point where the thread is disabled or sleeping. */
+ if (node->enabled_status(tid) != THREAD_ENABLED)
+ continue;
+
+ /* Check if this has been explored already */
+ if (node->has_been_explored(tid))
+ continue;
+
+ /* See if fairness allows */
+ if (model->params.fairwindow != 0 && !node->has_priority(tid)) {
+ bool unfair = false;
+ for (int t = 0; t < node->get_num_threads(); t++) {
+ thread_id_t tother = int_to_id(t);
+ if (node->is_enabled(tother) && node->has_priority(tother)) {
+ unfair = true;
+ break;
+ }
+ }
+ if (unfair)
+ continue;
+ }
+
+ /* See if CHESS-like yield fairness allows */
+ if (model->params.yieldon) {
+ bool unfair = false;
+ for (int t = 0; t < node->get_num_threads(); t++) {
+ thread_id_t tother = int_to_id(t);
+ if (node->is_enabled(tother) && node->has_priority_over(tid, tother)) {
+ unfair = true;
+ break;
+ }
+ }
+ if (unfair)
+ continue;
+ }
+
+ /* Cache the latest backtracking point */
+ set_latest_backtrack(prev);
+
+ /* If this is a new backtracking point, mark the tree */
+ if (!node->set_backtrack(tid))
+ continue;
+ DEBUG("Setting backtrack: conflict = %d, instead tid = %d\n",
+ id_to_int(prev->get_tid()),
+ id_to_int(t->get_id()));
+ if (DBG_ENABLED()) {
+ prev->print();
+ act->print();
+ }
+ }
+}
+
+/**
+ * @brief Cache the a backtracking point as the "most recent", if eligible
+ *
+ * Note that this does not prepare the NodeStack for this backtracking
+ * operation, it only caches the action on a per-execution basis
+ *
+ * @param act The operation at which we should explore a different next action
+ * (i.e., backtracking point)
+ * @return True, if this action is now the most recent backtracking point;
+ * false otherwise
+ */
+bool ModelChecker::set_latest_backtrack(ModelAction *act)
+{
+ if (!priv->next_backtrack || *act > *priv->next_backtrack) {
+ priv->next_backtrack = act;
+ return true;
+ }
+ return false;
+}
+
+/**
+ * Returns last backtracking point. The model checker will explore a different
+ * path for this point in the next execution.
+ * @return The ModelAction at which the next execution should diverge.
+ */
+ModelAction * ModelChecker::get_next_backtrack()
+{
+ ModelAction *next = priv->next_backtrack;
+ priv->next_backtrack = NULL;
+ return next;
+}
+
+/**
+ * Processes a read model action.
+ * @param curr is the read model action to process.
+ * @return True if processing this read updates the mo_graph.
+ */
+bool ModelChecker::process_read(ModelAction *curr)
+{
+ Node *node = curr->get_node();
+ while (true) {
+ bool updated = false;
+ switch (node->get_read_from_status()) {
+ case READ_FROM_PAST: {
+ const ModelAction *rf = node->get_read_from_past();
+ ASSERT(rf);
+
+ mo_graph->startChanges();
+
+ ASSERT(!is_infeasible());
+ if (!check_recency(curr, rf)) {
+ if (node->increment_read_from()) {
+ mo_graph->rollbackChanges();
+ continue;
+ } else {
+ priv->too_many_reads = true;
+ }
+ }
+
+ updated = r_modification_order(curr, rf);
+ read_from(curr, rf);
+ mo_graph->commitChanges();
+ mo_check_promises(curr, true);
+ break;
+ }
+ case READ_FROM_PROMISE: {
+ Promise *promise = curr->get_node()->get_read_from_promise();
+ if (promise->add_reader(curr))
+ priv->failed_promise = true;
+ curr->set_read_from_promise(promise);
+ mo_graph->startChanges();
+ if (!check_recency(curr, promise))
+ priv->too_many_reads = true;
+ updated = r_modification_order(curr, promise);
+ mo_graph->commitChanges();
+ break;
+ }
+ case READ_FROM_FUTURE: {
+ /* Read from future value */
+ struct future_value fv = node->get_future_value();
+ Promise *promise = new Promise(curr, fv);
+ curr->set_read_from_promise(promise);
+ promises->push_back(promise);
+ mo_graph->startChanges();
+ updated = r_modification_order(curr, promise);
+ mo_graph->commitChanges();
+ break;
+ }
+ default:
+ ASSERT(false);
+ }
+ get_thread(curr)->set_return_value(curr->get_return_value());
+ return updated;
+ }
+}
+
+/**
+ * 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 = curr->get_mutex();
+ struct std::mutex_state *state = NULL;
+
+ if (mutex)
+ state = mutex->get_state();
+
+ switch (curr->get_type()) {
+ case ATOMIC_TRYLOCK: {
+ bool success = !state->locked;
+ 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->locked = get_thread(curr);
+ ModelAction *unlock = get_last_unlock(curr);
+ //synchronize with the previous unlock statement
+ if (unlock != NULL) {
+ curr->synchronize_with(unlock);
+ return true;
+ }
+ break;
+ }
+ case ATOMIC_WAIT:
+ case ATOMIC_UNLOCK: {
+ /* wake up the other threads */
+ for (unsigned int i = 0; i < get_num_threads(); i++) {
+ Thread *t = get_thread(int_to_id(i));
+ Thread *curr_thrd = get_thread(curr);
+ if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
+ scheduler->wake(t);
+ }
+
+ /* unlock the lock - after checking who was waiting on it */
+ state->locked = NULL;
+
+ if (!curr->is_wait())
+ break; /* The rest is only for ATOMIC_WAIT */
+
+ /* Should we go to sleep? (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_thread(curr));
+ }
+ 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;
+}
+
+/**
+ * @brief Check if the current pending promises allow a future value to be sent
+ *
+ * If one of the following is true:
+ * (a) there are no pending promises
+ * (b) the reader and writer do not cross any promises
+ * Then, it is safe to pass a future value back now.
+ *
+ * Otherwise, we must save the pending future value until (a) or (b) is true
+ *
+ * @param writer The operation which sends the future value. Must be a write.
+ * @param reader The operation which will observe the value. Must be a read.
+ * @return True if the future value can be sent now; false if it must wait.
+ */
+bool ModelChecker::promises_may_allow(const ModelAction *writer,
+ const ModelAction *reader) const
+{
+ if (promises->empty())
+ return true;
+ for(int i=promises->size()-1;i>=0;i--) {
+ ModelAction *pr=(*promises)[i]->get_reader(0);
+ //reader is after promise...doesn't cross any promise
+ if (*reader > *pr)
+ return true;
+ //writer is after promise, reader before...bad...
+ if (*writer > *pr)
+ return false;
+ }
+ return true;
+}
+
+/**
+ * @brief Add a future value to a reader
+ *
+ * This function performs a few additional checks to ensure that the future
+ * value can be feasibly observed by the reader
+ *
+ * @param writer The operation whose value is sent. Must be a write.
+ * @param reader The read operation which may read the future value. Must be a read.
+ */
+void ModelChecker::add_future_value(const ModelAction *writer, ModelAction *reader)
+{
+ /* Do more ambitious checks now that mo is more complete */
+ if (!mo_may_allow(writer, reader))
+ return;
+
+ Node *node = reader->get_node();
+
+ /* Find an ancestor thread which exists at the time of the reader */
+ Thread *write_thread = get_thread(writer);
+ while (id_to_int(write_thread->get_id()) >= node->get_num_threads())
+ write_thread = write_thread->get_parent();
+
+ struct future_value fv = {
+ writer->get_write_value(),
+ writer->get_seq_number() + params.maxfuturedelay,
+ write_thread->get_id(),
+ };
+ if (node->add_future_value(fv))
+ set_latest_backtrack(reader);
+}
+
+/**
+ * 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)
+{
+ /* Readers to which we may send our future value */
+ ModelVector<ModelAction *> send_fv;
+
+ const ModelAction *earliest_promise_reader;
+ bool updated_promises = false;
+
+ bool updated_mod_order = w_modification_order(curr, &send_fv);
+ Promise *promise = pop_promise_to_resolve(curr);
+
+ if (promise) {
+ earliest_promise_reader = promise->get_reader(0);
+ updated_promises = resolve_promise(curr, promise);
+ } else
+ earliest_promise_reader = NULL;
+
+ for (unsigned int i = 0; i < send_fv.size(); i++) {
+ ModelAction *read = send_fv[i];
+
+ /* Don't send future values to reads after the Promise we resolve */
+ if (!earliest_promise_reader || *read < *earliest_promise_reader) {
+ /* Check if future value can be sent immediately */
+ if (promises_may_allow(curr, read)) {
+ add_future_value(curr, read);
+ } else {
+ futurevalues->push_back(PendingFutureValue(curr, read));
+ }
+ }
+ }
+
+ /* Check the pending future values */
+ for (int i = (int)futurevalues->size() - 1; i >= 0; i--) {
+ struct PendingFutureValue pfv = (*futurevalues)[i];
+ if (promises_may_allow(pfv.writer, pfv.reader)) {
+ add_future_value(pfv.writer, pfv.reader);
+ futurevalues->erase(futurevalues->begin() + i);
+ }
+ }
+
+ mo_graph->commitChanges();
+ mo_check_promises(curr, false);
+
+ 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
+ * fence-seq-cst: MO constraints formed in {r,w}_modification_order
+ */
+ 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 */