projects
/
model-checker.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
hashtable: style
[model-checker.git]
/
model.cc
diff --git
a/model.cc
b/model.cc
index 843034d31acec815eb8c8943d6910eb074103f0b..98df8f316106a5f4cce404f4cada60ee35c5898a 100644
(file)
--- a/
model.cc
+++ b/
model.cc
@@
-159,7
+159,7
@@
void ModelChecker::reset_to_initial_state()
/* Print all model-checker output before rollback */
fflush(model_out);
/* Print all model-checker output before rollback */
fflush(model_out);
- snapshot
Object->backTrackBeforeStep
(0);
+ snapshot
_backtrack_before
(0);
}
/** @return a thread ID for a new Thread */
}
/** @return a thread ID for a new Thread */
@@
-174,7
+174,12
@@
unsigned int ModelChecker::get_num_threads() const
return priv->next_thread_id;
}
return priv->next_thread_id;
}
-/** @return The currently executing Thread. */
+/**
+ * Must be called from user-thread context (e.g., through the global
+ * thread_current() interface)
+ *
+ * @return The currently executing Thread.
+ */
Thread * ModelChecker::get_current_thread() const
{
return scheduler->get_current_thread();
Thread * ModelChecker::get_current_thread() const
{
return scheduler->get_current_thread();
@@
-212,9
+217,8
@@
Thread * ModelChecker::get_next_thread(ModelAction *curr)
/* Do not split atomic actions. */
if (curr->is_rmwr())
return thread_current();
/* Do not split atomic actions. */
if (curr->is_rmwr())
return thread_current();
- /* The THREAD_CREATE action points to the created Thread */
else if (curr->get_type() == THREAD_CREATE)
else if (curr->get_type() == THREAD_CREATE)
- return
(Thread *)curr->get_location
();
+ return
curr->get_thread_operand
();
}
/* Have we completed exploring the preselected path? */
}
/* Have we completed exploring the preselected path? */
@@
-820,7
+824,7
@@
bool ModelChecker::process_mutex(ModelAction *curr)
if (curr->get_node()->get_misc() == 0) {
get_safe_ptr_action(condvar_waiters_map, curr->get_location())->push_back(curr);
//disable us
if (curr->get_node()->get_misc() == 0) {
get_safe_ptr_action(condvar_waiters_map, curr->get_location())->push_back(curr);
//disable us
- scheduler->sleep(get_
current_thread(
));
+ scheduler->sleep(get_
thread(curr
));
}
break;
}
}
break;
}
@@
-944,12
+948,12
@@
bool ModelChecker::process_thread_action(ModelAction *curr)
switch (curr->get_type()) {
case THREAD_CREATE: {
switch (curr->get_type()) {
case THREAD_CREATE: {
- Thread *th =
(Thread *)curr->get_location
();
+ Thread *th =
curr->get_thread_operand
();
th->set_creation(curr);
break;
}
case THREAD_JOIN: {
th->set_creation(curr);
break;
}
case THREAD_JOIN: {
- Thread *blocking =
(Thread *)curr->get_location
();
+ Thread *blocking =
curr->get_thread_operand
();
ModelAction *act = get_last_action(blocking->get_id());
curr->synchronize_with(act);
updated = true; /* trigger rel-seq checks */
ModelAction *act = get_last_action(blocking->get_id());
curr->synchronize_with(act);
updated = true; /* trigger rel-seq checks */
@@
-1192,11
+1196,10
@@
void ModelChecker::set_current_action(ModelAction *act) {
* execution when running permutations of previously-observed executions.
*
* @param curr The current action to process
* 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.)
+ * @return The ModelAction that is actually executed; may be different than
+ * curr; may be NULL, if the current action is not enabled to run
*/
*/
-
Thread
* ModelChecker::check_current_action(ModelAction *curr)
+
ModelAction
* ModelChecker::check_current_action(ModelAction *curr)
{
ASSERT(curr);
bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
{
ASSERT(curr);
bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
@@
-1204,13
+1207,17
@@
Thread * ModelChecker::check_current_action(ModelAction *curr)
if (!check_action_enabled(curr)) {
/* Make the execution look like we chose to run this action
* much later, when a lock/join can succeed */
if (!check_action_enabled(curr)) {
/* Make the execution look like we chose to run this action
* much later, when a lock/join can succeed */
- get_
current_thread(
)->set_pending(curr);
- scheduler->sleep(get_
current_thread(
));
- return
get_next_thread(NULL)
;
+ get_
thread(curr
)->set_pending(curr);
+ scheduler->sleep(get_
thread(curr
));
+ return
NULL
;
}
bool newly_explored = initialize_curr_action(&curr);
}
bool newly_explored = initialize_curr_action(&curr);
+ DBG();
+ if (DBG_ENABLED())
+ curr->print();
+
wake_up_sleeping_actions(curr);
/* Add the action to lists before any other model-checking tasks */
wake_up_sleeping_actions(curr);
/* Add the action to lists before any other model-checking tasks */
@@
-1288,7
+1295,7
@@
Thread * ModelChecker::check_current_action(ModelAction *curr)
check_curr_backtracking(curr);
set_backtracking(curr);
check_curr_backtracking(curr);
set_backtracking(curr);
- return
get_next_thread(curr)
;
+ return
curr
;
}
void ModelChecker::check_curr_backtracking(ModelAction *curr)
}
void ModelChecker::check_curr_backtracking(ModelAction *curr)
@@
-2504,14
+2511,8
@@
void ModelChecker::build_reads_from_past(ModelAction *curr)
else if (curr->get_sleep_flag() && !curr->is_seqcst() && !sleep_can_read_from(curr, act))
allow_read = false;
else if (curr->get_sleep_flag() && !curr->is_seqcst() && !sleep_can_read_from(curr, act))
allow_read = false;
- if (allow_read) {
- DEBUG("Adding action to may_read_from:\n");
- if (DBG_ENABLED()) {
- act->print();
- curr->print();
- }
+ if (allow_read)
curr->get_node()->add_read_from(act);
curr->get_node()->add_read_from(act);
- }
/* Include at most one act per-thread that "happens before" curr */
if (act->happens_before(curr))
/* Include at most one act per-thread that "happens before" curr */
if (act->happens_before(curr))
@@
-2723,12
+2724,7
@@
bool ModelChecker::take_step(ModelAction *curr)
Thread *curr_thrd = get_thread(curr);
ASSERT(curr_thrd->get_state() == THREAD_READY);
Thread *curr_thrd = get_thread(curr);
ASSERT(curr_thrd->get_state() == THREAD_READY);
- Thread *next_thrd = check_current_action(curr);
-
- if (curr_thrd->is_blocked() || curr_thrd->is_complete())
- scheduler->remove_thread(curr_thrd);
-
- next_thrd = scheduler->next_thread(next_thrd);
+ curr = check_current_action(curr);
/* Infeasible -> don't take any more steps */
if (is_infeasible())
/* Infeasible -> don't take any more steps */
if (is_infeasible())
@@
-2738,11
+2734,15
@@
bool ModelChecker::take_step(ModelAction *curr)
return false;
}
return false;
}
- if (params.bound != 0)
{
- if (priv->used_sequence_numbers > params.bound)
{
+ if (params.bound != 0)
+ if (priv->used_sequence_numbers > params.bound)
return false;
return false;
- }
- }
+
+ if (curr_thrd->is_blocked() || curr_thrd->is_complete())
+ scheduler->remove_thread(curr_thrd);
+
+ Thread *next_thrd = get_next_thread(curr);
+ next_thrd = scheduler->next_thread(next_thrd);
DEBUG("(%d, %d)\n", curr_thrd ? id_to_int(curr_thrd->get_id()) : -1,
next_thrd ? id_to_int(next_thrd->get_id()) : -1);
DEBUG("(%d, %d)\n", curr_thrd ? id_to_int(curr_thrd->get_id()) : -1,
next_thrd ? id_to_int(next_thrd->get_id()) : -1);