From 21d42a641226da15d191e45d6a8b92b160aeb07d Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Tue, 4 Sep 2012 14:13:28 -0700 Subject: [PATCH] model: document ModelChecker::check_current_action --- model.cc | 12 ++++++++++++ 1 file changed, 12 insertions(+) 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; -- 2.34.1