Remove promises
authorbdemsky <bdemsky@uci.edu>
Sat, 1 Jun 2019 06:19:23 +0000 (23:19 -0700)
committerbdemsky <bdemsky@uci.edu>
Tue, 4 Jun 2019 04:36:31 +0000 (21:36 -0700)
17 files changed:
Makefile
action.cc
action.h
cyclegraph.cc
cyclegraph.h
execution.cc
execution.h
futex.cc
model.cc
model.h
nodestack.cc
nodestack.h
promise.cc [deleted file]
promise.h [deleted file]
pthread.cc
schedule.cc
test/userprog.c

index 94109b4..313445d 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -3,7 +3,7 @@ include common.mk
 OBJECTS := libthreads.o schedule.o model.o threads.o librace.o action.o \
           nodestack.o clockvector.o main.o snapshot-interface.o cyclegraph.o \
           datarace.o impatomic.o cmodelint.o \
-          snapshot.o malloc.o mymemory.o common.o mutex.o promise.o conditionvariable.o \
+          snapshot.o malloc.o mymemory.o common.o mutex.o conditionvariable.o \
           context.o execution.o libannotate.o pthread.o futex.o
 
 CPPFLAGS += -Iinclude -I.
index 1416005..8395c88 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,8 +610,6 @@ 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;
@@ -651,19 +628,6 @@ bool ModelAction::may_read_from(const ModelAction *write) const
        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..06d76c2 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,8 @@ 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 +222,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..439e619 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. */
@@ -33,49 +32,12 @@ void CycleGraph::putNode(const ModelAction *act, CycleNode *node)
 #endif
 }
 
-/**
- * Add a CycleNode to the graph, corresponding to a Promise
- * @param promise The Promise that should be added
- * @param node The CycleNode that corresponds to the Promise
- */
-void CycleGraph::putNode(const Promise *promise, CycleNode *node)
-{
-       promiseToNode.put(promise, node);
-#if SUPPORT_MOD_ORDER_DUMP
-       nodeList.push_back(node);
-#endif
-}
-
-/**
- * @brief Remove the Promise node from the graph
- * @param promise The promise to remove from the graph
- */
-void CycleGraph::erasePromiseNode(const Promise *promise)
-{
-       promiseToNode.put(promise, NULL);
-#if SUPPORT_MOD_ORDER_DUMP
-       /* Remove the promise node from nodeList */
-       CycleNode *node = getNode_noCreate(promise);
-       for (unsigned int i = 0; i < nodeList.size(); )
-               if (nodeList[i] == node)
-                       nodeList.erase(nodeList.begin() + i);
-               else
-                       i++;
-#endif
-}
-
 /** @return The corresponding CycleNode, if exists; otherwise NULL */
 CycleNode * CycleGraph::getNode_noCreate(const ModelAction *act) const
 {
        return actionToNode.get(act);
 }
 
-/** @return The corresponding CycleNode, if exists; otherwise NULL */
-CycleNode * CycleGraph::getNode_noCreate(const Promise *promise) const
-{
-       return promiseToNode.get(promise);
-}
-
 /**
  * @brief Returns the CycleNode corresponding to a given ModelAction
  *
@@ -94,101 +56,6 @@ CycleNode * CycleGraph::getNode(const ModelAction *action)
        return node;
 }
 
-/**
- * @brief Returns a CycleNode corresponding to a promise
- *
- * Gets (or creates, if none exist) a CycleNode corresponding to a promised
- * value.
- *
- * @param promise The Promise generated by a reader
- * @return The CycleNode corresponding to the Promise
- */
-CycleNode * CycleGraph::getNode(const Promise *promise)
-{
-       CycleNode *node = getNode_noCreate(promise);
-       if (node == NULL) {
-               node = new CycleNode(promise);
-               putNode(promise, node);
-       }
-       return node;
-}
-
-/**
- * Resolve/satisfy a Promise with a particular store ModelAction, taking care
- * of the CycleGraph cleanups, including merging any necessary CycleNodes.
- *
- * @param promise The Promise to resolve
- * @param writer The store that will resolve this Promise
- * @return false if the resolution results in a cycle (or fails in some other
- * way); true otherwise
- */
-bool CycleGraph::resolvePromise(const Promise *promise, ModelAction *writer)
-{
-       CycleNode *promise_node = promiseToNode.get(promise);
-       CycleNode *w_node = actionToNode.get(writer);
-       ASSERT(promise_node);
-
-       if (w_node)
-               return mergeNodes(w_node, promise_node);
-       /* No existing write-node; just convert the promise-node */
-       promise_node->resolvePromise(writer);
-       erasePromiseNode(promise_node->getPromise());
-       putNode(writer, promise_node);
-       return true;
-}
-
-/**
- * @brief Merge two CycleNodes that represent the same write
- *
- * Note that this operation cannot be rolled back.
- *
- * @param w_node The write ModelAction node with which to merge
- * @param p_node The Promise node to merge. Will be destroyed after this
- * function.
- *
- * @return false if the merge cannot succeed; true otherwise
- */
-bool CycleGraph::mergeNodes(CycleNode *w_node, CycleNode *p_node)
-{
-       ASSERT(!w_node->is_promise());
-       ASSERT(p_node->is_promise());
-
-       const Promise *promise = p_node->getPromise();
-       if (!promise->is_compatible(w_node->getAction()) ||
-                       !promise->same_value(w_node->getAction()))
-               return false;
-
-       /* Transfer the RMW */
-       CycleNode *promise_rmw = p_node->getRMW();
-       if (promise_rmw && promise_rmw != w_node->getRMW() && w_node->setRMW(promise_rmw))
-               return false;
-
-       /* Transfer back edges to w_node */
-       while (p_node->getNumBackEdges() > 0) {
-               CycleNode *back = p_node->removeBackEdge();
-               if (back == w_node)
-                       continue;
-               addNodeEdge(back, w_node);
-               if (hasCycles)
-                       return false;
-       }
-
-       /* Transfer forward edges to w_node */
-       while (p_node->getNumEdges() > 0) {
-               CycleNode *forward = p_node->removeEdge();
-               if (forward == w_node)
-                       continue;
-               addNodeEdge(w_node, forward);
-               if (hasCycles)
-                       return false;
-       }
-
-       erasePromiseNode(promise);
-       /* Not deleting p_node, to maintain consistency if mergeNodes() fails */
-
-       return !hasCycles;
-}
-
 /**
  * Adds an edge between two CycleNodes.
  * @param fromnode The edge comes from this CycleNode
@@ -275,7 +142,6 @@ void CycleGraph::addRMWEdge(const T *from, const ModelAction *rmw)
 }
 /* Instantiate two forms of CycleGraph::addRMWEdge */
 template void CycleGraph::addRMWEdge(const ModelAction *from, const ModelAction *rmw);
-template void CycleGraph::addRMWEdge(const Promise *from, const ModelAction *rmw);
 
 /**
  * @brief Adds an edge between objects
@@ -303,35 +169,16 @@ bool CycleGraph::addEdge(const T *from, const U *to)
 }
 /* Instantiate four forms of CycleGraph::addEdge */
 template bool CycleGraph::addEdge(const ModelAction *from, const ModelAction *to);
