X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=action.cc;h=0084fd3411cdb57e888b1dcef161eb16a6d1398d;hb=20956d81209b12a99ced78f51dd4294a0638343f;hp=08cacd89227f880c1bb391a83f799283c5de4e03;hpb=f5305a99cba598d0de55358df103439831dd1eb2;p=model-checker.git

diff --git a/action.cc b/action.cc
index 08cacd8..0084fd3 100644
--- a/action.cc
+++ b/action.cc
@@ -1,6 +1,7 @@
 #include <stdio.h>
 #define __STDC_FORMAT_MACROS
 #include <inttypes.h>
+#include <stdlib.h>
 
 #include "model.h"
 #include "action.h"
@@ -11,10 +12,10 @@
 
 #define ACTION_INITIAL_CLOCK 0
 
-/** A special value to represent a successful trylock */
+/** @brief A special value to represent a successful trylock */
 #define VALUE_TRYSUCCESS 1
 
-/** A special value to represent a failed trylock */
+/** @brief A special value to represent a failed trylock */
 #define VALUE_TRYFAILED 0
 
 /**
@@ -279,11 +280,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)
 {
@@ -296,14 +303,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
 {
@@ -489,9 +500,8 @@ void ModelAction::set_read_from_promise(Promise *promise)
  */
 bool ModelAction::synchronize_with(const ModelAction *act)
 {
-	if (*this < *act && type != THREAD_JOIN && type != ATOMIC_LOCK)
+	if (*this < *act)
 		return false;
-	model->check_promises(act->get_tid(), cv, act->cv);
 	cv->merge(act->cv);
 	return true;
 }
@@ -608,7 +618,7 @@ void ModelAction::print() const
 		if (reads_from)
 			model_print("  Rf: %-3d", reads_from->get_seq_number());
 		else if (reads_from_promise) {
-			int idx = model->get_promise_number(reads_from_promise);
+			int idx = reads_from_promise->get_index();
 			if (idx >= 0)
 				model_print("  Rf: P%-2d", idx);
 			else
@@ -638,7 +648,7 @@ unsigned int ModelAction::hash() const
 	       if (reads_from)
 		       hash ^= reads_from->get_seq_number();
 	       else if (reads_from_promise)
-		       hash ^= model->get_promise_number(reads_from_promise);
+		       hash ^= reads_from_promise->get_index();
 	       hash ^= get_reads_from_value();
 	}
 	return hash;