From: Brian Norris <banorris@uci.edu>
Date: Tue, 16 Apr 2013 02:01:41 +0000 (-0700)
Subject: model: cleanup a few more interfaces
X-Git-Tag: oopsla2013~67^2~6
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=92dd847e38280a3bb0ec93781c47173a3848f1d7

model: cleanup a few more interfaces

These public interfaces are no longer presentin ModelChecker.
---

diff --git a/datarace.cc b/datarace.cc
index 5174c04..af70041 100644
--- a/datarace.cc
+++ b/datarace.cc
@@ -7,12 +7,17 @@
 #include "clockvector.h"
 #include "config.h"
 #include "action.h"
+#include "execution.h"
 
 static struct ShadowTable *root;
 SnapVector<struct DataRace *> unrealizedraces;
 static void *memory_base;
 static void *memory_top;
 
+static const ModelExecution * get_execution()
+{
+	return model->get_execution();
+}
 
 /** This function initialized the data race detector. */
 void initRaceDetector()
@@ -123,7 +128,7 @@ static void reportDataRace(thread_id_t oldthread, modelclock_t oldclock, bool is
  */
 bool checkDataRaces()
 {
-	if (model->isfeasibleprefix()) {
+	if (get_execution()->isfeasibleprefix()) {
 		bool race_asserted = false;
 		/* Prune the non-racing unrealized dataraces */
 		for (unsigned i = 0; i < unrealizedraces.size(); i++) {
@@ -180,7 +185,7 @@ void fullRaceCheckWrite(thread_id_t thread, void *location, uint64_t *shadow, Cl
 
 		if (clock_may_race(currClock, thread, readClock, readThread)) {
 			/* We have a datarace */
-			reportDataRace(readThread, readClock, false, model->get_parent_action(thread), true, location);
+			reportDataRace(readThread, readClock, false, get_execution()->get_parent_action(thread), true, location);
 		}
 	}
 
@@ -191,7 +196,7 @@ void fullRaceCheckWrite(thread_id_t thread, void *location, uint64_t *shadow, Cl
 
 	if (clock_may_race(currClock, thread, writeClock, writeThread)) {
 		/* We have a datarace */
-		reportDataRace(writeThread, writeClock, true, model->get_parent_action(thread), true, location);
+		reportDataRace(writeThread, writeClock, true, get_execution()->get_parent_action(thread), true, location);
 	}
 
 	record->numReads = 0;
@@ -205,7 +210,7 @@ void raceCheckWrite(thread_id_t thread, void *location)
 {
 	uint64_t *shadow = lookupAddressEntry(location);
 	uint64_t shadowval = *shadow;
-	ClockVector *currClock = model->get_cv(thread);
+	ClockVector *currClock = get_execution()->get_cv(thread);
 
 	/* Do full record */
 	if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
@@ -230,7 +235,7 @@ void raceCheckWrite(thread_id_t thread, void *location)
 
 	if (clock_may_race(currClock, thread, readClock, readThread)) {
 		/* We have a datarace */
-		reportDataRace(readThread, readClock, false, model->get_parent_action(thread), true, location);
+		reportDataRace(readThread, readClock, false, get_execution()->get_parent_action(thread), true, location);
 	}
 
 	/* Check for datarace against last write. */
@@ -240,7 +245,7 @@ void raceCheckWrite(thread_id_t thread, void *location)
 
 	if (clock_may_race(currClock, thread, writeClock, writeThread)) {
 		/* We have a datarace */
-		reportDataRace(writeThread, writeClock, true, model->get_parent_action(thread), true, location);
+		reportDataRace(writeThread, writeClock, true, get_execution()->get_parent_action(thread), true, location);
 	}
 	*shadow = ENCODEOP(0, 0, threadid, ourClock);
 }
@@ -257,7 +262,7 @@ void fullRaceCheckRead(thread_id_t thread, const void *location, uint64_t *shado
 
 	if (clock_may_race(currClock, thread, writeClock, writeThread)) {
 		/* We have a datarace */
-		reportDataRace(writeThread, writeClock, true, model->get_parent_action(thread), false, location);
+		reportDataRace(writeThread, writeClock, true, get_execution()->get_parent_action(thread), false, location);
 	}
 
 	/* Shorten vector when possible */
@@ -309,7 +314,7 @@ void raceCheckRead(thread_id_t thread, const void *location)
 {
 	uint64_t *shadow = lookupAddressEntry(location);
 	uint64_t shadowval = *shadow;
-	ClockVector *currClock = model->get_cv(thread);
+	ClockVector *currClock = get_execution()->get_cv(thread);
 
 	/* Do full record */
 	if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
@@ -334,7 +339,7 @@ void raceCheckRead(thread_id_t thread, const void *location)
 
 	if (clock_may_race(currClock, thread, writeClock, writeThread)) {
 		/* We have a datarace */
-		reportDataRace(writeThread, writeClock, true, model->get_parent_action(thread), false, location);
+		reportDataRace(writeThread, writeClock, true, get_execution()->get_parent_action(thread), false, location);
 	}
 
 	modelclock_t readClock = READVECTOR(shadowval);
diff --git a/model.h b/model.h
index 3f9e6c2..dd5df93 100644
--- a/model.h
+++ b/model.h
@@ -65,10 +65,7 @@ public:
 
 	void switch_from_master(Thread *thread);
 	uint64_t switch_to_master(ModelAction *act);
-	ClockVector * get_cv(thread_id_t tid) const;
-	ModelAction * get_parent_action(thread_id_t tid) const;
 	void check_promises_thread_disabled();
-	bool isfeasibleprefix() const;
 
 	bool assert_bug(const char *msg, ...);
 	void assert_user_bug(const char *msg);
diff --git a/mutex.cc b/mutex.cc
index da3184e..d5ec40f 100644
--- a/mutex.cc
+++ b/mutex.cc
@@ -1,6 +1,7 @@
 #include <mutex>
 
 #include "model.h"
+#include "execution.h"
 #include "threads-model.h"
 #include "clockvector.h"
 #include "action.h"
@@ -12,7 +13,7 @@ mutex::mutex()
 	state.locked = NULL;
 	thread_id_t tid = thread_current()->get_id();
 	state.alloc_tid = tid;
-	state.alloc_clock = model->get_cv(tid)->getClock(tid);
+	state.alloc_clock = model->get_execution()->get_cv(tid)->getClock(tid);
 }
 	
 void mutex::lock()