Fixed bug breaking our consolidation of future values...

diff --git a/model.cc b/model.cc
index a22e0214a6c2a3fdabd01a5442b3cba6643c616d..0665ff49b9762c0e9317d5688d21437f614535ca 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -25,6 +25,7 @@ ModelChecker::ModelChecker(struct model_params params) :
        num_executions(0),
        num_feasible_executions(0),
        diverge(NULL),
        num_executions(0),
        num_feasible_executions(0),
        diverge(NULL),

+       earliest_diverge(NULL),

        action_trace(new action_list_t()),
        thread_map(new HashTable<int, Thread *, int>()),
        obj_map(new HashTable<const void *, action_list_t, uintptr_t, 4>()),
        action_trace(new action_list_t()),
        thread_map(new HashTable<int, Thread *, int>()),
        obj_map(new HashTable<const void *, action_list_t, uintptr_t, 4>()),


@@ -180,8 +181,13 @@ bool ModelChecker::next_execution()
        DBG();
 
        num_executions++;
        DBG();
 
        num_executions++;

-       if (isfinalfeasible())
+       if (isfinalfeasible()) {
+               printf("Earliest divergence point since last feasible execution:\n");
+               earliest_diverge->print();
+
+               earliest_diverge = NULL;

                num_feasible_executions++;
                num_feasible_executions++;

+       }

 
        if (isfinalfeasible() || DBG_ENABLED())
                print_summary();
 
        if (isfinalfeasible() || DBG_ENABLED())
                print_summary();


@@ -189,6 +195,9 @@ bool ModelChecker::next_execution()
        if ((diverge = get_next_backtrack()) == NULL)
                return false;
 
        if ((diverge = get_next_backtrack()) == NULL)
                return false;
 

+       if (earliest_diverge == NULL || *diverge < *earliest_diverge)
+               earliest_diverge=diverge;
+

        if (DBG_ENABLED()) {
                printf("Next execution will diverge at:\n");
                diverge->print();
        if (DBG_ENABLED()) {
                printf("Next execution will diverge at:\n");
                diverge->print();

diff --git a/model.h b/model.h
index 4b9e3ff53f0082b30efd095b5618186480882d5e..073b96b976cd4807c45c8c5e6ffef415941a0a81 100644 (file)
--- a/model.h
+++ b/model.h
@@ -151,6 +151,7 @@ private:
        void do_complete_join(ModelAction *join);
 
        ModelAction *diverge;
        void do_complete_join(ModelAction *join);
 
        ModelAction *diverge;

+       ModelAction *earliest_diverge;

 
        ucontext_t system_context;
        action_list_t *action_trace;
 
        ucontext_t system_context;
        action_list_t *action_trace;

diff --git a/nodestack.cc b/nodestack.cc
index 23611f976dfc2c5cf35f66c65284d0e4f890b1d1..533f75a7fab1bbc2c014d7fc883133b957bb94ed 100644 (file)
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -158,7 +158,7 @@ bool Node::add_future_value(uint64_t value, modelclock_t expiration) {
                if (future_values[i].value == value) {
                        if (future_values[i].expiration>=expiration)
                                return false;
                if (future_values[i].value == value) {
                        if (future_values[i].expiration>=expiration)
                                return false;

-                       if (future_index < i) {
+                       if (future_index < ((int) i)) {

                                suitableindex=i;
                        }
                }
                                suitableindex=i;
                        }
                }


@@ -325,8 +325,11 @@ const ModelAction * Node::get_read_from() {
 bool Node::increment_read_from() {
        DBG();
        promises.clear();
 bool Node::increment_read_from() {
        DBG();
        promises.clear();

-       read_from_index++;
-       return (read_from_index < may_read_from.size());
+       if ((read_from_index+1) < may_read_from.size()) {
+               read_from_index++;
+               return true;
+       }
+       return false;

 }
 
 /**
 }
 
 /**


@@ -336,8 +339,11 @@ bool Node::increment_read_from() {
 bool Node::increment_future_value() {
        DBG();
        promises.clear();
 bool Node::increment_future_value() {
        DBG();
        promises.clear();

-       future_index++;
-       return (future_index < future_values.size());
+       if ((future_index+1) < future_values.size()) {
+               future_index++;
+               return true;
+       }
+       return false;

 }
 
 void Node::explore(thread_id_t tid)
 }
 
 void Node::explore(thread_id_t tid)

diff --git a/nodestack.h b/nodestack.h
index 1f7d3e4ad3fee660027e974261b8083b3a99e0c3..7402aa57d107aac938faab66ea13782ffaff3609 100644 (file)
--- a/nodestack.h
+++ b/nodestack.h
@@ -112,7 +112,7 @@ private:
 
        std::vector< struct future_value, MyAlloc<struct future_value> > future_values;
        std::vector< promise_t, MyAlloc<promise_t> > promises;
 
        std::vector< struct future_value, MyAlloc<struct future_value> > future_values;
        std::vector< promise_t, MyAlloc<promise_t> > promises;

-       unsigned int future_index;
+       int future_index;

 };
 
 typedef std::vector< Node *, MyAlloc< Node * > > node_list_t;
 };
 
 typedef std::vector< Node *, MyAlloc< Node * > > node_list_t;