+/** @file main.cc
+ * @brief Entry point for the model checker.
+ */
+
#include "libthreads.h"
#include "common.h"
#include "threads.h"
#include "model.h"
#include "snapshot-interface.h"
-/*
- * Return 1 if found next thread, 0 otherwise
+/** The thread_system_next function takes the next step in the
+ * execution. @return Returns the 1 if there is another step and 0
+ * otherwise.
*/
+
static int thread_system_next(void) {
Thread *curr, *next;
return Thread::swap(model->get_system_context(), next);
}
+/** The thread_wait_finish method runs the current execution until we
+ * have no more steps to take.
+ */
+
static void thread_wait_finish(void) {
DBG();
while (!thread_system_next());
}
+
+/** The real_main function contains the main model checking loop. */
+
void real_main() {
thrd_t user_thread;
ucontext_t main_context;
int main_numargs;
char ** main_args;
-/*
- * Main system function
+/**
+ * Main function. Just initializes snapshotting library and the
+ * snapshotting library calls the real_main function.
*/
int main(int numargs, char ** args) {
/* Stash this stuff in case someone wants it eventually */
#endif
/* Initialize snapshot data structure */
#if USE_MPROTECT_SNAPSHOT
+
+/** The initSnapShotRecord method initialized the snapshotting data
+ * structures for the mprotect based snapshot.
+ */
void initSnapShotRecord(unsigned int numbackingpages, unsigned int numsnapshots, unsigned int nummemoryregions) {
snapshotrecord=( struct SnapShot * )MYMALLOC(sizeof(struct SnapShot));
snapshotrecord->regionsToSnapShot=( struct MemoryRegion * )MYMALLOC(sizeof(struct MemoryRegion)*nummemoryregions);
}
/** The finalize method shuts down the snapshotting system. */
+//Subramanian -- remove this function from the external interface and
+//have us call it internally
void finalize(){
#if !USE_MPROTECT_SNAPSHOT