From: Brian Norris <banorris@uci.edu>
Date: Tue, 10 Apr 2012 22:14:45 +0000 (-0700)
Subject: model: add check_current_action() function
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=ed2579031bea4a2f3fc0adb1c7e979771a589b9c;p=c11tester.git

model: add check_current_action() function

This interface provides a wrapper for all our model checking operations on the
current action (at least, ideally this should work...I might need to work on
this a bit).

For now, we just record the program trace of all atomic/thread actions.
---

diff --git a/model.cc b/model.cc
index 88d5ce32..41dc44d3 100644
--- a/model.cc
+++ b/model.cc
@@ -2,6 +2,7 @@
 
 #include "model.h"
 #include "schedule.h"
+#include "common.h"
 
 ModelChecker *model;
 
@@ -30,6 +31,14 @@ void ModelChecker::add_system_thread(struct thread *t)
 	this->system_thread = t;
 }
 
+void ModelChecker::check_current_action(void)
+{
+	if (this->current_action)
+		this->action_trace.push_back(this->current_action);
+	else
+		DEBUG("trying to push NULL action...\n");
+}
+
 ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, int value)
 {
 	struct thread *t = thread_current();
diff --git a/model.h b/model.h
index 205b8d0b..aa7e9052 100644
--- a/model.h
+++ b/model.h
@@ -1,6 +1,8 @@
 #ifndef __MODEL_H__
 #define __MODEL_H__
 
+#include <list>
+
 #include "schedule.h"
 #include "libthreads.h"
 #include "libatomic.h"
@@ -38,10 +40,12 @@ public:
 	void assign_id(struct thread *t);
 
 	void set_current_action(ModelAction *act) { current_action = act; }
+	void check_current_action(void);
 
 private:
 	int used_thread_id;
 	class ModelAction *current_action;
+	std::list<class ModelAction *> action_trace;
 };
 
 extern ModelChecker *model;