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.
+/** @brief Constructor */
ModelChecker::ModelChecker()
:
/* Initialize default scheduler */
ModelChecker::ModelChecker()
:
/* Initialize default scheduler */
+/** @brief Destructor */
ModelChecker::~ModelChecker()
{
std::map<int, class Thread *>::iterator it;
ModelChecker::~ModelChecker()
{
std::map<int, class Thread *>::iterator it;
+/**
+ * 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");
void ModelChecker::reset_to_initial_state()
{
DEBUG("+++ Resetting to initial state +++\n");
snapshotObject->backTrackBeforeStep(0);
}
snapshotObject->backTrackBeforeStep(0);
}
+/** @returns a thread ID for a new Thread */
thread_id_t ModelChecker::get_next_id()
{
return next_thread_id++;
}
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;
}
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;
}
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;
Thread * ModelChecker::schedule_next_thread()
{
Thread *t;
- * 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()
{
*/
thread_id_t ModelChecker::get_next_replay_thread()
{
+/**
+ * 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();
bool ModelChecker::next_execution()
{
DBG();
/* Forward declaration */
class NodeStack;
/* Forward declaration */
class NodeStack;
+/** @brief The central structure for model-checking */
class ModelChecker {
public:
ModelChecker();
~ModelChecker();
class ModelChecker {
public:
ModelChecker();
~ModelChecker();
+
+ /** The scheduler to use: tracks the running/ready Threads */
class Scheduler *scheduler;
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; }
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; }
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);
void set_current_action(ModelAction *act) { current_action = act; }
void check_current_action(void);
void print_summary(void);
+/** @brief A Thread is created for each user-space thread */
class Thread {
public:
Thread(thrd_t *t, void (*func)(void *), void *a);
class Thread {
public:
Thread(thrd_t *t, void (*func)(void *), void *a);