fixup whitespace

[c11tester.git] / model.cc

diff --git a/model.cc b/model.cc
index de5687317c7e794f1a2dfa9bf99d01bb303e4036..c87f5f9d07813ecbd40cce8603369f24eebea459 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -133,11 +133,15 @@ thread_id_t ModelChecker::get_next_replay_thread()
        if (next == diverge) {
                Node *nextnode = next->get_node();
                /* Reached divergence point */
-               if (nextnode->increment_read_from()) {
+               if (nextnode->increment_promise()) {
+                       /* The next node will try to satisfy a different set of promises. */
+                       tid = next->get_tid();
+                       node_stack->pop_restofstack(2);
+               } else if (nextnode->increment_read_from()) {
                        /* The next node will read from a different value. */
                        tid = next->get_tid();
                        node_stack->pop_restofstack(2);
-               } else if (nextnode->increment_future_values()) {
+               } else if (nextnode->increment_future_value()) {
                        /* The next node will try to read from a different future value. */
                        tid = next->get_tid();
                        node_stack->pop_restofstack(2);
@@ -169,7 +173,7 @@ bool ModelChecker::next_execution()
 
        num_executions++;
 
-       if (isfeasible() || DBG_ENABLED())
+       if (isfinalfeasible() || DBG_ENABLED())
                print_summary();
 
        if ((diverge = model->get_next_backtrack()) == NULL)
@@ -275,6 +279,12 @@ void ModelChecker::check_current_action(void)
                        /* First restore type and order in case of RMW operation */
                        if (curr->is_rmwr())
                                tmp->copy_typeandorder(curr);
+
+                       /* If we have diverged, we need to reset the clock vector. */
+                       if (diverge==NULL) {
+                               tmp->create_cv(get_parent_action(tmp->get_tid()));
+                       }
+
                        delete curr;
                        curr = tmp;
                } else {
@@ -286,6 +296,8 @@ void ModelChecker::check_current_action(void)
                        /* Build may_read_from set */
                        if (curr->is_read())
                                build_reads_from_past(curr);
+                       if (curr->is_write())
+                               compute_promises(curr);
                }
        }
 
@@ -342,18 +354,23 @@ void ModelChecker::check_current_action(void)
        Node *currnode = curr->get_node();
        Node *parnode = currnode->get_parent();
 
-       if (!parnode->backtrack_empty()||!currnode->readsfrom_empty()||!currnode->futurevalues_empty())
+       if (!parnode->backtrack_empty()||!currnode->read_from_empty()||!currnode->future_value_empty()||!currnode->promise_empty())
                if (!next_backtrack || *curr > *next_backtrack)
                        next_backtrack = curr;
-       
+
        set_backtracking(curr);
 }
 
-/** @returns whether the current trace is feasible. */
+/** @returns whether the current partial trace is feasible. */
 bool ModelChecker::isfeasible() {
        return !cyclegraph->checkForCycles() && !failed_promise;
 }
 
+/** Returns whether the current completed trace is feasible. */
+bool ModelChecker::isfinalfeasible() {
+       return isfeasible() && promises->size()==0;
+}
+
 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
 ModelAction * ModelChecker::process_rmw(ModelAction * act) {
        int tid = id_to_int(act->get_tid());
@@ -435,11 +452,10 @@ void ModelChecker::w_modification_order(ModelAction * curr) {
                                                 (1) did not happen before us
                                                 (2) is a read and we are a write
                                                 (3) cannot synchronize with us
-                                                (4) is in a different thread 
+                                                (4) is in a different thread
                                                 =>
                                                 that read could potentially read from our write.
                                        */
-
                                        if (act->get_node()->add_future_value(curr->get_value())&&
                                                        (!next_backtrack || *act > * next_backtrack))
                                                next_backtrack = act;
@@ -516,9 +532,25 @@ ClockVector * ModelChecker::get_cv(thread_id_t tid) {
 }
 
 
-/** Resolve promises. */
+/** Resolve the given promises. */
 
-void ModelChecker::resolve_promises(ModelAction *curr) {
+void ModelChecker::resolve_promises(ModelAction *write) {
+       for(unsigned int i=0, promise_index=0;promise_index<promises->size(); i++) {
+               Promise * promise=(*promises)[promise_index];
+               if (write->get_node()->get_promise(i)) {
+                       ModelAction * read=promise->get_action();
+                       read->read_from(write);
+                       r_modification_order(read, write);
+                       promises->erase(promises->begin()+promise_index);
+               } else
+                       promise_index++;
+       }
+}
+
+/** Compute the set of promises that could potentially be satisfied by
+ *  this action. */
+
+void ModelChecker::compute_promises(ModelAction *curr) {
        for(unsigned int i=0;i<promises->size();i++) {
                Promise * promise=(*promises)[i];
                const ModelAction * act=promise->get_action();
@@ -527,8 +559,7 @@ void ModelChecker::resolve_promises(ModelAction *curr) {
                                !act->is_synchronizing(curr)&&
                                !act->same_thread(curr)&&
                                promise->get_value()==curr->get_value()) {
-                       
-                       
+                       curr->get_node()->set_promise(i);
                }
        }
 }
@@ -585,7 +616,7 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
                action_list_t::reverse_iterator rit;
                for (rit = list->rbegin(); rit != list->rend(); rit++) {
                        ModelAction *act = *rit;
-                       
+
                        /* Only consider 'write' actions */
                        if (!act->is_write())
                                continue;
@@ -645,7 +676,7 @@ void ModelChecker::print_summary(void)
 
        scheduler->print();
 
-       if (!isfeasible())
+       if (!isfinalfeasible())
                printf("INFEASIBLE EXECUTION!\n");
        print_list(action_trace);
        printf("\n");