projects
/
model-checker.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
add support for docs
[model-checker.git]
/
action.h
diff --git
a/action.h
b/action.h
index 62141749d5efafc34dc1bbe3fef6656b344571ec..53107ea81762d33ab6a63ef2fa7e69176b379b1c 100644
(file)
--- a/
action.h
+++ b/
action.h
@@
-14,12
+14,16
@@
typedef enum action_type {
THREAD_YIELD,
THREAD_JOIN,
ATOMIC_READ,
THREAD_YIELD,
THREAD_JOIN,
ATOMIC_READ,
- ATOMIC_WRITE
+ ATOMIC_WRITE,
+ ATOMIC_RMW
} action_type_t;
/* Forward declaration */
class Node;
class ClockVector;
} action_type_t;
/* Forward declaration */
class Node;
class ClockVector;
+/**
+ * The ModelAction class encapsulates an atomic action.
+ */
class ModelAction {
public:
class ModelAction {
public:
@@
-56,14
+60,29
@@
public:
MEMALLOC
private:
MEMALLOC
private:
+
+ /** Type of action (read, write, thread create, thread yield, thread join) */
action_type type;
action_type type;
+
+ /** The memory order for this operation. */
memory_order order;
memory_order order;
+
+ /** A pointer to the memory location for this action. */
void *location;
void *location;
+
+ /** The thread id that performed this action. */
thread_id_t tid;
thread_id_t tid;
+
+ /** The value written. This should probably be something longer. */
int value;
int value;
+
Node *node;
Node *node;
+
int seq_number;
int seq_number;
+ /** The clock vector stored with this action if this action is a
+ * store release */
+
ClockVector *cv;
};
ClockVector *cv;
};