changes

diff --git a/action.cc b/action.cc
index 33c69656d7702d757cd90d44a5884fdef99e2864..33dbe75b22c7c3daf8f25f0b51f4a077d652e682 100644 (file)
--- a/action.cc
+++ b/action.cc
@@ -165,11 +165,22 @@ void ModelAction::create_cv(const ModelAction *parent)
 void ModelAction::read_from(const ModelAction *act)
 {
        ASSERT(cv);
-       if (act->is_release() && this->is_acquire())
+       if (act->is_release() && this->is_acquire()) {
+               synchronized(act);
                cv->merge(act->cv);
+       }
        reads_from = act;
 }
 
+
+/** Synchronize the current thread with the thread corresponding to
+ *  the ModelAction parameter. */
+
+void ModelAction::synchronized(const ModelAction *act) {
+       model->check_promises(cv, act->cv);
+       cv->merge(act->cv);
+}
+
 /**
  * Check whether 'this' happens before act, according to the memory-model's
  * happens before relation. This is checked via the ClockVector constructs.

diff --git a/action.h b/action.h
index da22882c3870ae361758ae97a7700a728203ea7b..7c457076501f77f93550da6fe629e2e625a0f2cb 100644 (file)
--- a/action.h
+++ b/action.h
@@ -81,6 +81,8 @@ public:
        void create_cv(const ModelAction *parent = NULL);
        ClockVector * get_cv() const { return cv; }
        void read_from(const ModelAction *act);
+       void synchronized(const ModelAction *act);
+
 
        bool happens_before(const ModelAction *act) const;
 

diff --git a/model.cc b/model.cc
index bfa3e02997ee42ed860fcf872d297906a6ac38b5..29e16aa35ac75e63fc051e7fbf1062b5e95c143a 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -31,11 +31,12 @@ ModelChecker::ModelChecker()
        thread_map(new HashTable<int, Thread *, int>()),
        obj_map(new HashTable<const void *, action_list_t, uintptr_t, 4>()),
        obj_thrd_map(new HashTable<void *, std::vector<action_list_t>, uintptr_t, 4 >()),
-       promises(new std::vector<Promise *>(1)),
+       promises(new std::vector<Promise *>()),
        thrd_last_action(new std::vector<ModelAction *>(1)),
        node_stack(new NodeStack()),
        next_backtrack(NULL),
-       cyclegraph(new CycleGraph())
+       cyclegraph(new CycleGraph()),
+       failed_promise(false)
 {
 }
 
@@ -69,6 +70,7 @@ void ModelChecker::reset_to_initial_state()
        used_sequence_numbers = 0;
        nextThread = 0;
        next_backtrack = NULL;
+       failed_promise = false;
        snapshotObject->backTrackBeforeStep(0);
 }
 
@@ -133,7 +135,11 @@ thread_id_t ModelChecker::get_next_replay_thread()
                Node *nextnode = next->get_node();
                /* Reached divergence point */
                if (nextnode->increment_read_from()) {
-                       /* The next node will read from a different value */
+                       /* The next node will read from a different value. */
+                       tid = next->get_tid();
+                       node_stack->pop_restofstack(2);
+               } else if (nextnode->increment_future_values()) {
+                       /* The next node will try to read from a different future value. */
                        tid = next->get_tid();
                        node_stack->pop_restofstack(2);
                } else {
@@ -290,15 +296,28 @@ void ModelChecker::check_current_action(void)
                th->set_creation(curr);
        }
 
+       /* Deal with new thread */
+       if (curr->get_type() == THREAD_START) {
+               check_promises(NULL, curr->get_cv());
+       }
+
        /* Assign reads_from values */
        Thread *th = get_thread(curr->get_tid());
        uint64_t value = VALUE_NONE;
        if (curr->is_read()) {
                const ModelAction *reads_from = curr->get_node()->get_read_from();
-               value = reads_from->get_value();
-               /* Assign reads_from, perform release/acquire synchronization */
-               curr->read_from(reads_from);
-               r_modification_order(curr,reads_from);
+               if (reads_from!=NULL) {
+                       value = reads_from->get_value();
+                       /* Assign reads_from, perform release/acquire synchronization */
+                       curr->read_from(reads_from);
+                       r_modification_order(curr,reads_from);
+               } else {
+                       /* Read from future value */
+                       value = curr->get_node()->get_future_value();
+                       curr->read_from(NULL);
+                       Promise * valuepromise=new Promise(curr, value);
+                       promises->push_back(valuepromise);
+               }
        } else if (curr->is_write()) {
                w_modification_order(curr);
        }
@@ -323,16 +342,16 @@ void ModelChecker::check_current_action(void)
        Node *currnode = curr->get_node();
        Node *parnode = currnode->get_parent();
 
-       if (!parnode->backtrack_empty()||!currnode->readsfrom_empty())
+       if (!parnode->backtrack_empty()||!currnode->readsfrom_empty()||!currnode->futurevalues_empty())
                if (!next_backtrack || *curr > *next_backtrack)
                        next_backtrack = curr;
-
+       
        set_backtracking(curr);
 }
 
 /** @returns whether the current trace is feasible. */
 bool ModelChecker::isfeasible() {
-       return !cyclegraph->checkForCycles();
+       return !cyclegraph->checkForCycles() && !failed_promise;
 }
 
 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
