fun issues...
authorBrian Demsky <bdemsky@uci.edu>
Wed, 12 Sep 2012 09:52:34 +0000 (02:52 -0700)
committerBrian Demsky <bdemsky@uci.edu>
Wed, 12 Sep 2012 09:52:34 +0000 (02:52 -0700)
(1) need to compute promises for rmw nodes...they could satisfy them
(2) don't call rmwedge if you don't know where you are reading from yet
(3) miscopied commit from big merge (already_added -> !already_added)
(4) avoid adding rmw edges back to itself
(5) probably worth adding a check that the execution isfeasible before sending future values
(6) resolve promises should add rmwedges when appropriate
(7) fix seq_cst to mask earlier writes..

model.cc

index 4f29e21..0098213 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -324,6 +324,7 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
                second_part_of_rmw = true;
                delete curr;
                curr = tmp;
                second_part_of_rmw = true;
                delete curr;
                curr = tmp;
+               compute_promises(curr);
        } else {
                ModelAction *tmp = node_stack->explore_action(curr);
                if (tmp) {
        } else {
                ModelAction *tmp = node_stack->explore_action(curr);
                if (tmp) {
@@ -448,8 +449,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);
        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->addRMWEdge(lastread->get_reads_from(), lastread);
+               mo_graph->commitChanges();
+       }
        return lastread;
 }
 
        return lastread;
 }
 
@@ -485,7 +488,7 @@ void ModelChecker::check_recency(ModelAction *curr, bool already_added) {
 
                action_list_t::reverse_iterator rit = list->rbegin();
                /* Skip past curr */
 
                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 */
                        for (; (*rit) != curr; rit++)
                                ;
                        /* go past curr now */
@@ -664,9 +667,11 @@ bool ModelChecker::w_modification_order(ModelAction *curr)
                                 * The following edge should be handled elsewhere:
                                 *   readfrom(act) --mo--> act
                                 */
                                 * 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;
                                        mo_graph->addEdge(act->get_reads_from(), curr);
                                added = true;
                                break;
@@ -680,7 +685,7 @@ bool ModelChecker::w_modification_order(ModelAction *curr)
                                   =>
                                   that read could potentially read from our write.
                                 */
                                   =>
                                   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()) &&
                                                (!priv->next_backtrack || *act > *priv->next_backtrack))
                                        priv->next_backtrack = act;
                        }
                                                (!priv->next_backtrack || *act > *priv->next_backtrack))
                                        priv->next_backtrack = act;
                        }
@@ -969,6 +974,9 @@ bool ModelChecker::resolve_promises(ModelAction *write)
                if (write->get_node()->get_promise(i)) {
                        ModelAction *read = promise->get_action();
                        read->read_from(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);
                        r_modification_order(read, write);
                        post_r_modification_order(read, write);
                        promises->erase(promises->begin() + promise_index);
@@ -1059,7 +1067,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. */
                                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();
                                DEBUG("Adding action to may_read_from:\n");
                                if (DBG_ENABLED()) {
                                        act->print();