X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=nodestack.cc;h=a850478e95391a5eecf1ca26ee12c47e4ab4dfcb;hp=6b1d4ef9c86929fdd14d14172149abaacec96133;hb=1b793f0683aff025afe2e19519572e3599575a19;hpb=f8990cc12e0a21702f9af0b017518fba0b279668

diff --git a/nodestack.cc b/nodestack.cc
index 6b1d4ef..a850478 100644
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -4,7 +4,7 @@
 #include "action.h"
 #include "common.h"
 #include "model.h"
-#include "threads.h"
+#include "threads-model.h"
 
 /**
  * @brief Node constructor
@@ -32,7 +32,9 @@ Node::Node(ModelAction *act, Node *par, int nthreads, Node *prevfairness)
 	may_read_from(),
 	read_from_index(0),
 	future_values(),
-	future_index(-1)
+	future_index(-1),
+	relseq_break_writes(),
+	relseq_break_index(0)
 {
 	if (act) {
 		act->set_node(this);
@@ -47,7 +49,7 @@ Node::Node(ModelAction *act, Node *par, int nthreads, Node *prevfairness)
 				if (prevfi) {
 					*fi=*prevfi;
 				}
-				if (parent->enabled_array[i]) {
+				if (parent->is_enabled(i)) {
 					fi->enabled_count++;
 				}
 				if (i==currtid) {
@@ -56,7 +58,7 @@ Node::Node(ModelAction *act, Node *par, int nthreads, Node *prevfairness)
 				}
 				//Do window processing
 				if (prevfairness != NULL) {
-					if (prevfairness -> parent->enabled_array[i])
+					if (prevfairness -> parent->is_enabled(i))
 						fi->enabled_count--;
 					if (i==prevtid) {
 						fi->turns--;
@@ -216,15 +218,15 @@ bool Node::read_from_empty() {
  * Mark the appropriate backtracking information for exploring a thread choice.
  * @param act The ModelAction to explore
  */
-void Node::explore_child(ModelAction *act, bool * is_enabled)
+void Node::explore_child(ModelAction *act, enabled_type_t * is_enabled)
 {
 	if ( ! enabled_array )
-		enabled_array=(bool *)model_malloc(sizeof(bool)*num_threads);
+		enabled_array=(enabled_type_t *)model_malloc(sizeof(enabled_type_t)*num_threads);
 	if (is_enabled != NULL)
-		memcpy(enabled_array, is_enabled, sizeof(bool)*num_threads);
+		memcpy(enabled_array, is_enabled, sizeof(enabled_type_t)*num_threads);
 	else {
 		for(int i=0;i<num_threads;i++)
-			enabled_array[i]=false;
+			enabled_array[i]=THREAD_DISABLED;
 	}
 
 	explore(act->get_tid());
@@ -265,13 +267,13 @@ thread_id_t Node::get_next_backtrack()
 bool Node::is_enabled(Thread *t)
 {
 	int thread_id=id_to_int(t->get_id());
-	return thread_id < num_threads && enabled_array[thread_id];
+	return thread_id < num_threads && (enabled_array[thread_id] != THREAD_DISABLED);
 }
 
 bool Node::is_enabled(thread_id_t tid)
 {
 	int thread_id=id_to_int(tid);
-	return thread_id < num_threads && enabled_array[thread_id];
+	return thread_id < num_threads && (enabled_array[thread_id] != THREAD_DISABLED);
 }
 
 bool Node::has_priority(thread_id_t tid)
@@ -352,6 +354,58 @@ bool Node::increment_future_value() {
 	return false;
 }
 
+/**
+ * Add a write ModelAction to the set of writes that may break the release
+ * sequence. This is used during replay exploration of pending release
+ * sequences. This Node must correspond to a release sequence fixup action.
+ *
+ * @param write The write that may break the release sequence. NULL means we
+ * allow the release sequence to synchronize.
+ */
+void Node::add_relseq_break(const ModelAction *write)
+{
+	relseq_break_writes.push_back(write);
+}
+
+/**
+ * Get the write that may break the current pending release sequence,
+ * according to the replay / divergence pattern.
+ *
+ * @return A write that may break the release sequence. If NULL, that means
+ * the release sequence should not be broken.
+ */
+const ModelAction * Node::get_relseq_break()
+{
+	if (relseq_break_index < (int)relseq_break_writes.size())
+		return relseq_break_writes[relseq_break_index];
+	else
+		return NULL;
+}
+
+/**
+ * Increments the index into the relseq_break_writes set to explore the next
+ * item.
+ * @return Returns false if we have explored all values.
+ */
+bool Node::increment_relseq_break()
+{
+	DBG();
+	promises.clear();
+	if (relseq_break_index < ((int)relseq_break_writes.size())) {
+		relseq_break_index++;
+		return (relseq_break_index < ((int)relseq_break_writes.size()));
+	}
+	return false;
+}
+
+/**
+ * @return True if all writes that may break the release sequence have been
+ * explored
+ */
+bool Node::relseq_break_empty() {
+	return ((relseq_break_index + 1) >= ((int)relseq_break_writes.size()));
+}
+
 void Node::explore(thread_id_t tid)
 {
 	int i = id_to_int(tid);
@@ -391,7 +445,7 @@ void NodeStack::print()
 /** Note: The is_enabled set contains what actions were enabled when
  *  act was chosen. */
 
-ModelAction * NodeStack::explore_action(ModelAction *act, bool * is_enabled)
+ModelAction * NodeStack::explore_action(ModelAction *act, enabled_type_t * is_enabled)
 {
 	DBG();