add some comments

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index 29e16aa35ac75e63fc051e7fbf1062b5e95c143a..02a4a6a29206b34b8b3b22308439807b1b7c1188 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -22,7 +22,6 @@ ModelChecker::ModelChecker()
        /* First thread created will have id INITIAL_THREAD_ID */
        next_thread_id(INITIAL_THREAD_ID),
        used_sequence_numbers(0),
-
        num_executions(0),
        current_action(NULL),
        diverge(NULL),
@@ -134,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);
@@ -170,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)
@@ -276,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 {
@@ -287,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);
                }
        }
 
@@ -320,6 +331,7 @@ void ModelChecker::check_current_action(void)
                }
        } else if (curr->is_write()) {
                w_modification_order(curr);
+               resolve_promises(curr);
        }
 
        th->set_return_value(value);
@@ -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());
@@ -439,7 +456,6 @@ void ModelChecker::w_modification_order(ModelAction * curr) {
                                                 =>
                                                 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;
@@ -515,6 +531,39 @@ ClockVector * ModelChecker::get_cv(thread_id_t tid) {
        return get_parent_action(tid)->get_cv();
 }
 
+
+/** Resolve the given promises. */
+
+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();
+               if (!act->happens_before(curr)&&
+                               act->is_read()&&
+                               !act->is_synchronizing(curr)&&
+                               !act->same_thread(curr)&&
+                               promise->get_value()==curr->get_value()) {
+                       curr->get_node()->set_promise(i);
+               }
+       }
+}
+
 /** Checks promises in response to change in ClockVector Threads. */
 
 void ModelChecker::check_promises(ClockVector *old_cv, ClockVector * merge_cv) {
@@ -567,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;
@@ -627,7 +676,7 @@ void ModelChecker::print_summary(void)
 
        scheduler->print();
 
-       if (!isfeasible())
+       if (!isfinalfeasible())
                printf("INFEASIBLE EXECUTION!\n");
        print_list(action_trace);
        printf("\n");