- * 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.
- *
- * @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)