various fixes. linux rw locks should work again with -m 1

diff --git a/model.cc b/model.cc
index 09e6b9da3150ddc88de4cc4b8ce363725cc493f3..1ec72738ba3d0622bb27c8dedb3eab4c875aa90c 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -272,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;
@@ -1389,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];
@@ -1401,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;
        }
 
@@ -1856,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
@@ -1915,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/promise.cc b/promise.cc
index cbd45c2ffcf96f5398c49b29c4fdc2ef169c9b61..59fb9ee43115cd81ed60b2487ffbb563e90bd6da 100644 (file)
--- a/promise.cc
+++ b/promise.cc
@@ -13,9 +13,22 @@ 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();
-       for(unsigned int i=0;i<model->get_num_threads();i++) {
-               if ((i >= sync_size || !synced_thread[i]) && (enabled[i] != THREAD_DISABLED))
+       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]) && ( i != promise_tid ) && (enabled[i] != THREAD_DISABLED)) {
                        return false;
+               }
+       }
+       return true;
+}
+
+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();
 }
 
 /**