fix some of the bugs related to barrier example...

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index 7e8211daf523f37e2c110d3852912c203decb331..c0cc93eb0a80523eefc48f2fe7ec3c8119d8619c 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -12,7 +12,7 @@
 #include "promise.h"
 #include "datarace.h"
 #include "mutex.h"
-#include "threads.h"
+#include "threads-model.h"
 
 #define INITIAL_THREAD_ID      0
 
@@ -260,7 +260,8 @@ bool ModelChecker::next_execution()
        DEBUG("Number of acquires waiting on pending release sequences: %zu\n",
                        pending_rel_seqs->size());
 
-       if (isfinalfeasible() || DBG_ENABLED())
+
+       if (isfinalfeasible() || (params.bound != 0 && priv->used_sequence_numbers > params.bound ) || DBG_ENABLED() )
                print_summary();
 
        if ((diverge = get_next_backtrack()) == NULL)
@@ -557,26 +558,17 @@ bool ModelChecker::process_thread_action(ModelAction *curr)
                break;
        }
        case THREAD_JOIN: {
-               Thread *waiting, *blocking;
-               waiting = get_thread(curr);
-               blocking = (Thread *)curr->get_location();
-               if (!blocking->is_complete()) {
-                       blocking->push_wait_list(curr);
-                       scheduler->sleep(waiting);
-               } else {
-                       do_complete_join(curr);
-                       updated = true; /* trigger rel-seq checks */
-               }
+               Thread *blocking = (Thread *)curr->get_location();
+               ModelAction *act = get_last_action(blocking->get_id());
+               curr->synchronize_with(act);
+               updated = true; /* trigger rel-seq checks */
                break;
        }
        case THREAD_FINISH: {
                Thread *th = get_thread(curr);
                while (!th->wait_list_empty()) {
                        ModelAction *act = th->pop_wait_list();
-                       Thread *wake = get_thread(act);
-                       scheduler->wake(wake);
-                       do_complete_join(act);
-                       updated = true; /* trigger rel-seq checks */
+                       scheduler->wake(get_thread(act));
                }
                th->complete();
                updated = true; /* trigger rel-seq checks */
@@ -721,9 +713,12 @@ ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr)
 }
 
 /**
- * This method checks whether a model action is enabled at the given point.
- * At this point, it checks whether a lock operation would be successful at this point.
- * If not, it puts the thread in a waiter list.
+ * @brief Check whether a model action is enabled.
+ *
+ * Checks whether a lock or join operation would be successful (i.e., is the
+ * lock already locked, or is the joined thread already complete). If not, put
+ * the action in a waiter list.
+ *
  * @param curr is the ModelAction to check whether it is enabled.
  * @return a bool that indicates whether the action is enabled.
  */
@@ -736,6 +731,12 @@ bool ModelChecker::check_action_enabled(ModelAction *curr) {
                        lock_waiters_map->get_safe_ptr(curr->get_location())->push_back(curr);
                        return false;
                }
+       } else if (curr->get_type() == THREAD_JOIN) {
+               Thread *blocking = (Thread *)curr->get_location();
+               if (!blocking->is_complete()) {
+                       blocking->push_wait_list(curr);
+                       return false;
+               }
        }
 
        return true;
@@ -760,7 +761,7 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
 
        if (!check_action_enabled(curr)) {
                /* Make the execution look like we chose to run this action
-                * much later, when a lock is actually available to release */
+                * much later, when a lock/join can succeed */
                get_current_thread()->set_pending(curr);
                scheduler->sleep(get_current_thread());
                return get_next_thread(NULL);
@@ -847,19 +848,6 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
        return get_next_thread(curr);
 }
 
-/**
- * Complete a THREAD_JOIN operation, by synchronizing with the THREAD_FINISH
- * operation from the Thread it is joining with. Must be called after the
- * completion of the Thread in question.
- * @param join The THREAD_JOIN action
- */
-void ModelChecker::do_complete_join(ModelAction *join)
-{
-       Thread *blocking = (Thread *)join->get_location();
-       ModelAction *act = get_last_action(blocking->get_id());
-       join->synchronize_with(act);
-}
-
 void ModelChecker::check_curr_backtracking(ModelAction * curr) {
        Node *currnode = curr->get_node();
        Node *parnode = currnode->get_parent();
@@ -1312,9 +1300,8 @@ bool ModelChecker::mo_may_allow(const ModelAction * writer, const ModelAction *r
 
        if (first_write_after_read==NULL)
                return true;
-       return true;
 
-       //return !mo_graph->checkReachable(first_write_after_read, writer);
+       return !mo_graph->checkReachable(first_write_after_read, writer);
 }
 
 
@@ -1793,6 +1780,11 @@ void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write)
                        //do we have a pwrite for the promise, if not, set it
                        if (promise->get_write() == NULL ) {
                                promise->set_write(write);
+                               //The pwrite cannot happen before the promise
+                               if (write->happens_before(act) && (write != act)) {
+                                       failed_promise = true;
+                                       return;
+                               }
                        }
                        if (mo_graph->checkPromise(write, promise)) {
                                failed_promise = true;
@@ -1882,7 +1874,7 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
                                        curr->print();
                                }
 
-                               if (curr->get_sleep_flag()) {
+                               if (curr->get_sleep_flag() && ! curr->is_seqcst()) {
                                        if (sleep_can_read_from(curr, act))
                                                curr->get_node()->add_read_from(act);
                                } else
@@ -2082,6 +2074,12 @@ bool ModelChecker::take_step() {
        if (!isfeasible())
                return false;
 
+       if (params.bound != 0) {
+               if (priv->used_sequence_numbers > params.bound) {
+                       return false;
+               }
+       }
+
        DEBUG("(%d, %d)\n", curr ? id_to_int(curr->get_id()) : -1,
                        next ? id_to_int(next->get_id()) : -1);