model: rewrite mo_check_promises

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index 15718e1fe32a498a4d9d1c7b651c35a4c8b5f281..ef9bed305fc0295af447e25365cccd6a8f2399a3 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -729,7 +729,7 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw)
 
                        read_from(curr, reads_from);
                        mo_graph->commitChanges();
-                       mo_check_promises(curr->get_tid(), reads_from, NULL);
+                       mo_check_promises(curr, true);
 
                        updated |= r_status;
                } else if (!second_part_of_rmw) {
@@ -895,7 +895,7 @@ bool ModelChecker::process_write(ModelAction *curr)
        }
 
        mo_graph->commitChanges();
-       mo_check_promises(curr->get_tid(), curr, NULL);
+       mo_check_promises(curr, false);
 
        get_thread(curr)->set_return_value(VALUE_NONE);
        return updated_mod_order || updated_promises;
@@ -1619,6 +1619,14 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const rf_type *rf)
                }
        }
 
+       /*
+        * All compatible, thread-exclusive promises must be ordered after any
+        * concrete loads from the same thread
+        */
+       for (unsigned int i = 0; i < promises->size(); i++)
+               if ((*promises)[i]->is_compatible_exclusive(curr))
+                       added = mo_graph->addEdge(rf, (*promises)[i]) || added;
+
        return added;
 }
 
@@ -2304,7 +2312,7 @@ bool ModelChecker::resolve_promises(ModelAction *write)
 
        for (unsigned int i = 0; i < actions_to_check.size(); i++) {
                ModelAction *read = actions_to_check[i];
-               mo_check_promises(read->get_tid(), write, read);
+               mo_check_promises(read, true);
        }
 
        return haveResolved;
@@ -2364,70 +2372,39 @@ void ModelChecker::check_promises_thread_disabled()
  * @brief Checks promises in response to addition to modification order for
  * threads.
  *
- * Definitions:
- *
- * pthread is the thread that performed the read that created the promise
- *
- * pread is the read that created the promise
- *
- * pwrite is either the first write to same location as pread by
- * pthread that is sequenced after pread or the write read by the
- * first read to the same location as pread by pthread that is
- * sequenced after pread.
- *
- * 1. If tid=pthread, then we check what other threads are reachable
- * through the mod order starting with pwrite.  Those threads cannot
- * perform a write that will resolve the promise due to modification
- * order constraints.
- *
- * 2. If the tid is not pthread, we check whether pwrite can reach the
- * action write through the modification order.  If so, that thread
- * cannot perform a future write that will resolve the promise due to
- * modificatin order constraints.
- *
- * @param tid The thread that either read from the model action write, or
- * actually did the model action write.
+ * We test whether threads are still available for satisfying promises after an
+ * addition to our modification order constraints. Those that are unavailable
+ * are "eliminated". Once all threads are eliminated from satisfying a promise,
+ * that promise has failed.
  *
- * @param write The ModelAction representing the relevant write.
- * @param read  The ModelAction that reads a promised write, or NULL otherwise.
+ * @param act The ModelAction which updated the modification order
+ * @param is_read_check Should be true if act is a read and we must check for
+ * updates to the store from which it read (there is a distinction here for
+ * RMW's, which are both a load and a store)
  */
-void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write, const ModelAction *read)
+void ModelChecker::mo_check_promises(const ModelAction *act, bool is_read_check)
 {
+       const ModelAction *write = is_read_check ? act->get_reads_from() : act;
+
        for (unsigned int i = 0; i < promises->size(); i++) {
                Promise *promise = (*promises)[i];
-               const ModelAction *act = promise->get_action();
+               const ModelAction *pread = promise->get_action();
 
                // Is this promise on the same location?
-               if (!act->same_var(write))
+               if (!pread->same_var(write))
                        continue;
 
-               // same thread as the promise
-               if (act->get_tid() == tid) {
-                       // make sure that the reader of this write happens after the promise
-                       if ((read == NULL) || (promise->get_action()->happens_before(read))) {
-                               // do we have a pwrite for the promise, if not, set it
-                               if (promise->get_write() == NULL) {
-                                       promise->set_write(write);
-                                       // The pwrite cannot happen before the promise
-                                       if (write->happens_before(act) && (write != act)) {
-                                               priv->failed_promise = true;
-                                               return;
-                                       }
-                               }
-
-                               if (mo_graph->checkPromise(write, promise)) {
-                                       priv->failed_promise = true;
-                                       return;
-                               }
-                       }
+               if (pread->happens_before(act) && mo_graph->checkPromise(write, promise)) {
+                       priv->failed_promise = true;
+                       return;
                }
 
                // Don't do any lookups twice for the same thread
-               if (!promise->thread_is_available(tid))
+               if (!promise->thread_is_available(act->get_tid()))
                        continue;
 
-               if (promise->get_write() && mo_graph->checkReachable(promise->get_write(), write)) {
-                       if (promise->eliminate_thread(tid)) {
+               if (mo_graph->checkReachable(promise, write)) {
+                       if (mo_graph->checkPromise(write, promise)) {
                                priv->failed_promise = true;
                                return;
                        }