nodestack: pass 'struct future_value' to add_future_value()

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index cdafa697239a3d7035a0b6aa2a70cdaa618a3d31..40b25d0d635a32a5fdd2832001c638c3ee1986fc 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -855,10 +855,14 @@ bool ModelChecker::process_mutex(ModelAction *curr)
 void ModelChecker::add_future_value(const ModelAction *writer, ModelAction *reader)
 {
        /* Do more ambitious checks now that mo is more complete */
-       if (mo_may_allow(writer, reader) &&
-                       reader->get_node()->add_future_value(writer,
-                               writer->get_seq_number() + params.maxfuturedelay))
-               set_latest_backtrack(reader);
+       if (mo_may_allow(writer, reader)) {
+               struct future_value fv = {
+                       writer->get_value(),
+                       writer->get_seq_number() + params.maxfuturedelay,
+               };
+               if (reader->get_node()->add_future_value(fv))
+                       set_latest_backtrack(reader);
+       }
 }
 
 /**
@@ -2398,19 +2402,23 @@ void ModelChecker::check_promises_thread_disabled()
        }
 }
 
-/** Checks promises in response to addition to modification order for threads.
+/**
+ * @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 value read by the
- * first read to the same lcoation as pread by pthread that is
- * sequenced after pread..
+ * 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 mode order starting with pwrite.  Those threads cannot
+ * 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.
  *
@@ -2419,11 +2427,11 @@ void ModelChecker::check_promises_thread_disabled()
  * 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 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 write The ModelAction representing the relevant write.
+ * @param read  The ModelAction that reads a promised write, or NULL otherwise.
  */
 void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write, const ModelAction *read)
 {
@@ -2683,7 +2691,7 @@ Thread * ModelChecker::get_thread(thread_id_t tid) const
  * @param act The ModelAction
  * @return A Thread reference
  */
-Thread * ModelChecker::get_thread(ModelAction *act) const
+Thread * ModelChecker::get_thread(const ModelAction *act) const
 {
        return get_thread(act->get_tid());
 }