local commit... bug that prunes too many executions

diff --git a/Makefile b/Makefile
index 3a3d826107da6fe2c64082d60bd385afb7492d71..d530fee70ca50bb1702c7c098c565c6cdf28edb9 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -3,7 +3,7 @@ include common.mk
 OBJECTS = libthreads.o schedule.o model.o threads.o librace.o action.o \
          nodestack.o clockvector.o main.o snapshot-interface.o cyclegraph.o \
          datarace.o impatomic.o cmodelint.o \
-         snapshot.o malloc.o mymemory.o common.o mutex.o
+         snapshot.o malloc.o mymemory.o common.o mutex.o promise.o
 
 CPPFLAGS += -Iinclude -I. -rdynamic
 LDFLAGS = -ldl -lrt

diff --git a/action.cc b/action.cc
index 20777f96161cfa84c3130c07f11177258481eb5f..c6504cd388d0f44f6ec72c038d36996b79fad882 100644 (file)
--- a/action.cc
+++ b/action.cc
@@ -281,7 +281,7 @@ bool ModelAction::read_from(const ModelAction *act)
 bool ModelAction::synchronize_with(const ModelAction *act) {
        if (*this < *act && type != THREAD_JOIN && type != ATOMIC_LOCK)
                return false;
-       model->check_promises(cv, act->cv);
+       model->check_promises(act->get_tid(), cv, act->cv);
        cv->merge(act->cv);
        return true;
 }

diff --git a/cyclegraph.cc b/cyclegraph.cc
index f4d3b93314b4ad22dba40d4d56043fd5643c01d1..2280e76e3e208b8ac6ce6e2044433c1a866d2c85 100644 (file)
--- a/cyclegraph.cc
+++ b/cyclegraph.cc
@@ -1,6 +1,8 @@
 #include "cyclegraph.h"
 #include "action.h"
 #include "common.h"
+#include "promise.h"
+#include "model.h"
 
 /** Initializes a CycleGraph object. */
 CycleGraph::CycleGraph() :
@@ -195,6 +197,33 @@ bool CycleGraph::checkReachable(CycleNode *from, CycleNode *to) {
        return false;
 }
 
+bool CycleGraph::checkPromise(const ModelAction *fromact, Promise *promise) {
+       std::vector<CycleNode *, ModelAlloc<CycleNode *> > queue;
+       HashTable<CycleNode *, CycleNode *, uintptr_t, 4, model_malloc, model_calloc, model_free> discovered(64);
+       CycleNode *from = actionToNode.get(fromact);
+
+
+       queue.push_back(from);
+       discovered.put(from, from);
+       while(!queue.empty()) {
+               CycleNode * node=queue.back();
+               queue.pop_back();
+
+               if (promise->increment_threads(node->getAction()->get_tid())) {
+                       return true;
+               }
+
+               for(unsigned int i=0;i<node->getEdges()->size();i++) {
+                       CycleNode *next=(*node->getEdges())[i];
+                       if (!discovered.contains(next)) {
+                               discovered.put(next,next);
+                               queue.push_back(next);
+                       }
+               }
+       }
+       return false;
+}
+
 void CycleGraph::startChanges() {
        ASSERT(rollbackvector.size()==0);
        ASSERT(rmwrollbackvector.size()==0);

diff --git a/cyclegraph.h b/cyclegraph.h
index 42866a3b370ceb52ab85967c1cfe0c80f4aedf6f..1cc0d069531e6499aed90a3972bfd1ff533c3c8f 100644 (file)
--- a/cyclegraph.h
+++ b/cyclegraph.h
@@ -11,6 +11,7 @@
 #include "config.h"
 #include "mymemory.h"
 
+class Promise;
 class CycleNode;
 class ModelAction;
 
@@ -23,7 +24,7 @@ class CycleGraph {
        bool checkForCycles();
        bool checkForRMWViolation();
        void addRMWEdge(const ModelAction *from, const ModelAction *rmw);
-
+       bool checkPromise(const ModelAction *from, Promise *p);
        bool checkReachable(const ModelAction *from, const ModelAction *to);
        void startChanges();
        void commitChanges();

diff --git a/model.cc b/model.cc
index e3d9203eea60ec53010d67bb87da20331cfbf642..824e1e430c7e29c983a380a92ae821ddc425c721 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -52,7 +52,7 @@ ModelChecker::ModelChecker(struct model_params params) :
 /** @brief Destructor */
 ModelChecker::~ModelChecker()
 {
-       for (int i = 0; i < get_num_threads(); i++)
+       for (unsigned int i = 0; i < get_num_threads(); i++)
                delete thread_map->get(i);
        delete thread_map;
 
@@ -95,7 +95,7 @@ thread_id_t ModelChecker::get_next_id()
 }
 
 /** @return the number of user threads created during this execution */
-int ModelChecker::get_num_threads()
+unsigned int ModelChecker::get_num_threads()
 {
        return priv->next_thread_id;
 }
@@ -377,6 +377,8 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw)
 
                        curr->read_from(reads_from);
                        mo_graph->commitChanges();
+                       mo_check_promises(curr->get_tid(), reads_from);
+
                        updated |= r_status;
                } else if (!second_part_of_rmw) {
                        /* Read from future value */
@@ -474,6 +476,8 @@ bool ModelChecker::process_write(ModelAction *curr)
        }
 
        mo_graph->commitChanges();
