From ebab3e51073b1534ba5d9ce944568d933d16fb3d Mon Sep 17 00:00:00 2001
From: Brian Norris <banorris@uci.edu>
Date: Thu, 14 Jun 2012 23:09:05 -0700
Subject: [PATCH] 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.
---
 model.cc  | 33 +++++++++++++++++++++++++++++----
 model.h   | 15 +++++++++++++++
 threads.h |  1 +
 3 files changed, 45 insertions(+), 4 deletions(-)

diff --git a/model.cc b/model.cc
index 3716d78..27b6cd6 100644
--- 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 0f93920..8d79eb5 100644
--- 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 0e0293a..a97a04c 100644
--- 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);
-- 
2.34.1