From 7ae6e12db65b5addd144f7ab6db39874a8d0c38f Mon Sep 17 00:00:00 2001 From: Brian Demsky Date: Fri, 31 May 2019 22:21:31 -0700 Subject: [PATCH] partial conversion to fuzzer --- action.cc | 51 +--- action.h | 13 - cyclegraph.cc | 1 - execution.cc | 1 - model.cc | 48 +--- model.h | 1 - nodestack.cc | 736 +------------------------------------------------- nodestack.h | 112 +------- promise.cc | 204 -------------- promise.h | 78 ------ schedule.cc | 9 - schedule.h | 1 - 12 files changed, 8 insertions(+), 1247 deletions(-) delete mode 100644 promise.cc delete mode 100644 promise.h diff --git a/action.cc b/action.cc index 14160052..4e3b59a3 100644 --- a/action.cc +++ b/action.cc @@ -39,7 +39,6 @@ ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, location(loc), value(value), reads_from(NULL), - reads_from_promise(NULL), last_fence_release(NULL), node(NULL), seq_number(ACTION_INITIAL_CLOCK), @@ -430,8 +429,6 @@ uint64_t ModelAction::get_reads_from_value() const ASSERT(is_read()); if (reads_from) return reads_from->get_write_value(); - else if (reads_from_promise) - return reads_from_promise->get_value(); return VALUE_NONE; /* Only for new actions with no reads-from */ } @@ -489,7 +486,6 @@ void ModelAction::set_read_from(const ModelAction *act) ASSERT(act); reads_from = act; - reads_from_promise = NULL; if (act->is_uninitialized()) { // WL uint64_t val = *((uint64_t *) location); @@ -506,17 +502,6 @@ void ModelAction::set_read_from(const ModelAction *act) } } -/** - * Set this action's read-from promise - * @param promise The promise to read from - */ -void ModelAction::set_read_from_promise(Promise *promise) -{ - ASSERT(is_read()); - reads_from_promise = promise; - reads_from = NULL; -} - /** * Synchronize the current thread with the thread corresponding to the * ModelAction parameter. @@ -601,13 +586,7 @@ void ModelAction::print() const if (is_read()) { if (reads_from) model_print(" %-3d", reads_from->get_seq_number()); - else if (reads_from_promise) { - int idx = reads_from_promise->get_index(); - if (idx >= 0) - model_print(" P%-2d", idx); - else - model_print(" P? "); - } else + else model_print(" ? "); } if (cv) { @@ -631,39 +610,11 @@ unsigned int ModelAction::hash() const if (is_read()) { if (reads_from) hash ^= reads_from->get_seq_number(); - else if (reads_from_promise) - hash ^= reads_from_promise->get_index(); hash ^= get_reads_from_value(); } return hash; } -/** - * @brief Checks the NodeStack to see if a ModelAction is in our may-read-from set - * @param write The ModelAction to check for - * @return True if the ModelAction is found; false otherwise - */ -bool ModelAction::may_read_from(const ModelAction *write) const -{ - for (int i = 0; i < node->get_read_from_past_size(); i++) - if (node->get_read_from_past(i) == write) - return true; - return false; -} - -/** - * @brief Checks the NodeStack to see if a Promise is in our may-read-from set - * @param promise The Promise to check for - * @return True if the Promise is found; false otherwise - */ -bool ModelAction::may_read_from(const Promise *promise) const -{ - for (int i = 0; i < node->get_read_from_promise_size(); i++) - if (node->get_read_from_promise(i) == promise) - return true; - return false; -} - /** * Only valid for LOCK, TRY_LOCK, UNLOCK, and WAIT operations. * @return The mutex operated on by this action, if any; otherwise NULL diff --git a/action.h b/action.h index b0b3d51a..b815449f 100644 --- a/action.h +++ b/action.h @@ -16,7 +16,6 @@ /* Forward declarations */ class ClockVector; class Thread; -class Promise; namespace cdsc { class mutex; @@ -111,14 +110,12 @@ public: uint64_t get_write_value() const; uint64_t get_return_value() const; const ModelAction * get_reads_from() const { return reads_from; } - Promise * get_reads_from_promise() const { return reads_from_promise; } cdsc::mutex * get_mutex() const; Node * get_node() const; void set_node(Node *n) { node = n; } void set_read_from(const ModelAction *act); - void set_read_from_promise(Promise *promise); /** Store the most recent fence-release from the same thread * @param fence The fence-release that occured prior to this */ @@ -186,10 +183,7 @@ public: unsigned int hash() const; bool equals(const ModelAction *x) const { return this == x; } - bool equals(const Promise *x) const { return false; } - bool may_read_from(const ModelAction *write) const; - bool may_read_from(const Promise *promise) const; MEMALLOC void set_value(uint64_t val) { value = val; } @@ -227,13 +221,6 @@ private: */ const ModelAction *reads_from; - /** - * @brief The promise that this action reads from - * - * Only valid for reads - */ - Promise *reads_from_promise; - /** @brief The last fence release from the same thread */ const ModelAction *last_fence_release; diff --git a/cyclegraph.cc b/cyclegraph.cc index def51f96..6700b7d8 100644 --- a/cyclegraph.cc +++ b/cyclegraph.cc @@ -1,7 +1,6 @@ #include "cyclegraph.h" #include "action.h" #include "common.h" -#include "promise.h" #include "threads-model.h" /** Initializes a CycleGraph object. */ diff --git a/execution.cc b/execution.cc index 8fdc9fbe..c63b45ba 100644 --- a/execution.cc +++ b/execution.cc @@ -11,7 +11,6 @@ #include "common.h" #include "clockvector.h" #include "cyclegraph.h" -#include "promise.h" #include "datarace.h" #include "threads-model.h" #include "bugmessage.h" diff --git a/model.cc b/model.cc index c4bcaf9b..a4bba3cf 100644 --- a/model.cc +++ b/model.cc @@ -101,50 +101,7 @@ Thread * ModelChecker::get_next_thread() * Have we completed exploring the preselected path? Then let the * scheduler decide */ - if (diverge == NULL) // W: diverge is set to NULL permanently - return scheduler->select_next_thread(node_stack->get_head()); - - /* Else, we are trying to replay an execution */ - ModelAction *next = node_stack->get_next()->get_action(); - - if (next == diverge) { - if (earliest_diverge == NULL || *diverge < *earliest_diverge) - earliest_diverge = diverge; - - Node *nextnode = next->get_node(); - Node *prevnode = nextnode->get_parent(); - scheduler->update_sleep_set(prevnode); - - /* Reached divergence point */ - if (nextnode->increment_behaviors()) { - /* Execute the same thread with a new behavior */ - tid = next->get_tid(); - node_stack->pop_restofstack(2); - } else { - ASSERT(prevnode); - /* Make a different thread execute for next step */ - scheduler->add_sleep(get_thread(next->get_tid())); - tid = prevnode->get_next_backtrack(); - /* Make sure the backtracked thread isn't sleeping. */ - node_stack->pop_restofstack(1); - if (diverge == earliest_diverge) { - earliest_diverge = prevnode->get_action(); - } - } - /* Start the round robin scheduler from this thread id */ - scheduler->set_scheduler_thread(tid); - /* The correct sleep set is in the parent node. */ - execute_sleep_set(); - - DEBUG("*** Divergence point ***\n"); - - diverge = NULL; - } else { - tid = next->get_tid(); - } - DEBUG("*** ModelChecker chose next thread = %d ***\n", id_to_int(tid)); - ASSERT(tid != THREAD_ID_T_NONE); - return get_thread(id_to_int(tid)); + return scheduler->select_next_thread(node_stack->get_head()); } /** @@ -319,8 +276,7 @@ bool ModelChecker::next_execution() // test code execution_number++; reset_to_initial_state(); - node_stack->pop_restofstack(2); -// node_stack->full_reset(); + node_stack->full_reset(); diverge = NULL; return false; /* test diff --git a/model.h b/model.h index cdc317c9..18fcf0be 100644 --- a/model.h +++ b/model.h @@ -20,7 +20,6 @@ class Node; class NodeStack; class CycleGraph; -class Promise; class Scheduler; class Thread; class ClockVector; diff --git a/nodestack.cc b/nodestack.cc index fed7545f..a853321c 100644 --- a/nodestack.cc +++ b/nodestack.cc @@ -28,119 +28,15 @@ * execution trace. */ Node::Node(const struct model_params *params, ModelAction *act, Node *par, - int nthreads, Node *prevfairness) : - read_from_status(READ_FROM_PAST), + int nthreads) : action(act), params(params), uninit_action(NULL), parent(par), - num_threads(nthreads), - explored_children(num_threads), - backtrack(num_threads), - fairness(num_threads), - numBacktracks(0), - enabled_array(NULL), - read_from_past(), - read_from_past_idx(0), - read_from_promises(), - read_from_promise_idx(-1), - future_values(), - future_index(-1), - resolve_promise(), - resolve_promise_idx(-1), - relseq_break_writes(), - relseq_break_index(0), - misc_index(0), - misc_max(0), - yield_data(NULL) + num_threads(nthreads) { ASSERT(act); act->set_node(this); - int currtid = id_to_int(act->get_tid()); - int prevtid = prevfairness ? id_to_int(prevfairness->action->get_tid()) : 0; - - if (get_params()->fairwindow != 0) { - for (int i = 0; i < num_threads; i++) { - ASSERT(i < ((int)fairness.size())); - struct fairness_info *fi = &fairness[i]; - struct fairness_info *prevfi = (parent && i < parent->get_num_threads()) ? &parent->fairness[i] : NULL; - if (prevfi) { - *fi = *prevfi; - } - if (parent && parent->is_enabled(int_to_id(i))) { - fi->enabled_count++; - } - if (i == currtid) { - fi->turns++; - fi->priority = false; - } - /* Do window processing */ - if (prevfairness != NULL) { - if (prevfairness->parent->is_enabled(int_to_id(i))) - fi->enabled_count--; - if (i == prevtid) { - fi->turns--; - } - /* Need full window to start evaluating - * conditions - * If we meet the enabled count and have no - * turns, give us priority */ - if ((fi->enabled_count >= get_params()->enabledcount) && - (fi->turns == 0)) - fi->priority = true; - } - } - } -} - -int Node::get_yield_data(int tid1, int tid2) const { - if (tid1get_tid()); - - for(int u = 0; u < num_threads; u++) { - for(int v = 0; v < num_threads; v++) { - int yield_state=parent->get_yield_data(u, v); - bool next_enabled=scheduler->is_enabled(int_to_id(v)); - bool curr_enabled=parent->is_enabled(int_to_id(v)); - if (!next_enabled) { - //Compute intersection of ES and E - yield_state&=~YIELD_E; - //Check to see if we disabled the thread - if (u==curr_tid && curr_enabled) - yield_state|=YIELD_D; - } - yield_data[YIELD_INDEX(u, v, num_threads)]=yield_state; - } - yield_data[YIELD_INDEX(u, curr_tid, num_threads)]=(yield_data[YIELD_INDEX(u, curr_tid, num_threads)]&~YIELD_P)|YIELD_S; - } - //handle curr.yield(t) part of computation - if (action->is_yield()) { - for(int v = 0; v < num_threads; v++) { - int yield_state=yield_data[YIELD_INDEX(curr_tid, v, num_threads)]; - if ((yield_state & (YIELD_E | YIELD_D)) && (!(yield_state & YIELD_S))) - yield_state |= YIELD_P; - yield_state &= YIELD_P; - if (scheduler->is_enabled(int_to_id(v))) { - yield_state|=YIELD_E; - } - yield_data[YIELD_INDEX(curr_tid, v, num_threads)]=yield_state; - } - } } /** @brief Node desctructor */ @@ -149,610 +45,12 @@ Node::~Node() delete action; if (uninit_action) delete uninit_action; - if (enabled_array) - model_free(enabled_array); - if (yield_data) - model_free(yield_data); } /** Prints debugging info for the ModelAction associated with this Node */ void Node::print() const { action->print(); - model_print(" thread status: "); - if (enabled_array) { - for (int i = 0; i < num_threads; i++) { - char str[20]; - enabled_type_to_string(enabled_array[i], str); - model_print("[%d: %s]", i, str); - } - model_print("\n"); - } else - model_print("(info not available)\n"); - model_print(" backtrack: %s", backtrack_empty() ? "empty" : "non-empty "); - for (int i = 0; i < (int)backtrack.size(); i++) - if (backtrack[i] == true) - model_print("[%d]", i); - model_print("\n"); - - model_print(" read from past: %s", read_from_past_empty() ? "empty" : "non-empty "); - for (int i = read_from_past_idx + 1; i < (int)read_from_past.size(); i++) - model_print("[%d]", read_from_past[i]->get_seq_number()); - model_print("\n"); - - model_print(" read-from promises: %s", read_from_promise_empty() ? "empty" : "non-empty "); - for (int i = read_from_promise_idx + 1; i < (int)read_from_promises.size(); i++) - model_print("[%d]", read_from_promises[i]->get_seq_number()); - model_print("\n"); - - model_print(" future values: %s", future_value_empty() ? "empty" : "non-empty "); - for (int i = future_index + 1; i < (int)future_values.size(); i++) - model_print("[%#" PRIx64 "]", future_values[i].value); - model_print("\n"); - - model_print(" promises: %s\n", promise_empty() ? "empty" : "non-empty"); - model_print(" misc: %s\n", misc_empty() ? "empty" : "non-empty"); - model_print(" rel seq break: %s\n", relseq_break_empty() ? "empty" : "non-empty"); -} - -/****************************** threads backtracking **************************/ - -/** - * Checks if the Thread associated with this thread ID has been explored from - * this Node already. - * @param tid is the thread ID to check - * @return true if this thread choice has been explored already, false - * otherwise - */ -bool Node::has_been_explored(thread_id_t tid) const -{ - int id = id_to_int(tid); - return explored_children[id]; -} - -/** - * Checks if the backtracking set is empty. - * @return true if the backtracking set is empty - */ -bool Node::backtrack_empty() const -{ - return (numBacktracks == 0); -} - -void Node::explore(thread_id_t tid) -{ - int i = id_to_int(tid); - ASSERT(i < ((int)backtrack.size())); - if (backtrack[i]) { - backtrack[i] = false; - numBacktracks--; - } - explored_children[i] = true; -} - -/** - * Mark the appropriate backtracking information for exploring a thread choice. - * @param act The ModelAction to explore - */ -void Node::explore_child(ModelAction *act, enabled_type_t *is_enabled) -{ - if (!enabled_array) - enabled_array = (enabled_type_t *)model_malloc(sizeof(enabled_type_t) * num_threads); - if (is_enabled != NULL) - memcpy(enabled_array, is_enabled, sizeof(enabled_type_t) * num_threads); - else { - for (int i = 0; i < num_threads; i++) - enabled_array[i] = THREAD_DISABLED; - } - - explore(act->get_tid()); -} - -/** - * Records a backtracking reference for a thread choice within this Node. - * Provides feedback as to whether this thread choice is already set for - * backtracking. - * @return false if the thread was already set to be backtracked, true - * otherwise - */ -bool Node::set_backtrack(thread_id_t id) -{ - int i = id_to_int(id); - ASSERT(i < ((int)backtrack.size())); - if (backtrack[i]) - return false; - backtrack[i] = true; - numBacktracks++; - return true; -} - -thread_id_t Node::get_next_backtrack() -{ - /** @todo Find next backtrack */ - unsigned int i; - for (i = 0; i < backtrack.size(); i++) - if (backtrack[i] == true) - break; - /* Backtrack set was empty? */ - ASSERT(i != backtrack.size()); - - backtrack[i] = false; - numBacktracks--; - return int_to_id(i); -} - -void Node::clear_backtracking() -{ - for (unsigned int i = 0; i < backtrack.size(); i++) - backtrack[i] = false; - for (unsigned int i = 0; i < explored_children.size(); i++) - explored_children[i] = false; - numBacktracks = 0; -} - -/************************** end threads backtracking **************************/ - -/*********************************** promise **********************************/ - -/** - * Sets a promise to explore meeting with the given node. - * @param i is the promise index. - */ -void Node::set_promise(unsigned int i) -{ - if (i >= resolve_promise.size()) - resolve_promise.resize(i + 1, false); - resolve_promise[i] = true; -} - -/** - * Looks up whether a given promise should be satisfied by this node. - * @param i The promise index. - * @return true if the promise should be satisfied by the given ModelAction. - */ -bool Node::get_promise(unsigned int i) const -{ - return (i < resolve_promise.size()) && (int)i == resolve_promise_idx; -} - -/** - * Increments to the next promise to resolve. - * @return true if we have a valid combination. - */ -bool Node::increment_promise() -{ - DBG(); - if (resolve_promise.empty()) - return false; - int prev_idx = resolve_promise_idx; - resolve_promise_idx++; - for ( ; resolve_promise_idx < (int)resolve_promise.size(); resolve_promise_idx++) - if (resolve_promise[resolve_promise_idx]) - return true; - resolve_promise_idx = prev_idx; - return false; -} - -/** - * Returns whether the promise set is empty. - * @return true if we have explored all promise combinations. - */ -bool Node::promise_empty() const -{ - for (int i = resolve_promise_idx + 1; i < (int)resolve_promise.size(); i++) - if (i >= 0 && resolve_promise[i]) - return false; - return true; -} - -/** @brief Clear any promise-resolution information for this Node */ -void Node::clear_promise_resolutions() -{ - resolve_promise.clear(); - resolve_promise_idx = -1; -} - -/******************************* end promise **********************************/ - -void Node::set_misc_max(int i) -{ - misc_max = i; -} - -int Node::get_misc() const -{ - return misc_index; -} - -bool Node::increment_misc() -{ - return (misc_index < misc_max) && ((++misc_index) < misc_max); -} - -bool Node::misc_empty() const -{ - return (misc_index + 1) >= misc_max; -} - -bool Node::is_enabled(Thread *t) const -{ - int thread_id = id_to_int(t->get_id()); - return thread_id < num_threads && (enabled_array[thread_id] != THREAD_DISABLED); -} - -enabled_type_t Node::enabled_status(thread_id_t tid) const -{ - int thread_id = id_to_int(tid); - if (thread_id < num_threads) - return enabled_array[thread_id]; - else - return THREAD_DISABLED; -} - -bool Node::is_enabled(thread_id_t tid) const -{ - int thread_id = id_to_int(tid); - return thread_id < num_threads && (enabled_array[thread_id] != THREAD_DISABLED); -} - -bool Node::has_priority(thread_id_t tid) const -{ - return fairness[id_to_int(tid)].priority; -} - -bool Node::has_priority_over(thread_id_t tid1, thread_id_t tid2) const -{ - return get_yield_data(id_to_int(tid1), id_to_int(tid2)) & YIELD_P; -} - -/*********************************** read from ********************************/ - -/** - * Get the current state of the may-read-from set iteration - * @return The read-from type we should currently be checking (past or future) - */ -read_from_type_t Node::get_read_from_status() -{ - if (read_from_status == READ_FROM_PAST && read_from_past.empty()) - increment_read_from(); - return read_from_status; -} - -/** - * Iterate one step in the may-read-from iteration. This includes a step in - * reading from the either the past or the future. - * @return True if there is a new read-from to explore; false otherwise - */ -bool Node::increment_read_from() -{ - clear_promise_resolutions(); - if (increment_read_from_past()) { - read_from_status = READ_FROM_PAST; - return true; - } else if (increment_read_from_promise()) { - read_from_status = READ_FROM_PROMISE; - return true; - } else if (increment_future_value()) { - read_from_status = READ_FROM_FUTURE; - return true; - } - read_from_status = READ_FROM_NONE; - return false; -} - -/** - * @return True if there are any new read-froms to explore - */ -bool Node::read_from_empty() const -{ - return read_from_past_empty() && - read_from_promise_empty() && - future_value_empty(); -} - -/** - * Get the total size of the may-read-from set, including both past and future - * values - * @return The size of may-read-from - */ -unsigned int Node::read_from_size() const -{ - return read_from_past.size() + - read_from_promises.size() + - future_values.size(); -} - -/******************************* end read from ********************************/ - -/****************************** read from past ********************************/ - -/** @brief Prints info about read_from_past set */ -void Node::print_read_from_past() -{ - for (unsigned int i = 0; i < read_from_past.size(); i++) - read_from_past[i]->print(); -} - -/** - * Add an action to the read_from_past set. - * @param act is the action to add - */ -void Node::add_read_from_past(const ModelAction *act) -{ - read_from_past.push_back(act); -} - -/** - * Gets the next 'read_from_past' action from this Node. Only valid for a node - * where this->action is a 'read'. - * @return The first element in read_from_past - */ -const ModelAction * Node::get_read_from_past() const -{ - if (read_from_past_idx < read_from_past.size()) { - int random_index = rand() % read_from_past.size(); - return read_from_past[random_index]; - } -// return read_from_past[read_from_past_idx]; - else - return NULL; -} - -const ModelAction * Node::get_read_from_past(int i) const -{ - return read_from_past[i]; -} - -int Node::get_read_from_past_size() const -{ - return read_from_past.size(); -} - -/** - * Checks whether the readsfrom set for this node is empty. - * @return true if the readsfrom set is empty. - */ -bool Node::read_from_past_empty() const -{ - return ((read_from_past_idx + 1) >= read_from_past.size()); -} - -/** - * Increments the index into the readsfrom set to explore the next item. - * @return Returns false if we have explored all items. - */ -bool Node::increment_read_from_past() -{ - DBG(); - if (read_from_past_idx < read_from_past.size()) { - read_from_past_idx++; - return read_from_past_idx < read_from_past.size(); - } - return false; -} - -/************************** end read from past ********************************/ - -/***************************** read_from_promises *****************************/ - -/** - * Add an action to the read_from_promises set. - * @param reader The read which generated the Promise; we use the ModelAction - * instead of the Promise because the Promise does not last across executions - */ -void Node::add_read_from_promise(const ModelAction *reader) -{ - read_from_promises.push_back(reader); -} - -/** - * Gets the next 'read-from-promise' from this Node. Only valid for a node - * where this->action is a 'read'. - * @return The current element in read_from_promises - */ -Promise * Node::get_read_from_promise() const -{ - ASSERT(read_from_promise_idx >= 0 && read_from_promise_idx < ((int)read_from_promises.size())); - return read_from_promises[read_from_promise_idx]->get_reads_from_promise(); -} - -/** - * Gets a particular 'read-from-promise' form this Node. Only vlaid for a node - * where this->action is a 'read'. - * @param i The index of the Promise to get - * @return The Promise at index i, if the Promise is still available; NULL - * otherwise - */ -Promise * Node::get_read_from_promise(int i) const -{ - return read_from_promises[i]->get_reads_from_promise(); -} - -/** @return The size of the read-from-promise set */ -int Node::get_read_from_promise_size() const -{ - return read_from_promises.size(); -} - -/** - * Checks whether the read_from_promises set for this node is empty. - * @return true if the read_from_promises set is empty. - */ -bool Node::read_from_promise_empty() const -{ - return ((read_from_promise_idx + 1) >= ((int)read_from_promises.size())); -} - -/** - * Increments the index into the read_from_promises set to explore the next item. - * @return Returns false if we have explored all promises. - */ -bool Node::increment_read_from_promise() -{ - DBG(); - if (read_from_promise_idx < ((int)read_from_promises.size())) { - read_from_promise_idx++; - return (read_from_promise_idx < ((int)read_from_promises.size())); - } - return false; -} - -/************************* end read_from_promises *****************************/ - -/****************************** future values *********************************/ - -/** - * Adds a value from a weakly ordered future write to backtrack to. This - * operation may "fail" if the future value has already been run (within some - * sloppiness window of this expiration), or if the futurevalues set has - * reached its maximum. - * @see model_params.maxfuturevalues - * - * @param value is the value to backtrack to. - * @return True if the future value was successully added; false otherwise - */ -bool Node::add_future_value(struct future_value fv) -{ - uint64_t value = fv.value; - modelclock_t expiration = fv.expiration; - thread_id_t tid = fv.tid; - int idx = -1; /* Highest index where value is found */ - for (unsigned int i = 0; i < future_values.size(); i++) { - if (future_values[i].value == value && future_values[i].tid == tid) { - if (expiration <= future_values[i].expiration) - return false; - idx = i; - } - } - if (idx > future_index) { - /* Future value hasn't been explored; update expiration */ - future_values[idx].expiration = expiration; - return true; - } else if (idx >= 0 && expiration <= future_values[idx].expiration + get_params()->expireslop) { - /* Future value has been explored and is within the "sloppy" window */ - return false; - } - - /* Limit the size of the future-values set */ - if (get_params()->maxfuturevalues > 0 && - (int)future_values.size() >= get_params()->maxfuturevalues) - return false; - - future_values.push_back(fv); - return true; -} - -/** - * Gets the next 'future_value' from this Node. Only valid for a node where - * this->action is a 'read'. - * @return The first element in future_values - */ -struct future_value Node::get_future_value() const -{ - ASSERT(future_index >= 0 && future_index < ((int)future_values.size())); - return future_values[future_index]; -} - -/** - * Checks whether the future_values set for this node is empty. - * @return true if the future_values set is empty. - */ -bool Node::future_value_empty() const -{ - return ((future_index + 1) >= ((int)future_values.size())); -} - -/** - * Increments the index into the future_values set to explore the next item. - * @return Returns false if we have explored all values. - */ -bool Node::increment_future_value() -{ - DBG(); - if (future_index < ((int)future_values.size())) { - future_index++; - return (future_index < ((int)future_values.size())); - } - return false; -} - -/************************** end future values *********************************/ - -/*********************** breaking release sequences ***************************/ - -/** - * Add a write ModelAction to the set of writes that may break the release - * sequence. This is used during replay exploration of pending release - * sequences. This Node must correspond to a release sequence fixup action. - * - * @param write The write that may break the release sequence. NULL means we - * allow the release sequence to synchronize. - */ -void Node::add_relseq_break(const ModelAction *write) -{ - relseq_break_writes.push_back(write); -} - -/** - * Get the write that may break the current pending release sequence, - * according to the replay / divergence pattern. - * - * @return A write that may break the release sequence. If NULL, that means - * the release sequence should not be broken. - */ -const ModelAction * Node::get_relseq_break() const -{ - if (relseq_break_index < (int)relseq_break_writes.size()) - return relseq_break_writes[relseq_break_index]; - else - return NULL; -} - -/** - * Increments the index into the relseq_break_writes set to explore the next - * item. - * @return Returns false if we have explored all values. - */ -bool Node::increment_relseq_break() -{ - DBG(); - if (relseq_break_index < ((int)relseq_break_writes.size())) { - relseq_break_index++; - return (relseq_break_index < ((int)relseq_break_writes.size())); - } - return false; -} - -/** - * @return True if all writes that may break the release sequence have been - * explored - */ -bool Node::relseq_break_empty() const -{ - return ((relseq_break_index + 1) >= ((int)relseq_break_writes.size())); -} - -/******************* end breaking release sequences ***************************/ - -/** - * Increments some behavior's index, if a new behavior is available - * @return True if there is a new behavior available; otherwise false - */ -bool Node::increment_behaviors() -{ - /* satisfy a different misc_index values */ - if (increment_misc()) - return true; - /* satisfy a different set of promises */ - if (increment_promise()) - return true; - /* read from a different value */ - if (increment_read_from()) - return true; - /* resolve a release sequence differently */ - if (increment_relseq_break()) - return true; - return false; } NodeStack::NodeStack() : @@ -801,46 +99,18 @@ ModelAction * NodeStack::explore_action(ModelAction *act, enabled_type_t *is_ena { DBG(); - if ((head_idx + 1) < (int)node_list.size()) { - head_idx++; - return node_list[head_idx]->get_action(); - } - /* Record action */ Node *head = get_head(); - Node *prevfairness = NULL; - if (head) { - head->explore_child(act, is_enabled); - if (get_params()->fairwindow != 0 && head_idx > (int)get_params()->fairwindow) - prevfairness = node_list[head_idx - get_params()->fairwindow]; - } int next_threads = execution->get_num_threads(); if (act->get_type() == THREAD_CREATE || act->get_type() == PTHREAD_CREATE ) // may need to be changed next_threads++; - node_list.push_back(new Node(get_params(), act, head, next_threads, prevfairness)); + node_list.push_back(new Node(get_params(), act, head, next_threads)); total_nodes++; head_idx++; return NULL; } -/** - * Empties the stack of all trailing nodes after a given position and calls the - * destructor for each. This function is provided an offset which determines - * how many nodes (relative to the current replay state) to save before popping - * the stack. - * @param numAhead gives the number of Nodes (including this Node) to skip over - * before removing nodes. - */ -void NodeStack::pop_restofstack(int numAhead) -{ - /* Diverging from previous execution; clear out remainder of list */ - unsigned int it = head_idx + numAhead; - for (unsigned int i = it; i < node_list.size(); i++) - delete node_list[i]; - node_list.resize(it); - node_list.back()->clear_backtracking(); -} /** Reset the node stack. */ void NodeStack::full_reset() diff --git a/nodestack.h b/nodestack.h index 6ae96be8..c5da083c 100644 --- a/nodestack.h +++ b/nodestack.h @@ -10,7 +10,6 @@ #include "mymemory.h" #include "schedule.h" -#include "promise.h" #include "stl-model.h" class ModelAction; @@ -22,26 +21,6 @@ struct fairness_info { bool priority; }; -/** - * @brief Types of read-from relations - * - * Our "may-read-from" set is composed of multiple types of reads, and we have - * to iterate through all of them in the backtracking search. This enumeration - * helps to identify which type of read-from we are currently observing. - */ -typedef enum { - READ_FROM_PAST, /**< @brief Read from a prior, existing store */ - READ_FROM_PROMISE, /**< @brief Read from an existing promised future value */ - READ_FROM_FUTURE, /**< @brief Read from a newly-asserted future value */ - READ_FROM_NONE, /**< @brief A NULL state, which should not be reached */ -} read_from_type_t; - -#define YIELD_E 1 -#define YIELD_D 2 -#define YIELD_S 4 -#define YIELD_P 8 -#define YIELD_INDEX(tid1, tid2, num_threads) (tid1*num_threads+tid2) - /** * @brief A single node in a NodeStack @@ -55,18 +34,9 @@ typedef enum { class Node { public: Node(const struct model_params *params, ModelAction *act, Node *par, - int nthreads, Node *prevfairness); + int nthreads); ~Node(); - /* return true = thread choice has already been explored */ - bool has_been_explored(thread_id_t tid) const; - /* return true = backtrack set is empty */ - bool backtrack_empty() const; - - void clear_backtracking(); - void explore_child(ModelAction *act, enabled_type_t *is_enabled); - /* return false = thread was already in backtrack */ - bool set_backtrack(thread_id_t id); - thread_id_t get_next_backtrack(); + bool is_enabled(Thread *t) const; bool is_enabled(thread_id_t tid) const; enabled_type_t enabled_status(thread_id_t tid) const; @@ -83,97 +53,20 @@ public: * occurred previously in the stack. */ Node * get_parent() const { return parent; } - read_from_type_t get_read_from_status(); - bool increment_read_from(); - bool read_from_empty() const; - unsigned int read_from_size() const; - - void print_read_from_past(); - void add_read_from_past(const ModelAction *act); - const ModelAction * get_read_from_past() const; - const ModelAction * get_read_from_past(int i) const; - int get_read_from_past_size() const; - - void add_read_from_promise(const ModelAction *reader); - Promise * get_read_from_promise() const; - Promise * get_read_from_promise(int i) const; - int get_read_from_promise_size() const; - - bool add_future_value(struct future_value fv); - struct future_value get_future_value() const; - - void set_promise(unsigned int i); - bool get_promise(unsigned int i) const; - bool increment_promise(); - bool promise_empty() const; - void clear_promise_resolutions(); - - enabled_type_t *get_enabled_array() {return enabled_array;} - - void set_misc_max(int i); - int get_misc() const; - bool increment_misc(); - bool misc_empty() const; - void add_relseq_break(const ModelAction *write); - const ModelAction * get_relseq_break() const; - bool increment_relseq_break(); - bool relseq_break_empty() const; - - bool increment_behaviors(); void print() const; MEMALLOC private: - void explore(thread_id_t tid); - int get_yield_data(int tid1, int tid2) const; - bool read_from_past_empty() const; - bool increment_read_from_past(); - bool read_from_promise_empty() const; - bool increment_read_from_promise(); - bool future_value_empty() const; - bool increment_future_value(); - read_from_type_t read_from_status; const struct model_params * get_params() const { return params; } - ModelAction * const action; - const struct model_params * const params; /** @brief ATOMIC_UNINIT action which was created at this Node */ ModelAction *uninit_action; - Node * const parent; const int num_threads; - ModelVector explored_children; - ModelVector backtrack; - ModelVector fairness; - int numBacktracks; - enabled_type_t *enabled_array; - - /** - * The set of past ModelActions that this the action at this Node may - * read from. Only meaningful if this Node represents a 'read' action. - */ - ModelVector read_from_past; - unsigned int read_from_past_idx; - - ModelVector read_from_promises; - int read_from_promise_idx; - - ModelVector future_values; - int future_index; - - ModelVector resolve_promise; - int resolve_promise_idx; - - ModelVector relseq_break_writes; - int relseq_break_index; - - int misc_index; - int misc_max; - int * yield_data; }; typedef ModelVector node_list_t; @@ -197,7 +90,6 @@ public: Node * get_head() const; Node * get_next() const; void reset_execution(); - void pop_restofstack(int numAhead); void full_reset(); int get_total_nodes() { return total_nodes; } diff --git a/promise.cc b/promise.cc deleted file mode 100644 index a98403bb..00000000 --- a/promise.cc +++ /dev/null @@ -1,204 +0,0 @@ -#define __STDC_FORMAT_MACROS -#include - -#include "promise.h" -#include "execution.h" -#include "schedule.h" -#include "action.h" -#include "threads-model.h" - -/** - * @brief Promise constructor - * @param execution The execution which is creating this Promise - * @param read The read which reads from a promised future value - * @param fv The future value that is promised - */ -Promise::Promise(const ModelExecution *execution, ModelAction *read, struct future_value fv) : - execution(execution), - num_available_threads(0), - num_was_available_threads(0), - fv(fv), - readers(1, read), - write(NULL) -{ - add_thread(fv.tid); - eliminate_thread(read->get_tid()); -} - -/** - * Add a reader that reads from this Promise. Must be added in an order - * consistent with execution order. - * - * @param reader The ModelAction that reads from this promise. Must be a read. - * @return True if this new reader has invalidated the promise; false otherwise - */ -bool Promise::add_reader(ModelAction *reader) -{ - readers.push_back(reader); - return eliminate_thread(reader->get_tid()); -} - -/** - * Access a reader that read from this Promise. Readers must be inserted in - * order by execution order, so they can be returned in this order. - * - * @param i The index of the reader to return - * @return The i'th reader of this Promise - */ -ModelAction * Promise::get_reader(unsigned int i) const -{ - return i < readers.size() ? readers[i] : NULL; -} - -/** - * Eliminate a thread which no longer can satisfy this promise. Once all - * enabled threads have been eliminated, this promise is unresolvable. - * - * @param tid The thread ID of the thread to eliminate - * @return True, if this elimination has invalidated the promise; false - * otherwise - */ -bool Promise::eliminate_thread(thread_id_t tid) -{ - unsigned int id = id_to_int(tid); - if (!thread_is_available(tid)) - return false; - - available_thread[id] = false; - num_available_threads--; - return has_failed(); -} - -/** - * Add a thread which may resolve this promise - * - * @param tid The thread ID - */ -void Promise::add_thread(thread_id_t tid) -{ - unsigned int id = id_to_int(tid); - if (id >= available_thread.size()) - available_thread.resize(id + 1, false); - if (!available_thread[id]) { - available_thread[id] = true; - num_available_threads++; - } - if (id >= was_available_thread.size()) - was_available_thread.resize(id + 1, false); - if (!was_available_thread[id]) { - was_available_thread[id] = true; - num_was_available_threads++; - } -} - -/** - * Check if a thread is available for resolving this promise. That is, the - * thread must have been previously marked for resolving this promise, and it - * cannot have been eliminated due to synchronization, etc. - * - * @param tid Thread ID of the thread to check - * @return True if the thread is available; false otherwise - */ -bool Promise::thread_is_available(thread_id_t tid) const -{ - unsigned int id = id_to_int(tid); - if (id >= available_thread.size()) - return false; - return available_thread[id]; -} - -bool Promise::thread_was_available(thread_id_t tid) const -{ - unsigned int id = id_to_int(tid); - if (id >= was_available_thread.size()) - return false; - return was_available_thread[id]; -} - -/** - * @brief Get an upper bound on the number of available threads - * - * Gets an upper bound on the number of threads in the available threads set, - * useful for iterating over "thread_is_available()". - * - * @return The upper bound - */ -unsigned int Promise::max_available_thread_idx() const -{ - return available_thread.size(); -} - -/** @brief Print debug info about the Promise */ -void Promise::print() const -{ - model_print("Promised value %#" PRIx64 ", first read from thread %d, available threads to resolve: ", - fv.value, id_to_int(get_reader(0)->get_tid())); - bool failed = true; - for (unsigned int i = 0; i < available_thread.size(); i++) - if (available_thread[i]) { - model_print("[%d]", i); - failed = false; - } - if (failed) - model_print("(none)"); - model_print("\n"); -} - -/** - * Check if this promise has failed. A promise can fail when all threads which - * could possibly satisfy the promise have been eliminated. - * - * @return True, if this promise has failed; false otherwise - */ -bool Promise::has_failed() const -{ - return num_available_threads == 0; -} - -/** - * @brief Check if an action's thread and location are compatible for resolving - * this promise - * @param act The action to check against - * @return True if we are compatible; false otherwise - */ -bool Promise::is_compatible(const ModelAction *act) const -{ - return thread_is_available(act->get_tid()) && get_reader(0)->same_var(act); -} - -/** - * @brief Check if an action's thread and location are compatible for resolving - * this promise, and that the promise is thread-exclusive - * @param act The action to check against - * @return True if we are compatible and exclusive; false otherwise - */ -bool Promise::is_compatible_exclusive(const ModelAction *act) const -{ - return get_num_available_threads() == 1 && is_compatible(act); -} - -/** - * @brief Check if a store's value matches this Promise - * @param write The store to check - * @return True if the store's written value matches this Promise - */ -bool Promise::same_value(const ModelAction *write) const -{ - return get_value() == write->get_write_value(); -} - -/** - * @brief Check if a ModelAction's location matches this Promise - * @param act The ModelAction to check - * @return True if the action's location matches this Promise - */ -bool Promise::same_location(const ModelAction *act) const -{ - return get_reader(0)->same_var(act); -} - -/** @brief Get this Promise's index within the execution's promise array */ -int Promise::get_index() const -{ - return execution->get_promise_number(this); -} diff --git a/promise.h b/promise.h deleted file mode 100644 index e306e14a..00000000 --- a/promise.h +++ /dev/null @@ -1,78 +0,0 @@ -/** @file promise.h - * - * @brief Promise class --- tracks future obligations for execution - * related to weakly ordered writes. - */ - -#ifndef __PROMISE_H__ -#define __PROMISE_H__ - -#include - -#include "modeltypes.h" -#include "mymemory.h" -#include "stl-model.h" - -class ModelAction; -class ModelExecution; - -struct future_value { - uint64_t value; - modelclock_t expiration; - thread_id_t tid; -}; - -class Promise { - public: - Promise(const ModelExecution *execution, ModelAction *read, struct future_value fv); - bool add_reader(ModelAction *reader); - ModelAction * get_reader(unsigned int i) const; - unsigned int get_num_readers() const { return readers.size(); } - bool eliminate_thread(thread_id_t tid); - void add_thread(thread_id_t tid); - bool thread_is_available(thread_id_t tid) const; - bool thread_was_available(thread_id_t tid) const; - unsigned int max_available_thread_idx() const; - bool has_failed() const; - void set_write(const ModelAction *act) { write = act; } - const ModelAction * get_write() const { return write; } - int get_num_available_threads() const { return num_available_threads; } - int get_num_was_available_threads() const { return num_was_available_threads; } - bool is_compatible(const ModelAction *act) const; - bool is_compatible_exclusive(const ModelAction *act) const; - bool same_value(const ModelAction *write) const; - bool same_location(const ModelAction *act) const; - - modelclock_t get_expiration() const { return fv.expiration; } - uint64_t get_value() const { return fv.value; } - struct future_value get_fv() const { return fv; } - - int get_index() const; - - void print() const; - - bool equals(const Promise *x) const { return this == x; } - bool equals(const ModelAction *x) const { return false; } - - SNAPSHOTALLOC - private: - /** @brief The execution which created this Promise */ - const ModelExecution *execution; - - /** @brief Thread ID(s) for thread(s) that potentially can satisfy this - * promise */ - SnapVector available_thread; - SnapVector was_available_thread; - - int num_available_threads; - int num_was_available_threads; - - const future_value fv; - - /** @brief The action(s) which read the promised future value */ - SnapVector readers; - - const ModelAction *write; -}; - -#endif diff --git a/schedule.cc b/schedule.cc index 2a02e307..4ea351b1 100644 --- a/schedule.cc +++ b/schedule.cc @@ -131,15 +131,6 @@ enabled_type_t Scheduler::get_enabled(const Thread *t) const return enabled[id]; } -void Scheduler::update_sleep_set(Node *n) { - enabled_type_t *enabled_array = n->get_enabled_array(); - for (int i = 0; i < enabled_len; i++) { - if (enabled_array[i] == THREAD_SLEEP_SET) { - enabled[i] = THREAD_SLEEP_SET; - } - } -} - /** * Add a Thread to the sleep set. * @param t The Thread to add diff --git a/schedule.h b/schedule.h index 9b16a7a9..4269c4de 100644 --- a/schedule.h +++ b/schedule.h @@ -40,7 +40,6 @@ public: void remove_sleep(Thread *t); void add_sleep(Thread *t); enabled_type_t get_enabled(const Thread *t) const; - void update_sleep_set(Node *n); bool is_enabled(const Thread *t) const; bool is_enabled(thread_id_t tid) const; bool is_sleep_set(const Thread *t) const; -- 2.34.1