model: refactor r_modification_order 'act != curr' and 'act != rf'

We never want to process 'curr' or 'rf' in r_modification_order, so just
factor this out to the beginning of the loop to save on code clutter
(and potential bugs).

diff --git a/model.cc b/model.cc
index 2aa94cfd84b4da470277f0ea81f6118d880e9f3e..a03ea46224f1d7a4d10f64927b9df9d385eeb21e 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -1831,7 +1831,18 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const rf_type *rf)
                for (rit = list->rbegin(); rit != list->rend(); rit++) {
                        ModelAction *act = *rit;
 
                for (rit = list->rbegin(); rit != list->rend(); rit++) {
                        ModelAction *act = *rit;
 

-                       if (act->is_write() && !act->equals(rf) && act != curr) {
+                       /* Skip curr */
+                       if (act == curr)
+                               continue;
+                       /* Don't want to add reflexive edges on 'rf' */
+                       if (act->equals(rf)) {
+                               if (act->happens_before(curr))
+                                       break;
+                               else
+                                       continue;
+                       }
+
+                       if (act->is_write()) {

                                /* C++, Section 29.3 statement 5 */
                                if (curr->is_seqcst() && last_sc_fence_thread_local &&
                                                *act < *last_sc_fence_thread_local) {
                                /* C++, Section 29.3 statement 5 */
                                if (curr->is_seqcst() && last_sc_fence_thread_local &&
                                                *act < *last_sc_fence_thread_local) {


@@ -1854,13 +1865,11 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const rf_type *rf)
 
                        /*
                         * Include at most one act per-thread that "happens
 
                        /*
                         * Include at most one act per-thread that "happens

-                        * before" curr. Don't consider reflexively.
+                        * before" curr

                         */
                         */

-                       if (act->happens_before(curr) && act != curr) {
+                       if (act->happens_before(curr)) {

                                if (act->is_write()) {
                                if (act->is_write()) {

-                                       if (!act->equals(rf)) {
-                                               added = mo_graph->addEdge(act, rf) || added;
-                                       }
+                                       added = mo_graph->addEdge(act, rf) || added;

                                } else {
                                        const ModelAction *prevrf = act->get_reads_from();
                                        const Promise *prevrf_promise = act->get_reads_from_promise();
                                } else {
                                        const ModelAction *prevrf = act->get_reads_from();
                                        const Promise *prevrf_promise = act->get_reads_from_promise();