-template bool CycleGraph::addEdge(const ModelAction *from, const Promise *to);
-template bool CycleGraph::addEdge(const Promise *from, const ModelAction *to);
-template bool CycleGraph::addEdge(const Promise *from, const Promise *to);
 
 #if SUPPORT_MOD_ORDER_DUMP
 
 static void print_node(FILE *file, const CycleNode *node, int label)
 {
-       if (node->is_promise()) {
-               const Promise *promise = node->getPromise();
-               int idx = promise->get_index();
-               fprintf(file, "P%u", idx);
-               if (label) {
-                       int first = 1;
-                       fprintf(file, " [label=\"P%d, T", idx);
-                       for (unsigned int i = 0 ; i < promise->max_available_thread_idx(); i++)
-                               if (promise->thread_is_available(int_to_id(i))) {
-                                       fprintf(file, "%s%u", first ? "": ",", i);
-                                       first = 0;
-                               }
-                       fprintf(file, "\"]");
-               }
-       } else {
                const ModelAction *act = node->getAction();
                modelclock_t idx = act->get_seq_number();
                fprintf(file, "N%u", idx);
                if (label)
                        fprintf(file, " [label=\"N%u, T%u\"]", idx, act->get_tid());
-       }
 }
 
 static void print_edge(FILE *file, const CycleNode *from, const CycleNode *to, const char *prop)
@@ -358,7 +205,6 @@ void CycleGraph::dot_print_edge(FILE *file, const T *from, const U *to, const ch
        print_edge(file, fromnode, tonode, prop);
 }
 /* Instantiate two forms of CycleGraph::dot_print_edge */
-template void CycleGraph::dot_print_edge(FILE *file, const Promise *from, const ModelAction *to, const char *prop);
 template void CycleGraph::dot_print_edge(FILE *file, const ModelAction *from, const ModelAction *to, const char *prop);
 
 void CycleGraph::dumpNodes(FILE *file) const
@@ -434,41 +280,6 @@ bool CycleGraph::checkReachable(const T *from, const U *to) const
 /* Instantiate four forms of CycleGraph::checkReachable */
 template bool CycleGraph::checkReachable(const ModelAction *from,
                const ModelAction *to) const;
-template bool CycleGraph::checkReachable(const ModelAction *from,
-               const Promise *to) const;
-template bool CycleGraph::checkReachable(const Promise *from,
-               const ModelAction *to) const;
-template bool CycleGraph::checkReachable(const Promise *from,
-               const Promise *to) const;
-
-/** @return True, if the promise has failed; false otherwise */
-bool CycleGraph::checkPromise(const ModelAction *fromact, Promise *promise) const
-{
-       discovered->reset();
-       queue->clear();
-       CycleNode *from = actionToNode.get(fromact);
-
-       queue->push_back(from);
-       discovered->put(from, from);
-       while (!queue->empty()) {
-               const CycleNode *node = queue->back();
-               queue->pop_back();
-
-               if (node->getPromise() == promise)
-                       return true;
-               if (!node->is_promise())
-                       promise->eliminate_thread(node->getAction()->get_tid());
-
-               for (unsigned int i = 0; i < node->getNumEdges(); i++) {
-                       CycleNode *next = node->getEdge(i);
-                       if (!discovered->contains(next)) {
-                               discovered->put(next, next);
-                               queue->push_back(next);
-                       }
-               }
-       }
-       return false;
-}
 
 /** @brief Begin a new sequence of graph additions which can be rolled back */
 void CycleGraph::startChanges()
@@ -512,18 +323,6 @@ bool CycleGraph::checkForCycles() const
  */
 CycleNode::CycleNode(const ModelAction *act) :
        action(act),
-       promise(NULL),
-       hasRMW(NULL)
-{
-}
-
-/**
- * @brief Constructor for a Promise CycleNode
- * @param promise The Promise which was generated
- */
-CycleNode::CycleNode(const Promise *promise) :
-       action(NULL),
-       promise(promise),
        hasRMW(NULL)
 {
 }
@@ -640,19 +439,3 @@ bool CycleNode::setRMW(CycleNode *node)
        hasRMW = node;
        return false;
 }
-
-/**
- * Convert a Promise CycleNode into a concrete-valued CycleNode. Should only be
- * used when there's no existing ModelAction CycleNode for this write.
- *
- * @param writer The ModelAction which wrote the future value represented by
- * this CycleNode
- */
-void CycleNode::resolvePromise(const ModelAction *writer)
-{
-       ASSERT(is_promise());
-       ASSERT(promise->is_compatible(writer));
-       action = writer;
-       promise = NULL;
-       ASSERT(!is_promise());
-}
index 7e7d180..4f23e32 100644 (file)
@@ -17,7 +17,6 @@
 #include "mymemory.h"
 #include "stl-model.h"
 
-class Promise;
 class CycleNode;
 class ModelAction;
 
