execution: remove redundant condition, reword doc for promises_may_allow
authorBrian Norris <banorris@uci.edu>
Thu, 6 Jun 2013 00:25:30 +0000 (17:25 -0700)
committerBrian Norris <banorris@uci.edu>
Thu, 6 Jun 2013 00:25:30 +0000 (17:25 -0700)
promises_may_allow() doesn't actually need to check for
promises.empty(), as the loop bounds take care of that. In the same
spirit, we can reword the comments/documentation so that

 (1) it is not redundant (condition (a) is subsumed by (b))
 (2) we are more explicit about what we actually mean by "crossing
     promises"

execution.cc

index e04b672..53aa521 100644 (file)
@@ -755,12 +755,13 @@ bool ModelExecution::process_mutex(ModelAction *curr)
 /**
  * @brief Check if the current pending promises allow a future value to be sent
  *
 /**
  * @brief Check if the current pending promises allow a future value to be sent
  *
- * If one of the following is true:
- *  (a) there are no pending promises
- *  (b) the reader and writer do not cross any promises
- * Then, it is safe to pass a future value back now.
+ * It is unsafe to pass a future value back if there exists a pending promise Pr
+ * such that:
  *
  *
- * Otherwise, we must save the pending future value until (a) or (b) is true
+ *    reader --exec-> Pr --exec-> writer
+ *
+ * If such Pr exists, we must save the pending future value until Pr is
+ * resolved.
  *
  * @param writer The operation which sends the future value. Must be a write.
  * @param reader The operation which will observe the value. Must be a read.
  *
  * @param writer The operation which sends the future value. Must be a write.
  * @param reader The operation which will observe the value. Must be a read.
@@ -769,8 +770,6 @@ bool ModelExecution::process_mutex(ModelAction *curr)
 bool ModelExecution::promises_may_allow(const ModelAction *writer,
                const ModelAction *reader) const
 {
 bool ModelExecution::promises_may_allow(const ModelAction *writer,
                const ModelAction *reader) const
 {
-       if (promises.empty())
-               return true;
        for (int i = promises.size() - 1; i >= 0; i--) {
                ModelAction *pr = promises[i]->get_reader(0);
                //reader is after promise...doesn't cross any promise
        for (int i = promises.size() - 1; i >= 0; i--) {
                ModelAction *pr = promises[i]->get_reader(0);
                //reader is after promise...doesn't cross any promise