model: fix the maxreads support

diff --git a/model.cc b/model.cc
index b5a29dd5ff16d6f430c5e6771bbc5c495e8c47d5..2be1c82e9861760b321df7a8a54fcfad4ac82dd9 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -416,19 +416,26 @@ ModelAction * ModelChecker::process_rmw(ModelAction *act) {
 }
 
 /**
- * Checks whether a thread has read from the same write for too many times.
- * @todo This may be more subtle than this code segment addresses at this
- * point...  Potential problems to ponder and fix:
- * (1) What if the reads_from set keeps changing such that there is no common
- * write?
- * (2) What if the problem is that the other writes would break modification
- * order.
+ * Checks whether a thread has read from the same write for too many times
+ * without seeing the effects of a later write.
+ *
+ * Basic idea:
+ * 1) there must a different write that we could read from that would satisfy the modification order,
+ * 2) we must have read from the same value in excess of maxreads times, and
+ * 3) that other write must have been in the reads_from set for maxreads times.
+ *
+ * If so, we decide that the execution is no longer feasible.
  */
 void ModelChecker::check_recency(ModelAction *curr, bool already_added) {
        if (params.maxreads != 0) {
                if (curr->get_node()->get_read_from_size() <= 1)
                        return;
 
+               //Must make sure that execution is currently feasible...  We could
+               //accidentally clear by rolling back
+               if (!isfeasible())
+                       return;
+
                std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
                int tid = id_to_int(curr->get_tid());
 
@@ -447,8 +454,12 @@ void ModelChecker::check_recency(ModelAction *curr, bool already_added) {
                        rit++;
                }
 
+               action_list_t::reverse_iterator ritcopy=rit;
+               //See if we have enough reads from the same value
                int count=0;
-               for (; rit != list->rend(); rit++) {
+               for (; count < params.maxreads; rit++,count++) {
+                       if (rit==list->rend())
+                               return;
                        ModelAction *act = *rit;
                        if (!act->is_read())
                                return;
@@ -456,10 +467,44 @@ void ModelChecker::check_recency(ModelAction *curr, bool already_added) {
                                return;
                        if (act->get_node()->get_read_from_size() <= 1)
                                return;
-                       count++;
-                       if (count >= params.maxreads) {
-                               /* We've read from the same write for too many times */
+               }
+
+               for (int i=0;i<curr->get_node()->get_read_from_size();i++) {
+                       //Get write
+                       const ModelAction * write=curr->get_node()->get_read_from_at(i);
+                       //Need a different write
+                       if (write==curr->get_reads_from())
+                               continue;
+
+                       /* Test to see whether this is a feasible write to read from*/
+                       r_modification_order(curr, write);
+                       bool feasiblereadfrom=isfeasible();
+                       mo_graph->rollbackChanges();
+
+                       if (!feasiblereadfrom)
+                               continue;
+                       rit=ritcopy;
+
+                       bool feasiblewrite=true;
+                       //new we need to see if this write works for everyone
+
+                       for (int loop=count;loop>0;loop--,rit++) {
+                               ModelAction *act=*rit;
+                               bool foundvalue=false;
+                               for(int j=0;j<act->get_node()->get_read_from_size();j++) {
+                                       if (act->get_node()->get_read_from_at(i)==write) {
+                                               foundvalue=true;
+                                               break;
+                                       }
+                               }
+                               if (!foundvalue) {
+                                       feasiblewrite=false;
+                                       break;
+                               }
+                       }
+                       if (feasiblewrite) {
                                too_many_reads = true;
+                               return;
                        }
                }
        }

diff --git a/nodestack.cc b/nodestack.cc
index 71af6ef246314b0a40d373c7388418c5f4a01c82..a9399edbe9a35cd28328e438a8ce6e23c8cebeb3 100644 (file)
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -225,6 +225,10 @@ int Node::get_read_from_size() {
        return may_read_from.size();
 }
 
+const ModelAction * Node::get_read_from_at(int i) {
+       return may_read_from[i];
+}
+
 /**
  * Gets the next 'may_read_from' action from this Node. Only valid for a node
  * where this->action is a 'read'.

diff --git a/nodestack.h b/nodestack.h
index 8b4d7aef232bd2d5e09d899493c97c1e0de3d410..b391645b3af7a458e9271fc1bd60d762c5935605 100644 (file)
--- a/nodestack.h
+++ b/nodestack.h
@@ -65,6 +65,7 @@ public:
        bool increment_read_from();
        bool read_from_empty();
        int get_read_from_size();
+       const ModelAction * get_read_from_at(int i);
 
        void set_promise(unsigned int i);
        bool get_promise(unsigned int i);