@@ -34,7 +33,6 @@ class CycleGraph {
        void addRMWEdge(const T *from, const ModelAction *rmw);
 
        bool checkForCycles() const;
-       bool checkPromise(const ModelAction *from, Promise *p) const;
 
        template <typename T, typename U>
        bool checkReachable(const T *from, const U *to) const;
@@ -51,18 +49,13 @@ class CycleGraph {
        void dot_print_edge(FILE *file, const T *from, const U *to, const char *prop);
 #endif
 
-       bool resolvePromise(const Promise *promise, ModelAction *writer);
 
        SNAPSHOTALLOC
  private:
        bool addNodeEdge(CycleNode *fromnode, CycleNode *tonode);
        void putNode(const ModelAction *act, CycleNode *node);
-       void putNode(const Promise *promise, CycleNode *node);
-       void erasePromiseNode(const Promise *promise);
        CycleNode * getNode(const ModelAction *act);
-       CycleNode * getNode(const Promise *promise);
        CycleNode * getNode_noCreate(const ModelAction *act) const;
-       CycleNode * getNode_noCreate(const Promise *promise) const;
        bool mergeNodes(CycleNode *node1, CycleNode *node2);
 
        HashTable<const CycleNode *, const CycleNode *, uintptr_t, 4, model_malloc, model_calloc, model_free> *discovered;
@@ -71,8 +64,6 @@ class CycleGraph {
 
        /** @brief A table for mapping ModelActions to CycleNodes */
        HashTable<const ModelAction *, CycleNode *, uintptr_t, 4> actionToNode;
-       /** @brief A table for mapping Promises to CycleNodes */
-       HashTable<const Promise *, CycleNode *, uintptr_t, 4> promiseToNode;
 
 #if SUPPORT_MOD_ORDER_DUMP
        SnapVector<CycleNode *> nodeList;
@@ -90,13 +81,11 @@ class CycleGraph {
 };
 
 /**
- * @brief A node within a CycleGraph; corresponds either to one ModelAction or
- * to a promised future value
+ * @brief A node within a CycleGraph; corresponds either to one ModelAction
  */
 class CycleNode {
  public:
        CycleNode(const ModelAction *act);
-       CycleNode(const Promise *promise);
        bool addEdge(CycleNode *node);
        CycleNode * getEdge(unsigned int i) const;
        unsigned int getNumEdges() const;
@@ -109,19 +98,12 @@ class CycleNode {
        CycleNode * getRMW() const;
        void clearRMW() { hasRMW = NULL; }
        const ModelAction * getAction() const { return action; }
-       const Promise * getPromise() const { return promise; }
-       bool is_promise() const { return !action; }
-       void resolvePromise(const ModelAction *writer);
 
        SNAPSHOTALLOC
  private:
        /** @brief The ModelAction that this node represents */
        const ModelAction *action;
 
-       /** @brief The promise represented by this node; only valid when action
-        * is NULL */
-       const Promise *promise;
-
        /** @brief The edges leading out from this node */
        SnapVector<CycleNode *> edges;
 
index 8fdc9fb..7a51bca 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"
@@ -28,8 +27,6 @@ struct model_snapshot_members {
                used_sequence_numbers(0),
                next_backtrack(NULL),
                bugs(),
-               failed_promise(false),
-               hard_failed_promise(false),
                too_many_reads(false),
                no_valid_reads(false),
                bad_synchronization(false),
@@ -47,8 +44,6 @@ struct model_snapshot_members {
        modelclock_t used_sequence_numbers;
        ModelAction *next_backtrack;
        SnapVector<bug_message *> bugs;
-       bool failed_promise;
-       bool hard_failed_promise;
        bool too_many_reads;
        bool no_valid_reads;
        /** @brief Incorrectly-ordered synchronization was made */
@@ -64,19 +59,18 @@ ModelExecution::ModelExecution(ModelChecker *m,
                const struct model_params *params,
                Scheduler *scheduler,
                NodeStack *node_stack) :
+       pthread_counter(0),
        model(m),
        params(params),
        scheduler(scheduler),
        action_trace(),
        thread_map(2), /* We'll always need at least 2 threads */
        pthread_map(0),
-       pthread_counter(0),
        obj_map(),
        condvar_waiters_map(),
        obj_thrd_map(),
        mutex_map(),
-       promises(),
-       futurevalues(),
+       cond_map(),
        pending_rel_seqs(),
        thrd_last_action(1),
        thrd_last_fence_release(),
@@ -97,9 +91,6 @@ ModelExecution::~ModelExecution()
        for (unsigned int i = 0; i < get_num_threads(); i++)
                delete get_thread(int_to_id(i));
 
-       for (unsigned int i = 0; i < promises.size(); i++)
-               delete promises[i];
-
        delete mo_graph;
        delete priv;
 }
@@ -635,30 +626,6 @@ bool ModelExecution::process_read(ModelAction *curr)
                        updated = r_modification_order(curr, rf);
                        read_from(curr, rf);
                        mo_graph->commitChanges();
-                       mo_check_promises(curr, true);
-                       break;
-               }
-               case READ_FROM_PROMISE: {
-                       Promise *promise = curr->get_node()->get_read_from_promise();
-                       if (promise->add_reader(curr))
-                               priv->failed_promise = true;
-                       curr->set_read_from_promise(promise);
-                       mo_graph->startChanges();
-                       if (!check_recency(curr, promise))
-                               priv->too_many_reads = true;
-                       updated = r_modification_order(curr, promise);
-                       mo_graph->commitChanges();
-                       break;
-               }
-               case READ_FROM_FUTURE: {
-                       /* Read from future value */
-                       struct future_value fv = node->get_future_value();
-                       Promise *promise = new Promise(this, curr, fv);
-                       curr->set_read_from_promise(promise);
-                       promises.push_back(promise);
-                       mo_graph->startChanges();
-                       updated = r_modification_order(curr, promise);
-                       mo_graph->commitChanges();
                        break;
                }
                default:
@@ -770,67 +737,6 @@ bool ModelExecution::process_mutex(ModelAction *curr)
        return false;
 }
 
-/**
- * @brief Check if the current pending promises allow a future value to be sent
- *
- * It is unsafe to pass a future value back if there exists a pending promise Pr
- * such that:
- *
- *    reader --exec-> Pr --exec-> writer
- *
- * If such Pr exists, we must save the pending future value until Pr is
- * resolved.
- *
- * @param writer The operation which sends the future value. Must be a write.
- * @param reader The operation which will observe the value. Must be a read.
- * @return True if the future value can be sent now; false if it must wait.
- */
-bool ModelExecution::promises_may_allow(const ModelAction *writer,
-               const ModelAction *reader) const
-{
-       for (int i = promises.size() - 1; i >= 0; i--) {
-               ModelAction *pr = promises[i]->get_reader(0);
-               //reader is after promise...doesn't cross any promise
-               if (*reader > *pr)
-                       return true;
-               //writer is after promise, reader before...bad...
-               if (*writer > *pr)
-                       return false;
-       }
-       return true;
-}
-
-/**
- * @brief Add a future value to a reader
- *
- * This function performs a few additional checks to ensure that the future
- * value can be feasibly observed by the reader
- *
- * @param writer The operation whose value is sent. Must be a write.
- * @param reader The read operation which may read the future value. Must be a read.
- */
-void ModelExecution::add_future_value(const ModelAction *writer, ModelAction *reader)
-{
-       /* Do more ambitious checks now that mo is more complete */
-       if (!mo_may_allow(writer, reader))
-               return;
-
-       Node *node = reader->get_node();
-
-       /* Find an ancestor thread which exists at the time of the reader */
-       Thread *write_thread = get_thread(writer);
-       while (id_to_int(write_thread->get_id()) >= node->get_num_threads())
-               write_thread = write_thread->get_parent();
-
-       struct future_value fv = {
-               writer->get_write_value(),
-               writer->get_seq_number() + params->maxfuturedelay,
-               write_thread->get_id(),
-       };
-       if (node->add_future_value(fv))
-               set_latest_backtrack(reader);
-}
-
 /**
  * Process a write ModelAction
  * @param curr The ModelAction to process
@@ -842,46 +748,13 @@ bool ModelExecution::process_write(ModelAction *curr, work_queue_t *work)
        /* Readers to which we may send our future value */
        ModelVector<ModelAction *> send_fv;
 
-       const ModelAction *earliest_promise_reader;
-       bool updated_promises = false;
-
-       bool updated_mod_order = w_modification_order(curr, &send_fv);
-       Promise *promise = pop_promise_to_resolve(curr);
-
-       if (promise) {
-               earliest_promise_reader = promise->get_reader(0);
-               updated_promises = resolve_promise(curr, promise, work);
-       } else
-               earliest_promise_reader = NULL;
-
-       for (unsigned int i = 0; i < send_fv.size(); i++) {
-               ModelAction *read = send_fv[i];
-
-               /* Don't send future values to reads after the Promise we resolve */
-               if (!earliest_promise_reader || *read < *earliest_promise_reader) {
-                       /* Check if future value can be sent immediately */
-                       if (promises_may_allow(curr, read)) {
-                               add_future_value(curr, read);
-                       } else {
-                               futurevalues.push_back(PendingFutureValue(curr, read));
-                       }
-               }
-       }
 
-       /* Check the pending future values */
-       for (int i = (int)futurevalues.size() - 1; i >= 0; i--) {
-               struct PendingFutureValue pfv = futurevalues[i];
-               if (promises_may_allow(pfv.writer, pfv.reader)) {
-                       add_future_value(pfv.writer, pfv.reader);
-                       futurevalues.erase(futurevalues.begin() + i);
-               }
-       }
+       bool updated_mod_order = w_modification_order(curr);
 
        mo_graph->commitChanges();
-       mo_check_promises(curr, false);
 
        get_thread(curr)->set_return_value(VALUE_NONE);
-       return updated_mod_order || updated_promises;
+       return updated_mod_order;
 }
 
 /**
@@ -957,12 +830,6 @@ bool ModelExecution::process_thread_action(ModelAction *curr)
                curr->set_thread_operand(th);
                add_thread(th);
                th->set_creation(curr);
-               /* Promises can be satisfied by children */
-               for (unsigned int i = 0; i < promises.size(); i++) {
-                       Promise *promise = promises[i];
-                       if (promise->thread_is_available(curr->get_tid()))
-                               promise->add_thread(th->get_id());
-               }
                break;
        }
        case PTHREAD_CREATE: {
@@ -978,13 +845,6 @@ bool ModelExecution::process_thread_action(ModelAction *curr)
                        pthread_map.resize( pthread_counter );
                pthread_map[ pthread_counter-1 ] = th;
 
-               /* Promises can be satisfied by children */
-               for (unsigned int i = 0; i < promises.size(); i++) {
-                       Promise *promise = promises[i];
-                       if (promise->thread_is_available(curr->get_tid()))
-                               promise->add_thread(th->get_id());
-               }
-               
                break;
        }
        case THREAD_JOIN: {
@@ -1012,18 +872,10 @@ bool ModelExecution::process_thread_action(ModelAction *curr)
                                scheduler->wake(waiting);
                }
                th->complete();
-               /* Completed thread can't satisfy promises */
-               for (unsigned int i = 0; i < promises.size(); i++) {
-                       Promise *promise = promises[i];
-                       if (promise->thread_is_available(th->get_id()))
-                               if (promise->eliminate_thread(th->get_id()))
-                                       priv->failed_promise = true;
-               }
                updated = true; /* trigger rel-seq checks */
                break;
        }
        case THREAD_START: {
-               check_promises(curr->get_tid(), NULL, curr->get_cv());
                break;
        }
        default:
@@ -1107,9 +959,6 @@ bool ModelExecution::initialize_curr_action(ModelAction **curr)
                newcurr = process_rmw(*curr);
                delete *curr;
 
-               if (newcurr->is_rmw())
-                       compute_promises(newcurr);
-
                *curr = newcurr;
                return false;
        }
