From: Brian Norris <banorris@uci.edu>
Date: Fri, 8 Feb 2013 23:23:41 +0000 (-0800)
Subject: model: rename according to the comments
X-Git-Tag: oopsla2013~271
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=e67f2f90b92e9176dc3f574095ba05a062c87f72;p=model-checker.git

model: rename according to the comments

The documentation mentions 'pread' and 'pwrite'. Those names aren't
actually used in the code, though, so change that.
---

diff --git a/model.cc b/model.cc
index 3d89dc3..3a5a4ba 100644
--- a/model.cc
+++ b/model.cc
@@ -2403,21 +2403,21 @@ void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write,
 {
 	for (unsigned int i = 0; i < promises->size(); i++) {
 		Promise *promise = (*promises)[i];
-		const ModelAction *act = promise->get_action();
+		const ModelAction *pread = promise->get_action();
 
 		// Is this promise on the same location?
-		if (!act->same_var(write))
+		if (!pread->same_var(write))
 			continue;
 
-		// same thread as the promise
-		if (act->get_tid() == tid) {
+		// same thread as pread
+		if (pread->get_tid() == tid) {
 			// make sure that the reader of this write happens after the promise
-			if ((read == NULL) || (promise->get_action()->happens_before(read))) {
+			if ((read == NULL) || (pread->happens_before(read))) {
 				// do we have a pwrite for the promise, if not, set it
 				if (promise->get_write() == NULL) {
 					promise->set_write(write);
-					// The pwrite cannot happen before the promise
-					if (write->happens_before(act) && (write != act)) {
+					// The pwrite cannot happen before pread
+					if (write->happens_before(pread) && (write != pread)) {
 						priv->failed_promise = true;
 						return;
 					}
@@ -2434,7 +2434,8 @@ void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write,
 		if (!promise->thread_is_available(tid))
 			continue;
 
-		if (promise->get_write() && mo_graph->checkReachable(promise->get_write(), write)) {
+		const ModelAction *pwrite = promise->get_write();
+		if (pwrite && mo_graph->checkReachable(pwrite, write)) {
 			if (promise->eliminate_thread(tid)) {
 				priv->failed_promise = true;
 				return;