nodestack: improve bounds-checking assertion

[model-checker.git] / action.h

diff --git a/action.h b/action.h
index dfe2102d47b4ced0879f25509fd7ef1f7c7850f5..f7e7e5ea0febd7251ff91e49654807ed9e437a95 100644 (file)
--- a/action.h
+++ b/action.h
@@ -14,6 +14,7 @@
 #include "modeltypes.h"
 
 class ClockVector;
 #include "modeltypes.h"
 
 class ClockVector;

+class Thread;

 
 using std::memory_order;
 using std::memory_order_relaxed;
 
 using std::memory_order;
 using std::memory_order_relaxed;


@@ -25,7 +26,7 @@ using std::memory_order_seq_cst;
 /** Note that this value can be legitimately used by a program, and
                hence by iteself does not indicate no value. */
 
 /** Note that this value can be legitimately used by a program, and
                hence by iteself does not indicate no value. */
 

-#define VALUE_NONE 1234567890
+#define VALUE_NONE 0xdeadbeef

 
 /** A special value to represent a successful trylock */
 
 
 /** A special value to represent a successful trylock */
 


@@ -54,7 +55,10 @@ typedef enum action_type {
        ATOMIC_FENCE,         /**< A fence action */
        ATOMIC_LOCK,          /**< A lock action */
        ATOMIC_TRYLOCK,       /**< A trylock action */
        ATOMIC_FENCE,         /**< A fence action */
        ATOMIC_LOCK,          /**< A lock action */
        ATOMIC_TRYLOCK,       /**< A trylock action */

-       ATOMIC_UNLOCK         /**< An unlock action */
+       ATOMIC_UNLOCK,        /**< An unlock action */
+       ATOMIC_NOTIFY_ONE,    /**< A notify_one action */
+       ATOMIC_NOTIFY_ALL,    /**< A notify all action */
+       ATOMIC_WAIT           /**< A wait action */

 } action_type_t;
 
 /* Forward declaration */
 } action_type_t;
 
 /* Forward declaration */


@@ -66,7 +70,7 @@ class ClockVector;
  */
 class ModelAction {
 public:
  */
 class ModelAction {
 public:

-       ModelAction(action_type_t type, memory_order order, void *loc, uint64_t value = VALUE_NONE);
+       ModelAction(action_type_t type, memory_order order, void *loc, uint64_t value = VALUE_NONE, Thread *thread = NULL);

        ~ModelAction();
        void print() const;
 
        ~ModelAction();
        void print() const;
 


@@ -89,10 +93,14 @@ public:
        bool is_lock() const;
        bool is_trylock() const;
        bool is_unlock() const;
        bool is_lock() const;
        bool is_trylock() const;
        bool is_unlock() const;

+       bool is_wait() const;
+       bool is_notify() const;
+       bool is_notify_one() const;

        bool is_success_lock() const;
        bool is_failed_trylock() const;
        bool is_read() const;
        bool is_write() const;
        bool is_success_lock() const;
        bool is_failed_trylock() const;
        bool is_read() const;
        bool is_write() const;

+       bool could_be_write() const;

        bool is_rmwr() const;
        bool is_rmwc() const;
        bool is_rmw() const;
        bool is_rmwr() const;
        bool is_rmwc() const;
        bool is_rmw() const;


@@ -124,6 +132,10 @@ public:
        void process_rmw(ModelAction * act);
        void copy_typeandorder(ModelAction * act);
 
        void process_rmw(ModelAction * act);
        void copy_typeandorder(ModelAction * act);
 

+       void set_sleep_flag() { sleep_flag=true; }
+       bool get_sleep_flag() { return sleep_flag; }
+       unsigned int hash() const;
+

        MEMALLOC
 private:
 
        MEMALLOC
 private:
 


@@ -154,8 +166,10 @@ private:
        /** The clock vector stored with this action; only needed if this
         * action is a store release? */
        ClockVector *cv;
        /** The clock vector stored with this action; only needed if this
         * action is a store release? */
        ClockVector *cv;

+
+       bool sleep_flag;

 };
 
 };
 

-typedef std::list<ModelAction *> action_list_t;
+typedef std::list< ModelAction *, SnapshotAlloc<ModelAction *> > action_list_t;

 
 #endif /* __ACTION_H__ */
 
 #endif /* __ACTION_H__ */