model: bug fixes to new code

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index c8af6cc4f5bfb2d2c878e6aa035e2cf712d56e29..36435d944cc028fa2bd5f8357d3e26407c5b712c 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -33,6 +33,7 @@ ModelChecker::ModelChecker(struct model_params params) :
        node_stack(new NodeStack()),
        mo_graph(new CycleGraph()),
        failed_promise(false),
+       too_many_reads(false),
        asserted(false)
 {
        /* Allocate this "size" on the snapshotting heap */
@@ -75,6 +76,7 @@ void ModelChecker::reset_to_initial_state()
        DEBUG("+++ Resetting to initial state +++\n");
        node_stack->reset_execution();
        failed_promise = false;
+       too_many_reads = false;
        reset_asserted();
        snapshotObject->backTrackBeforeStep(0);
 }
@@ -322,25 +324,40 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
        uint64_t value = VALUE_NONE;
        bool updated = false;
        if (curr->is_read()) {
-               const ModelAction *reads_from = curr->get_node()->get_read_from();
-               if (reads_from != NULL) {
-                       value = reads_from->get_value();
-                       /* Assign reads_from, perform release/acquire synchronization */
-                       curr->read_from(reads_from);
-                       if (r_modification_order(curr,reads_from))
-                               updated = true;
-               } 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);
+               while(true) {
+                       const ModelAction *reads_from = curr->get_node()->get_read_from();
+                       if (reads_from != NULL) {
+                               value = reads_from->get_value();
+                               /* Assign reads_from, perform release/acquire synchronization */
+                               curr->read_from(reads_from);
+                               if (!already_added)
+                                       check_recency(curr,false);
+
+                               bool r_status=r_modification_order(curr,reads_from);
+
+                               if (!isfeasible()&&(curr->get_node()->increment_read_from()||!curr->get_node()->future_value_empty())) {
+                                       mo_graph->rollbackChanges();
+                                       too_many_reads=false;
+                                       continue;
+                               }
+
+                               mo_graph->commitChanges();
+                               updated |= r_status;
+                       } 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);
+                       }
+                       break;
                }
        } else if (curr->is_write()) {
                if (w_modification_order(curr))
                        updated = true;
                if (resolve_promises(curr))
                        updated = true;
+               mo_graph->commitChanges();
        }
 
        if (updated)
@@ -380,7 +397,7 @@ bool ModelChecker::isfeasibleprefix() {
 
 /** @returns whether the current partial trace is feasible. */
 bool ModelChecker::isfeasible() {
-       return !mo_graph->checkForCycles() && !failed_promise;
+       return !mo_graph->checkForCycles() && !failed_promise && !too_many_reads;
 }
 
 /** Returns whether the current completed trace is feasible. */
@@ -398,6 +415,56 @@ ModelAction * ModelChecker::process_rmw(ModelAction *act) {
        return lastread;
 }
 
+/**
+ * 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.
+ */
+void ModelChecker::check_recency(ModelAction *curr, bool already_added) {
+       if (params.maxreads != 0) {
+               if (curr->get_node()->get_read_from_size() <= 1)
+                       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());
+
+               /* Skip checks */
+               if ((int)thrd_lists->size() <= tid)
+                       return;
+
+               action_list_t *list = &(*thrd_lists)[tid];
+
+               action_list_t::reverse_iterator rit = list->rbegin();
+               /* Skip past curr */
+               if (!already_added) {
+                       for (; (*rit) != curr; rit++)
+                               ;
+                       /* go past curr now */
+                       rit++;
+               }
+
+               int count=0;
+               for (; rit != list->rend(); rit++) {
+                       ModelAction *act = *rit;
+                       if (!act->is_read())
+                               return;
+                       if (act->get_reads_from() != curr->get_reads_from())
+                               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 */
+                               too_many_reads = true;
+                       }
+               }
+       }
+}
+
 /**
  * Updates the mo_graph with the constraints imposed from the current read.
  * @param curr The current action. Must be a read.