okay...known bugs for my trivial test are out of send future values backwards

diff --git a/action.cc b/action.cc
index 33dbe75b22c7c3daf8f25f0b51f4a077d652e682..6a8dc60ba1f9bb3105ea1b2a8fab26af4e4a0025 100644 (file)
--- a/action.cc
+++ b/action.cc
@@ -152,7 +152,8 @@ bool ModelAction::is_synchronizing(const ModelAction *act) const
 
 void ModelAction::create_cv(const ModelAction *parent)
 {
-       ASSERT(cv == NULL);
+       if (cv)
+               delete cv;
 
        if (parent)
                cv = new ClockVector(parent->cv, this);
@@ -165,7 +166,7 @@ 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!=NULL && act->is_release() && this->is_acquire()) {
                synchronized(act);
                cv->merge(act->cv);
        }

diff --git a/model.cc b/model.cc
index d8699b0ebfe850b3a0a8d3d277f3ca914db0b59f..159dd705c8b567ae16600be6c278cf252772ce5d 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -173,7 +173,7 @@ bool ModelChecker::next_execution()
 
        num_executions++;
 
-       if (isfeasible() || DBG_ENABLED())
+       if (isfinalfeasible() || DBG_ENABLED())
                print_summary();
 
        if ((diverge = model->get_next_backtrack()) == NULL)
@@ -279,6 +279,12 @@ void ModelChecker::check_current_action(void)
                        /* First restore type and order in case of RMW operation */
                        if (curr->is_rmwr())
                                tmp->copy_typeandorder(curr);
+
+                       /* If we have diverged, we need to reset the clock vector. */
+                       if (diverge==NULL) {
+                               tmp->create_cv(get_parent_action(tmp->get_tid()));
+                       }
+                       
                        delete curr;
                        curr = tmp;
                } else {
@@ -360,6 +366,11 @@ bool ModelChecker::isfeasible() {
        return !cyclegraph->checkForCycles() && !failed_promise;
 }
 
+/** Returns whether the current trace is feasible. */
+bool ModelChecker::isfinalfeasible() {
+       return isfeasible() && promises->size()==0;
+}
+
 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
 ModelAction * ModelChecker::process_rmw(ModelAction * act) {
        int tid = id_to_int(act->get_tid());
@@ -445,7 +456,6 @@ void ModelChecker::w_modification_order(ModelAction * curr) {
                                                 =>
                                                 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;
@@ -525,13 +535,15 @@ ClockVector * ModelChecker::get_cv(thread_id_t tid) {
 /** Resolve promises. */
 
 void ModelChecker::resolve_promises(ModelAction *write) {
-       for(unsigned int i=0;i<promises->size();i++) {
-               Promise * promise=(*promises)[i];
+       for(unsigned int i=0, promise_index=0;promise_index<promises->size(); i++) {
+               Promise * promise=(*promises)[promise_index];
                if (write->get_node()->get_promise(i)) {
                        ModelAction * read=promise->get_action();
                        read->read_from(write);
                        r_modification_order(read, write);
-               }
+                       promises->erase(promises->begin()+promise_index);
+               } else
+                       promise_index++;
        }
 }
 
@@ -661,7 +673,7 @@ void ModelChecker::print_summary(void)
 
        scheduler->print();
 
-       if (!isfeasible())
+       if (!isfinalfeasible())
                printf("INFEASIBLE EXECUTION!\n");
        print_list(action_trace);
        printf("\n");

diff --git a/model.h b/model.h
index 574ed21a041f934c411992b9aa73f94d624b06a6..73605dbb2616aa26351fe8a4515b3eb7721ed77a 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();
+       bool isfinalfeasible();
        void check_promises(ClockVector *old_cv, ClockVector * merge_cv);
 
        MEMALLOC

diff --git a/nodestack.cc b/nodestack.cc
index 6eb71dc89c8f15097514781ed95209304414d1f6..4a6a26d5e2e7078ee74ab0636f7353d86f29f4e0 100644 (file)
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -27,7 +27,7 @@ Node::Node(ModelAction *act, Node *par, int nthreads)
        may_read_from(),
        read_from_index(0),
        future_values(),
-       future_index(0)
+       future_index(-1)
 {
        if (act)
                act->set_node(this);
@@ -71,11 +71,11 @@ bool Node::increment_promises() {
        for (unsigned int i=0;i<promises.size();i++) {
                if (promises[i]==1) {
                        promises[i]=2;
-                       do {
+                       while (i>0) {
                                i--;
                                if (promises[i]==2)
                                        promises[i]=1;
-                       } while(i>0);
+                       }
                        return true;
                }
        }
@@ -98,6 +98,7 @@ bool Node::add_future_value(uint64_t value) {
        for(unsigned int i=0;i<future_values.size();i++)
                if (future_values[i]==value)
                        return false;
+
        future_values.push_back(value);
        return true;
 }