model: bugfix - release sequences - handle Thread completion

[c11tester.git] / model.cc

diff --git a/model.cc b/model.cc
index d082d8358b8d2a1da69f94cec113bc6982335ceb..a9d94776cc3ec090d821caad3133441f2d2e2bcc 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -246,8 +246,6 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
  *
  * @param the ModelAction to find backtracking points for.
  */
-
-
 void ModelChecker::set_backtracking(ModelAction *act)
 {
        Thread *t = get_thread(act);
@@ -445,6 +443,63 @@ bool ModelChecker::process_write(ModelAction *curr)
        return updated_mod_order || updated_promises;
 }
 
+/**
+ * @brief Process the current action for thread-related activity
+ *
+ * Performs current-action processing for a THREAD_* ModelAction. Proccesses
+ * may include setting Thread status, completing THREAD_FINISH/THREAD_JOIN
+ * synchronization, etc.  This function is a no-op for non-THREAD actions
+ * (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.)
+ *
+ * @param curr The current action
+ * @return True if synchronization was updated
+ */
+bool ModelChecker::process_thread_action(ModelAction *curr)
+{
+       bool synchronized = false;
+
+       switch (curr->get_type()) {
+       case THREAD_CREATE: {
+               Thread *th = (Thread *)curr->get_location();
+               th->set_creation(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;
+               }
+               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;
+               }
+               th->complete();
+               break;
+       }
+       case THREAD_START: {
+               check_promises(NULL, curr->get_cv());
+               break;
+       }
+       default:
+               break;
+       }
+
+       return synchronized;
+}
+
 /**
  * Initialize the current action by performing one or more of the following
  * actions, as appropriate: merging RMWR and RMWC/RMW actions, stepping forward
@@ -502,7 +557,6 @@ ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr)
  * @param curr is the ModelAction to check whether it is enabled.
  * @return a bool that indicates whether the action is enabled.
  */
-
 bool ModelChecker::check_action_enabled(ModelAction *curr) {
        if (curr->is_lock()) {
                std::mutex * lock = (std::mutex *)curr->get_location();
@@ -536,8 +590,8 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
        bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
 
        if (!check_action_enabled(curr)) {
-               //we'll make the execution look like we chose to run this action
-               //much later...when a lock is actually available to relese
+               /* Make the execution look like we chose to run this action
+                * much later, when a lock is actually available to release */
                get_current_thread()->set_pending(curr);
                remove_thread(get_current_thread());
                return get_next_thread(NULL);
@@ -554,44 +608,6 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
                build_reads_from_past(curr);
        curr = newcurr;
 
-       /* Thread specific actions */
-       switch (curr->get_type()) {
-       case THREAD_CREATE: {
-               Thread *th = (Thread *)curr->get_location();
-               th->set_creation(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);
-               }
-               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);
-               }
-               th->complete();
-               break;
-       }
-       case THREAD_START: {
-               check_promises(NULL, curr->get_cv());
-               break;
-       }
-       default:
-               break;
-       }
-
        work_queue_t work_queue(1, CheckCurrWorkEntry(curr));
 
        while (!work_queue.empty()) {
@@ -602,6 +618,9 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
                case WORK_CHECK_CURR_ACTION: {
                        ModelAction *act = work.action;
                        bool updated = false;
+
+                       process_thread_action(curr);
+
                        if (act->is_read() && process_read(act, second_part_of_rmw))
                                updated = true;
 
@@ -899,7 +918,6 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf
  * @param rf is the write ModelAction that curr reads from.
  *
  */
-
 void ModelChecker::post_r_modification_order(ModelAction *curr, const ModelAction *rf)
 {
        std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
@@ -1039,7 +1057,6 @@ bool ModelChecker::w_modification_order(ModelAction *curr)
 /** Arbitrary reads from the future are not allowed.  Section 29.3
  * part 9 places some constraints.  This method checks one result of constraint
  * constraint.  Others require compiler support. */
-
 bool ModelChecker::thin_air_constraint_may_allow(const ModelAction * writer, const ModelAction *reader) {
        if (!writer->is_rmw())
                return true;
@@ -1144,7 +1161,8 @@ bool ModelChecker::release_seq_head(const ModelAction *rf, rel_heads_list_t *rel
                bool future_ordered = false;
 
                ModelAction *last = get_last_action(int_to_id(i));
-               if (last && rf->happens_before(last))
+               if (last && (rf->happens_before(last) ||
+                               last->get_type() == THREAD_FINISH))
                        future_ordered = true;
 
                for (rit = list->rbegin(); rit != list->rend(); rit++) {
@@ -1563,7 +1581,6 @@ void ModelChecker::add_thread(Thread *t)
  * Removes a thread from the scheduler. 
  * @param the thread to remove.
  */
-
 void ModelChecker::remove_thread(Thread *t)
 {
        scheduler->remove_thread(t);