From: Brian Norris <banorris@uci.edu>
Date: Thu, 10 Jan 2013 01:39:24 +0000 (-0800)
Subject: model: add immediate future value for RMW reordering
X-Git-Tag: oopsla2013~322
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=ed8d4600431acccf43e7ac67ab523fd7486861d0;p=model-checker.git

model: add immediate future value for RMW reordering

When RMW atomicity would otherwise rule an execution infeasible, we may
need to pass a future value back 'immediately,' to allow the
model-checker to effectively reorder the RMW's. For such cases, we don't
wait for all current promises to be resolved.
---

diff --git a/model.cc b/model.cc
index 6453d53..4ccdbce 100644
--- a/model.cc
+++ b/model.cc
@@ -721,7 +721,6 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw)
 				r_status = r_modification_order(curr, reads_from);
 			}
 
-
 			if (!second_part_of_rmw && is_infeasible() && (curr->get_node()->increment_read_from() || curr->get_node()->increment_future_value())) {
 				mo_graph->rollbackChanges();
 				priv->too_many_reads = false;
@@ -1811,10 +1810,10 @@ bool ModelChecker::w_modification_order(ModelAction *curr)
 
 				 */
 				if (thin_air_constraint_may_allow(curr, act)) {
-					if (!is_infeasible() ||
-							(curr->is_rmw() && act->is_rmw() && curr->get_reads_from() == act->get_reads_from() && !is_infeasible_ignoreRMW())) {
+					if (!is_infeasible())
 						futurevalues->push_back(PendingFutureValue(curr, act));
-					}
+					else if (curr->is_rmw() && act->is_rmw() && curr->get_reads_from() && curr->get_reads_from() == act->get_reads_from())
+						add_future_value(curr, act);
 				}
 			}
 		}