more implementation of scanalysis...

[model-checker.git] / action.cc

diff --git a/action.cc b/action.cc
index 4de6f354bfbccfbedc9061538ecb48be8e69e3e2..bd98f5ca2f490f4c3743641ee7018d8e178d72ec 100644 (file)
--- a/action.cc
+++ b/action.cc
@@ -11,6 +11,12 @@
 
 #define ACTION_INITIAL_CLOCK 0
 
+/** @brief A special value to represent a successful trylock */
+#define VALUE_TRYSUCCESS 1
+
+/** @brief A special value to represent a failed trylock */
+#define VALUE_TRYFAILED 0
+
 /**
  * @brief Construct a new ModelAction
  *
@@ -77,6 +83,11 @@ bool ModelAction::is_thread_start() const
        return type == THREAD_START;
 }
 
+bool ModelAction::is_thread_join() const
+{
+       return type == THREAD_JOIN;
+}
+
 bool ModelAction::is_relseq_fixup() const
 {
        return type == MODEL_FIXUP_RELSEQ;
@@ -268,11 +279,17 @@ Thread * ModelAction::get_thread_operand() const
                return NULL;
 }
 
-/** This method changes an existing read part of an RMW action into either:
- *  (1) a full RMW action in case of the completed write or
- *  (2) a READ action in case a failed action.
+/**
+ * @brief Convert the read portion of an RMW
+ *
+ * Changes an existing read part of an RMW action into either:
+ *  -# a full RMW action in case of the completed write or
+ *  -# a READ action in case a failed action.
+ *
  * @todo  If the memory_order changes, we may potentially need to update our
  * clock vector.
+ *
+ * @param act The second half of the RMW (either RMWC or RMW)
  */
 void ModelAction::process_rmw(ModelAction *act)
 {
@@ -285,14 +302,18 @@ void ModelAction::process_rmw(ModelAction *act)
        }
 }
 
-/** The is_synchronizing method should only explore interleavings if:
- *  (1) the operations are seq_cst and don't commute or
- *  (2) the reordering may establish or break a synchronization relation.
- *  Other memory operations will be dealt with by using the reads_from
- *  relation.
+/**
+ * @brief Check if this action should be backtracked with another, due to
+ * potential synchronization
+ *
+ * The is_synchronizing method should only explore interleavings if:
+ *  -# the operations are seq_cst and don't commute or
+ *  -# the reordering may establish or break a synchronization relation.
+ *
+ * Other memory operations will be dealt with by using the reads_from relation.
  *
- *  @param act is the action to consider exploring a reordering.
- *  @return tells whether we have to explore a reordering.
+ * @param act The action to consider exploring a reordering
+ * @return True, if we have to explore a reordering; otherwise false
  */
 bool ModelAction::could_synchronize_with(const ModelAction *act) const
 {
@@ -375,11 +396,9 @@ void ModelAction::create_cv(const ModelAction *parent)
                cv = new ClockVector(NULL, this);
 }
 
-void ModelAction::set_try_lock(bool obtainedlock) {
-       if (obtainedlock)
-               value = VALUE_TRYSUCCESS;
-       else
-               value = VALUE_TRYFAILED;
+void ModelAction::set_try_lock(bool obtainedlock)
+{
+       value = obtainedlock ? VALUE_TRYSUCCESS : VALUE_TRYFAILED;
 }
 
 /**
@@ -603,7 +622,7 @@ void ModelAction::print() const
                        if (idx >= 0)
                                model_print("  Rf: P%-2d", idx);
                        else
-                               model_print("  RF: P? ");
+                               model_print("  Rf: P? ");
                } else
                        model_print("  Rf: ?  ");
        }
@@ -625,8 +644,13 @@ unsigned int ModelAction::hash() const
        hash ^= seq_number << 5;
        hash ^= id_to_int(tid) << 6;
 
-       if (is_read() && reads_from)
-               hash ^= reads_from->get_seq_number();
+       if (is_read()) {
+              if (reads_from)
+                      hash ^= reads_from->get_seq_number();
+              else if (reads_from_promise)
+                      hash ^= model->get_promise_number(reads_from_promise);
+              hash ^= get_reads_from_value();
+       }
        return hash;
 }