model.h

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