@@ -1146,9 +995,7 @@ bool ModelExecution::initialize_curr_action(ModelAction **curr)
                 * Perform one-time actions when pushing new ModelAction onto
                 * NodeStack
                 */
-               if (newcurr->is_write())
-                       compute_promises(newcurr);
-               else if (newcurr->is_relseq_fixup())
+               if (newcurr->is_relseq_fixup())
                        compute_relseq_breakwrites(newcurr);
                else if (newcurr->is_wait())
                        newcurr->get_node()->set_misc_max(2);
@@ -1207,39 +1054,9 @@ bool ModelExecution::synchronize(const ModelAction *first, ModelAction *second)
                set_bad_synchronization();
                return false;
        }
-       check_promises(first->get_tid(), second->get_cv(), first->get_cv());
        return second->synchronize_with(first);
 }
 
-/**
- * Check promises and eliminate potentially-satisfying threads when a thread is
- * blocked (e.g., join, lock). A thread which is waiting on another thread can
- * no longer satisfy a promise generated from that thread.
- *
- * @param blocker The thread on which a thread is waiting
- * @param waiting The waiting thread
- */
-void ModelExecution::thread_blocking_check_promises(Thread *blocker, Thread *waiting)
-{
-       for (unsigned int i = 0; i < promises.size(); i++) {
-               Promise *promise = promises[i];
-               if (!promise->thread_is_available(waiting->get_id()))
-                       continue;
-               for (unsigned int j = 0; j < promise->get_num_readers(); j++) {
-                       ModelAction *reader = promise->get_reader(j);
-                       if (reader->get_tid() != blocker->get_id())
-                               continue;
-                       if (promise->eliminate_thread(waiting->get_id())) {
-                               /* Promise has failed */
-                               priv->failed_promise = true;
-                       } else {
-                               /* Only eliminate the 'waiting' thread once */
-                               return;
-                       }
-               }
-       }
-}
-
 /**
  * @brief Check whether a model action is enabled.
  *
@@ -1260,7 +1077,6 @@ bool ModelExecution::check_action_enabled(ModelAction *curr) {
        } else if (curr->is_thread_join()) {
                Thread *blocking = curr->get_thread_operand();
                if (!blocking->is_complete()) {
-                       thread_blocking_check_promises(blocking, get_thread(curr));
                        return false;
                }
        } else if (params->yieldblock && curr->is_yield()) {
@@ -1350,23 +1166,17 @@ ModelAction * ModelExecution::check_current_action(ModelAction *curr)
 
                        if (act->is_read()) {
                                const ModelAction *rf = act->get_reads_from();
-                               const Promise *promise = act->get_reads_from_promise();
-                               if (rf) {
-                                       if (r_modification_order(act, rf))
-                                               updated = true;
-                                       if (act->is_seqcst()) {
-                                               ModelAction *last_sc_write = get_last_seq_cst_write(act);
-                                               if (last_sc_write != NULL && rf->happens_before(last_sc_write)) {
-                                                       set_bad_sc_read();
-                                               }
-                                       }
-                               } else if (promise) {
-                                       if (r_modification_order(act, promise))
-                                               updated = true;
+                               if (r_modification_order(act, rf))
+                                 updated = true;
+                               if (act->is_seqcst()) {
+                                 ModelAction *last_sc_write = get_last_seq_cst_write(act);
+                                 if (last_sc_write != NULL && rf->happens_before(last_sc_write)) {
+                                   set_bad_sc_read();
+                                 }
                                }
                        }
                        if (act->is_write()) {
-                               if (w_modification_order(act, NULL))
+                               if (w_modification_order(act))
                                        updated = true;
                        }
                        mo_graph->commitChanges();
@@ -1394,22 +1204,11 @@ void ModelExecution::check_curr_backtracking(ModelAction *curr)
        if ((parnode && !parnode->backtrack_empty()) ||
                         !currnode->misc_empty() ||
                         !currnode->read_from_empty() ||
-                        !currnode->promise_empty() ||
                         !currnode->relseq_break_empty()) {
                set_latest_backtrack(curr);
        }
 }
 
-bool ModelExecution::promises_expired() const
-{
-       for (unsigned int i = 0; i < promises.size(); i++) {
-               Promise *promise = promises[i];
-               if (promise->get_expiration() < priv->used_sequence_numbers)
-                       return true;
-       }
-       return false;
-}
-
 /**
  * This is the strongest feasibility check available.
  * @return whether the current trace (partial or complete) must be a prefix of
@@ -1431,8 +1230,6 @@ void ModelExecution::print_infeasibility(const char *prefix) const
        char *ptr = buf;
        if (mo_graph->checkForCycles())
                ptr += sprintf(ptr, "[mo cycle]");
-       if (priv->failed_promise || priv->hard_failed_promise)
-               ptr += sprintf(ptr, "[failed promise]");
        if (priv->too_many_reads)
                ptr += sprintf(ptr, "[too many reads]");
        if (priv->no_valid_reads)
@@ -1441,10 +1238,6 @@ void ModelExecution::print_infeasibility(const char *prefix) const
                ptr += sprintf(ptr, "[bad sw ordering]");
        if (priv->bad_sc_read)
                ptr += sprintf(ptr, "[bad sc read]");
-       if (promises_expired())
-               ptr += sprintf(ptr, "[promise expired]");
-       if (promises.size() != 0)
-               ptr += sprintf(ptr, "[unresolved promise]");
        if (ptr != buf)
                model_print("%s: %s", prefix ? prefix : "Infeasible", buf);
 }
@@ -1455,7 +1248,7 @@ void ModelExecution::print_infeasibility(const char *prefix) const
  */
 bool ModelExecution::is_feasible_prefix_ignore_relseq() const
 {
-       return !is_infeasible() && promises.size() == 0 && ! priv->failed_promise;
+  return !is_infeasible() ;
 
 }
 
@@ -1471,9 +1264,7 @@ bool ModelExecution::is_infeasible() const
                priv->no_valid_reads ||
                priv->too_many_reads ||
                priv->bad_synchronization ||
-               priv->bad_sc_read ||
-               priv->hard_failed_promise ||
-               promises_expired();
+         priv->bad_sc_read;
 }
 
 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
