commit untested condvar code

[model-checker.git] / nodestack.cc

diff --git a/nodestack.cc b/nodestack.cc
index 4cf89500fc1faba0f98714173fbd4eca557edefa..ec7ce1694f764e640e099c9f2eb7a431c0b0763c 100644 (file)
--- 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,11 @@ 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),
+       misc_index(0),
+       misc_max(0)
 {
        if (act) {
                act->set_node(this);
@@ -47,7 +51,7 @@ Node::Node(ModelAction *act, Node *par, int nthreads, Node *prevfairness)
                                if (prevfi) {
                                        *fi=*prevfi;
                                }
-                               if (parent->enabled_array[i]==THREAD_ENABLED) {
+                               if (parent->is_enabled(i)) {
                                        fi->enabled_count++;
                                }
                                if (i==currtid) {
@@ -56,7 +60,7 @@ Node::Node(ModelAction *act, Node *par, int nthreads, Node *prevfairness)
                                }
                                //Do window processing
                                if (prevfairness != NULL) {
-                                       if (prevfairness -> parent->enabled_array[i] == THREAD_ENABLED)
+                                       if (prevfairness -> parent->is_enabled(i))
                                                fi->enabled_count--;
                                        if (i==prevtid) {
                                                fi->turns--;
@@ -149,6 +153,24 @@ bool Node::promise_empty() {
        return true;
 }
 
+
+void Node::set_misc_max(int i) {
+       misc_max=i;
+}
+
+int Node::get_misc() {
+       return misc_index;
+}
+
+bool Node::increment_misc() {
+       return (misc_index<misc_max)&&((++misc_index)<misc_max);
+}
+
+bool Node::misc_empty() {
+       return (misc_index+1)>=misc_max;
+}
+
+
 /**
  * Adds a value from a weakly ordered future write to backtrack to.
  * @param value is the value to backtrack to.
@@ -265,13 +287,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] == THREAD_ENABLED);
+       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] == THREAD_ENABLED);
+       return thread_id < num_threads && (enabled_array[thread_id] != THREAD_DISABLED);
 }
 
 bool Node::has_priority(thread_id_t tid)
@@ -352,6 +374,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);