Thread *thr=get_thread(tid);
if ( scheduler->get_enabled(thr) == THREAD_SLEEP_SET ) {
ModelAction *pending_act=thr->get_pending();
- if (pending_act->could_synchronize_with(curr)) {
+ if ((!curr->is_rmwr())&&pending_act->could_synchronize_with(curr)) {
//Remove this thread from sleep set
scheduler->remove_sleep(thr);
}
*/
bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw)
{
- uint64_t value;
+ uint64_t value = VALUE_NONE;
bool updated = false;
while (true) {
const ModelAction *reads_from = curr->get_node()->get_read_from();
* 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.
+ * freed/invalidated after the execution of this function, with a different
+ * action "returned" its place (pass-by-reference)
+ * @return True if curr is a newly-explored action; false otherwise
*/
-ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr)
+bool ModelChecker::initialize_curr_action(ModelAction **curr)
{
ModelAction *newcurr;
- if (curr->is_rmwc() || curr->is_rmw()) {
- newcurr = process_rmw(curr);
- delete curr;
+ if ((*curr)->is_rmwc() || (*curr)->is_rmw()) {
+ newcurr = process_rmw(*curr);
+ delete *curr;
if (newcurr->is_rmw())
compute_promises(newcurr);
- return newcurr;
+
+ *curr = newcurr;
+ return false;
}
- curr->set_seq_number(get_next_seq_num());
+ (*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());
if (newcurr) {
/* First restore type and order in case of RMW operation */
- if (curr->is_rmwr())
- newcurr->copy_typeandorder(curr);
+ if ((*curr)->is_rmwr())
+ newcurr->copy_typeandorder(*curr);
- ASSERT(curr->get_location() == newcurr->get_location());
- newcurr->copy_from_new(curr);
+ ASSERT((*curr)->get_location() == newcurr->get_location());
+ newcurr->copy_from_new(*curr);
/* Discard duplicate ModelAction; use action from NodeStack */
- delete curr;
+ delete *curr;
/* Always compute new clock vector */
newcurr->create_cv(get_parent_action(newcurr->get_tid()));
+
+ *curr = newcurr;
+ return false; /* Action was explored previously */
} else {
- newcurr = curr;
+ newcurr = *curr;
/* Always compute new clock vector */
newcurr->create_cv(get_parent_action(newcurr->get_tid()));
else if (newcurr->is_notify_one()) {
newcurr->get_node()->set_misc_max(condvar_waiters_map->get_safe_ptr(newcurr->get_location())->size());
}
+ return true; /* This was a new ModelAction */
}
- return newcurr;
}
/**
return get_next_thread(NULL);
}
- ModelAction *newcurr = initialize_curr_action(curr);
+ bool newly_explored = initialize_curr_action(&curr);
wake_up_sleeping_actions(curr);
/* Add the action to lists before any other model-checking tasks */
if (!second_part_of_rmw)
- add_action_to_lists(newcurr);
+ add_action_to_lists(curr);
/* Build may_read_from set for newly-created actions */
- if (curr == newcurr && curr->is_read())
+ if (newly_explored && curr->is_read())
build_reads_from_past(curr);
- curr = newcurr;
/* Initialize work_queue with the "current action" work */
work_queue_t work_queue(1, CheckCurrWorkEntry(curr));
return true;
}
-/** Arbitrary reads from the future are not allowed. Section 29.3
- * part 9 places some constraints. This method checks one result of constraint
- * constraint. Others require compiler support. */
-bool ModelChecker::mo_may_allow(const ModelAction * writer, const ModelAction *reader) {
+/**
+ * Arbitrary reads from the future are not allowed. Section 29.3 part 9 places
+ * some constraints. This method checks one the following constraint (others
+ * require compiler support):
+ *
+ * If X --hb-> Y --mo-> Z, then X should not read from Z.
+ */
+bool ModelChecker::mo_may_allow(const ModelAction *writer, const ModelAction *reader)
+{
std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(reader->get_location());
+ unsigned int i;
- //Get write that follows reader action
- action_list_t *list = &(*thrd_lists)[id_to_int(reader->get_tid())];
- action_list_t::reverse_iterator rit;
- ModelAction *first_write_after_read=NULL;
-
- for (rit = list->rbegin(); rit != list->rend(); rit++) {
- ModelAction *act = *rit;
- if (act==reader)
- break;
- if (act->is_write())
- first_write_after_read=act;
- }
+ /* Iterate over all threads */
+ for (i = 0; i < thrd_lists->size(); i++) {
+ ModelAction *write_after_read = NULL;
- if (first_write_after_read==NULL)
- return true;
+ /* Iterate over actions in thread, starting from most recent */
+ action_list_t *list = &(*thrd_lists)[i];
+ action_list_t::reverse_iterator rit;
+ for (rit = list->rbegin(); rit != list->rend(); rit++) {
+ ModelAction *act = *rit;
- return !mo_graph->checkReachable(first_write_after_read, writer);
-}
+ if (!reader->happens_before(act))
+ break;
+ else if (act->is_write())
+ write_after_read = act;
+ }
+ if (write_after_read && mo_graph->checkReachable(write_after_read, writer))
+ return false;
+ }
+ return true;
+}
/**
* Finds the head(s) of the release sequence(s) containing a given ModelAction.
continue;
}
- /* Only writes can break release sequences */
- if (!act->is_write())
+ /* Only non-RMW writes can break release sequences */
+ if (!act->is_write() || act->is_rmw())
continue;
/* Check modification order */
act->is_read() &&
!act->could_synchronize_with(curr) &&
!act->same_thread(curr) &&
+ act->get_location() == curr->get_location() &&
promise->get_value() == curr->get_value()) {
curr->get_node()->set_promise(i);
}
if (!initialized) {
/** @todo Need a more informative way of reporting errors. */
printf("ERROR: may read from uninitialized atomic\n");
+ set_assert();
}
if (DBG_ENABLED() || !initialized) {
curr->get_node()->print_may_read_from();
printf("End printing may_read_from\n");
}
-
- ASSERT(initialized);
}
bool ModelChecker::sleep_can_read_from(ModelAction * curr, const ModelAction *write) {
projects / model-checker.git / blobdiff