X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=action.h;h=96ea6fa902ae28e2da69aaef6b899a6621c777da;hb=872ca5527c4df3f59e09b7050fd9d099e73cd362;hp=c455ea780883b371d80caed2d25c95e3d16edf1b;hpb=c7cd65f78d1c7956a02ac1e1cbd833e3dd17a3f1;p=model-checker.git diff --git a/action.h b/action.h index c455ea7..96ea6fa 100644 --- a/action.h +++ b/action.h @@ -7,11 +7,13 @@ #include #include +#include -#include "threads.h" #include "mymemory.h" -#include "clockvector.h" #include "memoryorder.h" +#include "modeltypes.h" + +class ClockVector; using std::memory_order; using std::memory_order_relaxed; @@ -64,7 +66,7 @@ class ModelAction { public: ModelAction(action_type_t type, memory_order order, void *loc, uint64_t value = VALUE_NONE); ~ModelAction(); - void print(void) const; + void print() const; thread_id_t get_tid() const { return tid; } action_type get_type() const { return type; } @@ -78,6 +80,7 @@ public: void set_node(Node *n) { node = n; } void copy_from_new(ModelAction *newaction); + void set_seq_number(modelclock_t num); void set_try_lock(bool obtainedlock); bool is_mutex_op() const; bool is_lock() const; @@ -98,12 +101,12 @@ public: bool same_var(const ModelAction *act) const; bool same_thread(const ModelAction *act) const; bool is_conflicting_lock(const ModelAction *act) const; - bool is_synchronizing(const ModelAction *act) const; + bool could_synchronize_with(const ModelAction *act) const; void create_cv(const ModelAction *parent = NULL); ClockVector * get_cv() const { return cv; } - void read_from(const ModelAction *act); - void synchronize_with(const ModelAction *act); + bool read_from(const ModelAction *act); + bool synchronize_with(const ModelAction *act); bool has_synchronized_with(const ModelAction *act) const; bool happens_before(const ModelAction *act) const;