model: cosmetic improvements to resolve_promises()

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index 0c2b993868421edf898441896e6fb9f4236c0bea..465849afa03b5a0946236528b8aea7f7703940b4 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -739,6 +739,9 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw)
                        value = fv.value;
                        curr->set_read_from_promise(promise);
                        promises->push_back(promise);
+                       mo_graph->startChanges();
+                       updated = r_modification_order(curr, promise);
+                       mo_graph->commitChanges();
                }
                get_thread(curr)->set_return_value(value);
                return updated;
@@ -1304,8 +1307,14 @@ ModelAction * ModelChecker::check_current_action(ModelAction *curr)
 
                        if (act->is_read()) {
                                const ModelAction *rf = act->get_reads_from();
-                               if (rf != NULL && r_modification_order(act, rf))
-                                       updated = true;
+                               const Promise *promise = act->get_reads_from_promise();
+                               if (rf) {
+                                       if (r_modification_order(act, rf))
+                                               updated = true;
+                               } else if (promise) {
+                                       if (r_modification_order(act, promise))
+                                               updated = true;
+                               }
                        }
                        if (act->is_write()) {
                                if (w_modification_order(act))
@@ -1566,22 +1575,19 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const rf_type *rf)
                                /* C++, Section 29.3 statement 5 */
                                if (curr->is_seqcst() && last_sc_fence_thread_local &&
                                                *act < *last_sc_fence_thread_local) {
-                                       mo_graph->addEdge(act, rf);
-                                       added = true;
+                                       added = mo_graph->addEdge(act, rf) || added;
                                        break;
                                }
                                /* C++, Section 29.3 statement 4 */
                                else if (act->is_seqcst() && last_sc_fence_local &&
                                                *act < *last_sc_fence_local) {
-                                       mo_graph->addEdge(act, rf);
-                                       added = true;
+                                       added = mo_graph->addEdge(act, rf) || added;
                                        break;
                                }
                                /* C++, Section 29.3 statement 6 */
                                else if (last_sc_fence_thread_before &&
                                                *act < *last_sc_fence_thread_before) {
-                                       mo_graph->addEdge(act, rf);
-                                       added = true;
+                                       added = mo_graph->addEdge(act, rf) || added;
                                        break;
                                }
                        }
@@ -1593,8 +1599,7 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const rf_type *rf)
                        if (act->happens_before(curr) && act != curr) {
                                if (act->is_write()) {
                                        if (!act->equals(rf)) {
-                                               mo_graph->addEdge(act, rf);
-                                               added = true;
+                                               added = mo_graph->addEdge(act, rf) || added;
                                        }
                                } else {
                                        const ModelAction *prevreadfrom = act->get_reads_from();
@@ -1603,8 +1608,7 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const rf_type *rf)
                                                continue;
 
                                        if (!prevreadfrom->equals(rf)) {
-                                               mo_graph->addEdge(prevreadfrom, rf);
-                                               added = true;
+                                               added = mo_graph->addEdge(prevreadfrom, rf) || added;
                                        }
                                }
                                break;
@@ -1713,8 +1717,7 @@ bool ModelChecker::w_modification_order(ModelAction *curr)
                         so we are initialized. */
                ModelAction *last_seq_cst = get_last_seq_cst_write(curr);
                if (last_seq_cst != NULL) {
-                       mo_graph->addEdge(last_seq_cst, curr);
-                       added = true;
+                       added = mo_graph->addEdge(last_seq_cst, curr) || added;
                }
        }
 
@@ -1757,8 +1760,7 @@ bool ModelChecker::w_modification_order(ModelAction *curr)
                        /* C++, Section 29.3 statement 7 */
                        if (last_sc_fence_thread_before && act->is_write() &&
                                        *act < *last_sc_fence_thread_before) {
-                               mo_graph->addEdge(act, curr);
-                               added = true;
+                               added = mo_graph->addEdge(act, curr) || added;
                                break;
                        }
 
@@ -1774,14 +1776,13 @@ bool ModelChecker::w_modification_order(ModelAction *curr)
                                 *   readfrom(act) --mo--> act
                                 */
                                if (act->is_write())
-                                       mo_graph->addEdge(act, curr);
+                                       added = mo_graph->addEdge(act, curr) || added;
                                else if (act->is_read()) {
                                        //if previous read accessed a null, just keep going
                                        if (act->get_reads_from() == NULL)
                                                continue;
-                                       mo_graph->addEdge(act->get_reads_from(), curr);
+                                       added = mo_graph->addEdge(act->get_reads_from(), curr) || added;
                                }
-                               added = true;
                                break;
                        } else if (act->is_read() && !act->could_synchronize_with(curr) &&
                                                     !act->same_thread(curr)) {
@@ -1807,6 +1808,15 @@ bool ModelChecker::w_modification_order(ModelAction *curr)
                }
        }
 
+       /*
+        * All compatible, thread-exclusive promises must be ordered after any
+        * concrete stores to the same thread, or else they can be merged with
+        * this store later
+        */
+       for (unsigned int i = 0; i < promises->size(); i++)
+               if ((*promises)[i]->is_compatible_exclusive(curr))
+                       added = mo_graph->addEdge(curr, (*promises)[i]) || added;
+
        return added;
 }
 
@@ -2321,7 +2331,7 @@ ClockVector * ModelChecker::get_cv(thread_id_t tid) const
  */
 bool ModelChecker::resolve_promises(ModelAction *write)
 {
-       bool resolved = false;
+       bool haveResolved = false;
        std::vector< ModelAction *, ModelAlloc<ModelAction *> > actions_to_check;
 
        for (unsigned int i = 0, promise_index = 0; promise_index < promises->size(); i++) {
@@ -2339,13 +2349,13 @@ bool ModelChecker::resolve_promises(ModelAction *write)
                        //after the read.
                        post_r_modification_order(read, write);
                        //Make sure the promise's value matches the write's value
-                       ASSERT(promise->get_value() == write->get_value());
+                       ASSERT(promise->is_compatible(write));
                        delete promise;
 
                        promises->erase(promises->begin() + promise_index);
                        actions_to_check.push_back(read);
 
-                       resolved = true;
+                       haveResolved = true;
                } else
                        promise_index++;
        }
@@ -2354,11 +2364,11 @@ bool ModelChecker::resolve_promises(ModelAction *write)
        //resolve promises
 
        for (unsigned int i = 0; i < actions_to_check.size(); i++) {
-               ModelAction *read=actions_to_check[i];
+               ModelAction *read = actions_to_check[i];
                mo_check_promises(read->get_tid(), write, read);
        }
 
-       return resolved;
+       return haveResolved;
 }
 
 /**