(bug) revert JOIN/LOCK simplification

A test case throws an assertion when these changes are included. Maybe
I'll make a proper fix later, but for now, I mostly revert these.

Revert "model: remove obsolete ModelChecker::do_complete_join()"
This reverts commit cef10a2b49af5da16ffe59c5b9ddd210c668fbac.

Revert "model: unify JOIN- and LOCK-related sleep/wake code"
This reverts commit 620ae95ce4fed006d18a41b6ccfd949d7e77f677.

diff --git a/model.cc b/model.cc
index 38f40e5cd1ee55b47103883fa9677b6ad7ea7e6d..d0dc027150bc629a1df5a839d7c45c9ce1c4d5ee 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -488,17 +488,26 @@ bool ModelChecker::process_thread_action(ModelAction *curr)
                break;
        }
        case THREAD_JOIN: {
-               Thread *blocking = (Thread *)curr->get_location();
-               ModelAction *act = get_last_action(blocking->get_id());
-               curr->synchronize_with(act);
-               updated = true; /* trigger rel-seq checks */
+               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 */
+               }
                break;
        }
        case THREAD_FINISH: {
                Thread *th = get_thread(curr);
                while (!th->wait_list_empty()) {
                        ModelAction *act = th->pop_wait_list();
-                       scheduler->wake(get_thread(act));
+                       Thread *wake = get_thread(act);
+                       scheduler->wake(wake);
+                       do_complete_join(act);
+                       updated = true; /* trigger rel-seq checks */
                }
                th->complete();
                updated = true; /* trigger rel-seq checks */
@@ -571,12 +580,9 @@ ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr)
 }
 
 /**
- * @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.
- *
+ * 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.
  * @param curr is the ModelAction to check whether it is enabled.
  * @return a bool that indicates whether the action is enabled.
  */
@@ -589,12 +595,6 @@ 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;
@@ -620,7 +620,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/join can succeed */
+                * much later, when a lock is actually available to release */
                get_current_thread()->set_pending(curr);
                scheduler->sleep(get_current_thread());
                return get_next_thread(NULL);
@@ -704,6 +704,19 @@ 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 d6d6f090392b788b34df5dc91bd6cfcd9cf17079..a2d33432de948e4bc64b48ca6d7c1c7596f1a20f 100644 (file)
--- a/model.h
+++ b/model.h
@@ -153,6 +153,7 @@ 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;