add more documentation

I'm trying to add doxygen comments next to the definitions (not the
declaration) as much as possible, to keep the documentation as close to the
actual code as much as possible, helping to prevent errors as functionality
changes.

diff --git a/model.cc b/model.cc
index 3716d78838ba26ab694ef6faca6d66aa283b1b04..27b6cd6a9df24856be3c9b2cc712eb2972ae98f3 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -11,6 +11,7 @@
 
 ModelChecker *model;
 
+/** @brief Constructor */
 ModelChecker::ModelChecker()
        :
        /* Initialize default scheduler */
@@ -32,6 +33,7 @@ ModelChecker::ModelChecker()
 {
 }
 
+/** @brief Destructor */
 ModelChecker::~ModelChecker()
 {
        std::map<int, class Thread *>::iterator it;
@@ -46,6 +48,10 @@ ModelChecker::~ModelChecker()
        delete scheduler;
 }
 
+/**
+ * Restores user program to initial state and resets all model-checker data
+ * structures.
+ */
 void ModelChecker::reset_to_initial_state()
 {
        DEBUG("+++ Resetting to initial state +++\n");
@@ -58,21 +64,33 @@ void ModelChecker::reset_to_initial_state()
        snapshotObject->backTrackBeforeStep(0);
 }
 
+/** @returns a thread ID for a new Thread */
 thread_id_t ModelChecker::get_next_id()
 {
        return next_thread_id++;
 }
 
+/** @returns the number of user threads created during this execution */
 int ModelChecker::get_num_threads()
 {
        return next_thread_id;
 }
 
+/** @returns a sequence number for a new ModelAction */
 int ModelChecker::get_next_seq_num()
 {
        return ++used_sequence_numbers;
 }
 
+/**
+ * Performs the "scheduling" for the model-checker. That is, it checks if the
+ * model-checker has selected a "next thread to run" and returns it, if
+ * available. This function should be called from the Scheduler routine, where
+ * the Scheduler falls back to a default scheduling routine if needed.
+ *
+ * @return The next thread chosen by the model-checker. If the model-checker
+ * makes no selection, retuns NULL.
+ */
 Thread * ModelChecker::schedule_next_thread()
 {
        Thread *t;
@@ -86,11 +104,11 @@ Thread * ModelChecker::schedule_next_thread()
 }
 
 /**
- * get_next_replay_thread() - Choose the next thread in the replay sequence
+ * Choose the next thread in the replay sequence.
  *
- * If we've reached the 'diverge' point, then we pick a thread from the
- *   backtracking set.
- * Otherwise, we simply return the next thread in the sequence.
+ * If the replay sequence has reached the 'diverge' point, returns a thread
+ * from the backtracking set. Otherwise, simply returns the next thread in the
+ * sequence that is being replayed.
  */
 thread_id_t ModelChecker::get_next_replay_thread()
 {
@@ -118,6 +136,13 @@ thread_id_t ModelChecker::get_next_replay_thread()
        return tid;
 }
 
+/**
+ * Queries the model-checker for more executions to explore and, if one
+ * exists, resets the model-checker state to execute a new execution.
+ *
+ * @return If there are more executions to explore, return true. Otherwise,
+ * return false.
+ */
 bool ModelChecker::next_execution()
 {
        DBG();

diff --git a/model.h b/model.h
index 0f93920fc83bc5cb29ffc7da618923b8f5a266c9..8d79eb56a43ef36fe02dfc5ec4b6463f719b0126 100644 (file)
--- a/model.h
+++ b/model.h
@@ -22,15 +22,30 @@
 /* Forward declaration */
 class NodeStack;
 
+/** @brief The central structure for model-checking */
 class ModelChecker {
 public:
        ModelChecker();
        ~ModelChecker();
+
+       /** The scheduler to use: tracks the running/ready Threads */
        class Scheduler *scheduler;
 
+       /** Stores the context for the main model-checking system thread (call
+        * once)
+        * @param ctxt The system context structure
+        */
        void set_system_context(ucontext_t *ctxt) { system_context = ctxt; }
+
+       /** @returns the context for the main model-checking system thread */
        ucontext_t * get_system_context(void) { return system_context; }
 
+       /**
+        * Stores the ModelAction for the current thread action.  Call this
+        * immediately before switching from user- to system-context to pass
+        * data between them.
+        * @param act The ModelAction created by the user-thread action
+        */
        void set_current_action(ModelAction *act) { current_action = act; }
        void check_current_action(void);
        void print_summary(void);

diff --git a/threads.h b/threads.h
index 0e0293ad817332e867db1e7b92c490da3c3f9b19..a97a04c704449963981fe443a711c64abc716fb3 100644 (file)
--- a/threads.h
+++ b/threads.h
@@ -22,6 +22,7 @@ typedef enum thread_state {
 
 class ModelAction;
 
+/** @brief A Thread is created for each user-space thread */
 class Thread {
 public:
        Thread(thrd_t *t, void (*func)(void *), void *a);