model.h

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