@@ -410,6 +429,21 @@ void ModelChecker::w_modification_order(ModelAction * curr) {
                                } else
                                        cyclegraph->addEdge(curr, act);
                                break;
+                       } else {
+                               if (act->is_read()&&!act->is_synchronizing(curr)&&!act->same_thread(curr)) {
+                                       /* We have an action that:
+                                                (1) did not happen before us
+                                                (2) is a read and we are a write
+                                                (3) cannot synchronize with us
+                                                (4) is in a different thread 
+                                                =>
+                                                that read could potentially read from our write.
+                                       */
+
+                                       if (act->get_node()->add_future_value(curr->get_value())&&
+                                                       (!next_backtrack || *act > * next_backtrack))
+                                               next_backtrack = act;
+                               }
                        }
                }
        }
@@ -481,6 +515,25 @@ ClockVector * ModelChecker::get_cv(thread_id_t tid) {
        return get_parent_action(tid)->get_cv();
 }
 
+/** Checks promises in response to change in ClockVector Threads. */
+
+void ModelChecker::check_promises(ClockVector *old_cv, ClockVector * merge_cv) {
+       for(unsigned int i=0;i<promises->size();i++) {
+               Promise * promise=(*promises)[i];
+               const ModelAction * act=promise->get_action();
+               if ((old_cv==NULL||!old_cv->synchronized_since(act))&&
+                               merge_cv->synchronized_since(act)) {
+                       //This thread is no longer able to send values back to satisfy the promise
+                       int num_synchronized_threads=promise->increment_threads();
+                       if (num_synchronized_threads==model->get_num_threads()) {
+                               //Promise has failed
+                               failed_promise = true;
+                               return;
+                       }
+               }
+       }
+}
+
 /**
  * Build up an initial set of all past writes that this 'read' action may read
  * from. This set is determined by the clock vector's "happens before"

diff --git a/model.h b/model.h
index 41ec97b50bdb71744075d0216a4bb209813255a9..e6dc06ddd97c2aef7d7c7dd17ae71854162ffb5e 100644 (file)
--- a/model.h
+++ b/model.h
@@ -57,6 +57,7 @@ public:
        ClockVector * get_cv(thread_id_t tid);
        bool next_execution();
        bool isfeasible();
+       void check_promises(ClockVector *old_cv, ClockVector * merge_cv);
 
        MEMALLOC
 private:
@@ -86,8 +87,7 @@ private:
        ModelAction * process_rmw(ModelAction * curr);
        void r_modification_order(ModelAction * curr, const ModelAction *rf);
        void w_modification_order(ModelAction * curr);
-
-
+       
        ModelAction *current_action;
        ModelAction *diverge;
        thread_id_t nextThread;
@@ -106,6 +106,7 @@ private:
        NodeStack *node_stack;
        ModelAction *next_backtrack;
        CycleGraph * cyclegraph;
+       bool failed_promise;
 };
 
 extern ModelChecker *model;

diff --git a/nodestack.cc b/nodestack.cc
index 6295442606612f0feff684f3657756b167239628..082835802629ac989c13e57ed4adbdd8de81eb48 100644 (file)
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -62,11 +62,12 @@ void Node::print_may_read_from()
  * @param value is the value to backtrack to.
  */
 
-void Node::add_future_value(uint64_t value) {
+bool Node::add_future_value(uint64_t value) {
        for(int i=0;i<future_values.size();i++)
                if (future_values[i]==value)
-                       return;
+                       return false;
        future_values.push_back(value);
+       return true;
 }
 
 
@@ -184,8 +185,10 @@ uint64_t Node::get_future_value() {
  * @return The first element in may_read_from
  */
 const ModelAction * Node::get_read_from() {
-       ASSERT(read_from_index<may_read_from.size());
-       return may_read_from[read_from_index];
+       if (read_from_index<may_read_from.size())
+               return may_read_from[read_from_index];
+       else
+               return NULL;
 }
 
 /**

diff --git a/nodestack.h b/nodestack.h
index 16264a2bbf800c6832e312cab644e85febb4f566..9ccde8da34e953052660292d6b865cb53dbe76e0 100644 (file)
--- a/nodestack.h
+++ b/nodestack.h
@@ -46,7 +46,7 @@ public:
         * occurred previously in the stack. */
        Node * get_parent() const { return parent; }
 
-       void add_future_value(uint64_t value);
+       bool add_future_value(uint64_t value);
        void add_read_from(const ModelAction *act);
        const ModelAction * get_read_from();
        uint64_t get_future_value();

diff --git a/promise.h b/promise.h
index a47982d6d291078f547acfa2d3ddf9dc33881cc5..180d9b01cc3bfc723d8dc3deb62c83c1a4e90e5a 100644 (file)
--- a/promise.h
+++ b/promise.h
@@ -14,6 +14,9 @@ class ModelAction;
 class Promise {
  public:
        Promise(ModelAction * act, uint64_t value);
+       const ModelAction * get_action() { return read; }
+       int increment_threads() { return ++numthreads; }
+       
  private:
        uint64_t value;
        ModelAction *read;