deal with looping due to bogus future value via promise expiration

[c11tester.git] / model.cc

diff --git a/model.cc b/model.cc
index 3e54a001a4541b8d5acada69e76c189ff5e82b36..9611f2f615845c926485dd732ce26b026585c085 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -216,7 +216,7 @@ void ModelChecker::set_backtracking(ModelAction *act)
 {
        ModelAction *prev;
        Node *node;
-       Thread *t = get_thread(act->get_tid());
+       Thread *t = get_thread(act);
 
        prev = get_last_conflict(act);
        if (prev == NULL)
@@ -292,8 +292,9 @@ bool ModelChecker::process_read(ModelAction *curr, Thread * th, bool second_part
                } else {
                        /* Read from future value */
                        value = curr->get_node()->get_future_value();
+                       modelclock_t expiration = curr->get_node()->get_future_value_expiration();
                        curr->read_from(NULL);
-                       Promise *valuepromise = new Promise(curr, value);
+                       Promise *valuepromise = new Promise(curr, value, expiration);
                        promises->push_back(valuepromise);
                }
                th->set_return_value(value);
@@ -324,6 +325,7 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
                second_part_of_rmw = true;
                delete curr;
                curr = tmp;
+               compute_promises(curr);
        } else {
                ModelAction *tmp = node_stack->explore_action(curr);
                if (tmp) {
@@ -360,17 +362,20 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
                break;
        }
        case THREAD_JOIN: {
-               Thread *wait, *join;
-               wait = get_thread(curr->get_tid());
-               join = (Thread *)curr->get_location();
-               if (!join->is_complete())
-                       scheduler->wait(wait, join);
+               Thread *waiting, *blocking;
+               waiting = get_thread(curr);
+               blocking = (Thread *)curr->get_location();
+               if (!blocking->is_complete()) {
+                       blocking->push_wait_list(curr);
+                       scheduler->sleep(waiting);
+               }
                break;
        }
        case THREAD_FINISH: {
-               Thread *th = get_thread(curr->get_tid());
+               Thread *th = get_thread(curr);
                while (!th->wait_list_empty()) {
-                       Thread *wake = th->pop_wait_list();
+                       ModelAction *act = th->pop_wait_list();
+                       Thread *wake = get_thread(act);
                        scheduler->wake(wake);
                }
                th->complete();
@@ -384,7 +389,7 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
                break;
        }
 
-       Thread *th = get_thread(curr->get_tid());
+       Thread *th = get_thread(curr);
 
        bool updated = false;
        if (curr->is_read()) {
@@ -424,6 +429,16 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
        return get_next_thread(curr);
 }
 
+bool ModelChecker::promises_expired() {
+       for (unsigned int promise_index = 0; promise_index < promises->size(); promise_index++) {
+               Promise *promise = (*promises)[promise_index];
+               if (promise->get_expiration()<priv->used_sequence_numbers) {
+                       return true;
+               }
+       }
+       return false;
+}
+
 /** @returns whether the current partial trace must be a prefix of a
  * feasible trace. */
 bool ModelChecker::isfeasibleprefix() {
@@ -432,7 +447,7 @@ bool ModelChecker::isfeasibleprefix() {
 
 /** @returns whether the current partial trace is feasible. */
 bool ModelChecker::isfeasible() {
-       return !mo_graph->checkForCycles() && !failed_promise && !too_many_reads;
+       return !mo_graph->checkForCycles() && !failed_promise && !too_many_reads && !promises_expired();
 }
 
 /** Returns whether the current completed trace is feasible. */
@@ -445,8 +460,10 @@ ModelAction * ModelChecker::process_rmw(ModelAction *act) {
        int tid = id_to_int(act->get_tid());
        ModelAction *lastread = get_last_action(tid);
        lastread->process_rmw(act);
-       if (act->is_rmw())
+       if (act->is_rmw() && lastread->get_reads_from()!=NULL) {
                mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
+               mo_graph->commitChanges();
+       }
        return lastread;
 }
 
@@ -482,7 +499,7 @@ void ModelChecker::check_recency(ModelAction *curr, bool already_added) {
 
                action_list_t::reverse_iterator rit = list->rbegin();
                /* Skip past curr */
-               if (!already_added) {
+               if (already_added) {
                        for (; (*rit) != curr; rit++)
                                ;
                        /* go past curr now */
@@ -661,9 +678,11 @@ bool ModelChecker::w_modification_order(ModelAction *curr)
                                 * The following edge should be handled elsewhere:
                                 *   readfrom(act) --mo--> act
                                 */
-                               if (act->is_write())
-                                       mo_graph->addEdge(act, curr);
-                               else if (act->is_read() && act->get_reads_from() != NULL)
+                               if (act->is_write()) {
+                                       //RMW shouldn't have an edge to themselves
+                                       if (act!=curr)
+                                               mo_graph->addEdge(act, curr);
+                               } else if (act->is_read() && act->get_reads_from() != NULL)
                                        mo_graph->addEdge(act->get_reads_from(), curr);
                                added = true;
                                break;
@@ -677,7 +696,7 @@ bool ModelChecker::w_modification_order(ModelAction *curr)
                                   =>
                                   that read could potentially read from our write.
                                 */
-                               if (act->get_node()->add_future_value(curr->get_value()) &&
+                               if (isfeasible() && act->get_node()->add_future_value(curr->get_value(), curr->get_seq_number()+params.maxfuturedelay) &&
                                                (!priv->next_backtrack || *act > *priv->next_backtrack))
                                        priv->next_backtrack = act;
                        }
@@ -966,6 +985,9 @@ bool ModelChecker::resolve_promises(ModelAction *write)
                if (write->get_node()->get_promise(i)) {
                        ModelAction *read = promise->get_action();
                        read->read_from(write);
+                       if (read->is_rmw()) {
+                               mo_graph->addRMWEdge(write, read);
+                       }
                        r_modification_order(read, write);
                        post_r_modification_order(read, write);
                        promises->erase(promises->begin() + promise_index);
@@ -1056,7 +1078,7 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
                                continue;
 
                        /* Don't consider more than one seq_cst write if we are a seq_cst read. */
-                       if (!act->is_seqcst() || !curr->is_seqcst() || act == last_seq_cst) {
+                       if (!curr->is_seqcst()|| (!act->is_seqcst() && (last_seq_cst==NULL||!act->happens_before(last_seq_cst))) || act == last_seq_cst) {
                                DEBUG("Adding action to may_read_from:\n");
                                if (DBG_ENABLED()) {
                                        act->print();