model: bugfix - iterator naming conflict

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index a9d94776cc3ec090d821caad3133441f2d2e2bcc..fdefcc2bcf390dd4a2615a411920466a8f901022 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -374,8 +374,10 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw)
  *
  * The unlock operation has to re-enable all of the threads that are
  * waiting on the lock.
+ *
+ * @return True if synchronization was updated; false otherwise
  */
-void ModelChecker::process_mutex(ModelAction *curr) {
+bool ModelChecker::process_mutex(ModelAction *curr) {
        std::mutex *mutex = (std::mutex *)curr->get_location();
        struct std::mutex_state *state = mutex->get_state();
        switch (curr->get_type()) {
@@ -397,8 +399,10 @@ void ModelChecker::process_mutex(ModelAction *curr) {
                state->islocked = true;
                ModelAction *unlock = get_last_unlock(curr);
                //synchronize with the previous unlock statement
-               if (unlock != NULL)
+               if (unlock != NULL) {
                        curr->synchronize_with(unlock);
+                       return true;
+               }
                break;
        }
        case ATOMIC_UNLOCK: {
@@ -416,6 +420,7 @@ void ModelChecker::process_mutex(ModelAction *curr) {
        default:
                ASSERT(0);
        }
+       return false;
 }
 
 /**
@@ -608,6 +613,7 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
                build_reads_from_past(curr);
        curr = newcurr;
 
+       /* Initialize work_queue with the "current action" work */
        work_queue_t work_queue(1, CheckCurrWorkEntry(curr));
 
        while (!work_queue.empty()) {
@@ -617,20 +623,24 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
                switch (work.type) {
                case WORK_CHECK_CURR_ACTION: {
                        ModelAction *act = work.action;
-                       bool updated = false;
+                       bool update = false; /* update this location's release seq's */
+                       bool update_all = false; /* update all release seq's */
 
-                       process_thread_action(curr);
+                       if (process_thread_action(curr))
+                               update_all = true;
 
                        if (act->is_read() && process_read(act, second_part_of_rmw))
-                               updated = true;
+                               update = true;
 
                        if (act->is_write() && process_write(act))
-                               updated = true;
+                               update = true;
 
-                       if (act->is_mutex_op())
-                               process_mutex(act);
+                       if (act->is_mutex_op() && process_mutex(act))
+                               update_all = true;
 
-                       if (updated)
+                       if (update_all)
+                               work_queue.push_back(CheckRelSeqWorkEntry(NULL));
+                       else if (update)
                                work_queue.push_back(CheckRelSeqWorkEntry(act->get_location()));
                        break;
                }
@@ -1269,9 +1279,9 @@ bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_
                        work_queue->push_back(MOEdgeWorkEntry(act));
 
                        /* propagate synchronization to later actions */
-                       action_list_t::reverse_iterator it = action_trace->rbegin();
-                       for (; (*it) != act; it++) {
-                               ModelAction *propagate = *it;
+                       action_list_t::reverse_iterator rit = action_trace->rbegin();
+                       for (; (*rit) != act; rit++) {
+                               ModelAction *propagate = *rit;
                                if (act->happens_before(propagate)) {
                                        propagate->synchronize_with(act);
                                        /* Re-check 'propagate' for mo_graph edges */