From ed2579031bea4a2f3fc0adb1c7e979771a589b9c Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Tue, 10 Apr 2012 15:14:45 -0700 Subject: [PATCH] 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. --- model.cc | 9 +++++++++ model.h | 4 ++++ 2 files changed, 13 insertions(+) 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 + #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 action_trace; }; extern ModelChecker *model; -- 2.34.1