From: Brian Norris <banorris@uci.edu>
Date: Tue, 4 Sep 2012 21:13:28 +0000 (-0700)
Subject: model: document ModelChecker::check_current_action
X-Git-Tag: pldi2013~240
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=21d42a641226da15d191e45d6a8b92b160aeb07d;p=model-checker.git

model: document ModelChecker::check_current_action
---

diff --git a/model.cc b/model.cc
index 866bc94..ec953ef 100644
--- a/model.cc
+++ b/model.cc
@@ -244,6 +244,18 @@ ModelAction * ModelChecker::get_next_backtrack()
 	return next;
 }
 
+/**
+ * This is the heart of the model checker routine. It performs model-checking
+ * actions corresponding to a given "current action." Among other processes, it
+ * calculates reads-from relationships, updates synchronization clock vectors,
+ * forms a memory_order constraints graph, and handles replay/backtrack
+ * execution when running permutations of previously-observed executions.
+ *
+ * @param curr The current action to process
+ * @return The next Thread that must be executed. May be NULL if ModelChecker
+ * makes no choice (e.g., according to replay execution, combining RMW actions,
+ * etc.)
+ */
 Thread * ModelChecker::check_current_action(ModelAction *curr)
 {
 	bool already_added = false;