more documentation

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index fba2fe5c3ede9f821e1d54743d3f8ea894ebd017..aa83cfcfacf940e89f6d612151268324dfd36964 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -86,19 +86,19 @@ void ModelChecker::reset_to_initial_state()
        snapshotObject->backTrackBeforeStep(0);
 }
 
-/** @returns a thread ID for a new Thread */
+/** @return a thread ID for a new Thread */
 thread_id_t ModelChecker::get_next_id()
 {
        return priv->next_thread_id++;
 }
 
-/** @returns the number of user threads created during this execution */
+/** @return the number of user threads created during this execution */
 int ModelChecker::get_num_threads()
 {
        return priv->next_thread_id;
 }
 
-/** @returns a sequence number for a new ModelAction */
+/** @return a sequence number for a new ModelAction */
 modelclock_t ModelChecker::get_next_seq_num()
 {
        return ++priv->used_sequence_numbers;
@@ -243,6 +243,13 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
        return NULL;
 }
 
+/** This method find backtracking points where we should try to
+ * reorder the parameter ModelAction against.
+ *
+ * @param the ModelAction to find backtracking points for.
+ */
+
+
 void ModelChecker::set_backtracking(ModelAction *act)
 {
        Thread *t = get_thread(act);
@@ -344,6 +351,21 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw)
        }
 }
 
+/**
+ * Processes a lock, trylock, or unlock model action.  @param curr is
+ * the read model action to process.  
+ *
+ * The try lock operation checks whether the lock is taken.  If not,
+ * it falls to the normal lock operation case.  If so, it returns
+ * fail.
+ *
+ * The lock operation has already been checked that it is enabled, so
+ * it just grabs the lock and synchronizes with the previous unlock.
+ *
+ * The unlock operation has to re-enable all of the threads that are
+ * waiting on the lock.
+ */
+
 void ModelChecker::process_mutex(ModelAction *curr) {
        std::mutex * mutex=(std::mutex *) curr->get_location();
        struct std::mutex_state * state=mutex->get_state();
@@ -377,7 +399,7 @@ void ModelChecker::process_mutex(ModelAction *curr) {
                action_list_t * waiters = lock_waiters_map->get_safe_ptr(curr->get_location());
                //activate all the waiting threads
                for(action_list_t::iterator rit = waiters->begin(); rit!=waiters->end(); rit++) {
-                       add_thread(get_thread((*rit)->get_tid()));
+                       scheduler->add_thread(get_thread((*rit)->get_tid()));
                }
                waiters->clear();
                break;
@@ -463,6 +485,14 @@ ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr)
        return newcurr;
 }
 
+/**
+ * This method checks whether a model action is enabled at the given point.
+ * At this point, it checks whether a lock operation would be successful at this point.
+ * If not, it puts the thread in a waiter list.
+ * @param curr is the ModelAction to check whether it is enabled.
+ * @return a bool that indicates whether the action is enabled.
+ */
+
 bool ModelChecker::check_action_enabled(ModelAction *curr) {
        if (curr->is_lock()) {
                std::mutex * lock=(std::mutex *) curr->get_location();
@@ -646,18 +676,18 @@ bool ModelChecker::promises_expired() {
        return false;
 }
 
-/** @returns whether the current partial trace must be a prefix of a
+/** @return whether the current partial trace must be a prefix of a
  * feasible trace. */
 bool ModelChecker::isfeasibleprefix() {
        return promises->size() == 0 && *lazy_sync_size == 0;
 }
 
-/** @returns whether the current partial trace is feasible. */
+/** @return whether the current partial trace is feasible. */
 bool ModelChecker::isfeasible() {
        return !mo_graph->checkForRMWViolation() && isfeasibleotherthanRMW();
 }
 
-/** @returns whether the current partial trace is feasible other than
+/** @return whether the current partial trace is feasible other than
  * multiple RMW reading from the same store. */
 bool ModelChecker::isfeasibleotherthanRMW() {
        if (DBG_ENABLED()) {
@@ -1276,6 +1306,14 @@ ModelAction * ModelChecker::get_last_seq_cst(ModelAction *curr)
        return NULL;
 }
 
+/**
+ * Gets the last unlock operation
+ * performed on a particular mutex (i.e., memory location).
+ * @param curr The current ModelAction; also denotes the object location to
+ * check
+ * @return The last unlock operation
+ */
+
 ModelAction * ModelChecker::get_last_unlock(ModelAction *curr)
 {
        void *location = curr->get_location();
@@ -1494,6 +1532,11 @@ void ModelChecker::add_thread(Thread *t)
        scheduler->add_thread(t);
 }
 
+/**
+ * Removes a thread from the scheduler. 
+ * @param the thread to remove.
+ */
+
 void ModelChecker::remove_thread(Thread *t)
 {
        scheduler->remove_thread(t);