model: refactor process_read logic

[c11tester.git] / model.cc

diff --git a/model.cc b/model.cc
index 5a1f3992343bc4376fc1c0570832efe9e6bc43d9..63ff36386a1db6425ce124700d6c776349779cc0 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -864,21 +864,20 @@ bool ModelChecker::process_read(ModelAction *curr)
                        mo_graph->startChanges();
 
                        ASSERT(!is_infeasible());
-                       if (!check_recency(curr, rf))
-                               priv->too_many_reads = true;
-                       updated = r_modification_order(curr, rf);
-
-                       if (is_infeasible() && node->increment_read_from()) {
-                               mo_graph->rollbackChanges();
-                               priv->too_many_reads = false;
-                               continue;
+                       if (!check_recency(curr, rf)) {
+                               if (node->increment_read_from()) {
+                                       mo_graph->rollbackChanges();
+                                       continue;
+                               } else {
+                                       priv->too_many_reads = true;
+                               }
                        }
 
+                       updated = r_modification_order(curr, rf);
                        value = rf->get_value();
                        read_from(curr, rf);
                        mo_graph->commitChanges();
                        mo_check_promises(curr, true);
-
                        break;
                }
                case READ_FROM_PROMISE: {
@@ -1644,6 +1643,17 @@ ModelAction * ModelChecker::process_rmw(ModelAction *act) {
        return lastread;
 }
 
+/**
+ * A helper function for ModelChecker::check_recency, to check if the current
+ * thread is able to read from a different write/promise for 'params.maxreads'
+ * number of steps and if that write/promise should become visible (i.e., is
+ * ordered later in the modification order). This helps model memory liveness.
+ *
+ * @param curr The current action. Must be a read.
+ * @param rf The write/promise from which we plan to read
+ * @param other_rf The write/promise from which we may read
+ * @return True if we were able to read from other_rf for params.maxreads steps
+ */
 template <typename T, typename U>
 bool ModelChecker::should_read_instead(const ModelAction *curr, const T *rf, const U *other_rf) const
 {
@@ -1672,13 +1682,14 @@ bool ModelChecker::should_read_instead(const ModelAction *curr, const T *rf, con
 }
 
 /**
- * Checks whether a thread has read from the same write for too many times
- * without seeing the effects of a later write.
+ * Checks whether a thread has read from the same write or Promise for too many
+ * times without seeing the effects of a later write/Promise.
  *
  * Basic idea:
- * 1) there must a different write that we could read from that would satisfy the modification order,
- * 2) we must have read from the same value in excess of maxreads times, and
- * 3) that other write must have been in the reads_from set for maxreads times.
+ * 1) there must a different write/promise that we could read from,
+ * 2) we must have read from the same write/promise in excess of maxreads times,
+ * 3) that other write/promise must have been in the reads_from set for maxreads times, and
+ * 4) that other write/promise must be mod-ordered after the write/promise we are reading.
  *
  * If so, we decide that the execution is no longer feasible.
  *