projects
/
model-checker.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
local commit... bug that prunes too many executions
[model-checker.git]
/
model.h
diff --git
a/model.h
b/model.h
index d8dce07cbdf56423e04e2378d2e0715d18025559..dfc8e36c2be5e775ec82dab1e81a8adcfdaa2697 100644
(file)
--- a/
model.h
+++ b/
model.h
@@
-49,7
+49,7
@@
struct PendingFutureValue {
*/
struct model_snapshot_members {
ModelAction *current_action;
*/
struct model_snapshot_members {
ModelAction *current_action;
- int next_thread_id;
+
unsigned
int next_thread_id;
modelclock_t used_sequence_numbers;
Thread *nextThread;
ModelAction *next_backtrack;
modelclock_t used_sequence_numbers;
Thread *nextThread;
ModelAction *next_backtrack;
@@
-76,7
+76,7
@@
public:
Thread * get_thread(ModelAction *act) const;
thread_id_t get_next_id();
Thread * get_thread(ModelAction *act) const;
thread_id_t get_next_id();
- int get_num_threads();
+
unsigned
int get_num_threads();
Thread * get_current_thread();
int switch_to_master(ModelAction *act);
Thread * get_current_thread();
int switch_to_master(ModelAction *act);
@@
-86,7
+86,8
@@
public:
bool isfeasible();
bool isfeasibleotherthanRMW();
bool isfinalfeasible();
bool isfeasible();
bool isfeasibleotherthanRMW();
bool isfinalfeasible();
- void check_promises(ClockVector *old_cv, ClockVector * merge_cv);
+ void mo_check_promises(thread_id_t tid, const ModelAction *write);
+ void check_promises(thread_id_t tid, ClockVector *old_cv, ClockVector * merge_cv);
void get_release_seq_heads(ModelAction *act, rel_heads_list_t *release_heads);
void finish_execution();
bool isfeasibleprefix();
void get_release_seq_heads(ModelAction *act, rel_heads_list_t *release_heads);
void finish_execution();
bool isfeasibleprefix();
@@
-97,6
+98,7
@@
public:
void set_bad_synchronization() { bad_synchronization = true; }
const model_params params;
void set_bad_synchronization() { bad_synchronization = true; }
const model_params params;
+ Scheduler * get_scheduler() { return scheduler;}
MEMALLOC
private:
MEMALLOC
private: