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