projects
/
model-checker.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
threads: allocate on user's snapshotting heap
[model-checker.git]
/
model.h
diff --git
a/model.h
b/model.h
index 1bd32a1fffcb926449f2b5fc7a11f7d74410cf34..c99e0f8b424ddbe8079593713e498e53fe6fb80e 100644
(file)
--- a/
model.h
+++ b/
model.h
@@
-39,8
+39,7
@@
struct model_params {
};
struct PendingFutureValue {
};
struct PendingFutureValue {
- uint64_t value;
- modelclock_t expiration;
+ ModelAction *writer;
ModelAction * act;
};
ModelAction * act;
};
@@
-118,7
+117,9
@@
private:
/** The scheduler to use: tracks the running/ready Threads */
Scheduler *scheduler;
/** The scheduler to use: tracks the running/ready Threads */
Scheduler *scheduler;
+ bool sleep_can_read_from(ModelAction * curr, const ModelAction *write);
bool thin_air_constraint_may_allow(const ModelAction * writer, const ModelAction *reader);
bool thin_air_constraint_may_allow(const ModelAction * writer, const ModelAction *reader);
+ bool mo_may_allow(const ModelAction * writer, const ModelAction *reader);
bool has_asserted() {return asserted;}
void reset_asserted() {asserted=false;}
int num_executions;
bool has_asserted() {return asserted;}
void reset_asserted() {asserted=false;}
int num_executions;