Merge branch 'demsky'
authorBrian Norris <banorris@uci.edu>
Wed, 12 Sep 2012 00:52:02 +0000 (17:52 -0700)
committerBrian Norris <banorris@uci.edu>
Wed, 12 Sep 2012 00:56:14 +0000 (17:56 -0700)
Branch cleaned up by Brian Norris

1  2 
model.cc
model.h

diff --cc model.cc
index ba239b913b41a02ff401380ef65dfe743df76a58,6f144abab044d5d6a23880a9744e2b95ee5b3f24..3e54a001a4541b8d5acada69e76c189ff5e82b36
+++ b/model.cc
@@@ -329,40 -356,26 +374,30 @@@ Thread * ModelChecker::check_current_ac
                        scheduler->wake(wake);
                }
                th->complete();
 +              break;
        }
 -
 -      /* Deal with new thread */
 -      if (curr->get_type() == THREAD_START)
 +      case THREAD_START: {
                check_promises(NULL, curr->get_cv());
 +              break;
 +      }
 +      default:
 +              break;
 +      }
  
-       /* Assign reads_from values */
        Thread *th = get_thread(curr->get_tid());
-       uint64_t value = VALUE_NONE;
        bool updated = false;
        if (curr->is_read()) {
-               const ModelAction *reads_from = curr->get_node()->get_read_from();
-               if (reads_from != NULL) {
-                       value = reads_from->get_value();
-                       /* Assign reads_from, perform release/acquire synchronization */
-                       curr->read_from(reads_from);
-                       if (r_modification_order(curr,reads_from))
-                               updated = true;
-               } else {
-                       /* Read from future value */
-                       value = curr->get_node()->get_future_value();
-                       curr->read_from(NULL);
-                       Promise *valuepromise = new Promise(curr, value);
-                       promises->push_back(valuepromise);
-               }
-       } else if (curr->is_write()) {
-               if (w_modification_order(curr))
-                       updated = true;
-               if (resolve_promises(curr))
-                       updated = true;
+               updated=process_read(curr, th, second_part_of_rmw);
+       }
+       if (curr->is_write()) {
+               bool updated_mod_order=w_modification_order(curr);
+               bool updated_promises=resolve_promises(curr);
+               updated=updated_mod_order|updated_promises;
+               mo_graph->commitChanges();
+               th->set_return_value(VALUE_NONE);
        }
  
        if (updated)
diff --cc model.h
index 1b6bb10a285e4046e4b9bbe727526abf1849f071,d73e4574ec0fb8b860a2c89e1c87827fd4c65cbc..c3e5830211c9276ec7b5004504fbb9472df32069
+++ b/model.h
@@@ -103,9 -105,10 +105,10 @@@ private
  
        bool take_step();
  
+       void check_recency(ModelAction *curr, bool already_added);
        ModelAction * get_last_conflict(ModelAction *act);
        void set_backtracking(ModelAction *act);
 -      Thread * get_next_replay_thread();
 +      Thread * get_next_thread(ModelAction *curr);
        ModelAction * get_next_backtrack();
        void reset_to_initial_state();
        bool resolve_promises(ModelAction *curr);