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 88d5ce32e21195d7106c291220d4eb2af7bb80a0..41dc44d34a8a0626e1a82de4bb59023e88aaa1e3 100644 (file)
--- 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 205b8d0bd236989a6131efa45cdefba0f7cc1096..aa7e9052c8dafcddec751fd4f237c6ecd4dd4945 100644 (file)
--- 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;