be much more careful about sending values backwards...

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index d77ba4bdb7982b11757642d7ddb253703ecf7109..7e8211daf523f37e2c110d3852912c203decb331 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -179,7 +179,6 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr)
                        scheduler->add_sleep(thread_map->get(id_to_int(next->get_tid())));
                        tid = prevnode->get_next_backtrack();
                        /* Make sure the backtracked thread isn't sleeping. */
-                       scheduler->remove_sleep(thread_map->get(id_to_int(tid)));
                        node_stack->pop_restofstack(1);
                        if (diverge==earliest_diverge) {
                                earliest_diverge=prevnode->get_action();
@@ -213,6 +212,7 @@ void ModelChecker::execute_sleep_set() {
                        thr->set_state(THREAD_RUNNING);
                        scheduler->next_thread(thr);
                        Thread::swap(&system_context, thr);
+                       priv->current_action->set_sleep_flag();
                        thr->set_pending(priv->current_action);
                }
        }
@@ -346,7 +346,8 @@ void ModelChecker::set_backtracking(ModelAction *act)
        for(int i = low_tid; i < high_tid; i++) {
                thread_id_t tid = int_to_id(i);
 
-               if (!node->is_enabled(tid))
+               /* Don't backtrack into a point where the thread is disabled or sleeping. */
+               if (node->get_enabled_array()[i]!=THREAD_ENABLED)
                        continue;
        
                /* Check if this has been explored already */
@@ -518,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;
                }
@@ -1247,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);
                                        }
                                }
@@ -1284,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
@@ -1846,7 +1881,12 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
                                        act->print();
                                        curr->print();
                                }
-                               curr->get_node()->add_read_from(act);
+
+                               if (curr->get_sleep_flag()) {
+                                       if (sleep_can_read_from(curr, act))
+                                               curr->get_node()->add_read_from(act);
+                               } else
+                                       curr->get_node()->add_read_from(act);
                        }
 
                        /* Include at most one act per-thread that "happens before" curr */
@@ -1873,16 +1913,34 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
        ASSERT(initialized);
 }
 
+bool ModelChecker::sleep_can_read_from(ModelAction * curr, const ModelAction *write) {
+       while(true) {
+               Node *prevnode=write->get_node()->get_parent();
+               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()) {
+                       return false;
+               }
+               if (write->get_reads_from()==NULL)
+                       return true;
+               write=write->get_reads_from();
+       }
+}
+
 static void print_list(action_list_t *list)
 {
        action_list_t::iterator it;
 
        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");
 }