add hashtable
[model-checker.git] / action.h
index 53107ea81762d33ab6a63ef2fa7e69176b379b1c..976fd4881c8033c277d3d2b7d27b781a08b693a6 100644 (file)
--- a/action.h
+++ b/action.h
@@ -1,3 +1,7 @@
+/** @file action.h
+ *  @brief Models actions taken by threads.
+ */
+
 #ifndef __ACTION_H__
 #define __ACTION_H__
 
@@ -21,10 +25,10 @@ typedef enum action_type {
 /* Forward declaration */
 class Node;
 class ClockVector;
+
 /**
  * The ModelAction class encapsulates an atomic action.
  */
-
 class ModelAction {
 public:
        ModelAction(action_type_t type, memory_order order, void *loc, int value);
@@ -42,11 +46,13 @@ public:
 
        bool is_read();
        bool is_write();
+       bool is_rmw();
        bool is_acquire();
        bool is_release();
+       bool is_seqcst();
        bool same_var(ModelAction *act);
        bool same_thread(ModelAction *act);
-       bool is_dependent(ModelAction *act);
+       bool is_synchronizing(ModelAction *act);
 
        void create_cv(ModelAction *parent = NULL);
        void read_from(ModelAction *act);
@@ -73,16 +79,18 @@ private:
        /** The thread id that performed this action. */
        thread_id_t tid;
        
-       /** The value written.  This should probably be something longer. */
+       /** The value read or written (if RMW, then the value written). This
+        * should probably be something longer. */
        int value;
 
+       /** A back reference to a Node in NodeStack, if this ModelAction is
+        * saved on the NodeStack. */
        Node *node;
        
        int seq_number;
 
-       /** The clock vector stored with this action if this action is a
-        *  store release */
-
+       /** The clock vector stored with this action; only needed if this
+        * action is a store release? */
        ClockVector *cv;
 };