}
/** @return The currently executing Thread. */
-Thread * ModelChecker::get_current_thread()
+Thread * ModelChecker::get_current_thread() const
{
return scheduler->get_current_thread();
}
return ++priv->used_sequence_numbers;
}
-Node * ModelChecker::get_curr_node() {
+Node * ModelChecker::get_curr_node() const
+{
return node_stack->get_head();
}
(*curr)->set_seq_number(get_next_seq_num());
- newcurr = node_stack->explore_action(*curr, scheduler->get_enabled());
+ newcurr = node_stack->explore_action(*curr, scheduler->get_enabled_array());
if (newcurr) {
/* First restore type and order in case of RMW operation */
if ((*curr)->is_rmwr())
if (curr->is_seqcst()) {
/* We have to at least see the last sequentially consistent write,
so we are initialized. */
- ModelAction *last_seq_cst = get_last_seq_cst(curr);
+ ModelAction *last_seq_cst = get_last_seq_cst_write(curr);
if (last_seq_cst != NULL) {
mo_graph->addEdge(last_seq_cst, curr);
added = true;
* check
* @return The last seq_cst write
*/
-ModelAction * ModelChecker::get_last_seq_cst(ModelAction *curr) const
+ModelAction * ModelChecker::get_last_seq_cst_write(ModelAction *curr) const
{
void *location = curr->get_location();
action_list_t *list = get_safe_ptr_action(obj_map, location);
return NULL;
}
-ModelAction * ModelChecker::get_parent_action(thread_id_t tid)
+ModelAction * ModelChecker::get_parent_action(thread_id_t tid) const
{
ModelAction *parent = get_last_action(tid);
if (!parent)
* @param tid The thread whose clock vector we want
* @return Desired clock vector
*/
-ClockVector * ModelChecker::get_cv(thread_id_t tid)
+ClockVector * ModelChecker::get_cv(thread_id_t tid) const
{
return get_parent_action(tid)->get_cv();
}
bool initialized = false;
if (curr->is_seqcst()) {
- last_seq_cst = get_last_seq_cst(curr);
+ last_seq_cst = get_last_seq_cst_write(curr);
/* We have to at least see the last sequentially consistent write,
so we are initialized. */
if (last_seq_cst != NULL)