From: Brian Norris Date: Sat, 7 Jul 2012 01:58:21 +0000 (-0700) Subject: document some enumerated types X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=b49d9950a21123b6f84b6c594232eb950221f6ba;p=cdsspec-compiler.git document some enumerated types --- diff --git a/action.h b/action.h index f9c6d41..111ac31 100644 --- a/action.h +++ b/action.h @@ -15,14 +15,17 @@ #define VALUE_NONE -1 +/** @brief Represents an action type, identifying one of several types of + * ModelAction */ typedef enum action_type { - THREAD_CREATE, - THREAD_YIELD, - THREAD_JOIN, - ATOMIC_READ, - ATOMIC_WRITE, - ATOMIC_RMW, - ATOMIC_INIT + THREAD_CREATE, /**< A thread creation action */ + THREAD_YIELD, /**< A thread yield action */ + THREAD_JOIN, /**< A thread join action */ + ATOMIC_READ, /**< An atomic read action */ + ATOMIC_WRITE, /**< An atomic write action */ + ATOMIC_RMW, /**< An atomic read-modify-write action */ + ATOMIC_INIT /**< Initialization of an atomic object (e.g., + * atomic_init()) */ } action_type_t; /* Forward declaration */ diff --git a/libatomic.h b/libatomic.h index f24b5fb..71482c3 100644 --- a/libatomic.h +++ b/libatomic.h @@ -9,6 +9,7 @@ extern "C" { #endif + /** @brief The memory orders specified by the C11/C++11 memory models */ typedef enum memory_order { memory_order_relaxed, memory_order_consume, diff --git a/threads.h b/threads.h index ed9cbfe..0f39a83 100644 --- a/threads.h +++ b/threads.h @@ -13,10 +13,19 @@ typedef int thread_id_t; #define THREAD_ID_T_NONE -1 +/** @brief Represents the state of a user Thread */ typedef enum thread_state { + /** Thread was just created and hasn't run yet */ THREAD_CREATED, + /** Thread is running */ THREAD_RUNNING, + /** + * Thread has yielded to the model-checker but is ready to run. Used + * during an action that caused a context switch to the model-checking + * context. + */ THREAD_READY, + /** Thread has completed its execution */ THREAD_COMPLETED } thread_state;