@@ -1481,10 +1272,7 @@ ModelAction * ModelExecution::process_rmw(ModelAction *act) {
        ModelAction *lastread = get_last_action(act->get_tid());
        lastread->process_rmw(act);
        if (act->is_rmw()) {
-               if (lastread->get_reads_from())
-                       mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
-               else
-                       mo_graph->addRMWEdge(lastread->get_reads_from_promise(), lastread);
+         mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
                mo_graph->commitChanges();
        }
        return lastread;
@@ -1551,8 +1339,7 @@ bool ModelExecution::check_recency(ModelAction *curr, const T *rf) const
                return true;
 
        //NOTE: Next check is just optimization, not really necessary....
-       if (curr->get_node()->get_read_from_past_size() +
-                       curr->get_node()->get_read_from_promise_size() <= 1)
+       if (curr->get_node()->get_read_from_past_size() <= 1)
                return true;
 
        SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
@@ -1572,12 +1359,9 @@ bool ModelExecution::check_recency(ModelAction *curr, const T *rf) const
                ModelAction *act = *ritcopy;
                if (!act->is_read())
                        return true;
-               if (act->get_reads_from_promise() && !act->get_reads_from_promise()->equals(rf))
-                       return true;
                if (act->get_reads_from() && !act->get_reads_from()->equals(rf))
                        return true;
-               if (act->get_node()->get_read_from_past_size() +
-                               act->get_node()->get_read_from_promise_size() <= 1)
+               if (act->get_node()->get_read_from_past_size() <= 1)
                        return true;
        }
        for (int i = 0; i < curr->get_node()->get_read_from_past_size(); i++) {
@@ -1585,11 +1369,6 @@ bool ModelExecution::check_recency(ModelAction *curr, const T *rf) const
                if (should_read_instead(curr, rf, write))
                        return false; /* liveness failure */
        }
-       for (int i = 0; i < curr->get_node()->get_read_from_promise_size(); i++) {
-               const Promise *promise = curr->get_node()->get_read_from_promise(i);
-               if (should_read_instead(curr, rf, promise))
-                       return false; /* liveness failure */
-       }
        return true;
 }
 
@@ -1682,13 +1461,8 @@ bool ModelExecution::r_modification_order(ModelAction *curr, const rf_type *rf)
                                        added = mo_graph->addEdge(act, rf) || added;
                                } else {
                                        const ModelAction *prevrf = act->get_reads_from();
-                                       const Promise *prevrf_promise = act->get_reads_from_promise();
-                                       if (prevrf) {
-                                               if (!prevrf->equals(rf))
-                                                       added = mo_graph->addEdge(prevrf, rf) || added;
-                                       } else if (!prevrf_promise->equals(rf)) {
-                                               added = mo_graph->addEdge(prevrf_promise, rf) || added;
-                                       }
+                                       if (!prevrf->equals(rf))
+                                         added = mo_graph->addEdge(prevrf, rf) || added;
                                }
                                break;
                        }
@@ -1699,9 +1473,6 @@ bool ModelExecution::r_modification_order(ModelAction *curr, const rf_type *rf)
         * All compatible, thread-exclusive promises must be ordered after any
         * concrete loads from the same thread
         */
-       for (unsigned int i = 0; i < promises.size(); i++)
-               if (promises[i]->is_compatible_exclusive(curr))
-                       added = mo_graph->addEdge(rf, promises[i]) || added;
 
        return added;
 }
@@ -1730,7 +1501,7 @@ bool ModelExecution::r_modification_order(ModelAction *curr, const rf_type *rf)
  * value. If NULL, then don't record any future values.
  * @return True if modification order edges were added; false otherwise
  */
-bool ModelExecution::w_modification_order(ModelAction *curr, ModelVector<ModelAction *> *send_fv)
+bool ModelExecution::w_modification_order(ModelAction *curr)
 {
        SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
        unsigned int i;
@@ -1804,10 +1575,7 @@ bool ModelExecution::w_modification_order(ModelAction *curr, ModelVector<ModelAc
                                        added = mo_graph->addEdge(act, curr) || added;
                                else if (act->is_read()) {
                                        //if previous read accessed a null, just keep going
-                                       if (act->get_reads_from() == NULL) {
-                                               added = mo_graph->addEdge(act->get_reads_from_promise(), curr) || added;
-                                       } else
-                                               added = mo_graph->addEdge(act->get_reads_from(), curr) || added;
+                                 added = mo_graph->addEdge(act->get_reads_from(), curr) || added;
                                }
                                break;
                        } else if (act->is_read() && !act->could_synchronize_with(curr) &&
@@ -1825,94 +1593,13 @@ bool ModelExecution::w_modification_order(ModelAction *curr, ModelVector<ModelAc
 
                                 */
 
-                               if (send_fv && thin_air_constraint_may_allow(curr, act) && check_coherence_promise(curr, act)) {
-                                       if (!is_infeasible())
-                                               send_fv->push_back(act);
-                                       else if (curr->is_rmw() && act->is_rmw() && curr->get_reads_from() && curr->get_reads_from() == act->get_reads_from())
-                                               add_future_value(curr, act);
-                               }
                        }
                }
        }
 
-       /*
-        * All compatible, thread-exclusive promises must be ordered after any
-        * concrete stores to the same thread, or else they can be merged with
-        * this store later
-        */
-       for (unsigned int i = 0; i < promises.size(); i++)
-               if (promises[i]->is_compatible_exclusive(curr))
-                       added = mo_graph->addEdge(curr, promises[i]) || added;
-
        return added;
 }
 
