partial conversion to fuzzer
authorBrian Demsky <bdemsky@uci.edu>
Sat, 1 Jun 2019 05:21:31 +0000 (22:21 -0700)
committerBrian Demsky <bdemsky@uci.edu>
Sat, 1 Jun 2019 05:21:31 +0000 (22:21 -0700)
12 files changed:
action.cc
action.h
cyclegraph.cc
execution.cc
model.cc
model.h
nodestack.cc
nodestack.h
promise.cc [deleted file]
promise.h [deleted file]
schedule.cc
schedule.h

index 1416005..4e3b59a 100644 (file)
--- 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
index b0b3d51..b815449 100644 (file)
--- 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;
 
index def51f9..6700b7d 100644 (file)
@@ -1,7 +1,6 @@
 #include "cyclegraph.h"
 #include "action.h"
 #include "common.h"
-#include "promise.h"
 #include "threads-model.h"
 
 /** Initializes a CycleGraph object. */
index 8fdc9fb..c63b45b 100644 (file)
@@ -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"
index c4bcaf9..a4bba3c 100644 (file)
--- 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 cdc317c..18fcf0b 100644 (file)
--- a/model.h
+++ b/model.h
@@ -20,7 +20,6 @@
 class Node;
 class NodeStack;
 class CycleGraph;
-class Promise;
 class Scheduler;
 class Thread;
 class ClockVector;
index fed7545..a853321 100644 (file)
  * 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 (tid1<num_threads && tid2 < num_threads)
-               return yield_data[YIELD_INDEX(tid1,tid2,num_threads)];
-       else
-               return YIELD_S | YIELD_D;
-}
-
-void Node::update_yield(Scheduler * scheduler) {
-       if (yield_data==NULL)
-               yield_data=(int *) model_calloc(1, sizeof(int)*num_threads*num_threads);
-       //handle base case
-       if (parent == NULL) {
-               for(int i = 0; i < num_threads*num_threads; i++) {
-                       yield_data[i] = YIELD_S | YIELD_D;
-               }
-               return;
-       }
-       int curr_tid=id_to_int(action->get_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() 
index 6ae96be..c5da083 100644 (file)
@@ -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<bool> explored_children;
-       ModelVector<bool> backtrack;
-       ModelVector<struct fairness_info> 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<const ModelAction *> read_from_past;
-       unsigned int read_from_past_idx;
-
-       ModelVector<const ModelAction *> read_from_promises;
-       int read_from_promise_idx;
-
-       ModelVector<struct future_value> future_values;
-       int future_index;
-
-       ModelVector<bool> resolve_promise;
-       int resolve_promise_idx;
-
-       ModelVector<const ModelAction *> relseq_break_writes;
-       int relseq_break_index;
-
-       int misc_index;
-       int misc_max;
-       int * yield_data;
 };
 
 typedef ModelVector<Node *> 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 (file)
index a98403b..0000000
+++ /dev/null
@@ -1,204 +0,0 @@
-#define __STDC_FORMAT_MACROS
-#include <inttypes.h>
-
-#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 (file)
index e306e14..0000000
--- 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 <inttypes.h>
-
-#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<bool> available_thread;
-       SnapVector<bool> 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<ModelAction *> readers;
-
-       const ModelAction *write;
-};
-
-#endif
index 2a02e30..4ea351b 100644 (file)
@@ -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
index 9b16a7a..4269c4d 100644 (file)
@@ -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;