execution: bugfix - resolved promises should propagate synchronization
authorBrian Norris <banorris@uci.edu>
Wed, 8 May 2013 17:09:52 +0000 (10:09 -0700)
committerBrian Norris <banorris@uci.edu>
Wed, 8 May 2013 17:09:52 +0000 (10:09 -0700)
A new write ModelAction may resolve a Promise, completing a release
sequence and updating the read's clock vector. This update should be
propagated to any ModelAction later in the execution order which had
previously "happened after" the read.

execution.cc
execution.h

index 4e15427..4496b9c 100644 (file)
@@ -817,9 +817,10 @@ void ModelExecution::add_future_value(const ModelAction *writer, ModelAction *re
 /**
  * Process a write ModelAction
  * @param curr The ModelAction to process
 /**
  * Process a write ModelAction
  * @param curr The ModelAction to process
+ * @param work The work queue, for adding fixup work
  * @return True if the mo_graph was updated or promises were resolved
  */
  * @return True if the mo_graph was updated or promises were resolved
  */
-bool ModelExecution::process_write(ModelAction *curr)
+bool ModelExecution::process_write(ModelAction *curr, work_queue_t *work)
 {
        /* Readers to which we may send our future value */
        ModelVector<ModelAction *> send_fv;
 {
        /* Readers to which we may send our future value */
        ModelVector<ModelAction *> send_fv;
@@ -832,7 +833,7 @@ bool ModelExecution::process_write(ModelAction *curr)
 
        if (promise) {
                earliest_promise_reader = promise->get_reader(0);
 
        if (promise) {
                earliest_promise_reader = promise->get_reader(0);
-               updated_promises = resolve_promise(curr, promise);
+               updated_promises = resolve_promise(curr, promise, work);
        } else
                earliest_promise_reader = NULL;
 
        } else
                earliest_promise_reader = NULL;
 
@@ -1272,7 +1273,7 @@ ModelAction * ModelExecution::check_current_action(ModelAction *curr)
                        if (act->is_read() && !second_part_of_rmw && process_read(act))
                                update = true;
 
                        if (act->is_read() && !second_part_of_rmw && process_read(act))
                                update = true;
 
-                       if (act->is_write() && process_write(act))
+                       if (act->is_write() && process_write(act, &work_queue))
                                update = true;
 
                        if (act->is_fence() && process_fence(act))
                                update = true;
 
                        if (act->is_fence() && process_fence(act))
@@ -2333,15 +2334,20 @@ Promise * ModelExecution::pop_promise_to_resolve(const ModelAction *curr)
  * Resolve a Promise with a current write.
  * @param write The ModelAction that is fulfilling Promises
  * @param promise The Promise to resolve
  * Resolve a Promise with a current write.
  * @param write The ModelAction that is fulfilling Promises
  * @param promise The Promise to resolve
+ * @param work The work queue, for adding new fixup work
  * @return True if the Promise was successfully resolved; false otherwise
  */
  * @return True if the Promise was successfully resolved; false otherwise
  */
-bool ModelExecution::resolve_promise(ModelAction *write, Promise *promise)
+bool ModelExecution::resolve_promise(ModelAction *write, Promise *promise,
+               work_queue_t *work)
 {
        ModelVector<ModelAction *> actions_to_check;
 
        for (unsigned int i = 0; i < promise->get_num_readers(); i++) {
                ModelAction *read = promise->get_reader(i);
 {
        ModelVector<ModelAction *> actions_to_check;
 
        for (unsigned int i = 0; i < promise->get_num_readers(); i++) {
                ModelAction *read = promise->get_reader(i);
-               read_from(read, write);
+               if (read_from(read, write)) {
+                       /* Propagate the changed clock vector */
+                       propagate_clockvector(read, work);
+               }
                actions_to_check.push_back(read);
        }
        /* Make sure the promise's value matches the write's value */
                actions_to_check.push_back(read);
        }
        /* Make sure the promise's value matches the write's value */
index bb4ebb0..ab4df36 100644 (file)
@@ -141,7 +141,7 @@ private:
        ModelAction * check_current_action(ModelAction *curr);
        bool initialize_curr_action(ModelAction **curr);
        bool process_read(ModelAction *curr);
        ModelAction * check_current_action(ModelAction *curr);
        bool initialize_curr_action(ModelAction **curr);
        bool process_read(ModelAction *curr);
-       bool process_write(ModelAction *curr);
+       bool process_write(ModelAction *curr, work_queue_t *work);
        bool process_fence(ModelAction *curr);
        bool process_mutex(ModelAction *curr);
        bool process_thread_action(ModelAction *curr);
        bool process_fence(ModelAction *curr);
        bool process_mutex(ModelAction *curr);
        bool process_thread_action(ModelAction *curr);
@@ -160,7 +160,8 @@ private:
        void set_backtracking(ModelAction *act);
        bool set_latest_backtrack(ModelAction *act);
        Promise * pop_promise_to_resolve(const ModelAction *curr);
        void set_backtracking(ModelAction *act);
        bool set_latest_backtrack(ModelAction *act);
        Promise * pop_promise_to_resolve(const ModelAction *curr);
-       bool resolve_promise(ModelAction *curr, Promise *promise);
+       bool resolve_promise(ModelAction *curr, Promise *promise,
+                       work_queue_t *work);
        void compute_promises(ModelAction *curr);
        void compute_relseq_breakwrites(ModelAction *curr);
 
        void compute_promises(ModelAction *curr);
        void compute_relseq_breakwrites(ModelAction *curr);