document some enumerated types

diff --git a/action.h b/action.h
index f9c6d417084e62d39956ad1b1775c236b7bc48b8..111ac31124ef89d796e8d163c1b39a097c9a2c7c 100644 (file)
--- a/action.h
+++ b/action.h
@@ -15,14 +15,17 @@
 
 #define VALUE_NONE -1
 
 
 #define VALUE_NONE -1
 

+/** @brief Represents an action type, identifying one of several types of
+ * ModelAction */

 typedef enum action_type {
 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 */
 } action_type_t;
 
 /* Forward declaration */

diff --git a/libatomic.h b/libatomic.h
index f24b5fbff35a10a3dcc2c88beca108ecb9093e75..71482c3d0a505d050fafc912951d8c084ee7fac6 100644 (file)
--- a/libatomic.h
+++ b/libatomic.h
@@ -9,6 +9,7 @@
 extern "C" {
 #endif
 
 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,
        typedef enum memory_order {
                memory_order_relaxed,
                memory_order_consume,

diff --git a/threads.h b/threads.h
index ed9cbfed118a20561f271aaace5acc67f5b47f6e..0f39a836f49efae34c63415f433e37715a43d258 100644 (file)
--- a/threads.h
+++ b/threads.h
@@ -13,10 +13,19 @@ typedef int thread_id_t;
 
 #define THREAD_ID_T_NONE       -1
 
 
 #define THREAD_ID_T_NONE       -1
 

+/** @brief Represents the state of a user Thread */

 typedef enum thread_state {
 typedef enum thread_state {

+       /** Thread was just created and hasn't run yet */

        THREAD_CREATED,
        THREAD_CREATED,

+       /** Thread is running */

        THREAD_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_READY,

+       /** Thread has completed its execution */

        THREAD_COMPLETED
 } thread_state;
 
        THREAD_COMPLETED
 } thread_state;