model.h

   1 #ifndef __MODEL_H__
   2 #define __MODEL_H__
   3
   4 #include <list>
   5 #include <map>
   6
   7 #include "schedule.h"
   8 #include "libthreads.h"
   9 #include "libatomic.h"
  10 #include "threads.h"
  11 #include "tree.h"
  12
  13 #define VALUE_NONE -1
  14
  15 typedef enum action_type {
  16         THREAD_CREATE,
  17         THREAD_YIELD,
  18         THREAD_JOIN,
  19         ATOMIC_READ,
  20         ATOMIC_WRITE
  21 } action_type_t;
  22
  23 class ModelAction {
  24 public:
  25         ModelAction(action_type_t type, memory_order order, void *loc, int value);
  26         void print(void);
  27 private:
  28         action_type type;
  29         memory_order order;
  30         void *location;
  31         thread_id_t tid;
  32         int value;
  33 };
  34
  35 class ModelChecker {
  36 public:
  37         ModelChecker();
  38         ~ModelChecker();
  39         class Scheduler *scheduler;
  40         Thread *system_thread;
  41
  42         void add_system_thread(Thread *t);
  43
  44         void set_current_action(ModelAction *act) { current_action = act; }
  45         void check_current_action(void);
  46         void print_trace(void);
  47
  48         int add_thread(Thread *t);
  49         Thread *get_thread(thread_id_t tid) { return thread_map[tid]; }
  50
  51         void assign_id(Thread *t);
  52
  53         int switch_to_master(ModelAction *act);
  54 private:
  55         int used_thread_id;
  56         class ModelAction *current_action;
  57         std::list<class ModelAction *> action_trace;
  58         std::map<thread_id_t, class Thread *> thread_map;
  59         class TreeNode *rootNode, *currentNode;
  60 };
  61
  62 extern ModelChecker *model;
  63
  64 int thread_switch_to_master(ModelAction *act);
  65
  66 #endif /* __MODEL_H__ */