Merge remote-tracking branch 'origin/master' into pldi13

diff --git a/action.cc b/action.cc
index 140d59098f8c37732753e4f80ddc58f8a883810b..1387ed15b67c9ac25d7fcba68491bbb72d8ff236 100644 (file)
--- a/action.cc
+++ b/action.cc
@@ -365,7 +365,7 @@ bool ModelAction::synchronize_with(const ModelAction *act) {
 
 bool ModelAction::has_synchronized_with(const ModelAction *act) const
 {
-       return cv->has_synchronized_with(act->cv);
+       return cv->synchronized_since(act);
 }
 
 /**

diff --git a/clockvector.cc b/clockvector.cc
index 7d947c63873cc41abc2b0cfb2cff85868ba6765d..e56c2ace662507be12875c18446932fe54593252 100644 (file)
--- a/clockvector.cc
+++ b/clockvector.cc
@@ -75,17 +75,6 @@ bool ClockVector::synchronized_since(const ModelAction *act) const
        return false;
 }
 
-bool ClockVector::has_synchronized_with(const ClockVector *cv) const
-{
-       ASSERT(cv);
-       if (cv->num_threads > num_threads)
-               return false;
-       for (int i = 0; i < cv->num_threads; i++)
-               if (cv->clock[i] > clock[i])
-                       return false;
-       return true;
-}
-
 /** Gets the clock corresponding to a given thread id from the clock vector. */
 modelclock_t ClockVector::getClock(thread_id_t thread) {
        int threadid = id_to_int(thread);

diff --git a/clockvector.h b/clockvector.h
index 6a902c5215342bae0313d56b3e6cfa8267bd79cf..9000a5d72eddd90ba1ba5964e4a12105a75ca9b1 100644 (file)
--- a/clockvector.h
+++ b/clockvector.h
@@ -17,7 +17,6 @@ public:
        ~ClockVector();
        void merge(const ClockVector *cv);
        bool synchronized_since(const ModelAction *act) const;
-       bool has_synchronized_with(const ClockVector *cv) const;
 
        void print() const;
        modelclock_t getClock(thread_id_t thread);

diff --git a/model.cc b/model.cc
index 7808b104969f72fd9f9b62fe25a8574fffdac9b5..1e730d794baca5dc99387053bb98125b3756193a 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -218,7 +218,8 @@ void ModelChecker::execute_sleep_set() {
        for(unsigned int i=0;i<get_num_threads();i++) {
                thread_id_t tid=int_to_id(i);
                Thread *thr=get_thread(tid);
-               if ( scheduler->get_enabled(thr) == THREAD_SLEEP_SET ) {
+               if ( scheduler->get_enabled(thr) == THREAD_SLEEP_SET &&
+                                thr->get_pending() == NULL ) {
                        thr->set_state(THREAD_RUNNING);
                        scheduler->next_thread(thr);
                        Thread::swap(&system_context, thr);
@@ -271,8 +272,10 @@ bool ModelChecker::next_execution()
                        pending_rel_seqs->size());
 
 
-       if (isfinalfeasible() || (params.bound != 0 && priv->used_sequence_numbers > params.bound ) || DBG_ENABLED() )
+       if (isfinalfeasible() || (params.bound != 0 && priv->used_sequence_numbers > params.bound ) || DBG_ENABLED() ) {
+               checkDataRaces();
                print_summary();
+       }
 
        if ((diverge = get_next_backtrack()) == NULL)
                return false;
@@ -971,7 +974,7 @@ bool ModelChecker::promises_expired() {
 /** @return whether the current partial trace must be a prefix of a
  * feasible trace. */
 bool ModelChecker::isfeasibleprefix() {
-       return promises->size() == 0 && pending_rel_seqs->size() == 0;
+       return promises->size() == 0 && pending_rel_seqs->size() == 0 && isfeasible();
 }
 
 /** @return whether the current partial trace is feasible. */
@@ -1094,7 +1097,7 @@ void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) {
                                ModelAction *act=*rit;
                                bool foundvalue = false;
                                for (int j = 0; j<act->get_node()->get_read_from_size(); j++) {
-                                       if (act->get_node()->get_read_from_at(i)==write) {
+                                       if (act->get_node()->get_read_from_at(j)==write) {
                                                foundvalue = true;
                                                break;
                                        }
@@ -1388,7 +1391,7 @@ bool ModelChecker::mo_may_allow(const ModelAction *writer, const ModelAction *re
 
        /* Iterate over all threads */
        for (i = 0; i < thrd_lists->size(); i++) {
-               ModelAction *write_after_read = NULL;
+               const ModelAction *write_after_read = NULL;
 
                /* Iterate over actions in thread, starting from most recent */
                action_list_t *list = &(*thrd_lists)[i];
@@ -1400,9 +1403,12 @@ bool ModelChecker::mo_may_allow(const ModelAction *writer, const ModelAction *re
                                break;
                        else if (act->is_write())
                                write_after_read = act;
+                       else if (act->is_read()&&act->get_reads_from()!=NULL) {
+                               write_after_read = act->get_reads_from();
+                       }
                }
-
-               if (write_after_read && mo_graph->checkReachable(write_after_read, writer))
+               
+               if (write_after_read && write_after_read!=writer && mo_graph->checkReachable(write_after_read, writer))
                        return false;
        }
 
@@ -1833,7 +1839,7 @@ void ModelChecker::compute_promises(ModelAction *curr)
                                !act->same_thread(curr) &&
                                act->get_location() == curr->get_location() &&
                                promise->get_value() == curr->get_value()) {
-                       curr->get_node()->set_promise(i);
+                       curr->get_node()->set_promise(i, act->is_rmw());
                }
        }
 }
@@ -1855,6 +1861,16 @@ void ModelChecker::check_promises(thread_id_t tid, ClockVector *old_cv, ClockVec
        }
 }
 
+void ModelChecker::check_promises_thread_disabled() {
+       for (unsigned int i = 0; i < promises->size(); i++) {
+               Promise *promise = (*promises)[i];
+               if (promise->check_promise()) {
+                       failed_promise = true;
+                       return;
+               }
+       }
+}
+
 /** Checks promises in response to addition to modification order for threads.
  * Definitions:
  * pthread is the thread that performed the read that created the promise
@@ -1914,7 +1930,7 @@ void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write)
                if (promise->has_sync_thread(tid))
                        continue;
                
-               if (mo_graph->checkReachable(promise->get_write(), write)) {
+               if (promise->get_write()&&mo_graph->checkReachable(promise->get_write(), write)) {
                        if (promise->increment_threads(tid)) {
                                failed_promise = true;
                                return;

diff --git a/model.h b/model.h
index 8ff9d375838b193bec751f9b7f0d419a89f07a8d..59a07597bb5bf0436752ad6a4fca2f22d9fa2fe8 100644 (file)
--- a/model.h
+++ b/model.h
@@ -99,6 +99,7 @@ public:
        bool isfeasible();
        bool isfeasibleotherthanRMW();
        bool isfinalfeasible();
+       void check_promises_thread_disabled();
        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);

diff --git a/nodestack.cc b/nodestack.cc
index d08fa5c733e126f1faa710bfb613bb1df6ecccff..743cb864452589f615d937220fe9440bf8bad093 100644 (file)
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -105,11 +105,14 @@ void Node::print_may_read_from()
  * Sets a promise to explore meeting with the given node.
  * @param i is the promise index.
  */
-void Node::set_promise(unsigned int i) {
+void Node::set_promise(unsigned int i, bool is_rmw) {
        if (i >= promises.size())
                promises.resize(i + 1, PROMISE_IGNORE);
-       if (promises[i] == PROMISE_IGNORE)
+       if (promises[i] == PROMISE_IGNORE) {
                promises[i] = PROMISE_UNFULFILLED;
+               if (is_rmw)
+                       promises[i] |= PROMISE_RMW;
+       }
 }
 
 /**
@@ -118,7 +121,7 @@ void Node::set_promise(unsigned int i) {
  * @return true if the promise should be satisfied by the given model action.
  */
 bool Node::get_promise(unsigned int i) {
-       return (i < promises.size()) && (promises[i] == PROMISE_FULFILLED);
+       return (i < promises.size()) && ((promises[i] & PROMISE_MASK) == PROMISE_FULFILLED);
 }
 
 /**
@@ -127,16 +130,27 @@ bool Node::get_promise(unsigned int i) {
  */
 bool Node::increment_promise() {
        DBG();
-
+       unsigned int rmw_count=0;
+       for (unsigned int i = 0; i < promises.size(); i++) {
+               if (promises[i]==(PROMISE_RMW|PROMISE_FULFILLED))
+                       rmw_count++;
+       }
+       
        for (unsigned int i = 0; i < promises.size(); i++) {
-               if (promises[i] == PROMISE_UNFULFILLED) {
-                       promises[i] = PROMISE_FULFILLED;
+               if ((promises[i] & PROMISE_MASK) == PROMISE_UNFULFILLED) {
+                       if ((rmw_count > 0) && (promises[i] & PROMISE_RMW)) {
+                               //sending our value to two rmws... not going to work..try next combination
+                               continue;
+                       }
+                       promises[i] = (promises[i] & PROMISE_RMW) |PROMISE_FULFILLED;
                        while (i > 0) {
                                i--;
-                               if (promises[i] == PROMISE_FULFILLED)
-                                       promises[i] = PROMISE_UNFULFILLED;
+                               if ((promises[i] & PROMISE_MASK) == PROMISE_FULFILLED)
+                                       promises[i] = (promises[i] & PROMISE_RMW) | PROMISE_UNFULFILLED;
                        }
                        return true;
+               } else if (promises[i] == (PROMISE_RMW|PROMISE_FULFILLED)) {
+                       rmw_count--;
                }
        }
        return false;
@@ -147,9 +161,15 @@ bool Node::increment_promise() {
  * @return true if we have explored all promise combinations.
  */
 bool Node::promise_empty() {
-       for (unsigned int i = 0; i < promises.size();i++)
-               if (promises[i] == PROMISE_UNFULFILLED)
+       bool fulfilledrmw=false;
+       for (int i = promises.size()-1 ; i>=0; i--) {
+               if (promises[i]==PROMISE_UNFULFILLED)
+                       return false;
+               if (!fulfilledrmw && ((promises[i]&PROMISE_MASK)==PROMISE_UNFULFILLED))
                        return false;
+               if (promises[i]==(PROMISE_FULFILLED|PROMISE_RMW))
+                       fulfilledrmw=true;
+       }
        return true;
 }
 

diff --git a/nodestack.h b/nodestack.h
index 648ef4dfc318afc38a4e98b1e31bf4a1bcc944eb..986b9c9df4be85f15d57cbf13f46d62626a3c35d 100644 (file)
--- a/nodestack.h
+++ b/nodestack.h
@@ -24,11 +24,14 @@ class Thread;
  * <li>@b fulfilled: satisfied by this Node's ModelAction under the current
  * configuration.</li></ol>
  */
-typedef enum {
-       PROMISE_IGNORE = 0, /**< This promise is inapplicable; ignore it */
-       PROMISE_UNFULFILLED, /**< This promise is applicable but unfulfilled */
-       PROMISE_FULFILLED /**< This promise is applicable and fulfilled */
-} promise_t;
+
+#define        PROMISE_IGNORE 0 /**< This promise is inapplicable; ignore it */
+#define        PROMISE_UNFULFILLED 1 /**< This promise is applicable but unfulfilled */
+#define        PROMISE_FULFILLED 2 /**< This promise is applicable and fulfilled */
+#define PROMISE_MASK 0xf
+#define PROMISE_RMW 0x10
+
+typedef int promise_t;
 
 struct future_value {
        uint64_t value;
@@ -88,7 +91,7 @@ public:
        int get_read_from_size();
        const ModelAction * get_read_from_at(int i);
 
-       void set_promise(unsigned int i);
+       void set_promise(unsigned int i, bool is_rmw);
        bool get_promise(unsigned int i);
        bool increment_promise();
        bool promise_empty();

diff --git a/promise.cc b/promise.cc
index 5197ed3a1e0376d1ea4f6060bcfa042f7cd4f0e9..68290eecefac6c7ed72673e01a941e9f0afda3be 100644 (file)
--- a/promise.cc
+++ b/promise.cc
@@ -4,7 +4,7 @@
 
 bool Promise::increment_threads(thread_id_t tid) { 
        unsigned int id=id_to_int(tid); 
-       if (id>=synced_thread.size()) {
+       if ( id >= synced_thread.size() ) {
                synced_thread.resize(id+1, false);
        }
        if (synced_thread[id])
@@ -12,10 +12,23 @@ bool Promise::increment_threads(thread_id_t tid) {
        
        synced_thread[id]=true;
        enabled_type_t * enabled=model->get_scheduler()->get_enabled();
+       unsigned int sync_size=synced_thread.size();
+       int promise_tid=id_to_int(read->get_tid());
+       for(unsigned int i=1;i<model->get_num_threads();i++) {
+               if ((i >= sync_size || !synced_thread[i]) && ( (int)i != promise_tid ) && (enabled[i] != THREAD_DISABLED)) {
+                       return false;
+               }
+       }
+       return true;
+}
 
-       for(unsigned int i=0;i<model->get_num_threads();i++) {
-               if (!synced_thread[id] && (enabled[id] == THREAD_ENABLED))
+bool Promise::check_promise() {
+       enabled_type_t * enabled=model->get_scheduler()->get_enabled();
+       unsigned int sync_size=synced_thread.size();
+       for(unsigned int i=1;i<model->get_num_threads();i++) {
+               if ((i >= sync_size || !synced_thread[i]) && (enabled[i] != THREAD_DISABLED)) {
                        return false;
+               }
        }
        return true;
 }

diff --git a/promise.h b/promise.h
index ce84ede68b0e58e4c76c280cb6632bc85d76cb02..ea40df0112b183b515258877af1ce20cb606b30d 100644 (file)
--- a/promise.h
+++ b/promise.h
@@ -31,6 +31,7 @@ class Promise {
                return synced_thread[id];
        }
 
+       bool check_promise();
        uint64_t get_value() const { return value; }
        void set_write(const ModelAction *act) { write = act; }
        const ModelAction * get_write() { return write; }

diff --git a/schedule.cc b/schedule.cc
index 1cd5b0f1a9f3db7410965a8afad7e67f27a360d3..93379c2d9df3f1a03a4046ae4753a07115400625 100644 (file)
--- a/schedule.cc
+++ b/schedule.cc
@@ -29,6 +29,8 @@ void Scheduler::set_enabled(Thread *t, enabled_type_t enabled_status) {
                enabled_len=threadid+1;
        }
        enabled[threadid]=enabled_status;
+       if (enabled_status == THREAD_DISABLED)
+               model->check_promises_thread_disabled();
 }
 
 /**