Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/model-checker

diff --git a/Makefile b/Makefile
index fbbc3a1c39419b5fe7527976cfb2966389d338d9..b65830fa2ce0e222d04163c563ec33676aa997b6 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -30,7 +30,7 @@ mac: LDFLAGS=-ldl
 mac: SHARED=-Wl,-undefined,dynamic_lookup -dynamiclib
 mac: all
 
-docs:
+docs: *.c *.cc *.h
        doxygen
 
 $(BIN): $(USER_O) $(LIB_SO)

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/mymemory.h b/mymemory.h
index b200ae0160c8c0c8ba39ad31384689271986a384..56e690436d1e573da00bf287e6aff2388f476c0c 100644 (file)
--- a/mymemory.h
+++ b/mymemory.h
@@ -35,7 +35,7 @@ void MYFREE(void *ptr);
 void system_free( void * ptr );
 void *system_malloc( size_t size );
 
-/** @brief Provides a non-snapshotting allocators for a STL class.
+/** @brief Provides a non-snapshotting allocator for use in STL classes.
  *
  * The code was adapted from a code example from the book The C++
  * Standard Library - A Tutorial and Reference by Nicolai M. Josuttis,

diff --git a/schedule.h b/schedule.h
index ad9f11af035b460cf9c5c0457addf44bb6e172db..cba4b11a6d597011910ceec3a55324d5edf136f4 100644 (file)
--- a/schedule.h
+++ b/schedule.h
@@ -11,7 +11,8 @@
 /* Forward declaration */
 class Thread;
 
-/** @brief The Scheduler class controls the Thread execution schedule. */
+/** @brief The Scheduler class performs the mechanics of Thread execution
+ * scheduling. */
 class Scheduler {
 public:
        Scheduler();

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);