Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/model-checker

diff --git a/action.cc b/action.cc
index 0063d0b27169f29dbe46d2fa71c3535fea2abc9c..383be230aaea3f4b505266688fde98ce7a6a8640 100644 (file)
--- a/action.cc
+++ b/action.cc
@@ -8,17 +8,19 @@
 #include "clockvector.h"
 #include "common.h"
 
+#define ACTION_INITIAL_CLOCK 0
+
 ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, uint64_t value) :
        type(type),
        order(order),
        location(loc),
        value(value),
        reads_from(NULL),
+       seq_number(ACTION_INITIAL_CLOCK),
        cv(NULL)
 {
        Thread *t = thread_current();
        this->tid = t->get_id();
-       this->seq_number = model->get_next_seq_num();
 }
 
 ModelAction::~ModelAction()
@@ -27,31 +29,44 @@ ModelAction::~ModelAction()
                delete cv;
 }
 
-void ModelAction::copy_from_new(ModelAction *newaction) {
-       seq_number=newaction->seq_number;
+void ModelAction::copy_from_new(ModelAction *newaction)
+{
+       seq_number = newaction->seq_number;
+}
+
+void ModelAction::set_seq_number(modelclock_t num)
+{
+       ASSERT(seq_number == ACTION_INITIAL_CLOCK);
+       seq_number = num;
 }
 
-bool ModelAction::is_mutex_op() const {
+bool ModelAction::is_mutex_op() const
+{
        return type == ATOMIC_LOCK || type == ATOMIC_TRYLOCK || type == ATOMIC_UNLOCK;
 }
 
-bool ModelAction::is_lock() const {
+bool ModelAction::is_lock() const
+{
        return type == ATOMIC_LOCK;
 }
 
-bool ModelAction::is_unlock() const {
+bool ModelAction::is_unlock() const
+{
        return type == ATOMIC_UNLOCK;
 }
 
-bool ModelAction::is_trylock() const {
+bool ModelAction::is_trylock() const
+{
        return type == ATOMIC_TRYLOCK;
 }
 
-bool ModelAction::is_success_lock() const {
+bool ModelAction::is_success_lock() const
+{
        return type == ATOMIC_LOCK || (type == ATOMIC_TRYLOCK && value == VALUE_TRYSUCCESS);
 }
 
-bool ModelAction::is_failed_trylock() const {
+bool ModelAction::is_failed_trylock() const
+{
        return (type == ATOMIC_TRYLOCK && value == VALUE_TRYFAILED);
 }
 
@@ -130,8 +145,8 @@ bool ModelAction::same_thread(const ModelAction *act) const
 }
 
 void ModelAction::copy_typeandorder(ModelAction * act) {
-       this->type=act->type;
-       this->order=act->order;
+       this->type = act->type;
+       this->order = act->order;
 }
 
 /** This method changes an existing read part of an RMW action into either:
@@ -268,7 +283,13 @@ bool ModelAction::happens_before(const ModelAction *act) const
        return act->cv->synchronized_since(this);
 }
 
-void ModelAction::print(void) const
+/**
+ * Print nicely-formatted info about this ModelAction
+ *
+ * @param print_cv True if we want to print clock vector data. Might be false,
+ * for instance, in situations where the clock vector might be invalid
+ */
+void ModelAction::print(bool print_cv) const
 {
        const char *type_str, *mo_str;
        switch (this->type) {
@@ -352,7 +373,7 @@ void ModelAction::print(void) const
                else
                        printf(" Rf: ?");
        }
-       if (cv) {
+       if (cv && print_cv) {
                printf("\t");
                cv->print();
        } else

diff --git a/action.h b/action.h
index fecef4dbf3043ac920d5fb09efef85ffb8d6e863..f6fb06236fe0230eb942c38dcc177c081db341bd 100644 (file)
--- a/action.h
+++ b/action.h
@@ -64,7 +64,7 @@ class ModelAction {
 public:
        ModelAction(action_type_t type, memory_order order, void *loc, uint64_t value = VALUE_NONE);
        ~ModelAction();
-       void print(void) const;
+       void print(bool print_cv = true) const;
 
        thread_id_t get_tid() const { return tid; }
        action_type get_type() const { return type; }
@@ -78,6 +78,7 @@ public:
        void set_node(Node *n) { node = n; }
 
        void copy_from_new(ModelAction *newaction);
+       void set_seq_number(modelclock_t num);
        void set_try_lock(bool obtainedlock);
        bool is_mutex_op() const;
        bool is_lock() const;

diff --git a/model.cc b/model.cc
index 0006fd63d66e172336df1296c417a787fe559d2a..4f600a91f5eab4bb65420974e78651f0e53cfcfb 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -191,7 +191,7 @@ bool ModelChecker::next_execution()
        if (isfinalfeasible()) {
                printf("Earliest divergence point since last feasible execution:\n");
                if (earliest_diverge)
-                       earliest_diverge->print();
+                       earliest_diverge->print(false);
                else
                        printf("(Not set)\n");
 
@@ -430,7 +430,7 @@ bool ModelChecker::process_mutex(ModelAction *curr) {
                action_list_t *waiters = lock_waiters_map->get_safe_ptr(curr->get_location());
                //activate all the waiting threads
                for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) {
-                       scheduler->add_thread(get_thread((*rit)->get_tid()));
+                       scheduler->wake(get_thread(*rit));
                }
                waiters->clear();
                break;
@@ -488,26 +488,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);
-                       synchronized = true;
-               }
+               Thread *blocking = (Thread *)curr->get_location();
+               ModelAction *act = get_last_action(blocking->get_id());
+               curr->synchronize_with(act);
+               synchronized = true;
                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);
-                       synchronized = true;
+                       scheduler->wake(get_thread(act));
                }
                th->complete();
                break;
@@ -547,6 +538,8 @@ ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr)
                return newcurr;
        }
 
+       curr->set_seq_number(get_next_seq_num());
+
        newcurr = node_stack->explore_action(curr, scheduler->get_enabled());
        if (newcurr) {
                /* First restore type and order in case of RMW operation */
@@ -577,9 +570,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.
  */
@@ -592,6 +588,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;
@@ -617,9 +619,9 @@ 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);
-               remove_thread(get_current_thread());
+               scheduler->sleep(get_current_thread());
                return get_next_thread(NULL);
        }
 
@@ -701,19 +703,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();

diff --git a/model.h b/model.h
index 6f082c66a71653f7240fcf8102223f60845e870f..d6d6f090392b788b34df5dc91bd6cfcd9cf17079 100644 (file)
--- a/model.h
+++ b/model.h
@@ -78,7 +78,6 @@ public:
 
        thread_id_t get_next_id();
        int get_num_threads();
-       modelclock_t get_next_seq_num();
 
        /** @return The currently executing Thread. */
        Thread * get_current_thread() { return scheduler->get_current_thread(); }
@@ -114,6 +113,8 @@ private:
        int num_feasible_executions;
        bool promises_expired();
 
+       modelclock_t get_next_seq_num();
+
        /**
         * Stores the ModelAction for the current thread action.  Call this
         * immediately before switching from user- to system-context to pass
@@ -152,7 +153,6 @@ private:
        bool w_modification_order(ModelAction *curr);
        bool release_seq_head(const ModelAction *rf, rel_heads_list_t *release_heads) const;
        bool resolve_release_sequences(void *location, work_queue_t *work_queue);
-       void do_complete_join(ModelAction *join);
 
        ModelAction *diverge;
        ModelAction *earliest_diverge;