be much more careful about sending values backwards...

also implement hashing for traces...just an easy way to confirm whether we lose new traces...

diff --git a/action.cc b/action.cc
index b7bf024a4e79447220bfb50cd5268413e474f9b3..3aeb7377e2b328fad8b24748744274ab1386e25d 100644 (file)
--- a/action.cc
+++ b/action.cc
@@ -415,3 +415,18 @@ void ModelAction::print() const
        } else
                printf("\n");
 }
+
+/** @brief Print nicely-formatted info about this ModelAction */
+unsigned int ModelAction::hash() const
+{
+       unsigned int hash=(unsigned int) this->type;
+       hash^=((unsigned int)this->order)<<3;
+       hash^=seq_number<<5;
+       hash^=tid<<6;
+
+       if (is_read()) {
+               if (reads_from)
+                       hash^=reads_from->get_seq_number();
+       }
+       return hash;
+}

diff --git a/action.h b/action.h
index 68db2c35899c479b5aa1b0b9329f049a14b84e45..496093134ec7b6c96437c6ffa6f060e87894bdd9 100644 (file)
--- a/action.h
+++ b/action.h
@@ -127,6 +127,7 @@ public:
 
        void set_sleep_flag() { sleep_flag=true; }
        bool get_sleep_flag() { return sleep_flag; }
+       unsigned int hash() const;
 
        MEMALLOC
 private:

diff --git a/model.cc b/model.cc
index f8482cbf7b9db9eb9689a213c5de18cf3b583ad9..7e8211daf523f37e2c110d3852912c203decb331 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -519,7 +519,9 @@ bool ModelChecker::process_write(ModelAction *curr)
        if (promises->size() == 0) {
                for (unsigned int i = 0; i < futurevalues->size(); i++) {
                        struct PendingFutureValue pfv = (*futurevalues)[i];
-                       if (pfv.act->get_node()->add_future_value(pfv.value, pfv.expiration) &&
+                       //Do more ambitious checks now that mo is more complete
+                       if (mo_may_allow(pfv.writer, pfv.act)&&
+                                       pfv.act->get_node()->add_future_value(pfv.writer->get_value(), pfv.writer->get_seq_number()+params.maxfuturedelay) &&
                                        (!priv->next_backtrack || *pfv.act > *priv->next_backtrack))
                                priv->next_backtrack = pfv.act;
                }
@@ -1248,12 +1250,16 @@ bool ModelChecker::w_modification_order(ModelAction *curr)
                                   (3) cannot synchronize with us
                                   (4) is in a different thread
                                   =>
-                                  that read could potentially read from our write.
+                                  that read could potentially read from our write.  Note that
+                                  these checks are overly conservative at this point, we'll
+                                  do more checks before actually removing the
+                                  pendingfuturevalue.
+
                                 */
                                if (thin_air_constraint_may_allow(curr, act)) {
                                        if (isfeasible() ||
                                                        (curr->is_rmw() && act->is_rmw() && curr->get_reads_from() == act->get_reads_from() && isfeasibleotherthanRMW())) {
-                                               struct PendingFutureValue pfv = {curr->get_value(),curr->get_seq_number()+params.maxfuturedelay,act};
+                                               struct PendingFutureValue pfv = {curr,act};
                                                futurevalues->push_back(pfv);
                                        }
                                }
@@ -1285,6 +1291,34 @@ bool ModelChecker::thin_air_constraint_may_allow(const ModelAction * writer, con
        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 ModelChecker::mo_may_allow(const ModelAction * writer, const ModelAction *reader) {
+       std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(reader->get_location());
+
+       //Get write that follows reader action
+       action_list_t *list = &(*thrd_lists)[id_to_int(reader->get_tid())];
+       action_list_t::reverse_iterator rit;
+       ModelAction *first_write_after_read=NULL;
+
+       for (rit = list->rbegin(); rit != list->rend(); rit++) {
+               ModelAction *act = *rit;
+               if (act==reader)
+                       break;
+               if (act->is_write())
+                       first_write_after_read=act;
+       }
+
+       if (first_write_after_read==NULL)
+               return true;
+       return true;
+
+       //return !mo_graph->checkReachable(first_write_after_read, writer);
+}
+
+
+
 /**
  * Finds the head(s) of the release sequence(s) containing a given ModelAction.
  * The ModelAction under consideration is expected to be taking part in
@@ -1885,8 +1919,9 @@ bool ModelChecker::sleep_can_read_from(ModelAction * curr, const ModelAction *wr
                bool thread_sleep=prevnode->get_enabled_array()[id_to_int(curr->get_tid())]==THREAD_SLEEP_SET;
                if (write->is_release()&&thread_sleep)
                        return true;
-               if (!write->is_rmw())
+               if (!write->is_rmw()) {
                        return false;
+               }
                if (write->get_reads_from()==NULL)
                        return true;
                write=write->get_reads_from();
@@ -1899,10 +1934,13 @@ static void print_list(action_list_t *list)
 
        printf("---------------------------------------------------------------------\n");
        printf("Trace:\n");
-
+       unsigned int hash=0;
+       
        for (it = list->begin(); it != list->end(); it++) {
                (*it)->print();
+               hash=hash^(hash<<3)^((*it)->hash());
        }
+       printf("HASH %u\n", hash);
        printf("---------------------------------------------------------------------\n");
 }
 

diff --git a/model.h b/model.h
index 8316f04bd7aef32986f3d54f31dd1ca8afdca090..c99e0f8b424ddbe8079593713e498e53fe6fb80e 100644 (file)
--- a/model.h
+++ b/model.h
@@ -39,8 +39,7 @@ struct model_params {
 };
 
 struct PendingFutureValue {
-       uint64_t value;
-       modelclock_t expiration;
+       ModelAction *writer;
        ModelAction * act;
 };
 
@@ -120,6 +119,7 @@ private:
 
        bool sleep_can_read_from(ModelAction * curr, const ModelAction *write);
        bool thin_air_constraint_may_allow(const ModelAction * writer, const ModelAction *reader);
+       bool mo_may_allow(const ModelAction * writer, const ModelAction *reader);
        bool has_asserted() {return asserted;}
        void reset_asserted() {asserted=false;}
        int num_executions;