X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=nodestack.h;h=986b9c9df4be85f15d57cbf13f46d62626a3c35d;hb=6b87c110fbda87ccec4f58b1e292d5f9434c8691;hp=648ef4dfc318afc38a4e98b1e31bf4a1bcc944eb;hpb=d884d14a6288f1ee1809158e81ffb05bf83f483b;p=model-checker.git diff --git a/nodestack.h b/nodestack.h index 648ef4d..986b9c9 100644 --- a/nodestack.h +++ b/nodestack.h @@ -24,11 +24,14 @@ class Thread; *
  • @b fulfilled: satisfied by this Node's ModelAction under the current * configuration.
  • */ -typedef enum { - PROMISE_IGNORE = 0, /**< This promise is inapplicable; ignore it */ - PROMISE_UNFULFILLED, /**< This promise is applicable but unfulfilled */ - PROMISE_FULFILLED /**< This promise is applicable and fulfilled */ -} promise_t; + +#define PROMISE_IGNORE 0 /**< This promise is inapplicable; ignore it */ +#define PROMISE_UNFULFILLED 1 /**< This promise is applicable but unfulfilled */ +#define PROMISE_FULFILLED 2 /**< This promise is applicable and fulfilled */ +#define PROMISE_MASK 0xf +#define PROMISE_RMW 0x10 + +typedef int promise_t; struct future_value { uint64_t value; @@ -88,7 +91,7 @@ public: int get_read_from_size(); const ModelAction * get_read_from_at(int i); - void set_promise(unsigned int i); + void set_promise(unsigned int i, bool is_rmw); bool get_promise(unsigned int i); bool increment_promise(); bool promise_empty();