projects
/
model-checker.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
promise: record multiple readers in the same Promise
[model-checker.git]
/
promise.h
diff --git
a/promise.h
b/promise.h
index c131d743aa185d2972cd2d1922fb7ac43d6c3c8d..5ea7dc58d0470a29a537985c6322f8792be1f856 100644
(file)
--- a/
promise.h
+++ b/
promise.h
@@
-24,7
+24,9
@@
struct future_value {
class Promise {
public:
Promise(ModelAction *read, struct future_value fv);
class Promise {
public:
Promise(ModelAction *read, struct future_value fv);
- ModelAction * get_action() const { return read; }
+ bool add_reader(ModelAction *reader);
+ ModelAction * get_reader(unsigned int i) const;
+ unsigned int get_num_readers() const { return readers.size(); }
bool eliminate_thread(thread_id_t tid);
void add_thread(thread_id_t tid);
bool thread_is_available(thread_id_t tid) const;
bool eliminate_thread(thread_id_t tid);
void add_thread(thread_id_t tid);
bool thread_is_available(thread_id_t tid) const;
@@
-54,8
+56,8
@@
class Promise {
const future_value fv;
const future_value fv;
- /** @brief The action
which reads a promised
value */
-
ModelAction * const read
;
+ /** @brief The action
(s) which read the promised future
value */
+
std::vector< ModelAction *, SnapshotAlloc<ModelAction *> > readers
;
const ModelAction *write;
};
const ModelAction *write;
};