model: THREAD_JOIN synchronizes with THREAD_FINISH
authorBrian Norris <banorris@uci.edu>
Wed, 19 Sep 2012 01:45:17 +0000 (18:45 -0700)
committerBrian Norris <banorris@uci.edu>
Wed, 19 Sep 2012 01:45:17 +0000 (18:45 -0700)
model.cc
model.h

index e41bc4e..2b295de 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -423,6 +423,8 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
                if (!blocking->is_complete()) {
                        blocking->push_wait_list(curr);
                        scheduler->sleep(waiting);
+               } else {
+                       do_complete_join(curr);
                }
                break;
        }
@@ -432,6 +434,7 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
                        ModelAction *act = th->pop_wait_list();
                        Thread *wake = get_thread(act);
                        scheduler->wake(wake);
+                       do_complete_join(act);
                }
                th->complete();
                break;
@@ -498,6 +501,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 b8a4859..b2b312f 100644 (file)
--- a/model.h
+++ b/model.h
@@ -139,6 +139,7 @@ private:
        bool release_seq_head(const ModelAction *rf,
                        std::vector< const ModelAction *, MyAlloc<const ModelAction *> > *release_heads) const;
        bool resolve_release_sequences(void *location, work_queue_t *work_queue);
+       void do_complete_join(ModelAction *join);
 
        ModelAction *diverge;