+       mo_check_promises(curr->get_tid(), curr);
+
        get_thread(curr)->set_return_value(VALUE_NONE);
        return updated_mod_order || updated_promises;
 }
@@ -526,7 +530,7 @@ bool ModelChecker::process_thread_action(ModelAction *curr)
                break;
        }
        case THREAD_START: {
-               check_promises(NULL, curr->get_cv());
+               check_promises(curr->get_tid(), NULL, curr->get_cv());
                break;
        }
        default:
@@ -1503,6 +1507,7 @@ bool ModelChecker::resolve_promises(ModelAction *write)
                        post_r_modification_order(read, write);
                        //Make sure the promise's value matches the write's value
                        ASSERT(promise->get_value() == write->get_value());
+                       mo_check_promises(read->get_tid(), write);
 
                        delete(promise);
                        promises->erase(promises->begin() + promise_index);
@@ -1535,16 +1540,14 @@ void ModelChecker::compute_promises(ModelAction *curr)
 }
 
 /** Checks promises in response to change in ClockVector Threads. */
-void ModelChecker::check_promises(ClockVector *old_cv, ClockVector *merge_cv)
+void ModelChecker::check_promises(thread_id_t tid, ClockVector *old_cv, ClockVector *merge_cv)
 {
        for (unsigned int i = 0; i < promises->size(); i++) {
                Promise *promise = (*promises)[i];
                const ModelAction *act = promise->get_action();
                if ((old_cv == NULL || !old_cv->synchronized_since(act)) &&
                                merge_cv->synchronized_since(act)) {
-                       //This thread is no longer able to send values back to satisfy the promise
-                       int num_synchronized_threads = promise->increment_threads();
-                       if (num_synchronized_threads == get_num_threads()) {
+                       if (promise->increment_threads(tid)) {
                                //Promise has failed
                                failed_promise = true;
                                return;
@@ -1553,6 +1556,40 @@ void ModelChecker::check_promises(ClockVector *old_cv, ClockVector *merge_cv)
        }
 }
 
+/** Checks promises in response to change in ClockVector Threads. */
+void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write) {
+       void * location = write->get_location();
+       for (unsigned int i = 0; i < promises->size(); i++) {
+               Promise *promise = (*promises)[i];
+               const ModelAction *act = promise->get_action();
+               
+               //Is this promise on the same location?
+               if ( act->get_location() != location )
+                       continue;
+
+               if ( act->get_tid()==tid) {
+                       if (promise->get_write() == NULL ) {
+                               promise->set_write(write);
+                       }
+                       if (mo_graph->checkPromise(write, promise)) {
+                               failed_promise = true;
+                               return;
+                       }
+               }
+               
+               //Don't do any lookups twice for the same thread
+               if (promise->has_sync_thread(tid))
+                       continue;
+               
+               if (mo_graph->checkReachable(promise->get_write(), write)) {
+                       if (promise->increment_threads(tid)) {
+                               failed_promise = true;
+                               return;
+                       }
+               }
+       }
+}
+
 /**
  * Build up an initial set of all past writes that this 'read' action may read
  * from. This set is determined by the clock vector's "happens before"

diff --git a/model.h b/model.h
index d8dce07cbdf56423e04e2378d2e0715d18025559..dfc8e36c2be5e775ec82dab1e81a8adcfdaa2697 100644 (file)
--- a/model.h
+++ b/model.h
@@ -49,7 +49,7 @@ struct PendingFutureValue {
  */
 struct model_snapshot_members {
        ModelAction *current_action;
-       int next_thread_id;
+       unsigned int next_thread_id;
        modelclock_t used_sequence_numbers;
        Thread *nextThread;
        ModelAction *next_backtrack;
@@ -76,7 +76,7 @@ public:
        Thread * get_thread(ModelAction *act) const;
 
        thread_id_t get_next_id();
-       int get_num_threads();
+       unsigned int get_num_threads();
        Thread * get_current_thread();
 
        int switch_to_master(ModelAction *act);
@@ -86,7 +86,8 @@ public:
        bool isfeasible();
        bool isfeasibleotherthanRMW();
        bool isfinalfeasible();
-       void check_promises(ClockVector *old_cv, ClockVector * merge_cv);
+       void mo_check_promises(thread_id_t tid, const ModelAction *write);
+       void check_promises(thread_id_t tid, ClockVector *old_cv, ClockVector * merge_cv);
        void get_release_seq_heads(ModelAction *act, rel_heads_list_t *release_heads);
        void finish_execution();
        bool isfeasibleprefix();
@@ -97,6 +98,7 @@ public:
        void set_bad_synchronization() { bad_synchronization = true; }
 
        const model_params params;
+       Scheduler * get_scheduler() { return scheduler;}
 
        MEMALLOC
 private:

diff --git a/promise.cc b/promise.cc
new file mode 100644 (file)
index 0000000..259ba05
--- /dev/null
+++ b/promise.cc
@@ -0,0 +1,21 @@
+#include "promise.h"
+#include "model.h"
+#include "schedule.h"
+
+bool Promise::increment_threads(thread_id_t tid) { 
+       unsigned int id=id_to_int(tid); 
+       if (id>=synced_thread.size()) {
+               synced_thread.resize(id+1, false);
+       }
+       if (synced_thread[id])
+               return false;
+       
+       synced_thread[id]=true;
+       bool * enabled=model->get_scheduler()->get_enabled();
+
+       for(unsigned int i=0;i<model->get_num_threads();i++) {
+               if (!synced_thread[id] && enabled[id])
+                       return false;
+       }
+       return true;
+}

diff --git a/promise.h b/promise.h
index 11719fc3b2c291307f61e9480205265436ca7b48..2ce3e297305125baa0a057da571cf266965b916e 100644 (file)
--- a/promise.h
+++ b/promise.h
@@ -8,25 +8,40 @@
 #define __PROMISE_H__
 
 #include <inttypes.h>
+#include "threads.h"
 
-class ModelAction;
+#include "model.h"
 
 class Promise {
  public:
  Promise(ModelAction *act, uint64_t value, modelclock_t expiration) :
-       value(value), expiration(expiration), read(act), numthreads(1)
-       { }
+       value(value), expiration(expiration), read(act), write(NULL)
+       { 
+               increment_threads(act->get_tid());
+       }
        modelclock_t get_expiration() const {return expiration;}
        ModelAction * get_action() const { return read; }
-       int increment_threads() { return ++numthreads; }
+       bool increment_threads(thread_id_t tid);
+
+       bool has_sync_thread(thread_id_t tid) { 
+               unsigned int id=id_to_int(tid); 
+               if (id>=synced_thread.size()) {
+                       return false;
+               }
+               return synced_thread[id];
+       }
+
        uint64_t get_value() const { return value; }
+       void set_write(const ModelAction *act) { write = act; }
+       const ModelAction * get_write() { return write; }
 
        SNAPSHOTALLOC
  private:
+       std::vector<bool> synced_thread;
        const uint64_t value;
        const modelclock_t expiration;
        ModelAction * const read;
-       unsigned int numthreads;
+       const ModelAction * write;
 };
 
 #endif

diff --git a/threads.h b/threads.h
index b69f4265618d1dd2eb4ef18c66aef2b4442a0496..a379494d43bd93ee78dea0f3f0bb98dcd0af60a4 100644 (file)
--- a/threads.h
+++ b/threads.h
@@ -81,6 +81,14 @@ public:
         */
        void push_wait_list(ModelAction *act) { wait_list.push_back(act); }
 
+       unsigned int num_wait_list() {
+               return wait_list.size();
+       }
+
+       ModelAction * get_waiter(unsigned int i) {
+               return wait_list[i];
+       }
+
        ModelAction * get_pending() { return pending; }
        void set_pending(ModelAction *act) { pending = act; }
        /**