model: we only resolve one promise at a time

[c11tester.git] / model.cc

diff --git a/model.cc b/model.cc
index d7ffc8e972d7466c7611b393d03afd5a96d5cce0..618b37e00ee86ad5fd03c03216218e7f36ed0067 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -483,10 +483,16 @@ void ModelChecker::record_stats()
                stats.num_buggy_executions++;
        else if (is_complete_execution())
                stats.num_complete++;
-       else if (scheduler->all_threads_sleeping())
+       else {
                stats.num_redundant++;
-       else
-               ASSERT(false);
+
+               /**
+                * @todo We can violate this ASSERT() when fairness/sleep sets
+                * conflict to cause an execution to terminate, e.g. with:
+                * Scheduler: [0: disabled][1: disabled][2: sleep][3: current, enabled]
+                */
+               //ASSERT(scheduler->all_threads_sleeping());
+       }
 }
 
 /** @brief Print execution stats */
@@ -1039,7 +1045,11 @@ void ModelChecker::add_future_value(const ModelAction *writer, ModelAction *read
 bool ModelChecker::process_write(ModelAction *curr)
 {
        bool updated_mod_order = w_modification_order(curr);
-       bool updated_promises = resolve_promises(curr);
+       int promise_idx = get_promise_to_resolve(curr);
+       bool updated_promises = false;
+
+       if (promise_idx >= 0)
+               updated_promises = resolve_promise(curr, promise_idx);
 
        if (promises->size() == 0) {
                for (unsigned int i = 0; i < futurevalues->size(); i++) {
@@ -2446,44 +2456,49 @@ ClockVector * ModelChecker::get_cv(thread_id_t tid) const
 }
 
 /**
- * Resolve a set of Promises with a current write. The set is provided in the
- * Node corresponding to @a write.
+ * @brief Find the promise, if any to resolve for the current action
+ * @param curr The current ModelAction. Should be a write.
+ * @return The (non-negative) index for the Promise to resolve, if any;
+ * otherwise -1
+ */
+int ModelChecker::get_promise_to_resolve(const ModelAction *curr) const
+{
+       for (unsigned int i = 0; i < promises->size(); i++)
+               if (curr->get_node()->get_promise(i))
+                       return i;
+       return -1;
+}
+
+/**
+ * Resolve a Promise with a current write.
  * @param write The ModelAction that is fulfilling Promises
- * @return True if promises were resolved; false otherwise
+ * @param promise_idx The index corresponding to the promise
+ * @return True if the Promise was successfully resolved; false otherwise
  */
-bool ModelChecker::resolve_promises(ModelAction *write)
+bool ModelChecker::resolve_promise(ModelAction *write, unsigned int promise_idx)
 {
-       bool haveResolved = false;
        std::vector< ModelAction *, ModelAlloc<ModelAction *> > actions_to_check;
-       promise_list_t mustResolve, resolved;
-
-       for (unsigned int i = 0, promise_index = 0; promise_index < promises->size(); i++) {
-               Promise *promise = (*promises)[promise_index];
-               if (write->get_node()->get_promise(i)) {
-                       for (unsigned int j = 0; j < promise->get_num_readers(); j++) {
-                               ModelAction *read = promise->get_reader(j);
-                               read_from(read, write);
-                               actions_to_check.push_back(read);
-                       }
-                       //Make sure the promise's value matches the write's value
-                       ASSERT(promise->is_compatible(write));
-                       mo_graph->resolvePromise(promise, write, &mustResolve);
-
-                       resolved.push_back(promise);
-                       promises->erase(promises->begin() + promise_index);
+       promise_list_t mustResolve;
+       Promise *promise = (*promises)[promise_idx];
 
-                       haveResolved = true;
-               } else
-                       promise_index++;
+       for (unsigned int i = 0; i < promise->get_num_readers(); i++) {
+               ModelAction *read = promise->get_reader(i);
+               read_from(read, write);
+               actions_to_check.push_back(read);
        }
+       /* Make sure the promise's value matches the write's value */
+       ASSERT(promise->is_compatible(write) && promise->same_value(write));
+       mo_graph->resolvePromise(promise, write, &mustResolve);
+
+       promises->erase(promises->begin() + promise_idx);
+
+       /** @todo simplify the 'mustResolve' stuff */
+       ASSERT(mustResolve.size() <= 1);
+
+       if (!mustResolve.empty() && mustResolve[0] != promise)
+               priv->failed_promise = true;
+       delete promise;
 
-       for (unsigned int i = 0; i < mustResolve.size(); i++) {
-               if (std::find(resolved.begin(), resolved.end(), mustResolve[i])
-                               == resolved.end())
-                       priv->failed_promise = true;
-       }
-       for (unsigned int i = 0; i < resolved.size(); i++)
-               delete resolved[i];
        //Check whether reading these writes has made threads unable to
        //resolve promises
 
@@ -2492,7 +2507,7 @@ bool ModelChecker::resolve_promises(ModelAction *write)
                mo_check_promises(read, true);
        }
 
-       return haveResolved;
+       return true;
 }
 
 /**
@@ -2505,7 +2520,7 @@ void ModelChecker::compute_promises(ModelAction *curr)
 {
        for (unsigned int i = 0; i < promises->size(); i++) {
                Promise *promise = (*promises)[i];
-               if (!promise->is_compatible(curr) || promise->get_value() != curr->get_value())
+               if (!promise->is_compatible(curr) || !promise->same_value(curr))
                        continue;
 
                bool satisfy = true;