projects
/
model-checker.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
rename threads_internal.h -> threads.h
[model-checker.git]
/
model.h
diff --git
a/model.h
b/model.h
index d3229b296526db6ee54c07d0055e22a336011b5a..cd922dff7f945d1808b3e44b91ec433971ab71c2 100644
(file)
--- a/
model.h
+++ b/
model.h
@@
-1,9
+1,13
@@
#ifndef __MODEL_H__
#define __MODEL_H__
#ifndef __MODEL_H__
#define __MODEL_H__
+#include <list>
+#include <map>
+
#include "schedule.h"
#include "libthreads.h"
#include "libatomic.h"
#include "schedule.h"
#include "libthreads.h"
#include "libatomic.h"
+#include "threads.h"
#define VALUE_NONE -1
#define VALUE_NONE -1
@@
-32,15
+36,29
@@
public:
ModelChecker();
~ModelChecker();
class Scheduler *scheduler;
ModelChecker();
~ModelChecker();
class Scheduler *scheduler;
- struct thread *system_thread;
+ Thread *system_thread;
+
+ void add_system_thread(Thread *t);
+
+ void set_current_action(ModelAction *act) { current_action = act; }
+ void check_current_action(void);
+ void print_trace(void);
-
void add_system_thread(struct t
hread *t);
- void assign_id(struct thread *t);
+
int add_thread(T
hread *t);
+ Thread *get_thread(thread_id_t tid) { return thread_map[tid]; }
+ void assign_id(Thread *t);
+
+ int switch_to_master(ModelAction *act);
private:
int used_thread_id;
private:
int used_thread_id;
+ class ModelAction *current_action;
+ std::list<class ModelAction *> action_trace;
+ std::map<thread_id_t, class Thread *> thread_map;
};
extern ModelChecker *model;
};
extern ModelChecker *model;
+int thread_switch_to_master(ModelAction *act);
+
#endif /* __MODEL_H__ */
#endif /* __MODEL_H__ */