From: Brian Norris Date: Mon, 30 Apr 2012 07:36:33 +0000 (-0700) Subject: split header out to action.h X-Git-Tag: pldi2013~481 X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;ds=sidebyside;h=996d51da9229031b9d7841c2f3d3b7629db2cba9;p=model-checker.git split header out to action.h --- diff --git a/Makefile b/Makefile index 1f91c5d..4a5360d 100644 --- a/Makefile +++ b/Makefile @@ -10,7 +10,7 @@ USER_H=libthreads.h libatomic.h MODEL_CC=libthreads.cc schedule.cc libatomic.cc model.cc malloc.c threads.cc tree.cc librace.cc MODEL_O=libthreads.o schedule.o libatomic.o model.o malloc.o threads.o tree.o librace.o -MODEL_H=libthreads.h schedule.h common.h libatomic.h model.h threads.h tree.h librace.h +MODEL_H=libthreads.h schedule.h common.h libatomic.h model.h threads.h tree.h librace.h action.h CPPFLAGS=-Wall -g LDFLAGS=-ldl diff --git a/action.h b/action.h new file mode 100644 index 0000000..f9f0c41 --- /dev/null +++ b/action.h @@ -0,0 +1,54 @@ +#ifndef __ACTION_H__ +#define __ACTION_H__ + +#include + +#include "libthreads.h" +#include "libatomic.h" +#include "threads.h" + +#define VALUE_NONE -1 + +typedef enum action_type { + THREAD_CREATE, + THREAD_YIELD, + THREAD_JOIN, + ATOMIC_READ, + ATOMIC_WRITE +} action_type_t; + +/* Forward declaration (tree.h) */ +class TreeNode; + +class ModelAction { +public: + ModelAction(action_type_t type, memory_order order, void *loc, int value); + void print(void); + + thread_id_t get_tid() { return tid; } + action_type get_type() { return type; } + memory_order get_mo() { return order; } + void * get_location() { return location; } + + TreeNode * get_node() { return node; } + void set_node(TreeNode *n) { node = n; } + + bool is_read(); + bool is_write(); + bool is_acquire(); + bool is_release(); + bool same_var(ModelAction *act); + bool same_thread(ModelAction *act); + bool is_dependent(ModelAction *act); +private: + action_type type; + memory_order order; + void *location; + thread_id_t tid; + int value; + TreeNode *node; +}; + +typedef std::list action_list_t; + +#endif /* __ACTION_H__ */ diff --git a/model.cc b/model.cc index 84b296e..f447c1d 100644 --- a/model.cc +++ b/model.cc @@ -1,6 +1,8 @@ #include #include "model.h" +#include "action.h" +#include "tree.h" #include "schedule.h" #include "common.h" diff --git a/model.h b/model.h index d04fa62..83db4d8 100644 --- a/model.h +++ b/model.h @@ -10,48 +10,10 @@ #include "libthreads.h" #include "libatomic.h" #include "threads.h" -#include "tree.h" +#include "action.h" -#define VALUE_NONE -1 - -typedef enum action_type { - THREAD_CREATE, - THREAD_YIELD, - THREAD_JOIN, - ATOMIC_READ, - ATOMIC_WRITE -} action_type_t; - -typedef std::list action_list_t; - -class ModelAction { -public: - ModelAction(action_type_t type, memory_order order, void *loc, int value); - void print(void); - - thread_id_t get_tid() { return tid; } - action_type get_type() { return type; } - memory_order get_mo() { return order; } - void * get_location() { return location; } - - TreeNode * get_node() { return node; } - void set_node(TreeNode *n) { node = n; } - - bool is_read(); - bool is_write(); - bool is_acquire(); - bool is_release(); - bool same_var(ModelAction *act); - bool same_thread(ModelAction *act); - bool is_dependent(ModelAction *act); -private: - action_type type; - memory_order order; - void *location; - thread_id_t tid; - int value; - TreeNode *node; -}; +/* Forward declaration */ +class TreeNode; class Backtrack { public: