model: fixup happens_before/reflexivity, add 'curr' to lists earlier

Some code under 'check_current_action' assumes that the current action is not
added to the ModelChecker trace/list data structures yet. However, some
features I need to add will require the current action to be in these
data structures already. So there are a few spots I need to fixup so that the
code can handle "happens_before" reflexivity properly.

This commit moves the "add_action_to_lists()" call as well as fixes up
reflexivity.

diff --git a/model.cc b/model.cc
index 954c07dd6dacdfc9473a4aa3f5e0a2f8db38bcbf..acd20790f00eb20bf6675bba550a326a52ae3353 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -420,6 +420,10 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
                break;
        }
 
                break;
        }
 

+       /* Add current action to lists before work_queue loop */
+       if (!second_part_of_rmw)
+               add_action_to_lists(curr);
+

        work_queue_t work_queue(1, CheckCurrWorkEntry(curr));
 
        while (!work_queue.empty()) {
        work_queue_t work_queue(1, CheckCurrWorkEntry(curr));
 
        while (!work_queue.empty()) {


@@ -451,10 +455,6 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
                }
        }
 
                }
        }
 

-       /* Add action to list.  */
-       if (!second_part_of_rmw)
-               add_action_to_lists(curr);
-

        check_curr_backtracking(curr);
 
        set_backtracking(curr);
        check_curr_backtracking(curr);
 
        set_backtracking(curr);


@@ -648,8 +648,11 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf
                for (rit = list->rbegin(); rit != list->rend(); rit++) {
                        ModelAction *act = *rit;
 
                for (rit = list->rbegin(); rit != list->rend(); rit++) {
                        ModelAction *act = *rit;
 

-                       /* Include at most one act per-thread that "happens before" curr */
-                       if (act->happens_before(curr)) {
+                       /*
+                        * Include at most one act per-thread that "happens
+                        * before" curr. Don't consider reflexively.
+                        */
+                       if (act->happens_before(curr) && act != curr) {

                                if (act->is_write()) {
                                        if (rf != act && act != curr) {
                                                mo_graph->addEdge(act, rf);
                                if (act->is_write()) {
                                        if (rf != act && act != curr) {
                                                mo_graph->addEdge(act, rf);


@@ -770,8 +773,12 @@ bool ModelChecker::w_modification_order(ModelAction *curr)
                for (rit = list->rbegin(); rit != list->rend(); rit++) {
                        ModelAction *act = *rit;
 
                for (rit = list->rbegin(); rit != list->rend(); rit++) {
                        ModelAction *act = *rit;
 

-                       /* Include at most one act per-thread that "happens before" curr */
-                       if (act->happens_before(curr)) {
+                       /*
+                        * Include at most one act per-thread that "happens
+                        * before" curr. Only consider reflexively if curr is
+                        * RMW.
+                        */
+                       if (act->happens_before(curr) && (act != curr || curr->is_rmw())) {

                                /*
                                 * Note: if act is RMW, just add edge:
                                 *   act --mo--> curr
                                /*
                                 * Note: if act is RMW, just add edge:
                                 *   act --mo--> curr