From: Brian Norris <banorris@uci.edu>
Date: Tue, 18 Sep 2012 23:35:46 +0000 (-0700)
Subject: model: document behavior of ModelChecker::initialize_curr_action
X-Git-Tag: pldi2013~177^2^2~5
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=7bd10d9157220e7eebfbb67c3c3f12ad2a9deb97;p=model-checker.git

model: document behavior of ModelChecker::initialize_curr_action
---

diff --git a/model.cc b/model.cc
index a13ccb7..ebadbb6 100644
--- a/model.cc
+++ b/model.cc
@@ -333,6 +333,17 @@ bool ModelChecker::process_write(ModelAction *curr)
 	return updated_mod_order || updated_promises;
 }
 
+/**
+ * Initialize the current action by performing one or more of the following
+ * actions, as appropriate: merging RMWR and RMWC/RMW actions, stepping forward
+ * in the NodeStack, manipulating backtracking sets, allocating and
+ * initializing clock vectors, and computing the promises to fulfill.
+ *
+ * @param curr The current action, as passed from the user context; may be
+ * freed/invalidated after the execution of this function
+ * @return The current action, as processed by the ModelChecker. Is only the
+ * same as the parameter @a curr if this is a newly-explored action.
+ */
 ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr)
 {
 	ModelAction *newcurr;