fix bug.... not quite perfect for linux locks, but runs to completion...

Revert "model: revert broken bugfix"

This reverts commit ae7fcd2e5e499f72d9d1530bdc293f4fbc5f0644.

diff --git a/config.h b/config.h
index ab54e3a..5509363 100644 (file)
--- a/config.h
+++ b/config.h
@@ -29,7 +29,7 @@
 
 /** If USE_MPROTECT_SNAPSHOT=1, then snapshot by using mmap() and mprotect()
  * If USE_MPROTECT_SNAPSHOT=0, then snapshot by using fork() */
-#define USE_MPROTECT_SNAPSHOT 1
+#define USE_MPROTECT_SNAPSHOT 0
 
 /** Size of signal stack */
 #define SIGSTACKSIZE 32768

diff --git a/nodestack.cc b/nodestack.cc
index b33d247..c364df9 100644 (file)
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -325,8 +325,11 @@ const ModelAction * Node::get_read_from() {
 bool Node::increment_read_from() {
        DBG();
        promises.clear();
-       read_from_index++;
-       return (read_from_index < may_read_from.size());
+       if (read_from_index < may_read_from.size()) {
+               read_from_index++;
+               return read_from_index < may_read_from.size();
+       }
+       return false;
 }
 
 /**
@@ -336,8 +339,11 @@ bool Node::increment_read_from() {
 bool Node::increment_future_value() {
        DBG();
        promises.clear();
-       future_index++;
-       return (future_index < (int)future_values.size());
+       if (future_index < ((int)future_values.size())) {
+               future_index++;
+               return (future_index < ((int)future_values.size()));
+       }
+       return false;
 }
 
 void Node::explore(thread_id_t tid)