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 ab54e3abe68e12e8199976dfb415d188dff54258..55093637a175186bddebb46b9a37b2f3a5117666 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 b33d24739ca89399ffb363c1ba3bdecd61ca6dc2..c364df9f7613178e2453d05bd667f64f44ed4fde 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)