X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=promise.h;h=ce84ede68b0e58e4c76c280cb6632bc85d76cb02;hb=d2cbbe4ce6d8f6e1aa23b8fe639ed58edf1789b7;hp=a47982d6d291078f547acfa2d3ddf9dc33881cc5;hpb=bdef0741b8a01e16946d261bc2a657af5a683b3e;p=model-checker.git diff --git a/promise.h b/promise.h index a47982d..ce84ede 100644 --- a/promise.h +++ b/promise.h @@ -6,18 +6,42 @@ #ifndef __PROMISE_H__ #define __PROMISE_H__ -#include +#include +#include "threads-model.h" -class ModelAction; +#include "model.h" class Promise { public: - Promise(ModelAction * act, uint64_t value); + Promise(ModelAction *act, uint64_t value, modelclock_t expiration) : + value(value), expiration(expiration), read(act), write(NULL) + { + increment_threads(act->get_tid()); + } + modelclock_t get_expiration() const {return expiration;} + ModelAction * get_action() const { return read; } + bool increment_threads(thread_id_t tid); + + bool has_sync_thread(thread_id_t tid) { + unsigned int id=id_to_int(tid); + if (id>=synced_thread.size()) { + return false; + } + return synced_thread[id]; + } + + uint64_t get_value() const { return value; } + void set_write(const ModelAction *act) { write = act; } + const ModelAction * get_write() { return write; } + + SNAPSHOTALLOC private: - uint64_t value; - ModelAction *read; - unsigned int numthreads; + std::vector synced_thread; + const uint64_t value; + const modelclock_t expiration; + ModelAction * const read; + const ModelAction * write; }; #endif