-//This procedure uses cohere to prune future values that are
-//guaranteed to generate a coherence violation.
-//
-//need to see if there is (1) a promise for thread write, (2)
-//the promise is sb before write, (3) the promise can only be
-//resolved by the thread read, and (4) the promise has same
-//location as read/write
-
-bool ModelExecution::check_coherence_promise(const ModelAction * write, const ModelAction *read) {
-       thread_id_t write_tid=write->get_tid();
-       for(unsigned int i = promises.size(); i>0; i--) {
-               Promise *pr=promises[i-1];
-               if (!pr->same_location(write))
-                       continue;
-               //the reading thread is the only thread that can resolve the promise
-               if (pr->get_num_was_available_threads()==1 && pr->thread_was_available(read->get_tid())) {
-                       for(unsigned int j=0;j<pr->get_num_readers();j++) {
-                               ModelAction *prreader=pr->get_reader(j);
-                               //the writing thread reads from the promise before the write
-                               if (prreader->get_tid()==write_tid &&
-                                               (*prreader)<(*write)) {
-                                       if ((*read)>(*prreader)) {
-                                               //check that we don't have a read between the read and promise
-                                               //from the same thread as read
-                                               bool okay=false;
-                                               for(const ModelAction *tmp=read;tmp!=prreader;) {
-                                                       tmp=tmp->get_node()->get_parent()->get_action();
-                                                       if (tmp->is_read() && tmp->same_thread(read)) {
-                                                               okay=true;
-                                                               break;
-                                                       }
-                                               }
-                                               if (okay)
-                                                       continue;
-                                       }
-                                       return false;
-                               }
-                       }
-               }
-       }
-       return true;
-}
-
-
-/** Arbitrary reads from the future are not allowed.  Section 29.3
- * part 9 places some constraints.  This method checks one result of constraint
- * constraint.  Others require compiler support. */
-bool ModelExecution::thin_air_constraint_may_allow(const ModelAction *writer, const ModelAction *reader) const
-{
-       if (!writer->is_rmw())
-               return true;
-
-       if (!reader->is_rmw())
-               return true;
-
-       for (const ModelAction *search = writer->get_reads_from(); search != NULL; search = search->get_reads_from()) {
-               if (search == reader)
-                       return false;
-               if (search->get_tid() == reader->get_tid() &&
-                               search->happens_before(reader))
-                       break;
-       }
-
-       return true;
-}
-
 /**
  * Arbitrary reads from the future are not allowed. Section 29.3 part 9 places
  * some constraints. This method checks one the following constraint (others
@@ -2414,177 +2101,6 @@ ClockVector * ModelExecution::get_cv(thread_id_t tid) const
        return get_parent_action(tid)->get_cv();
 }
 
-/**
- * @brief Find the promise (if any) to resolve for the current action and
- * remove it from the pending promise vector
- * @param curr The current ModelAction. Should be a write.
- * @return The Promise to resolve, if any; otherwise NULL
- */
-Promise * ModelExecution::pop_promise_to_resolve(const ModelAction *curr)
-{
-       for (unsigned int i = 0; i < promises.size(); i++)
-               if (curr->get_node()->get_promise(i)) {
-                       Promise *ret = promises[i];
-                       promises.erase(promises.begin() + i);
-                       return ret;
-               }
-       return NULL;
-}
-
-/**
- * Resolve a Promise with a current write.
- * @param write The ModelAction that is fulfilling Promises
- * @param promise The Promise to resolve
- * @param work The work queue, for adding new fixup work
- * @return True if the Promise was successfully resolved; false otherwise
- */
-bool ModelExecution::resolve_promise(ModelAction *write, Promise *promise,
-               work_queue_t *work)
-{
-       ModelVector<ModelAction *> actions_to_check;
-
-       for (unsigned int i = 0; i < promise->get_num_readers(); i++) {
-               ModelAction *read = promise->get_reader(i);
-               if (read_from(read, write)) {
-                       /* Propagate the changed clock vector */
-                       propagate_clockvector(read, work);
-               }
-               actions_to_check.push_back(read);
-       }
-       /* Make sure the promise's value matches the write's value */
-       ASSERT(promise->is_compatible(write) && promise->same_value(write));
-       if (!mo_graph->resolvePromise(promise, write))
-               priv->hard_failed_promise = true;
-
-       /**
-        * @todo  It is possible to end up in an inconsistent state, where a
-        * "resolved" promise may still be referenced if
-        * CycleGraph::resolvePromise() failed, so don't delete 'promise'.
-        *
-        * Note that the inconsistency only matters when dumping mo_graph to
-        * file.
-        *
-        * delete promise;
-        */
-
-       //Check whether reading these writes has made threads unable to
-       //resolve promises
-       for (unsigned int i = 0; i < actions_to_check.size(); i++) {
-               ModelAction *read = actions_to_check[i];
-               mo_check_promises(read, true);
-       }
-
-       return true;
-}
-
-/**
- * Compute the set of promises that could potentially be satisfied by this
- * action. Note that the set computation actually appears in the Node, not in
- * ModelExecution.
- * @param curr The ModelAction that may satisfy promises
- */
-void ModelExecution::compute_promises(ModelAction *curr)
-{
-       for (unsigned int i = 0; i < promises.size(); i++) {
-               Promise *promise = promises[i];
-               if (!promise->is_compatible(curr) || !promise->same_value(curr))
-                       continue;
-
-               bool satisfy = true;
-               for (unsigned int j = 0; j < promise->get_num_readers(); j++) {
-                       const ModelAction *act = promise->get_reader(j);
-                       if (act->happens_before(curr) ||
-                                       act->could_synchronize_with(curr)) {
-                               satisfy = false;
-                               break;
-                       }
-               }
-               if (satisfy)
-                       curr->get_node()->set_promise(i);
-       }
-}
-
-/** Checks promises in response to change in ClockVector Threads. */
-void ModelExecution::check_promises(thread_id_t tid, ClockVector *old_cv, ClockVector *merge_cv)
-{
-       for (unsigned int i = 0; i < promises.size(); i++) {
-               Promise *promise = promises[i];
-               if (!promise->thread_is_available(tid))
-                       continue;
-               for (unsigned int j = 0; j < promise->get_num_readers(); j++) {
-                       const ModelAction *act = promise->get_reader(j);
-                       if ((!old_cv || !old_cv->synchronized_since(act)) &&
-                                       merge_cv->synchronized_since(act)) {
-                               if (promise->eliminate_thread(tid)) {
-                                       /* Promise has failed */
-                                       priv->failed_promise = true;
-                                       return;
-                               }
-                       }
-               }
-       }
-}
-
-void ModelExecution::check_promises_thread_disabled()
-{
-       for (unsigned int i = 0; i < promises.size(); i++) {
-               Promise *promise = promises[i];
-               if (promise->has_failed()) {
-                       priv->failed_promise = true;
-                       return;
-               }
-       }
-}
-
-/**
- * @brief Checks promises in response to addition to modification order for
- * threads.
- *
- * We test whether threads are still available for satisfying promises after an
- * addition to our modification order constraints. Those that are unavailable
- * are "eliminated". Once all threads are eliminated from satisfying a promise,
- * that promise has failed.
- *
- * @param act The ModelAction which updated the modification order
- * @param is_read_check Should be true if act is a read and we must check for
- * updates to the store from which it read (there is a distinction here for
- * RMW's, which are both a load and a store)
- */
-void ModelExecution::mo_check_promises(const ModelAction *act, bool is_read_check)
-{
-       const ModelAction *write = is_read_check ? act->get_reads_from() : act;
-
-       for (unsigned int i = 0; i < promises.size(); i++) {
-               Promise *promise = promises[i];
-
-               // Is this promise on the same location?
-               if (!promise->same_location(write))
-                       continue;
-
-               for (unsigned int j = 0; j < promise->get_num_readers(); j++) {
-                       const ModelAction *pread = promise->get_reader(j);
-                       if (!pread->happens_before(act))
-                              continue;
-                       if (mo_graph->checkPromise(write, promise)) {
-                               priv->hard_failed_promise = true;
-                               return;
-                       }
-                       break;
-               }
-
-               // Don't do any lookups twice for the same thread
-               if (!promise->thread_is_available(act->get_tid()))
-                       continue;
-
-               if (mo_graph->checkReachable(promise, write)) {
-                       if (mo_graph->checkPromise(write, promise)) {
-                               priv->hard_failed_promise = true;
-                               return;
-                       }
-               }
-       }
-}
-
 /**
  * Compute the set of writes that may break the current pending release
  * sequence. This information is extracted from previou release sequence
@@ -2661,20 +2177,6 @@ void ModelExecution::build_may_read_from(ModelAction *curr)
                }
        }
 
-       /* Inherit existing, promised future values */
-       for (i = 0; i < promises.size(); i++) {
-               const Promise *promise = promises[i];
-               const ModelAction *promise_read = promise->get_reader(0);
-               if (promise_read->same_var(curr)) {
-                       /* Only add feasible future-values */
-                       mo_graph->startChanges();
-                       r_modification_order(curr, promise);
-                       if (!is_infeasible())
-                               curr->get_node()->add_read_from_promise(promise_read);
-                       mo_graph->rollbackChanges();
-               }
-       }
-
        /* We may find no valid may-read-from only if the execution is doomed */
        if (!curr->get_node()->read_from_size()) {
                priv->no_valid_reads = true;
@@ -2761,16 +2263,10 @@ void ModelExecution::dumpGraph(char *filename) const
                ModelAction *act = *it;
                if (act->is_read()) {
                        mo_graph->dot_print_node(file, act);
-                       if (act->get_reads_from())
-                               mo_graph->dot_print_edge(file,
+                       mo_graph->dot_print_edge(file,
                                                act->get_reads_from(),
                                                act,
                                                "label=\"rf\", color=red, weight=2");
-                       else
-                               mo_graph->dot_print_edge(file,
-                                               act->get_reads_from_promise(),
-                                               act,
-                                               "label=\"rf\", color=red");
                }
                if (thread_array[act->get_tid()]) {
                        mo_graph->dot_print_edge(file,
@@ -2813,14 +2309,6 @@ void ModelExecution::print_summary() const
        print_list(&action_trace);
        model_print("\n");
 
-       if (!promises.empty()) {
-               model_print("Pending promises:\n");
-               for (unsigned int i = 0; i < promises.size(); i++) {
-                       model_print(" [P%u] ", i);
-                       promises[i]->print();
-               }
-               model_print("\n");
-       }
 }
 
 /**
@@ -2871,26 +2359,6 @@ Thread * ModelExecution::get_pthread(pthread_t pid) {
         else return NULL;
 }
 
-/**
- * @brief Get a Promise's "promise number"
- *
- * A "promise number" is an index number that is unique to a promise, valid
- * only for a specific snapshot of an execution trace. Promises may come and go
- * as they are generated an resolved, so an index only retains meaning for the
- * current snapshot.
- *
- * @param promise The Promise to check
- * @return The promise index, if the promise still is valid; otherwise -1
- */
-int ModelExecution::get_promise_number(const Promise *promise) const
-{
-       for (unsigned int i = 0; i < promises.size(); i++)
-               if (promises[i] == promise)
-                       return i;
-       /* Not found */
-       return -1;
-}
-
 /**
  * @brief Check if a Thread is currently enabled
  * @param t The Thread to check
index fdc226b..579e9b7 100644 (file)
@@ -23,7 +23,6 @@
 class Node;
 class NodeStack;
 class CycleGraph;
-class Promise;
 class Scheduler;
 class Thread;
 class ClockVector;
@@ -87,8 +86,6 @@ public:
        void incr_pthread_counter() { pthread_counter++; }
        Thread * get_pthread(pthread_t pid);
 
-       int get_promise_number(const Promise *promise) const;
-
        bool is_enabled(Thread *t) const;
        bool is_enabled(thread_id_t tid) const;
 
@@ -97,7 +94,6 @@ public:
 
        ClockVector * get_cv(thread_id_t tid) const;
        ModelAction * get_parent_action(thread_id_t tid) const;
-       void check_promises_thread_disabled();
        bool isfeasibleprefix() const;
 
        action_list_t * get_actions_on_obj(void * obj, thread_id_t tid) const;
@@ -125,10 +121,9 @@ public:
        action_list_t * get_action_trace() { return &action_trace; }
 
        CycleGraph * const get_mo_graph() { return mo_graph; }
-
-       HashTable<pthread_mutex_t *, cdsc::mutex *, uintptr_t, 4> mutex_map;
-       HashTable<pthread_cond_t *, cdsc::condition_variable *, uintptr_t, 4> cond_map;
-
+  HashTable<pthread_cond_t *, cdsc::condition_variable *, uintptr_t, 4> * getCondMap() {return &cond_map;}
+  HashTable<pthread_mutex_t *, cdsc::mutex *, uintptr_t, 4> * getMutexMap() {return &mutex_map;}
+  
        SNAPSHOTALLOC
 private:
        int get_execution_number() const;
@@ -144,10 +139,8 @@ private:
        bool sleep_can_read_from(ModelAction *curr, const ModelAction *write);
        bool thin_air_constraint_may_allow(const ModelAction *writer, const ModelAction *reader) const;
        bool mo_may_allow(const ModelAction *writer, const ModelAction *reader);
-       bool promises_may_allow(const ModelAction *writer, const ModelAction *reader) const;
        void set_bad_synchronization();
        void set_bad_sc_read();
-       bool promises_expired() const;
        bool should_wake_up(const ModelAction *curr, const Thread *thread) const;
        void wake_up_sleeping_actions(ModelAction *curr);
        modelclock_t get_next_seq_num();
@@ -175,16 +168,8 @@ private:
        ModelAction * get_last_conflict(ModelAction *act) const;
        void set_backtracking(ModelAction *act);
        bool set_latest_backtrack(ModelAction *act);
-       Promise * pop_promise_to_resolve(const ModelAction *curr);
-       bool resolve_promise(ModelAction *curr, Promise *promise,
-                       work_queue_t *work);
-       void compute_promises(ModelAction *curr);
        void compute_relseq_breakwrites(ModelAction *curr);
 
-       void check_promises(thread_id_t tid, ClockVector *old_cv, ClockVector *merge_cv);
-       void mo_check_promises(const ModelAction *act, bool is_read_check);
-       void thread_blocking_check_promises(Thread *blocker, Thread *waiting);
-
        void check_curr_backtracking(ModelAction *curr);
        void add_action_to_lists(ModelAction *act);
        ModelAction * get_last_fence_release(thread_id_t tid) const;
@@ -197,13 +182,12 @@ private:
        template <typename rf_type>
        bool r_modification_order(ModelAction *curr, const rf_type *rf);
 
-       bool w_modification_order(ModelAction *curr, ModelVector<ModelAction *> *send_fv);
+       bool w_modification_order(ModelAction *curr);
        void get_release_seq_heads(ModelAction *acquire, ModelAction *read, rel_heads_list_t *release_heads);
        bool release_seq_heads(const ModelAction *rf, rel_heads_list_t *release_heads, struct release_seq *pending) const;
        void propagate_clockvector(ModelAction *acquire, work_queue_t *work);
        bool resolve_release_sequences(void *location, work_queue_t *work_queue);
        void add_future_value(const ModelAction *writer, ModelAction *reader);
-       bool check_coherence_promise(const ModelAction *write, const ModelAction *read);
        ModelAction * get_uninitialized_action(const ModelAction *curr) const;
 
        action_list_t action_trace;
@@ -220,16 +204,8 @@ private:
 
        HashTable<void *, SnapVector<action_list_t> *, uintptr_t, 4> obj_thrd_map;
 
-//     HashTable<pthread_mutex_t *, cdsc::mutex *, uintptr_t, 4> mutex_map;
-
-       /**
-        * @brief List of currently-pending promises
-        *
-        * Promises are sorted by the execution order of the read(s) which
-        * created them
-        */
-       SnapVector<Promise *> promises;
-       SnapVector<struct PendingFutureValue> futurevalues;
+  HashTable<pthread_mutex_t *, cdsc::mutex *, uintptr_t, 4> mutex_map;
+       HashTable<pthread_cond_t *, cdsc::condition_variable *, uintptr_t, 4> cond_map;
 
        /**
         * List of pending release sequences. Release sequences might be
index 64ec6b4..fa32e9a 100644 (file)
--- a/futex.cc
+++ b/futex.cc
@@ -48,8 +48,8 @@ _GLIBCXX_BEGIN_NAMESPACE_VERSION
                cdsc::condition_variable *v = new cdsc::condition_variable();
                cdsc::mutex *m = new cdsc::mutex();
 
-               execution->cond_map.put( (pthread_cond_t *) __addr, v);
-               execution->mutex_map.put( (pthread_mutex_t *) __addr, m);
+               execution->getCondMap()->put( (pthread_cond_t *) __addr, v);
+               execution->getMutexMap()->put( (pthread_mutex_t *) __addr, m);
 
                v->wait(*m);
                return true;
@@ -60,7 +60,7 @@ _GLIBCXX_BEGIN_NAMESPACE_VERSION
        {
                // INT_MAX wakes all the waiters at the address __addr
                ModelExecution *execution = model->get_execution();
-               cdsc::condition_variable *v = execution->cond_map.get( (pthread_cond_t *) __addr);
+               cdsc::condition_variable *v = execution->getCondMap()->get( (pthread_cond_t *) __addr);
                v->notify_all();
        }
 
index c4bcaf9..6f6ba3e 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -471,7 +471,6 @@ void ModelChecker::do_restart()
 /** @brief Run ModelChecker for the user program */
 void ModelChecker::run()
 {
-       bool has_next;
        int i = 0;
        do {
                thrd_t user_thread;
@@ -541,7 +540,7 @@ void ModelChecker::run()
                        t = execution->take_step(curr);
                } while (!should_terminate_execution());
 
-               has_next = next_execution();
+               next_execution();
                i++;
        } while (i<2); // while (has_next);
 
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..e3bccc9 100644 (file)
@@ -42,12 +42,6 @@ Node::Node(const struct model_params *params, ModelAction *act, Node *par,
        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),
@@ -180,17 +174,6 @@ void Node::print() const
                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");
 }
@@ -292,68 +275,6 @@ void Node::clear_backtracking()
 
 /************************** 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;
@@ -409,7 +330,7 @@ bool Node::has_priority_over(thread_id_t tid1, thread_id_t tid2) const
 
 /**
  * Get the current state of the may-read-from set iteration
- * @return The read-from type we should currently be checking (past or future)
+ * @return The read-from type we should currently be checking (past)
  */
 read_from_type_t Node::get_read_from_status()
 {
@@ -425,16 +346,9 @@ read_from_type_t Node::get_read_from_status()
  */
 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;
@@ -445,21 +359,16 @@ bool Node::increment_read_from()
  */
 bool Node::read_from_empty() const
 {
-       return read_from_past_empty() &&
-               read_from_promise_empty() &&
-               future_value_empty();
+  return read_from_past_empty();
 }
 
 /**
- * Get the total size of the may-read-from set, including both past and future
- * values
+ * Get the total size of the may-read-from set, including both past
  * @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();
+  return read_from_past.size();
 }
 
 /******************************* end read from ********************************/
@@ -533,151 +442,6 @@ bool Node::increment_read_from_past()
 
 /************************** 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 ***************************/
 
 /**
@@ -743,9 +507,6 @@ 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;
index 6ae96be..b7e630b 100644 (file)
@@ -10,7 +10,6 @@
 
 #include "mymemory.h"
 #include "schedule.h"
-#include "promise.h"
 #include "stl-model.h"
 
 class ModelAction;
@@ -31,8 +30,6 @@ struct fairness_info {
  */
 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;
 
@@ -94,20 +91,6 @@ public:
        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);
@@ -130,8 +113,6 @@ private:
        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;
@@ -159,15 +140,6 @@ private:
        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;
 
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 dec0ddf..723e60b 100644 (file)
@@ -93,7 +93,7 @@ int pthread_mutex_init(pthread_mutex_t *p_mutex, const pthread_mutexattr_t *) {
        cdsc::mutex *m = new cdsc::mutex();
 
        ModelExecution *execution = model->get_execution();
-       execution->mutex_map.put(p_mutex, m);
+       execution->getMutexMap()->put(p_mutex, m);
        return 0;
 }
 
@@ -103,11 +103,11 @@ int pthread_mutex_lock(pthread_mutex_t *p_mutex) {
        /* to protect the case where PTHREAD_MUTEX_INITIALIZER is used 
           instead of pthread_mutex_init, or where *p_mutex is not stored
           in the execution->mutex_map for some reason. */
-       if (!execution->mutex_map.contains(p_mutex)) {  
+       if (!execution->getMutexMap()->contains(p_mutex)) {     
                pthread_mutex_init(p_mutex, NULL);
        }
 
-       cdsc::mutex *m = execution->mutex_map.get(p_mutex);
+       cdsc::mutex *m = execution->getMutexMap()->get(p_mutex);
 
        if (m != NULL) {
                m->lock();
@@ -120,12 +120,12 @@ int pthread_mutex_lock(pthread_mutex_t *p_mutex) {
 
 int pthread_mutex_trylock(pthread_mutex_t *p_mutex) {
        ModelExecution *execution = model->get_execution();
-       cdsc::mutex *m = execution->mutex_map.get(p_mutex);
+       cdsc::mutex *m = execution->getMutexMap()->get(p_mutex);
        return m->try_lock();
 }
 int pthread_mutex_unlock(pthread_mutex_t *p_mutex) {   
        ModelExecution *execution = model->get_execution();
-       cdsc::mutex *m = execution->mutex_map.get(p_mutex);
+       cdsc::mutex *m = execution->getMutexMap()->get(p_mutex);
 
        if (m != NULL) {
                m->unlock();
@@ -172,17 +172,17 @@ int pthread_cond_init(pthread_cond_t *p_cond, const pthread_condattr_t *attr) {
        cdsc::condition_variable *v = new cdsc::condition_variable();
 
        ModelExecution *execution = model->get_execution();
-       execution->cond_map.put(p_cond, v);
+       execution->getCondMap()->put(p_cond, v);
        return 0;
 }
 
 int pthread_cond_wait(pthread_cond_t *p_cond, pthread_mutex_t *p_mutex) {
        ModelExecution *execution = model->get_execution();
-       if ( !execution->cond_map.contains(p_cond) )
+       if ( !execution->getCondMap()->contains(p_cond) )
                pthread_cond_init(p_cond, NULL);
 
-       cdsc::condition_variable *v = execution->cond_map.get(p_cond);
-       cdsc::mutex *m = execution->mutex_map.get(p_mutex);
+       cdsc::condition_variable *v = execution->getCondMap()->get(p_cond);
+       cdsc::mutex *m = execution->getMutexMap()->get(p_mutex);
 
        v->wait(*m);
        return 0;
@@ -193,13 +193,13 @@ int pthread_cond_timedwait(pthread_cond_t *p_cond,
 // implement cond_timedwait as a noop and let the scheduler decide which thread goes next
        ModelExecution *execution = model->get_execution();
 
-       if ( !execution->cond_map.contains(p_cond) )
+       if ( !execution->getCondMap()->contains(p_cond) )
                pthread_cond_init(p_cond, NULL);
-       if ( !execution->mutex_map.contains(p_mutex) )
+       if ( !execution->getMutexMap()->contains(p_mutex) )
                pthread_mutex_init(p_mutex, NULL);
 
-       cdsc::condition_variable *v = execution->cond_map.get(p_cond);
-       cdsc::mutex *m = execution->mutex_map.get(p_mutex);
+       cdsc::condition_variable *v = execution->getCondMap()->get(p_cond);
+       cdsc::mutex *m = execution->getMutexMap()->get(p_mutex);
 
        model->switch_to_master(new ModelAction(NOOP, std::memory_order_seq_cst, v, NULL));
 //     v->wait(*m);
@@ -210,10 +210,10 @@ int pthread_cond_timedwait(pthread_cond_t *p_cond,
 int pthread_cond_signal(pthread_cond_t *p_cond) {
        // notify only one blocked thread
        ModelExecution *execution = model->get_execution();
-       if ( !execution->cond_map.contains(p_cond) )
+       if ( !execution->getCondMap()->contains(p_cond) )
                pthread_cond_init(p_cond, NULL);
 
-       cdsc::condition_variable *v = execution->cond_map.get(p_cond);
+       cdsc::condition_variable *v = execution->getCondMap()->get(p_cond);
 
        v->notify_one();
        return 0;
index 2a02e30..63204f5 100644 (file)
@@ -66,8 +66,6 @@ void Scheduler::set_enabled(Thread *t, enabled_type_t enabled_status) {
                enabled_len = threadid + 1;
        }
        enabled[threadid] = enabled_status;
-       if (enabled_status == THREAD_DISABLED)
-               execution->check_promises_thread_disabled();
 }
 
 /**
index 0ff8f12..415eb24 100644 (file)
@@ -24,7 +24,7 @@ static void b(void *obj)
        printf("r2=%d\n",r2);
 }
 
-int main(int argc, char **argv)
+int user_main(int argc, char **argv)
 {
        thrd_t t1, t2;